src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_FinalizerThread.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.JPFException;
  21 import gov.nasa.jpf.annotation.MJI;
  22 import gov.nasa.jpf.util.Predicate;
  23
  24 /**
  25  * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
  26  *
  27  * A native peer for FinalizerThread. This is also an interface between the FinalizerThread
  28  * object at the SUT level and it corresponding FinalizerThreadInfo object at the JPF
  29  * level.
  30  */
  31 public class JPF_gov_nasa_jpf_FinalizerThread extends NativePeer {
  32
  33   @MJI
  34   public void runFinalizer__Ljava_lang_Object_2__V (MJIEnv env, int tiRef, int objRef) {
  35     int queueRef = env.getReferenceField(tiRef, "finalizeQueue");
  36     int[] elements = env.getReferenceArrayObject(queueRef);
  37
  38     if(elements.length>0 && elements[0]==objRef) {
  39       ThreadInfo finalizerTi = env.getThreadInfo();
  40       ClassInfo objCi = env.getElementInfo(objRef).getClassInfo();
  41       MethodInfo mi = objCi.getMethod("finalize()V", false);
  42
  43       // create and push a stack frame for finalize()V
  44       DirectCallStackFrame frame = mi.createDirectCallStackFrame(finalizerTi, 0);
  45       frame.setReferenceArgument(0, objRef, frame);
  46       finalizerTi.pushFrame(frame);
  47
  48       removeElement(env, tiRef, objRef);
  49     }
  50   }
  51
  52   // removes the very first element in the list, which is the last finalizable objects processed
  53   void removeElement(MJIEnv env, int tiRef, int objRef) {
  54     int queueRef = env.getReferenceField(tiRef, "finalizeQueue");
  55     ThreadInfo ti = env.getThreadInfo();
  56     int[] oldValues = env.getReferenceArrayObject(queueRef);
  57
  58     assert (objRef == oldValues[0]);
  59
  60     assert (oldValues.length>0);
  61
  62     int len = oldValues.length - 1;
  63     ElementInfo newQueue = env.getHeap().newArray("Ljava/lang/Object;", len, ti);
  64     int[] newValues = newQueue.asReferenceArray();
  65
  66     System.arraycopy(oldValues, 1, newValues, 0, len);
  67     env.getModifiableElementInfo(tiRef).setReferenceField("finalizeQueue", newQueue.getObjectRef());
  68   }
  69
  70   // a predicate to obtain all alive, non-finalizer threads within the ti process
  71   Predicate<ThreadInfo> getAppAliveUserPredicate (final ThreadInfo ti){
  72     return new Predicate<ThreadInfo>(){
  73       @Override
  74         public boolean isTrue (ThreadInfo t){
  75         return (t.isAlive() && !t.isSystemThread() && t.appCtx == ti.appCtx);
  76       }
  77     };
  78   }
  79
  80   @MJI
  81   public void manageState____V (MJIEnv env, int objref){
  82     ApplicationContext appCtx = env.getVM().getApplicationContext(objref);
  83     FinalizerThreadInfo tiFinalizer = appCtx.getFinalizerThread();
  84     VM vm = env.getVM();
  85
  86     // check for termination - Note that the finalizer thread has to be the last alive thread
  87     // of the process
  88     if(!vm.getThreadList().hasAnyMatching(getAppAliveUserPredicate(tiFinalizer))) {
  89       shutdown(env, objref);
  90     }
  91     // make the thread wait until more objects are added to finalizerQueue
  92     else {
  93       tiFinalizer.waitOnSemaphore();
  94
  95       assert tiFinalizer.isWaiting();
  96
  97       // this one has to consult the syncPolicy since there might be scheduling choices
  98       if (!tiFinalizer.getScheduler().setsPostFinalizeCG(tiFinalizer)){
  99         throw new JPFException("no transition break after finalization");
 100       }
 101     }
 102   }
 103
 104   protected void shutdown(MJIEnv env, int objRef) {
 105     env.getModifiableElementInfo(objRef).setBooleanField("done", true);
 106   }
 107 }