00001 package gov.nasa.arc.ase.jpf;
00002
00003 import java.util.*;
00004 import gov.nasa.arc.ase.util.Debug;
00005 import gov.nasa.arc.ase.jpf.jvm.*;
00006 import java.io.*;
00007
00008 public class Scheduler implements iScheduler,Cloneable{
00009 private int current_thread;
00010 private int current_notify;
00011 private int current_random;
00012
00013 private boolean lastMoveWasSafe;
00014 private boolean foundSafeMove = false;
00015
00016 BitSet alreadyRan = new BitSet(10);
00017 private int how_many_safe_moves = 0;
00018
00019 private static BufferedReader br = new BufferedReader(new InputStreamReader(System.in));
00020 private static boolean quit = false;
00021
00022 public Object clone(){
00023 try{
00024 Scheduler sd = (Scheduler) super.clone();
00025 if (Engine.options.po_reduction) {
00026 sd.alreadyRan = new BitSet();
00027 for(int i = 0; i < alreadyRan.size(); i++) {
00028 if (alreadyRan.get(i))
00029 sd.alreadyRan.set(i);
00030 }
00031 }
00032 return sd;
00033 }
00034 catch(CloneNotSupportedException e){
00035 throw new InternalError(e.toString());
00036 };
00037 }
00038 public int getCurrentNotify(){
00039 return current_notify;
00040 }
00041 public int getCurrentRandom(){
00042 return current_random;
00043 }
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058
00059 public int getCurrentThread(){
00060 return current_thread;
00061 }
00062
00063
00064
00065
00066
00067
00068
00069
00070 public iThreadInfo getCurrentThreadInfo(iKernelState ks){
00071 return ks.getThreadInfo(current_thread);
00072 }
00073 public int getSafeMoves() {
00074 return how_many_safe_moves;
00075 }
00076 public void incCurrentNotify(iScheduler current){
00077 int n = ((Scheduler)current).current_notify;
00078
00079 current_notify = n+1;
00080 }
00081 public void incCurrentRandom(iScheduler current){
00082 int n = ((Scheduler)current).current_random;
00083
00084 current_random = n+1;
00085 }
00086 public void incCurrentThread(iScheduler current) {
00087 int th = ((Scheduler)current).current_thread;
00088 setAlreadyRanThread(th);
00089 current_thread = th+1;
00090 lastMoveWasSafe = foundSafeMove;
00091
00092
00093
00094
00095
00096 }
00097 public void initialize(){
00098 current_thread = 0;
00099 current_notify = 0;
00100 current_random = 0;
00101
00102 lastMoveWasSafe = false;
00103 if (Engine.options.po_reduction) {
00104 for(int i= 0; i < alreadyRan.size(); i++)
00105 alreadyRan.clear(i);
00106 }
00107 }
00108
00109 public iThreadInfo locateRandomRunningThread(iKernelState ks){
00110 boolean flag;
00111 int limit = ks.getThreadCount();
00112
00113
00114
00115
00116
00117
00118
00119 current_thread = (current_thread + 1) % limit;
00120
00121 while (current_thread < limit &&
00122 !ks.getThreadInfo(current_thread).isEnabled()) {
00123 current_thread++;
00124 }
00125 if (current_thread == limit) {
00126
00127
00128
00129
00130 current_thread = 0;
00131 while (current_thread < limit &&
00132 !ks.getThreadInfo(current_thread).isEnabled()) {
00133 current_thread++;
00134 }
00135 }
00136 if (current_thread == limit)
00137 return null;
00138 else {
00139
00140 return ks.getThreadInfo(current_thread);
00141 }
00142 }
00143 public iThreadInfo locateRunningThread(iSystemState ss, iKernelState ks) {
00144 if(Engine.options.interactive)
00145 return locateRunningThreadInteractive(ss, ks);
00146
00147
00148
00149
00150 int limit = ks.getThreadCount();
00151
00152 while(current_thread < limit) {
00153 iThreadInfo th = ks.getThreadInfo(current_thread);
00154 if(th.isRunnable(ss, ks)) break;
00155 current_thread++;
00156 }
00157
00158 if (current_thread >= limit)
00159 return null;
00160 else {
00161 return ks.getThreadInfo(current_thread);
00162 }
00163 }
00164 public iThreadInfo locateRunningThreadInteractive(iSystemState ss, iKernelState ks) {
00165 if (quit) return null;
00166
00167 int nthreads = ks.getThreadCount();
00168 int nrunnable = 0;
00169 BitSet runnable = new BitSet();
00170
00171 for(int i = 0; i < nthreads; i++) {
00172 iThreadInfo th = ks.getThreadInfo(i);
00173 if(th.isRunnable(ss, ks)) {
00174 runnable.set(i);
00175 nrunnable++;
00176 }
00177 }
00178
00179 if(nrunnable == 0) {
00180 System.out.println("Deadlock: backing up");
00181 return null;
00182 }
00183
00184 System.out.print("Runnable threads [" + nrunnable + "]: ");
00185 for(int i = 0; i < nthreads; i++) {
00186 if(runnable.get(i)) {
00187 if(i == current_thread) {
00188 System.err.print("[" + i + "] ");
00189 } else {
00190 System.err.print(i + " ");
00191 }
00192 }
00193 }
00194 System.out.println();
00195
00196 while(true) {
00197 try {
00198 System.out.print("> ");
00199 String s = br.readLine();
00200 if(s.equals("quit") || s.equals("q")) {
00201 quit = true;
00202 return null;
00203 } else if(s.equals("backtrack") || s.equals("back") || s.equals("b")) {
00204 return null;
00205 } else if(s.equals("show") || s.equals("s")) {
00206 while(true) {
00207 System.out.print("show> ");
00208 s = br.readLine();
00209 if(s.equals("")) break;
00210 try {
00211 int l = Integer.parseInt(s);
00212 if(runnable.get(l)) {
00213 ThreadInfo th = (ThreadInfo)ks.getThreadInfo(l);
00214 System.out.print(th.getTrailInfo());
00215 break;
00216 }
00217 } catch(NumberFormatException e) {
00218 }
00219 }
00220 } else if(s.equals("random") || s.equals("r")) {
00221 while(true) {
00222 System.out.println("Current random: " + current_random);
00223 System.out.print("random> ");
00224 s = br.readLine();
00225 if(s.equals("")) break;
00226 try {
00227 current_random = Integer.parseInt(s);
00228 break;
00229 } catch(NumberFormatException e) {
00230 }
00231 }
00232 } else if(s.equals("help") || s.equals("h") || s.equals("?")) {
00233 System.out.println("command:");
00234 System.out.println(" quit");
00235 System.out.println(" random");
00236 System.out.println(" backtrack");
00237 System.out.println(" help");
00238 } else {
00239 if(runnable.get(current_thread) && s.equals(""))
00240 break;
00241 try {
00242 int i = Integer.parseInt(s);
00243 if(runnable.get(i)) {
00244 current_thread = i;
00245 break;
00246 }
00247 } catch(NumberFormatException e) {
00248 }
00249 }
00250 } catch(IOException e) {
00251 throw new InternalError();
00252 }
00253 }
00254
00255 System.out.println("Running thread " + current_thread);
00256
00257 return ks.getThreadInfo(current_thread);
00258 }
00259 public iThreadInfo locateSafeThread(iSystemState ss, iKernelState ks) {
00260 int limit = ks.getThreadCount();
00261 int unsafe_thread = 999;
00262
00263
00264
00265
00266 foundSafeMove = false;
00267 if (lastMoveWasSafe) return null;
00268
00269
00270
00271
00272 while (current_thread < limit) {
00273 if (ks.getThreadInfo(current_thread).isRunnable(ss, ks)) {
00274 if (!alreadyRan.get(current_thread)) {
00275 if (!ks.getThreadInfo(current_thread).isSafe()) {
00276 if (unsafe_thread == 999)
00277 unsafe_thread = current_thread;
00278 }
00279 else
00280 break;
00281 }
00282 }
00283 current_thread++;
00284 }
00285 if (current_thread >= limit) {
00286 if (unsafe_thread != 999) {
00287 current_thread = unsafe_thread;
00288
00289
00290
00291 foundSafeMove = false;
00292 return ks.getThreadInfo(current_thread);
00293 }
00294 else
00295 return null;
00296 } else {
00297 how_many_safe_moves++;
00298
00299
00300
00301 foundSafeMove = true;
00302 return ks.getThreadInfo(current_thread);
00303 }
00304 }
00305
00306
00307
00308 public void print(){
00309
00310
00311
00312 }
00313 public void setAlreadyRanThread(int i) {
00314 alreadyRan.set(i);
00315 }
00316
00317
00318 public void setCurrentRandom(int random){
00319 current_random = random;
00320 }
00321 public void setCurrentThread(int thread){
00322 lastMoveWasSafe = foundSafeMove;
00323 current_thread = thread;
00324 }
00325 public void setLastSafeMove(boolean v) {
00326 lastMoveWasSafe = v;
00327 }
00328 }