src/peers/gov/nasa/jpf/vm/JPF_java_lang_Thread.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.vm;
  19
  20 import gov.nasa.jpf.JPF;
  21 import gov.nasa.jpf.JPFException;
  22 import gov.nasa.jpf.annotation.MJI;
  23 import gov.nasa.jpf.util.JPFLogger;
  24
  25
  26 /**
  27  * MJI NativePeer class for java.lang.Thread library abstraction
  28  *
  29  * NOTE - this implementation depends on all live thread objects being
  30  * in ThreadList
  31  */
  32 public class JPF_java_lang_Thread extends NativePeer {
  33
  34   static JPFLogger log = JPF.getLogger("gov.nasa.jpf.vm.ThreadInfo");
  35
  36
  37   /**
  38    * This method is the common initializer for all Thread ctors, and the only
  39    * single location where we can init our ThreadInfo, but it is PRIVATE
  40    */
  41   @MJI
  42   public void init0__Ljava_lang_ThreadGroup_2Ljava_lang_Runnable_2Ljava_lang_String_2J__V (MJIEnv env,
  43                          int objRef, int groupRef, int runnableRef, int nameRef, long stackSize) {
  44     VM vm = env.getVM();
  45
  46     // TODO: Fix for Groovy's model-checking
  47     // we only need to create the ThreadInfo - its initialization will take care
  48     // of proper linkage to the java.lang.Thread object (objRef)
  49     vm.createThreadInfo( objRef, groupRef, runnableRef, nameRef);
  50   }
  51
  52   @MJI
  53   public boolean isAlive____Z (MJIEnv env, int objref) {
  54     ThreadInfo ti = env.getThreadInfoForObjRef(objref);
  55     if (ti != null){
  56       return ti.isAlive();
  57     } else {
  58       return false; // not in ThreadList anymore
  59     }
  60   }
  61
  62   @MJI
  63   public void setDaemon0__Z__V (MJIEnv env, int objref, boolean isDaemon) {
  64     ThreadInfo ti = env.getThreadInfoForObjRef(objref);
  65     ti.setDaemon(isDaemon);
  66   }
  67
  68   @MJI
  69   public void dumpStack____V (MJIEnv env, int clsObjRef){
  70     ThreadInfo ti = env.getThreadInfo();
  71     ti.printStackTrace(); // this is not correct, we should go through VM.print
  72   }
  73
  74   @MJI
  75   public void setName0__Ljava_lang_String_2__V (MJIEnv env, int objref, int nameRef) {
  76     // it bails if you try to set a null name
  77     if (nameRef == MJIEnv.NULL) {
  78       env.throwException("java.lang.IllegalArgumentException");
  79
  80       return;
  81     }
  82
  83     // we have to intercept this to cache the name as a Java object
  84     // (to be stored in ThreadData)
  85     // luckily enough, it's copied into the java.lang.Thread object
  86     // as a char[], i.e. does not have to preserve identity
  87     // Note the nastiness in here - the java.lang.Thread object is only used
  88     // to get the initial values into ThreadData, and gets inconsistent
  89     // if this method is called (just works because the 'name' field is only
  90     // directly accessed from within the Thread ctors)
  91     ThreadInfo ti = env.getThreadInfoForObjRef(objref);
  92     ti.setName(env.getStringObject(nameRef));
  93   }
  94
  95   @MJI
  96   public void setPriority0__I__V (MJIEnv env, int objref, int prio) {
  97     // again, we have to cache this in ThreadData for performance reasons
  98     ThreadInfo ti = env.getThreadInfoForObjRef(objref);
  99
 100     if (prio != ti.getPriority()){
 101       ti.setPriority(prio);
 102
 103       // this could cause a context switch in a priority based scheduler
 104       if (ti.getScheduler().setsPriorityCG(ti)){
 105         env.repeatInvocation();
 106         return;
 107       }
 108     }
 109   }
 110
 111   @MJI
 112   public int countStackFrames____I (MJIEnv env, int objref) {
 113     ThreadInfo ti = env.getThreadInfoForObjRef(objref);
 114     return ti.countStackFrames();
 115   }
 116
 117   @MJI
 118   public int currentThread____Ljava_lang_Thread_2 (MJIEnv env, int clsObjRef) {
 119     ThreadInfo ti = env.getThreadInfo();
 120     return ti.getThreadObjectRef();
 121   }
 122
 123   @MJI
 124   public boolean holdsLock__Ljava_lang_Object_2__Z (MJIEnv env, int clsObjRef, int objref) {
 125     ThreadInfo  ti = env.getThreadInfo();
 126     ElementInfo ei = env.getElementInfo(objref);
 127
 128     return ei.isLockedBy(ti);
 129   }
 130
 131   @MJI
 132   public void interrupt____V (MJIEnv env, int objref) {
 133     ThreadInfo tiCurrent = env.getThreadInfo();
 134     ThreadInfo tiInterrupted = env.getThreadInfoForObjRef(objref);
 135
 136     if (!tiCurrent.isFirstStepInsn()) {
 137       tiInterrupted.interrupt();
 138     }
 139
 140     if (tiCurrent.getScheduler().setsInterruptCG(tiCurrent, tiInterrupted)) {
 141       env.repeatInvocation();
 142       return;
 143     }
 144   }
 145
 146   // these could be in the model, but we keep it symmetric, which also saves
 147   // us the effort of avoiding unwanted shared object field access CGs
 148   @MJI
 149   public boolean isInterrupted____Z (MJIEnv env, int objref) {
 150     ThreadInfo ti = env.getThreadInfoForObjRef(objref);
 151     return ti.isInterrupted(false);
 152   }
 153
 154   @MJI
 155   public boolean interrupted____Z (MJIEnv env, int clsObjRef) {
 156     ThreadInfo ti = env.getThreadInfo();
 157     return ti.isInterrupted(true);
 158   }
 159
 160   @MJI
 161   public void start____V (MJIEnv env, int objref) {
 162     ThreadInfo tiCurrent = env.getThreadInfo();
 163     ThreadInfo tiStarted = env.getThreadInfoForObjRef(objref);
 164     VM vm = tiCurrent.getVM();
 165
 166     //--- actions that are only performed upon first execution
 167     if (!tiCurrent.isFirstStepInsn()){
 168       if (tiStarted.isStopped()) {
 169         // don't do anything but set it terminated - it hasn't acquired any resources yet.
 170         // note that apparently host VMs don't schedule this thread, so there is no handler invocation
 171         tiStarted.setTerminated();
 172         return;
 173       }
 174
 175       if (!tiStarted.isNew()) {
 176         // alredy running, throw a IllegalThreadStateException. If it already terminated, it just gets
 177         // silently ignored in Java 1.4, but the 1.5 spec explicitly marks this
 178         // as illegal, so we adopt this by throwing an IllegalThreadState, too
 179         env.throwException("java.lang.IllegalThreadStateException");
 180         return;
 181       }
 182
 183       int runnableRef = tiStarted.getRunnableRef();
 184       if (runnableRef == MJIEnv.NULL) {
 185         // note that we don't set the 'tiSuspended' field, since java.lang.Thread doesn't
 186         runnableRef = objref;
 187       }
 188
 189       ElementInfo eiTarget = env.getElementInfo(runnableRef);
 190       ClassInfo   ci = eiTarget.getClassInfo();
 191       MethodInfo  miRun = ci.getMethod("run()V", true);
 192
 193       // we do direct call run() invocation so that we have a well defined
 194       // exit point (DIRECTCALLRETURN) in case the thread is stopped or there is
 195       // a fail-safe UncaughtExceptionHandler set
 196       DirectCallStackFrame runFrame = miRun.createRunStartStackFrame(tiStarted);
 197       runFrame.setReferenceArgument(0, runnableRef, null);
 198
 199       tiStarted.pushFrame(runFrame);
 200       tiStarted.setState(ThreadInfo.State.RUNNING);
 201
 202       vm.notifyThreadStarted(tiStarted);
 203     }
 204
 205     //--- scheduling point
 206     if (tiCurrent.getScheduler().setsStartCG(tiCurrent, tiStarted)){
 207       env.repeatInvocation();
 208     }
 209     // everything that would follow would be re-executed
 210   }
 211
 212   @MJI
 213   public void yield____V (MJIEnv env, int clsObjRef) {
 214     ThreadInfo ti = env.getThreadInfo();
 215     if (ti.getScheduler().setsYieldCG(ti)){
 216       env.repeatInvocation();
 217     }
 218   }
 219
 220   @MJI
 221   public void sleep__JI__V (MJIEnv env, int clsObjRef, long millis, int nanos) {
 222     ThreadInfo ti = env.getThreadInfo();
 223
 224     // check scheduling point
 225     if (ti.getScheduler().setsSleepCG(ti, millis, nanos)){
 226       ti.setSleeping();
 227       env.repeatInvocation();
 228       return;
 229     }
 230
 231     if (ti.isSleeping()){
 232       ti.setRunning();
 233     }
 234   }
 235
 236   @MJI
 237   public void suspend____V (MJIEnv env, int threadObjRef) {
 238     ThreadInfo tiCurrent = env.getThreadInfo();
 239     ThreadInfo tiSuspended = env.getThreadInfoForObjRef(threadObjRef);
 240
 241     if (tiSuspended.isTerminated()) {
 242       return;  // nothing to do, it's already gone
 243     }
 244
 245     if (!tiCurrent.isFirstStepInsn()){ // do this just once
 246       tiSuspended.suspend();
 247     }
 248
 249     // scheduling point
 250     if (tiCurrent.getScheduler().setsSuspendCG(tiCurrent, tiSuspended)){
 251       env.repeatInvocation();
 252     }
 253   }
 254
 255   @MJI
 256   public void resume____V (MJIEnv env, int threadObjRef) {
 257     ThreadInfo tiCurrent = env.getThreadInfo();
 258     ThreadInfo tiResumed = env.getThreadInfoForObjRef(threadObjRef);
 259
 260     if (tiCurrent == tiResumed){
 261       return;  // no self resume prior to suspension
 262     }
 263
 264     if (tiResumed.isTerminated()) {
 265       return;  // nothing to resume
 266     }
 267
 268     if (!tiCurrent.isFirstStepInsn()) { // do this just once
 269       tiResumed.resume();
 270     }
 271
 272     // check scheduling point
 273     if (tiCurrent.getScheduler().setsResumeCG(tiCurrent, tiResumed)){
 274       env.repeatInvocation();
 275       return;
 276     }
 277   }
 278
 279   /*
 280    * the join() workhorse. We use lockfree waits instead of a simple wait from a synchronized block
 281    * to save states
 282    */
 283   protected void join0 (MJIEnv env, int joineeRef, long timeout){
 284     ThreadInfo tiCurrent = env.getThreadInfo();
 285     ThreadInfo tiJoinee = env.getThreadInfoForObjRef(joineeRef);
 286     ElementInfo eiJoinee = env.getModifiableElementInfo(joineeRef); // the thread object to wait on
 287
 288     if (timeout < 0) {
 289       env.throwException("java.lang.IllegalArgumentException", "timeout value is negative");
 290       return;
 291     }
 292
 293     if (tiCurrent.isInterrupted(true)){ // interrupt status is set, throw and bail
 294       // since we use lock-free waits, we need to remove ourselves from the lock contender list
 295       eiJoinee.setMonitorWithoutLocked(tiCurrent);
 296
 297       // note that we have to throw even if the thread to join to is not alive anymore
 298       env.throwInterrupt();
 299       return;
 300     }
 301
 302     if (!tiCurrent.isFirstStepInsn()){ // to be executed only once
 303       if (tiJoinee.isAlive()) {
 304         // block in first top half so that following transitions see this thread as not runnable
 305         eiJoinee.wait( tiCurrent, timeout, false);
 306       } else {
 307         return; // nothing to do
 308       }
 309     }
 310
 311     if (tiCurrent.getScheduler().setsJoinCG(tiCurrent, tiJoinee, timeout)) {
 312       env.repeatInvocation();
 313       return;
 314     }
 315
 316     // unblock in bottom half
 317     switch (tiCurrent.getState()) {
 318       case WAITING:
 319       case TIMEOUT_WAITING:
 320         throw new JPFException("blocking join without transition break");
 321
 322       case UNBLOCKED:
 323         // Thread was owning the lock when it joined - we have to wait until
 324         // we can reacquire it
 325         eiJoinee.lockNotified(tiCurrent);
 326         break;
 327
 328       case TIMEDOUT:
 329         eiJoinee.resumeNonlockedWaiter(tiCurrent);
 330         break;
 331
 332       case RUNNING:
 333         if (tiJoinee.isAlive()) { // we still need to wait
 334           eiJoinee.wait(tiCurrent, timeout, false); // no need for a new CG
 335           env.repeatInvocation();
 336         }
 337         break;
 338     }
 339   }
 340
 341   @MJI
 342   public void join____V (MJIEnv env, int objref){
 343     join0(env,objref,0);
 344   }
 345
 346   @MJI
 347   public void join__J__V (MJIEnv env, int objref, long millis) {
 348     join0(env,objref,millis);
 349
 350   }
 351
 352   @MJI
 353   public void join__JI__V (MJIEnv env, int objref, long millis, int nanos) {
 354     join0(env,objref,millis); // <2do> we ignore nanos for now
 355   }
 356
 357   @MJI
 358   public int getState0____I (MJIEnv env, int objref) {
 359     // return the state index with respect to one of the public Thread.States
 360     ThreadInfo ti = env.getThreadInfoForObjRef(objref);
 361
 362     switch (ti.getState()) {
 363       case NEW:
 364         return 1;
 365       case RUNNING:
 366         return 2;
 367       case BLOCKED:
 368         return 0;
 369       case UNBLOCKED:
 370         return 2;
 371       case WAITING:
 372         return 5;
 373       case TIMEOUT_WAITING:
 374         return 4;
 375       case SLEEPING:
 376         return 4;
 377       case NOTIFIED:
 378         return 0;
 379       case INTERRUPTED:
 380         return 0;
 381       case TIMEDOUT:
 382         return 2;
 383       case TERMINATED:
 384         return 3;
 385       default:
 386         throw new JPFException("illegal thread state: " + ti.getState());
 387     }
 388   }
 389
 390   @MJI
 391   public long getId____J (MJIEnv env, int objref) {
 392     ThreadInfo ti = env.getThreadInfoForObjRef(objref);
 393     return ti.getId();
 394   }
 395
 396   @MJI
 397   public void stop____V (MJIEnv env, int threadRef) {
 398     stop__Ljava_lang_Throwable_2__V(env, threadRef, MJIEnv.NULL);
 399   }
 400
 401   @MJI
 402   public void stop__Ljava_lang_Throwable_2__V (MJIEnv env, int threadRef, int throwableRef) {
 403     ThreadInfo tiCurrent = env.getThreadInfo();
 404     ThreadInfo tiStopped = env.getThreadInfoForObjRef(threadRef);
 405
 406     if (tiStopped.isTerminated() || tiStopped.isStopped()) {
 407       return; // silently ignored
 408     }
 409
 410     if (tiCurrent.getScheduler().setsStopCG(tiCurrent, tiStopped)){
 411       env.repeatInvocation();
 412       return;
 413     }
 414
 415     // stop thread in bottom half
 416     tiStopped.setStopped(throwableRef);
 417   }
 418 }