src/tests/gov/nasa/jpf/test/java/concurrent/CountDownLatchTest.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.java.concurrent;
  20
  21 import gov.nasa.jpf.util.test.TestJPF;
  22 import gov.nasa.jpf.vm.Verify;
  23
  24 import java.util.concurrent.CountDownLatch;
  25 import java.util.concurrent.Exchanger;
  26 import java.util.concurrent.ExecutorService;
  27 import java.util.concurrent.Executors;
  28
  29 import org.junit.Test;
  30
  31 public class CountDownLatchTest extends TestJPF {
  32
  33   private static final int N = 2;                    // Too many states to test if set higher than 2.  jpf-concurrent's gov.nasa.jpf.test.java.concurrent.CountDownLatchTest can handle more threads.
  34   private static final int COUNTER_SUCCESS   = 0;
  35   private static final int COUNTER_EXCHANGED = 1;
  36
  37
  38   //@Ignore("detects deadlock with exposure CG??")
  39   @Test
  40   public void testCountDown() throws InterruptedException {
  41     if (verifyNoPropertyViolation("+vm.time.model=ConstantZero", "+vm.por.break_on_exposure=true")) {
  42
  43       final CountDownLatch    latch     = new CountDownLatch(N);
  44       final Exchanger<Object> exchanger = new Exchanger<Object>();
  45       final ExecutorService   service   = Executors.newFixedThreadPool(N);
  46
  47       Runnable task = new Runnable() {
  48         @Override
  49                 public void run() {
  50           try {
  51             Object source = new Object();
  52             Object result = exchanger.exchange(source);
  53             //Object result = exchanger.exchange(source, 1L, TimeUnit.SECONDS); // If N==2 and without jpf-concurrent, the timeout causes 149,808 states to be explored.
  54             assert source != result : "source != result";
  55             assert result != null : "result != null";
  56             latch.countDown();
  57             Verify.incrementCounter(COUNTER_EXCHANGED);
  58           } catch (InterruptedException e) {
  59             throw new Error(e);
  60           }
  61         }
  62       };
  63
  64       for (int i = 0; i < N; i++) {
  65         service.execute(task);
  66       }
  67
  68       latch.await();
  69       service.shutdown();
  70
  71       Verify.incrementCounter(COUNTER_SUCCESS);
  72
  73     } else { // outside JPF
  74       assert Verify.getCounter(COUNTER_SUCCESS) > 0 : "never succeeded";
  75       assert Verify.getCounter(COUNTER_EXCHANGED) > 0 : "never exchanged";
  76     }
  77   }
  78 }