src/tests/gov/nasa/jpf/test/mc/threads/HORaceTest.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.test.mc.threads;
  20
  21 import gov.nasa.jpf.util.test.TestJPF;
  22
  23 import org.junit.Test;
  24
  25 /**
  26  * high order data race
  27  */
  28 public class HORaceTest extends TestJPF {
  29
  30   static class D {
  31     int a;
  32     int b;
  33
  34     D (int x, int y){
  35       a = x;
  36       b = y;
  37     }
  38
  39     D (D other){
  40       setA( other.getA());
  41       Thread.yield(); // give the 2nd thread a chance to interfere
  42       setB( other.getB());
  43     }
  44
  45     synchronized int getA() { return a; }
  46     synchronized int getB() { return b; }
  47     synchronized void setA(int x){ a = x; }
  48     synchronized void setB(int x){ b = x; }
  49
  50     synchronized void change(int delta) {
  51       a += delta;
  52       b += delta;
  53     }
  54
  55     synchronized boolean isConsistent() {
  56       return a == b;
  57     }
  58   }
  59
  60   static D d1;
  61   static D d2;
  62
  63   @Test
  64   public void testHighOrderRace() {
  65
  66     if (verifyAssertionErrorDetails("inconsistent d2")) {
  67       d1 = new D(42, 42);
  68
  69       Thread t1 = new Thread() {
  70
  71         @Override
  72                 public void run() {
  73           d2 = new D(d1);
  74         }
  75       };
  76       Thread t2 = new Thread() {
  77
  78         @Override
  79                 public void run() {
  80           d1.change(-1);
  81         }
  82       };
  83
  84       t1.start();
  85       t2.start();
  86
  87       try {
  88         t1.join();
  89         t2.join();
  90       } catch (InterruptedException ix) {
  91         fail("unexpected interrupt during {t1,t2}.join()");
  92       }
  93
  94       System.out.print("d2 = ");
  95       System.out.print(d2.a);
  96       System.out.print(',');
  97       System.out.println(d2.b);
  98
  99       assert d2.isConsistent() : "inconsistent d2";
 100     }
 101   }
 102
 103 }