Main Page   Packages   Class Hierarchy   Alphabetical List   Compound List   File List   Compound Members  

Scheduler.java

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   //private boolean isNotifying;
00013   private boolean lastMoveWasSafe;
00014   private boolean foundSafeMove = false;
00015   // use to indicate which threads has run, or must still run
00016   BitSet alreadyRan  = new BitSet(10); //default size = 64
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 // ifdef DEBUG
00045 
00046 
00047 
00048 
00049 
00050 
00051 
00052 
00053 
00054 
00055 
00056 
00057 //#endif DEBUG
00058 
00059   public int getCurrentThread(){
00060     return current_thread;
00061   }  
00062   //public void setNotifying(){
00063   //  isNotifying = true;
00064   //}
00065 
00066   //public void clearNotifying(){
00067   //  isNotifying = false;
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     //current_notify++;
00079     current_notify = n+1;
00080   }  
00081   public void incCurrentRandom(iScheduler current){
00082     int n = ((Scheduler)current).current_random;
00083     //current_random++;
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     setAlreadyRanThread(current_thread);
00093     current_thread = current_thread+1;
00094     lastMoveWasSafe = foundSafeMove;
00095     */
00096   }  
00097   public void initialize(){
00098     current_thread = 0;
00099     current_notify = 0;
00100     current_random = 0;
00101     //isNotifying = false;
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   // used during simulation
00109   public iThreadInfo locateRandomRunningThread(iKernelState ks){
00110     boolean flag;
00111     int limit = ks.getThreadCount();
00112 
00113     //Random r = new Random();
00114 
00115     //current_thread = r.nextInt() % limit;
00116     //while(current_thread < 0) {
00117     //  current_thread = r.nextInt() % limit;
00118     //}
00119     current_thread = (current_thread + 1) % limit;
00120     //Debug.println(Debug.DEBUG, "Cthread Thread " + current_thread);
00121     while (current_thread < limit &&
00122            !ks.getThreadInfo(current_thread).isEnabled()) {
00123       current_thread++;
00124     }
00125     if (current_thread == limit) {
00126 // ifdef DEBUG
00127 
00128 //#endif DEBUG
00129       // make sure there was not something that could run
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       //Debug.println(Debug.DEBUG, "Cthread Thread " + current_thread);
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 // ifdef DEBUG
00147 
00148 
00149 //#endif DEBUG
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 // ifdef DEBUG
00264 
00265 //#endif DEBUG
00266     foundSafeMove = false;
00267     if (lastMoveWasSafe) return null;
00268 // ifdef DEBUG
00269 
00270 //#endif DEBUG
00271     //current_thread = 0; is WRONG here! why?
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 // enabled && !Ran && Safe
00280         break;
00281     }
00282       }
00283       current_thread++;
00284     }
00285     if (current_thread >= limit) { // could not find safe move
00286       if (unsafe_thread != 999) { // maybe there was an unsafe one
00287     current_thread = unsafe_thread;
00288 // ifdef DEBUG
00289 
00290 //#endif DEBUG
00291     foundSafeMove = false;
00292     return ks.getThreadInfo(current_thread);
00293       }
00294       else // there was no move at all
00295     return null;
00296     } else { // found safe move
00297       how_many_safe_moves++;
00298 // ifdef DEBUG
00299 
00300 //#endif DEBUG
00301       foundSafeMove = true;
00302       return ks.getThreadInfo(current_thread);
00303     }
00304   }  
00305   /************************************************************************/
00306 
00307 
00308   public void print(){
00309 // ifdef DEBUG
00310 
00311 //#endif DEBUG
00312   }  
00313   public void setAlreadyRanThread(int i) {
00314     alreadyRan.set(i);
00315   }  
00316   /************************************************************************/
00317   // used in path simulation
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 }

Generated at Thu Feb 7 06:54:31 2002 for Bandera by doxygen1.2.10 written by Dimitri van Heesch, © 1997-2001