001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package DEOS;
020:
021: import gov.nasa.jpf.jvm.Verify;
022:
023: /**
024: * DOCUMENT ME!
025: */
026: class Timer {
027: static final int uSecsPeriod = Registry.uSecsInFastestPeriod;
028: static int Start_time = 0; // time 'requested' by thread and 'written to timer'
029: static int Remaining_time = 0;
030: static int Used_time = 0;
031:
032: // JAVA DEOS these indicate that this _could_ happen, not that it will
033: static boolean tick = false;
034: static boolean timer = false;
035:
036: public Timer() {
037: }
038:
039: public static void clearInterrupts() {
040: timer = false;
041: tick = false;
042: }
043:
044: public int timeRemaining() {
045: //Verify.beginAtomic();
046: int used_in_period = 0; // how much time did thread use
047: int time_to_eop = uSecsPeriod - Used_time; // time left in period
048:
049: // if tick and timer are still set, then you know they happended -
050: // they are (should be) cleared by the threads otherwise
051: if (tick) { // used all the time to eop OR no time
052: used_in_period = time_to_eop;
053:
054: //System.out.println(" system tick interrupt");
055: } else if (timer) { // used all the time OR no time
056: used_in_period = Start_time;
057:
058: //System.out.println(" timer interrupt");
059: } else if (time_to_eop <= Start_time) {
060: DEOS.inc();
061:
062: if (!Verify.randomBool()) { // used all the time to eop OR no time
063: used_in_period = time_to_eop;
064:
065: //DEOS.println("going to end of period");
066: } else {
067: used_in_period = 0;
068:
069: //DEOS.println("going no where");
070: }
071: } else { // time_to_eop > Start_time, i.e. use Start_time for calculations
072: DEOS.inc();
073:
074: if (Verify.randomBool()) {
075: used_in_period = Start_time;
076:
077: //DEOS.println("using full budget");
078: } else {
079: used_in_period = 0;
080:
081: //DEOS.println("using no budget");
082: }
083: }
084:
085: Used_time += used_in_period;
086:
087: if (tick) {
088: Used_time = 0; // this is to help the invariant...
089: }
090:
091: clearInterrupts();
092:
093: Remaining_time = Start_time - used_in_period;
094:
095: //DEOS.println("thread: " + used_in_period + " used, " +
096: // Remaining_time + " remaining. total period usage: " + Used_time);
097: // Verify.endAtomic();
098: //assert (Remaining_time >= 0);
099: // }
100: //System.out.println("Timer.timeRemaining " + Remaining_time);
101: return Remaining_time;
102: }
103:
104: public/*synchronized*/
105: void write(int delayInMicroseconds) {
106: Start_time = delayInMicroseconds;
107:
108: //DEOS.println("setting timer with " + Start_time);
109: if ((Start_time + Used_time) >= uSecsPeriod) {
110: tick = true; // tick may happen
111: } else if ((Start_time + Used_time) < uSecsPeriod) {
112: timer = true;
113: } else {
114: System.out
115: .println("Timer ERROR - this case should not happen");
116:
117: //assert (true);
118: }
119: }
120: }
|