--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/tests/gov/nasa/jpf/test/vm/threads/SuspendResumeTest.java	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,283 @@
+/*
+ * Copyright (C) 2014, 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.test.vm.threads;
+
+import gov.nasa.jpf.util.test.TestJPF;
+
+import org.junit.Test;
+
+/**
+ * regression test for suspend/resume
+ */
+@SuppressWarnings("deprecation")
+public class SuspendResumeTest extends TestJPF {
+
+  static boolean isRunning;
+  static boolean pass = false;
+  
+  static class T1 extends Thread {
+    @Override
+	public void run(){
+      System.out.println("t1 running");
+      isRunning = true;
+      while (!pass){
+        Thread.yield();
+      }
+      System.out.println("t1 terminating");
+    }
+  }
+
+  @Test
+  public void testBasicSuspendDeadlock(){
+    if (verifyDeadlock("+cg.threads.break_yield")) {
+      Thread t1 = new T1();
+      t1.start();
+
+      while (!isRunning) {
+        Thread.yield();
+      }
+
+      t1.suspend();
+      assertTrue(t1.getState() == Thread.State.RUNNABLE);
+
+      pass = true;
+      
+      // without resuming, T1 should not be scheduled again, despite being in a RUNNABLE state
+      //t1.resume();
+    }
+  }
+  
+  @Test
+  public void testBasicSuspendResume(){
+    if (verifyNoPropertyViolation("+cg.threads.break_yield")) {
+      Thread t1 = new T1();
+      t1.start();
+
+      while (!isRunning) {
+        Thread.yield();
+      }
+
+      System.out.println("main suspending t1");
+      t1.suspend();
+      assertTrue(t1.getState() == Thread.State.RUNNABLE);
+
+      pass = true;
+      
+      System.out.println("main resuming t1");
+      t1.resume();
+      try {
+        System.out.println("main joining t1");
+        t1.join();
+      } catch (InterruptedException ix){
+        fail("t1.join got interrupted");
+      }
+      
+      System.out.println("main terminating after t1.join");
+    }
+  }
+
+  //---------------
+  // this is the main reason to model suspend/resume, since suspension does
+  // *not* give up any held locks, and hence is very prone to creating deadlocks
+  
+  static class T2 extends Thread {
+    @Override
+	public synchronized void run(){
+      System.out.println("t2 running with lock");
+      isRunning = true;
+      while (!pass){
+        Thread.yield();
+      }
+      System.out.println("t2 terminating");
+    }
+  }
+  
+  @Test
+  public void testLockholderSuspendDeadlock(){
+
+    if (verifyDeadlock("+cg.threads.break_yield")) {
+      Thread t2 = new T2();
+      t2.start();
+
+      while (!isRunning) {
+        Thread.yield();
+      }
+
+      System.out.println("main suspending t2");
+      t2.suspend();
+      // now t2 should hold and never give up its lock 
+      
+      synchronized (t2){
+        fail("main should never get here");
+      }
+    }
+  }
+  
+  //------------
+  
+  static class T3 extends Thread {
+    @Override
+	public synchronized void run(){
+      System.out.println("t3 running");
+      isRunning = true;
+      try {
+        wait();
+      } catch (InterruptedException ix){
+        fail("t3 got interrupted");
+      }
+      System.out.println("t3 terminating");
+    }
+  }
+
+  @Test
+  public void testWaitingSuspendNotifyDeadlock(){
+    if (verifyDeadlock("+cg.threads.break_yield")) {
+      Thread t3 = new T3();
+      t3.start();
+
+      while (!isRunning) {
+        Thread.yield();
+      }
+      
+      synchronized (t3){
+        assertTrue( t3.getState() == Thread.State.WAITING);
+        
+        System.out.println("main suspending t3");
+        t3.suspend();
+        
+        System.out.println("main notifying t3");
+        t3.notify();
+        // t3 should be still suspended, despite being notified
+      }
+    }    
+  }
+  
+  @Test
+  public void testWaitingSuspendNotifyResume(){
+    if (verifyNoPropertyViolation("+cg.threads.break_yield")) {
+      Thread t3 = new T3();
+      t3.start();
+
+      while (!isRunning) {
+        Thread.yield();
+      }
+      
+      synchronized (t3){
+        assertTrue( t3.getState() == Thread.State.WAITING);
+        
+        System.out.println("main suspending t3");
+        t3.suspend();
+        
+        System.out.println("main notifying t3");
+        t3.notify();
+        // t3 should be still suspended, despite being notified
+        
+        System.out.println("main resuming t3");
+        t3.resume();
+        try {
+          System.out.println("main joining t3");
+          t3.join();
+        } catch (InterruptedException ix) {
+          fail("t3.join got interrupted");
+        }
+
+        System.out.println("main terminating after t3.join");
+      }
+    }    
+  }
+  
+  
+  //----------------
+  
+  static class T4 extends Thread {
+    @Override
+	public void run(){
+      System.out.println("t4 running ");
+      isRunning = true;
+      while (!pass){
+        Thread.yield();
+      }
+      
+      System.out.println("t4 trying to obtain lock");      
+      synchronized (this){
+        System.out.println("t4 obtained lock");
+      }
+      System.out.println("t4 terminating");
+    }
+  }
+  
+  @Test
+  public void testBlockSuspendUnblockDeadlock(){
+    if (verifyDeadlock("+cg.threads.break_yield")) {
+      Thread t4 = new T4();
+      t4.start();
+
+      while (!isRunning) {
+        Thread.yield();
+      }
+      
+      synchronized (t4){
+        pass = true;
+        
+        while (t4.getState() != Thread.State.BLOCKED){
+          Thread.yield();
+        }
+        
+        System.out.println("main suspending t4");
+        t4.suspend();
+      }
+      System.out.println("main released t4 lock");
+    }
+  }
+
+  
+  @Test
+  public void testBlockSuspendUnblockResume(){
+    if (verifyNoPropertyViolation("+cg.threads.break_yield")) {
+      Thread t4 = new T4();
+      t4.start();
+
+      while (!isRunning) {
+        Thread.yield();
+      }
+      
+      synchronized (t4){
+        pass = true;
+        
+        while (t4.getState() != Thread.State.BLOCKED){
+          Thread.yield();
+        }
+        
+        System.out.println("main suspending t4");
+        t4.suspend();
+      }
+      System.out.println("main released t4 lock");
+
+      System.out.println("main resuming t4");
+      t4.resume();
+      try {
+        System.out.println("main joining t4");
+        t4.join();
+      } catch (InterruptedException ix) {
+        fail("t4.join got interrupted");
+      }
+
+      System.out.println("main terminating after t4.join");
+    }
+  }
+}