src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_Exchanger.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
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.JPFException;
  22 import gov.nasa.jpf.annotation.MJI;
  23 import gov.nasa.jpf.util.InstructionState;
  24
  25 /**
  26  * peer class for java.util.concurrent.Exchanger
  27  */
  28 public class JPF_java_util_concurrent_Exchanger extends NativePeer {
  29
  30   static class ExchangeState extends InstructionState {
  31     int exchangeRef; // has to be a ref because the ElementInfo is modified
  32     boolean isWaiter;
  33
  34     static ExchangeState createWaiterState (MJIEnv env, int exchangeRef){
  35       ExchangeState s = new ExchangeState();
  36
  37       s.exchangeRef = exchangeRef;
  38       s.isWaiter = true;
  39       return s;
  40     }
  41
  42     static ExchangeState createResponderState (MJIEnv env, int exchangeRef){
  43       ExchangeState s = new ExchangeState();
  44
  45       s.exchangeRef = exchangeRef;
  46       s.isWaiter = false;
  47       return s;
  48     }
  49   }
  50
  51   ElementInfo createExchangeObject (MJIEnv env, int waiterDataRef) throws ClinitRequired {
  52     ElementInfo ei = env.newElementInfo("java.util.concurrent.Exchanger$Exchange");
  53     ei.setReferenceField("waiterData", waiterDataRef);
  54     ei.setReferenceField("waiterThread", env.getThreadInfo().getThreadObjectRef());
  55     return ei;
  56   }
  57
  58   private int repeatInvocation (MJIEnv env, StackFrame frame, ElementInfo exchange, ExchangeState state){
  59     frame.addFrameAttr(state);
  60     env.registerPinDown(exchange);
  61     env.repeatInvocation();
  62     return MJIEnv.NULL;
  63   }
  64
  65   //--- native methods
  66
  67   @MJI
  68   public int exchange__Ljava_lang_Object_2__Ljava_lang_Object_2 (MJIEnv env, int objRef, int dataRef){
  69     return exchange0__Ljava_lang_Object_2J__Ljava_lang_Object_2(env, objRef, dataRef, -1L);
  70   }
  71
  72   @MJI
  73   public int exchange0__Ljava_lang_Object_2J__Ljava_lang_Object_2 (MJIEnv env, int objRef, int dataRef, long timeoutMillis) {
  74     ThreadInfo ti = env.getThreadInfo();
  75     StackFrame frame = ti.getModifiableTopFrame();
  76     ExchangeState state = frame.getFrameAttr(ExchangeState.class);
  77     long to = (timeoutMillis <0) ? 0 : timeoutMillis;
  78
  79     if (state == null){ // first time for waiter or responder
  80       int eRef = env.getReferenceField(objRef, "exchange");
  81
  82       if (eRef == MJIEnv.NULL){ // first waiter, this has to block unless there is a timeout value of 0
  83         ElementInfo eiExchanger;
  84
  85         try {
  86           eiExchanger = createExchangeObject(env, dataRef);
  87         } catch (ClinitRequired x){
  88           // need to come back after class init
  89           env.repeatInvocation();
  90           return MJIEnv.NULL;
  91         }
  92
  93         eRef = eiExchanger.getObjectRef();
  94         env.setReferenceField(objRef, "exchange", eRef);
  95
  96         // timeout semantics differ - Object.wait(0) waits indefinitely, whereas here it
  97         // should throw immediately. We use -1 as non-timeout value
  98         if (timeoutMillis == 0) {
  99           env.throwException("java.util.concurrent.TimeoutException");
 100           return MJIEnv.NULL;
 101         }
 102
 103         eiExchanger.wait(ti, to, false);  // lockfree wait
 104
 105         if (ti.getScheduler().setsWaitCG(ti, to)) {
 106           return repeatInvocation(env, frame, eiExchanger, ExchangeState.createWaiterState(env, eRef));
 107         } else {
 108           throw new JPFException("blocked exchange() waiter without transition break");
 109         }
 110
 111       } else { // first responder (can reschedule)
 112         ElementInfo ei = ti.getModifiableElementInfo(eRef);
 113         ei.setReferenceField("responderData", dataRef);
 114         state = ExchangeState.createResponderState(env, eRef);
 115
 116         if (ei.getBooleanField("waiterTimedOut")){
 117           // depending on own timeout, this might deadlock because the waiter already timed out
 118           ei.wait(ti, to, false);
 119
 120           if (ti.getScheduler().setsWaitCG(ti, to)) {
 121             return repeatInvocation(env, frame, ei, state);
 122           } else {
 123             throw new JPFException("blocked exchange() responder without transition break");
 124           }
 125         }
 126
 127         // if we get here, the waiter is still waiting and we return right away
 128
 129         boolean didNotify = ei.notifies(env.getSystemState(), ti, false); // this changes the tiWaiter status
 130         env.setReferenceField(objRef, "exchange", MJIEnv.NULL); // re-arm Exchange object
 131
 132         if (ti.getScheduler().setsNotifyCG(ti, didNotify)){
 133           return repeatInvocation(env, frame, ei, state);
 134         }
 135
 136         return ei.getReferenceField("waiterData");
 137       }
 138
 139     } else { // re-execution(s)
 140       ElementInfo eiExchanger = env.getElementInfo(state.exchangeRef);
 141
 142       int retRef = MJIEnv.NULL;
 143
 144       if (ti.isInterrupted(true)) {
 145         env.throwException("java.lang.InterruptedException");
 146
 147       } else if (ti.isTimedOut()){
 148         if (state.isWaiter) {
 149           eiExchanger = eiExchanger.getModifiableInstance();
 150           eiExchanger.setBooleanField("waiterTimedOut", true);
 151
 152           // we are still lockfree waiting on the exChanger object
 153           eiExchanger.notifies(env.getSystemState(), ti, false);
 154         }
 155
 156         env.throwException("java.util.concurrent.TimeoutException");
 157
 158       } else {
 159         retRef = eiExchanger.getReferenceField( state.isWaiter ? "responderData" : "waiterData");
 160       }
 161
 162       //-- processed
 163       frame.removeFrameAttr(state);
 164       eiExchanger = eiExchanger.getModifiableInstance();
 165       env.releasePinDown(eiExchanger);
 166       return retRef;
 167     }
 168   }
 169 }