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 DEOSThread {
027: Thread thread; // which "Thread" object is this Thread one related to
028: boolean running = false;
029:
030: // run at a time
031: boolean isMain = false;
032: boolean isIdle = false;
033: boolean firstTime = true;
034: boolean setDelete = false;
035: boolean setWaitUntilNextPeriod = false;
036:
037: public DEOSThread(Thread th) {
038: thread = th;
039: isIdle = thread.isIdle();
040: isMain = thread.isMain();
041:
042: System.out.println(thread.toString() + " created");
043: }
044:
045: public void run(int tickResult) {
046: //Verify.assert(Timer.timer || Timer.tick);
047: DEOS.inc();
048:
049: if (tickResult == Clock.NOTIMECHANGE) {
050: if (Verify.randomBool()) {
051: //System.out.println("Thread: " + thread + " - Depth: " + depth);
052: DEOS.println("No interrupt - Choice 0:");
053: DEOS.println(thread.toString()
054: + " waiting until next period");
055: DEOSKernel.waitUntilNextPeriodK(thread);
056:
057: //yieldCPU();
058: } else {
059: //System.out.println("Thread: " + thread + " - Depth: " + depth);
060: DEOS.println("No interrupt - Choice 1:");
061: DEOS.println(thread.toString() + " deleting");
062: DEOSKernel.deleteThreadK(thread); //deleteThread();
063: }
064: } else {
065: switch (Verify.random(2)) {
066: case 0:
067:
068: //System.out.println("Thread: " + thread + " - Depth: " + depth);
069: DEOS.println("Choice 0:");
070: DEOS.println(thread.toString()
071: + " waiting until next period");
072: DEOSKernel.waitUntilNextPeriodK(thread);
073:
074: //yieldCPU();
075: break;
076:
077: case 2:
078:
079: //System.out.println("Thread: " + thread + " - Depth: " + depth);
080: DEOS.println("Choice 2:");
081: DEOS.println(thread.toString() + " deleting");
082: DEOSKernel.deleteThreadK(thread);
083:
084: //deleteThread();
085: break;
086:
087: case 1:
088:
089: //System.out.println("Thread: " + thread + " - Depth: " + depth);
090: DEOS.println("Choice 1: ");
091: getInterrupted(tickResult);
092:
093: break;
094: }
095: }
096: }
097:
098: // Modified by ckong - June 26, 2001
099: void getInterrupted(int tickResult) {
100: if (tickResult == Clock.SYSTEMINTERRUPT) {
101: DEOS.println(thread.toString()
102: + " interrupted by system tick");
103: DEOS.thePeriodicClock.resetUsedTime();
104: Scheduler.handleSystemTickInterrupt();
105: } else if (tickResult == Clock.TIMEOUT) {
106: DEOS.println(thread.toString() + " interrupted by timer");
107: Scheduler.handleTimerInterrupt();
108: } else {
109: DEOS.println(thread.toString()
110: + " waiting for time to pass");
111: }
112: }
113: }
|