src/tests/gov/nasa/jpf/vm/multiProcess/ThreadTest.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.vm.multiProcess;
  20
  21 import gov.nasa.jpf.ListenerAdapter;
  22 import gov.nasa.jpf.util.test.TestMultiProcessJPF;
  23 import gov.nasa.jpf.vm.ChoiceGenerator;
  24 import gov.nasa.jpf.vm.Scheduler;
  25 import gov.nasa.jpf.vm.SyncPolicy;
  26 import gov.nasa.jpf.vm.ThreadInfo;
  27 import gov.nasa.jpf.vm.VM;
  28
  29 import java.util.List;
  30
  31 import org.junit.Test;
  32
  33 /**
  34  * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
  35  */
  36 public class ThreadTest extends TestMultiProcessJPF {
  37   private native void keepThread(Thread thd, int prcId);
  38
  39   // To make sure that each process has its own main thread
  40   @Test
  41   public void mainThreadsIdTest() {
  42     if(!isJPFRun()) {
  43       JPF_gov_nasa_jpf_vm_multiProcess_ThreadTest.resetPrcIds();
  44     }
  45
  46     if (mpVerifyNoPropertyViolation(2)) {
  47       int prcId = getProcessId();
  48       keepThread(Thread.currentThread(), prcId);
  49     }
  50
  51     if(!isJPFRun()) {
  52       List<ThreadInfo> threads = JPF_gov_nasa_jpf_vm_multiProcess_ThreadTest.getThreads();
  53       assertEquals(threads.size(), 2);
  54       assertTrue(threads.get(0)!=threads.get(1));
  55     }
  56   }
  57
  58   private native void addToThreads(Thread thd);
  59
  60   public class TestThread extends Thread {
  61     @Override
  62         public void run() {
  63       addToThreads(this);
  64     }
  65   }
  66
  67   // To make sure that the total number of threads created does not exceed 4
  68   // where each processes includes two threads
  69   @Test
  70   public void numOfThreadsTest() {
  71     if(!isJPFRun()) {
  72       JPF_gov_nasa_jpf_vm_multiProcess_ThreadTest.resetThreads();
  73     }
  74
  75     if (mpVerifyNoPropertyViolation(2)) {
  76       TestThread thd = new TestThread();
  77       thd.start();
  78
  79       addToThreads(Thread.currentThread());
  80     }
  81
  82     if(!isJPFRun()) {
  83       assertEquals(JPF_gov_nasa_jpf_vm_multiProcess_ThreadTest.getThreadIds().size(), 4);
  84     }
  85   }
  86
  87   public static class InterleaveCheckListener extends ListenerAdapter {
  88     static int numOfCG = 0;
  89
  90     @Override
  91     public void choiceGeneratorProcessed (VM vm, ChoiceGenerator<?> newCG) {
  92       String id = newCG.getId();
  93
  94       if(!id.equals(SyncPolicy.ROOT) && !id.equals(SyncPolicy.TERMINATE)) {
  95         fail("Threads from two different processes should only interleave at the thread termination point!");
  96       }
  97
  98       numOfCG++;
  99     }
 100   }
 101
 102   private static int counter = 0;
 103
 104   // To make sure that the only point that threads from two processes interleave
 105   // is the thread termination point & number of choice generators does not
 106   // exceed 3
 107   @Test
 108   public void threadInterleavingTest() {
 109     if (mpVerifyNoPropertyViolation(2, "+listener=gov.nasa.jpf.vm.multiProcess.ThreadTest$InterleaveCheckListener",
 110             "+vm.max_transition_length=MAX")) {
 111       // InterleaveCheck listener makes sure that transition is not broken at the
 112       // static field access
 113       counter = 0;
 114     }
 115
 116     if(!isJPFRun()) {
 117       assertEquals(InterleaveCheckListener.numOfCG, 3);
 118     }
 119   }
 120 }