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 gov.nasa.jpf.jvm;
020:
021: import gov.nasa.jpf.Config;
022: import gov.nasa.jpf.util.Debug;
023:
024: import java.util.BitSet;
025: import java.util.Random;
026:
027: /**
028: * scheduler that picks runnable threads in random order
029: *
030: * <2do> make this thing more efficient by using primitive types instead of
031: * BitSet
032: */
033: public class RandomOrderScheduler extends Scheduler implements
034: Cloneable {
035: private static Random rand;
036:
037: private int thread;
038: private int random;
039: private BitSet runThread;
040: private BitSet[] runRandom;
041: private int[] randomSize;
042:
043: private RandomOrderScheduler() {
044: // for the clone
045: }
046:
047: public RandomOrderScheduler(Config config) {
048:
049: long seed;
050: if (config.getBoolean("vm.scheduler.use_time_for_seed")) {
051: seed = System.currentTimeMillis();
052: } else {
053: seed = config.getLong("vm.scheduler.random_seed", 0L);
054: }
055: rand = new Random(seed);
056:
057: Debug.println(Debug.MESSAGE, "Random Order Scheduler");
058: initialize();
059: }
060:
061: public Object getBacktrackData() {
062: return clone();
063: }
064:
065: public int getRandom() {
066: return random;
067: }
068:
069: public int[] getStoringData() {
070: return new int[0];
071: }
072:
073: public int getThread() {
074: return thread;
075: }
076:
077: public void backtrackTo(ArrayOffset storing, Object backtrack) {
078: copy((RandomOrderScheduler) backtrack);
079: }
080:
081: public Object clone() {
082: RandomOrderScheduler s = new RandomOrderScheduler();
083:
084: s.thread = thread;
085: s.random = random;
086:
087: if (runThread != null) {
088: s.runThread = (BitSet) runThread.clone();
089: }
090:
091: if (runRandom != null) {
092: s.runRandom = new BitSet[runRandom.length];
093:
094: for (int i = 0; i < runRandom.length; i++) {
095: if (runRandom[i] != null) {
096: s.runRandom[i] = (BitSet) runRandom[i].clone();
097: }
098: }
099: }
100:
101: if (randomSize != null) {
102: s.randomSize = (int[]) randomSize.clone();
103: }
104:
105: return s;
106: }
107:
108: public void copy(RandomOrderScheduler sch) {
109: if (sch.runThread != null) {
110: runThread = (BitSet) sch.runThread.clone();
111: }
112:
113: if (sch.runRandom != null) {
114: runRandom = new BitSet[sch.runRandom.length];
115:
116: for (int i = 0; i < sch.runRandom.length; i++) {
117: runRandom[i] = (BitSet) sch.runRandom[i].clone();
118: }
119: }
120:
121: if (sch.randomSize != null) {
122: randomSize = (int[]) sch.randomSize.clone();
123: }
124:
125: thread = sch.thread;
126: random = sch.random;
127: }
128:
129: public void initialize() {
130: thread = 0;
131: random = -1;
132: runThread = new BitSet();
133: runRandom = null;
134: randomSize = null;
135: }
136:
137: public ThreadInfo locateThread(SystemState ss) {
138: thread = pickNextThread(ss);
139:
140: if (thread == -1) {
141: //thread = 0;
142: return null;
143: }
144:
145: return ss.getThreadInfo(thread);
146: }
147:
148: public void next() {
149: if (isComplete(thread)) {
150: runThread.set(thread);
151: }
152: }
153:
154: public int random(int max) {
155: if (random == -1) {
156: random = 0;
157: }
158:
159: random = pickNextRandom(thread, max);
160:
161: return random;
162: }
163:
164: private boolean isComplete(int th) {
165: if (randomSize[th] == 0) {
166: return true;
167: }
168:
169: boolean finished = true;
170:
171: for (int i = 0; i < randomSize[th]; i++) {
172: finished = finished && runRandom[th].get(i);
173: }
174:
175: return finished;
176: }
177:
178: private int pickNextRandom(int th, int n) {
179: randomSize[th] = n;
180:
181: int nchoices = 0;
182: int[] choices = new int[n];
183:
184: for (int i = 0; i < n; i++) {
185: if (!runRandom[th].get(i)) {
186: choices[nchoices++] = i;
187: }
188: }
189:
190: int r = rand.nextInt(nchoices);
191: runRandom[th].set(choices[r]);
192:
193: return choices[r];
194: }
195:
196: private int pickNextThread(SystemState ss) {
197: int nthreads = 0;
198: int n = ss.getThreadCount();
199: int[] refs = new int[n];
200:
201: if (runRandom == null) {
202: runRandom = new BitSet[n];
203:
204: for (int i = 0; i < n; i++) {
205: runRandom[i] = new BitSet();
206: }
207: }
208:
209: if (randomSize == null) {
210: randomSize = new int[n];
211: }
212:
213: for (int i = 0; i < n; i++) {
214: ThreadInfo th = ss.getThreadInfo(i);
215:
216: if (!(runThread.get(i)) && (th.isRunnable())) {
217: refs[nthreads++] = i;
218: }
219: }
220:
221: if (nthreads == 0) {
222: return -1;
223: }
224:
225: int r = rand.nextInt(nthreads);
226:
227: return refs[r];
228: }
229: }
|