|
1 package gov.nasa.jpf.jvm;
20
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.util.Debug;
23
24 import java.util.BitSet  ;
25 import java.util.Random ;
26
27
28
34 public class RandomOrderScheduler extends Scheduler implements Cloneable {
35 private static Random rand;
36
37 private int thread;
38 private int random;
39 private BitSet runThread;
40 private BitSet [] runRandom;
41 private int[] randomSize;
42
43 private RandomOrderScheduler () {
44 }
46
47 public RandomOrderScheduler (Config config) {
48
49 long seed;
50 if (config.getBoolean("vm.scheduler.use_time_for_seed")) {
51 seed = System.currentTimeMillis();
52 } else {
53 seed = config.getLong("vm.scheduler.random_seed", 0L);
54 }
55 rand = new Random (seed);
56
57 Debug.println(Debug.MESSAGE, "Random Order Scheduler");
58 initialize();
59 }
60
61 public Object getBacktrackData () {
62 return clone();
63 }
64
65 public int getRandom () {
66 return random;
67 }
68
69 public int[] getStoringData () {
70 return new int[0];
71 }
72
73 public int getThread () {
74 return thread;
75 }
76
77 public void backtrackTo (ArrayOffset storing, Object backtrack) {
78 copy((RandomOrderScheduler) backtrack);
79 }
80
81 public Object clone () {
82 RandomOrderScheduler s = new RandomOrderScheduler();
83
84 s.thread = thread;
85 s.random = random;
86
87 if (runThread != null) {
88 s.runThread = (BitSet ) runThread.clone();
89 }
90
91 if (runRandom != null) {
92 s.runRandom = new BitSet [runRandom.length];
93
94 for (int i = 0; i < runRandom.length; i++) {
95 if (runRandom[i] != null) {
96 s.runRandom[i] = (BitSet ) runRandom[i].clone();
97 }
98 }
99 }
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 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 } |
Popular Tags |
Java API By Example, From Geeks To Geeks.