src/tests/gov/nasa/jpf/test/mc/threads/NestedInitTest.java

   1 /*
   2  * Copyright (C) 2015, 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 org.junit.Test;
  22
  23 /**
  24  * test deadlock detection during concurrent class init.
  25  *
  26  * This models hotspot behavior that can explode the state space
  27  * and hence needs to be explicitly configured to perform
  28  * nested locking during class init
  29  */
  30 public class NestedInitTest extends TestJPF {
  31
  32   //------------------------------------------------ check normal clinit execution
  33   static class Root {
  34     static int data;
  35
  36     static {
  37       System.out.print( Thread.currentThread().getName());
  38       System.out.println(" in Root.<clinit>()");
  39       data = 40;
  40     }
  41   }
  42
  43   static class Base extends Root {
  44     static int data;
  45
  46     static {
  47       System.out.print( Thread.currentThread().getName());
  48       System.out.println(" in Base.<clinit>()");
  49       data = Root.data + 1;
  50     }
  51   }
  52
  53   static class Derived extends Base {
  54     static int data;
  55
  56     static {
  57       System.out.print( Thread.currentThread().getName());
  58       System.out.println(" in Derived.<clinit>()");
  59       data = Base.data + 1;
  60     }
  61   }
  62
  63   @Test
  64   public void testNestedInitSingleOk() {
  65     if (verifyNoPropertyViolation("+jvm.nested_init")){
  66       new Derived(); // force clinit
  67       System.out.print("Derived.data = ");
  68       System.out.println(Derived.data);
  69       assertTrue(Derived.data == 42);
  70     }
  71   }
  72
  73   @Test
  74   public void testNestedInitConcurrentOk() {
  75     if (verifyNoPropertyViolation("+jvm.nested_init")){
  76       new Thread( new Runnable(){
  77         public void run(){
  78           new Derived();
  79           System.out.print("t: Derived.data = ");
  80           System.out.println(Derived.data);
  81           assertTrue(Derived.data == 42);
  82         }
  83       }).start();
  84
  85       new Derived(); // force clinit
  86       System.out.print("main: Derived.data = ");
  87       System.out.println(Derived.data);
  88       assertTrue(Derived.data == 42);
  89     }
  90   }
  91
  92   //--- and now the nasty cases
  93
  94   //------------------------------------------ symmetric case
  95
  96   static class A {
  97     static final B b = new B();
  98   }
  99
 100   static class B {
 101     static final A a = new A();
 102   }
 103
 104   @Test
 105   public void testSymmetricDeadlock() {
 106     if (verifyDeadlock("+jvm.nested_init")) {
 107       new Thread() {
 108         public void run() {
 109           new A();
 110         }
 111       }.start();
 112       new B();
 113     }
 114   }
 115
 116   //------------------------------------------- hierarchical case
 117   public static class CyclicBase {
 118     static CyclicDerived sub = new CyclicDerived();
 119   }
 120
 121   public static class CyclicDerived extends CyclicBase {
 122   }
 123
 124
 125   @Test
 126   public void testCyclicHierarchyDeadlock (){
 127     if (verifyDeadlock("+jvm.nested_init")) {
 128       new Thread() {
 129         public void run() {
 130           new CyclicDerived(); // causes class inits via CyclicDerived
 131         }
 132       }.start();
 133
 134       Object o = CyclicBase.sub; // causes class inits via CyclicBase
 135     }
 136   }
 137
 138 }