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 PriorityListOfThreads {
027: static final int numberOfThreadPriorities = 4; // from spin code
028: int itsHighestPriorityMember;
029: threadList[] itsList;
030:
031: public PriorityListOfThreads() {
032: //System.out.println("PriorityListOfThreads Constructor");
033: itsHighestPriorityMember = 0;
034: itsList = new threadList[numberOfThreadPriorities];
035:
036: for (int i = 0; i < numberOfThreadPriorities; i++) {
037: itsList[i] = new threadList();
038: }
039: }
040:
041: public boolean isEmpty() {
042: return highestPriorityMember().isEmpty();
043: }
044:
045: public void addAtBeginning(threadListNode theNode) {
046: //Verify.beginAtomic();
047: //System.out.println("PriorityListOfThreads.addAtBeginning");
048: int threadPriority = theNode.parent().currentPriority();
049: itsList[threadPriority].addAtBeginning(theNode);
050:
051: if (itsHighestPriorityMember < threadPriority) {
052: itsHighestPriorityMember = threadPriority;
053: }
054:
055: //Verify.endAtomic();
056: }
057:
058: public void addAtEnd(threadListNode theNode) {
059: //Verify.beginAtomic();
060: int threadPriority = theNode.parent().currentPriority();
061: itsList[threadPriority].addAtEnd(theNode);
062:
063: if (itsHighestPriorityMember < threadPriority) {
064: itsHighestPriorityMember = threadPriority;
065: }
066:
067: //Verify.endAtomic();
068: }
069:
070: public threadListNode head() {
071: return highestPriorityMember().head();
072: }
073:
074: public void mergeList(PriorityListOfThreads otherList) {
075: //Verify.beginAtomic();
076: threadList mine = itsList[0];
077: threadList his = otherList.itsList[0];
078: int end = otherList.itsHighestPriorityMember + 1;
079: int i = 0;
080:
081: do {
082: mine.mergeList(his);
083: i++;
084: mine = itsList[i];
085: his = otherList.itsList[i];
086: } while (i != end);
087:
088: if (itsHighestPriorityMember < otherList.itsHighestPriorityMember) {
089: itsHighestPriorityMember = otherList.itsHighestPriorityMember;
090: }
091:
092: otherList.itsHighestPriorityMember = 0;
093:
094: //Verify.endAtomic();
095: }
096:
097: public void mergeList(threadList otherList) {
098: //Verify.beginAtomic();
099: //System.out.println("PriorityListOfThreads.mergeList");
100: if (!otherList.isEmpty()) {
101: int otherListPriority = otherList.head().parent()
102: .currentPriority();
103:
104: //System.out.println("otherListPriority = " + otherListPriority);
105: //System.out.println("itsHighestPriorityMember = "
106: // +itsHighestPriorityMember);
107: itsList[otherListPriority].mergeList(otherList);
108:
109: if (itsHighestPriorityMember < otherListPriority) {
110: itsHighestPriorityMember = otherListPriority;
111: }
112: }
113:
114: //Verify.endAtomic();
115: }
116:
117: private threadList highestPriorityMember() {
118: //Verify.beginAtomic();
119: int hipri = itsHighestPriorityMember;
120:
121: for (; hipri > 0; hipri--) {
122: if (!itsList[hipri].isEmpty()) {
123: break;
124: }
125: }
126:
127: itsHighestPriorityMember = hipri;
128:
129: //System.out.println("HIPRI = " + hipri);
130: //Verify.endAtomic();
131: return itsList[hipri];
132: }
133: }
|