2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.vm;
21 import gov.nasa.jpf.JPFException;
22 import gov.nasa.jpf.annotation.MJI;
23 import gov.nasa.jpf.util.InstructionState;
26 * peer class for java.util.concurrent.Exchanger
28 public class JPF_java_util_concurrent_Exchanger extends NativePeer {
30 static class ExchangeState extends InstructionState {
31 int exchangeRef; // has to be a ref because the ElementInfo is modified
34 static ExchangeState createWaiterState (MJIEnv env, int exchangeRef){
35 ExchangeState s = new ExchangeState();
37 s.exchangeRef = exchangeRef;
42 static ExchangeState createResponderState (MJIEnv env, int exchangeRef){
43 ExchangeState s = new ExchangeState();
45 s.exchangeRef = exchangeRef;
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());
58 private int repeatInvocation (MJIEnv env, StackFrame frame, ElementInfo exchange, ExchangeState state){
59 frame.addFrameAttr(state);
60 env.registerPinDown(exchange);
61 env.repeatInvocation();
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);
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;
79 if (state == null){ // first time for waiter or responder
80 int eRef = env.getReferenceField(objRef, "exchange");
82 if (eRef == MJIEnv.NULL){ // first waiter, this has to block unless there is a timeout value of 0
83 ElementInfo eiExchanger;
86 eiExchanger = createExchangeObject(env, dataRef);
87 } catch (ClinitRequired x){
88 // need to come back after class init
89 env.repeatInvocation();
93 eRef = eiExchanger.getObjectRef();
94 env.setReferenceField(objRef, "exchange", eRef);
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");
103 eiExchanger.wait(ti, to, false); // lockfree wait
105 if (ti.getScheduler().setsWaitCG(ti, to)) {
106 return repeatInvocation(env, frame, eiExchanger, ExchangeState.createWaiterState(env, eRef));
108 throw new JPFException("blocked exchange() waiter without transition break");
111 } else { // first responder (can reschedule)
112 ElementInfo ei = ti.getModifiableElementInfo(eRef);
113 ei.setReferenceField("responderData", dataRef);
114 state = ExchangeState.createResponderState(env, eRef);
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);
120 if (ti.getScheduler().setsWaitCG(ti, to)) {
121 return repeatInvocation(env, frame, ei, state);
123 throw new JPFException("blocked exchange() responder without transition break");
127 // if we get here, the waiter is still waiting and we return right away
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
132 if (ti.getScheduler().setsNotifyCG(ti, didNotify)){
133 return repeatInvocation(env, frame, ei, state);
136 return ei.getReferenceField("waiterData");
139 } else { // re-execution(s)
140 ElementInfo eiExchanger = env.getElementInfo(state.exchangeRef);
142 int retRef = MJIEnv.NULL;
144 if (ti.isInterrupted(true)) {
145 env.throwException("java.lang.InterruptedException");
147 } else if (ti.isTimedOut()){
148 if (state.isWaiter) {
149 eiExchanger = eiExchanger.getModifiableInstance();
150 eiExchanger.setBooleanField("waiterTimedOut", true);
152 // we are still lockfree waiting on the exChanger object
153 eiExchanger.notifies(env.getSystemState(), ti, false);
156 env.throwException("java.util.concurrent.TimeoutException");
159 retRef = eiExchanger.getReferenceField( state.isWaiter ? "responderData" : "waiterData");
163 frame.removeFrameAttr(state);
164 eiExchanger = eiExchanger.getModifiableInstance();
165 env.releasePinDown(eiExchanger);