--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/annotations/gov/nasa/jpf/annotation/NonShared.java	Mon May 04 22:10:33 2015 -0700
@@ -0,0 +1,30 @@
+/*
+ * Copyright (C) 2015, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.annotation;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+
+/**
+ * instances of @NonShared classes are not allowed to be referenced from
+ * more than one thread (but do allow hand-over)
+ */
+@Retention(RetentionPolicy.RUNTIME)
+public @interface NonShared {
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/listener/NonSharedChecker.java	Mon May 04 22:10:33 2015 -0700
@@ -0,0 +1,161 @@
+/*
+ * Copyright (C) 2015, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.listener;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.ListenerAdapter;
+import gov.nasa.jpf.vm.ClassInfo;
+import gov.nasa.jpf.vm.ElementInfo;
+import gov.nasa.jpf.vm.VM;
+import gov.nasa.jpf.vm.ThreadInfo;
+import gov.nasa.jpf.jvm.bytecode.ALOAD;
+import gov.nasa.jpf.jvm.bytecode.ARETURN;
+import gov.nasa.jpf.jvm.bytecode.ASTORE;
+import gov.nasa.jpf.jvm.bytecode.IFNONNULL;
+import gov.nasa.jpf.jvm.bytecode.IFNULL;
+import gov.nasa.jpf.vm.bytecode.InstanceFieldInstruction;
+import gov.nasa.jpf.vm.Instruction;
+import gov.nasa.jpf.jvm.bytecode.MONITORENTER;
+import gov.nasa.jpf.jvm.bytecode.VirtualInvocation;
+import gov.nasa.jpf.vm.StackFrame;
+
+/**
+ *
+ */
+public class NonSharedChecker extends ListenerAdapter {
+
+  boolean throwOnCycle = false;
+
+  static class Access {
+    ThreadInfo ti;
+    Access prev;
+
+    Access(ThreadInfo ti, Access prev){
+      this.ti = ti;
+      this.prev = prev;
+    }
+
+    // <2do> get a better hashCode for state hashing
+    public int hashCode() {
+      int h = ti.getId();
+      for (Access p = prev; p!= null; p = p.prev){
+        h = 31*h + p.ti.getId();
+      }
+      return h;
+    }
+    // but we don't care for equals()
+  }
+
+  public NonSharedChecker (Config conf){
+    throwOnCycle = conf.getBoolean("nonshared.throw_on_cycle");
+  }
+
+  boolean isNonShared(ElementInfo ei){
+    ClassInfo ci = ei.getClassInfo();
+    return (ci.getAnnotation("gov.nasa.jpf.annotation.NonShared") != null);
+  }
+
+  boolean checkLiveCycles (ElementInfo ei, ThreadInfo ti, Access ac){
+    if (ti == ac.ti){
+      return true; // Ok, fine - no need to record
+
+    } else {
+      boolean foundLiveOne = false;
+      for (Access a = ac; a != null; a = a.prev){
+        ThreadInfo t = a.ti;
+        if (t == ti){ // cycle detected
+          return !foundLiveOne;
+        }
+        foundLiveOne = (foundLiveOne || t.isAlive()); // <2do> maybe we should check for non-blocked threads
+      }
+
+      // new one, record it in the access history of the object
+      ac = new Access(ti, ac);
+      ei = ei.getModifiableInstance();
+      ei.setObjectAttr(ac);
+    }
+
+    return true;
+  }
+
+
+  @Override
+  public void executeInstruction (VM vm, ThreadInfo ti, Instruction insn){
+
+    ElementInfo ei = null;
+
+    if (ti.isFirstStepInsn()) {
+      return;
+    }
+
+    if (insn instanceof InstanceFieldInstruction){
+      ei = ((InstanceFieldInstruction)insn).peekElementInfo(ti);
+    } else if (insn instanceof VirtualInvocation){
+      ei = ((VirtualInvocation)insn).getThisElementInfo(ti);  // Outch - that's expensive
+    } else if (insn instanceof MONITORENTER ||
+               insn instanceof ASTORE ||
+               insn instanceof ARETURN ||
+               insn instanceof IFNONNULL ||
+               insn instanceof IFNULL) {
+      StackFrame frame = ti.getTopFrame();
+      int ref = frame.peek();
+      if (ref != -1){
+        ei = ti.getElementInfo(ref);
+      }
+    } else if (insn instanceof ALOAD){
+      StackFrame frame = ti.getTopFrame();
+      int ref = frame.getLocalVariable(((ALOAD)insn).getLocalVariableIndex());
+      if (ref != -1){
+        ei = ti.getElementInfo(ref);
+      }
+    }
+
+    if (ei != null){
+      Access ac = ei.getObjectAttr(Access.class);
+      if (ac != null){
+        if (!checkLiveCycles(ei,ti,ac)){
+          StringBuilder sb = new StringBuilder("NonShared object: ");
+          sb.append( ei);
+          sb.append(" accessed in live thread cycle: ");
+          sb.append( ti.getName());
+          for (Access a = ac; a != null; a = a.prev ){
+            sb.append(',');
+            sb.append(a.ti.getName());
+          }
+          String msg = sb.toString();
+
+          if (throwOnCycle){
+            ti.setNextPC( ti.createAndThrowException("java.lang.AssertionError", msg));
+          } else {
+            System.err.println("WARNING: " + msg);
+            System.err.println("\tat " + insn.getSourceLocation());
+          }
+          return;
+        }
+      }
+    }
+  }
+
+  @Override
+  public void objectCreated (VM vm, ThreadInfo ti, ElementInfo ei){
+    if (isNonShared(ei)){
+      ei.setObjectAttrNoClone(new Access(ti, null));
+    }
+  }
+}
+