src/tests/gov/nasa/jpf/test/mc/threads/AtomicTest.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.test.mc.threads;
  19
  20 import gov.nasa.jpf.util.test.TestJPF;
  21 import gov.nasa.jpf.vm.Verify;
  22
  23 import org.junit.Test;
  24
  25
  26 public class AtomicTest extends TestJPF {
  27
  28   static int data = 42;
  29
  30   @Test public void testNoRace () {
  31     if (verifyNoPropertyViolation("+cg.enable_atomic")) {
  32       Runnable r = new Runnable() {
  33
  34         @Override
  35                 public void run() {
  36           System.out.println("  enter run in Thread-0");
  37           assert data == 42;
  38           data += 1;
  39           assert data == 43;
  40           data -= 1;
  41           assert data == 42;
  42           System.out.println("  exit run in Thread-0");
  43         }
  44       };
  45
  46       Thread t = new Thread(r);
  47
  48       Verify.beginAtomic();
  49       System.out.println("enter atomic section in main");
  50       t.start();
  51       assert data == 42;
  52       data += 2;
  53       assert data == 44;
  54       data -= 2;
  55       assert data == 42;
  56       System.out.println("exit atomic section in main");
  57       Verify.endAtomic();
  58     }
  59   }
  60
  61   @Test
  62   public void testDataCG () {
  63     if (verifyNoPropertyViolation("+cg.enable_atomic")) {
  64       Runnable r = new Runnable() {
  65
  66         @Override
  67                 public void run() {
  68           data += 10;
  69         }
  70       };
  71
  72       Thread t = new Thread(r);
  73
  74       Verify.beginAtomic();
  75       t.start();
  76       int i = Verify.getInt(1, 2);
  77       data += i;
  78       assert data < 45 : "data got incremented: " + data;
  79       Verify.incrementCounter(0);
  80       assert i == Verify.getCounter(0);
  81       Verify.endAtomic();
  82     }
  83   }
  84
  85   @Test public void testBlockedInAtomic () {
  86     if (verifyDeadlock("+cg.enable_atomic")){
  87       Runnable r = new Runnable() {
  88
  89         @Override
  90                 public synchronized void run() {
  91           System.out.println("T notifying..");
  92           this.notify();
  93         }
  94       };
  95
  96       Thread t = new Thread(r);
  97
  98       synchronized (r){
  99         System.out.println("main going atomic, holding r lock");
 100         Verify.beginAtomic();
 101         t.start();
 102
 103         try {
 104           System.out.println("main waiting on r");
 105           r.wait();
 106         } catch (InterruptedException x){
 107           System.out.println("main got interrupted");
 108         }
 109         System.out.println("main leaving atomic");
 110         Verify.endAtomic();
 111       }
 112     }
 113   }
 114 }