src/tests/gov/nasa/jpf/test/java/concurrent/SemaphoreTest.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.java.concurrent;
  19
  20 import gov.nasa.jpf.util.test.TestJPF;
  21
  22 import java.util.concurrent.Semaphore;
  23
  24 import org.junit.Test;
  25
  26 /**
  27  * simple test for Java 1.5 java.util.concurrent support
  28  */
  29 public class SemaphoreTest extends TestJPF {
  30
  31   //--- test methods
  32
  33   static final int MAX = 1;
  34   static final Semaphore avail = new Semaphore(MAX, true);
  35   static Resource[] items = new Resource[MAX];
  36   static boolean[] isUsed = new boolean[MAX];
  37   static final Object lock = new Object();
  38
  39
  40   static {
  41     for (int i = 0; i < items.length; i++) {
  42       items[i] = new Resource(i);
  43     }
  44   }
  45
  46   static class Resource {
  47
  48     String id;
  49     String user;
  50
  51     Resource(int id) {
  52       this.id = "Resource-" + id;
  53     }
  54
  55     public void use(String newUser) {
  56       assert user == null : "resource " + id + " in use by " + user +
  57               ", but attempted to be acquired by: " + newUser;
  58       user = newUser;
  59     }
  60
  61     public void release() {
  62       user = null;
  63     }
  64
  65     @Override
  66         public String toString() {
  67       return id;
  68     }
  69   }
  70
  71   public static Resource getItem() throws InterruptedException {
  72     avail.acquire();
  73
  74     synchronized (lock) {
  75       for (int i = 0; i < MAX; i++) {
  76         if (!isUsed[i]) {
  77           isUsed[i] = true;
  78           return items[i];
  79         }
  80       }
  81     }
  82     assert false : "couldn't find unused resource";
  83     return null;
  84   }
  85
  86   public static void putItem(Resource o) {
  87     synchronized (lock) {
  88       for (int i = 0; i < MAX; i++) {
  89         if (items[i] == o) {
  90           if (isUsed[i]) {
  91             isUsed[i] = false;
  92             avail.release();
  93           }
  94           break;
  95         }
  96       }
  97     }
  98   }
  99
 100   static class Client implements Runnable {
 101
 102     @Override
 103         public void run() {
 104       String id = Thread.currentThread().getName();
 105
 106       try {
 107         System.out.println(id + " acquiring resource..");
 108         Resource r = SemaphoreTest.getItem();
 109         System.out.println(id + " got resource: " + r);
 110
 111         r.use(id);
 112         //.. more stuff here
 113         r.release();
 114
 115         System.out.println(id + " releasing resource: " + r);
 116         SemaphoreTest.putItem(r);
 117         System.out.println(id + " released");
 118
 119       } catch (InterruptedException ix) {
 120         System.out.println("!! INTERRUPTED");
 121       }
 122     }
 123   }
 124
 125   //--------------- the test cases
 126   @Test
 127   public void testResourceAcquisition() {
 128     if (verifyNoPropertyViolation()) {
 129       for (int i = 0; i <= MAX; i++) {
 130         Thread t = new Thread(new Client());
 131         t.start();
 132       }
 133     }
 134   }
 135 }