examples/BoundedBuffer.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 /**
  20  * concurrency example with deadlock
  21  * adapted from "Concurrency: State Models & Java Programs", Jeff Magee & Jeff Kramer
  22  *
  23  * Note there need to be at least 2x buffer_size instances of either producers or
  24  * consumers in order to produce the deadlock, which basically depends on
  25  * a notification choice between a consumer and a producer in a context where
  26  * only threads of the notifier type are still runnable
  27  *
  28  * This is a good benchmark for state management/matching in a small heap context.
  29  * Higher numbers of buffer size and producers/consumers result in a nice
  30  * state explosion
  31  */
  32 public class BoundedBuffer {
  33
  34   static int BUFFER_SIZE = 1;
  35   static int N_PRODUCERS = 4;
  36   static int N_CONSUMERS = 4;
  37
  38   static Object DATA = "fortytwo";
  39
  40   //--- the bounded buffer implementation
  41   protected Object[] buf;
  42   protected int in = 0;
  43   protected int out= 0;
  44   protected int count= 0;
  45   protected int size;
  46
  47   public BoundedBuffer(int size) {
  48     this.size = size;
  49     buf = new Object[size];
  50   }
  51
  52   public synchronized void put(Object o) throws InterruptedException {
  53     while (count == size) {
  54       wait();
  55     }
  56     buf[in] = o;
  57     //System.out.println("PUT from " + Thread.currentThread().getName());
  58     ++count;
  59     in = (in + 1) % size;
  60     notify(); // if this is not a notifyAll() we might notify the wrong waiter
  61   }
  62
  63   public synchronized Object get() throws InterruptedException {
  64     while (count == 0) {
  65       wait();
  66     }
  67     Object o = buf[out];
  68     buf[out] = null;
  69     //System.out.println("GET from " + Thread.currentThread().getName());
  70     --count;
  71     out = (out + 1) % size;
  72     notify(); // if this is not a notifyAll() we might notify the wrong waiter
  73     return (o);
  74   }
  75
  76   //--- the producer
  77   static class Producer extends Thread {
  78     static int nProducers = 1;
  79     BoundedBuffer buf;
  80
  81     Producer(BoundedBuffer b) {
  82       buf = b;
  83       setName("P" + nProducers++);
  84     }
  85
  86     @Override
  87         public void run() {
  88       try {
  89         while(true) {
  90           // to ease state matching, we don't put different objects in the buffer
  91           buf.put(DATA);
  92         }
  93       } catch (InterruptedException e){}
  94     }
  95   }
  96
  97   //--- the consumer
  98   static class Consumer extends Thread {
  99     static int nConsumers = 1;
 100     BoundedBuffer buf;
 101
 102     Consumer(BoundedBuffer b) {
 103       buf = b;
 104       setName( "C" + nConsumers++);
 105     }
 106
 107     @Override
 108         public void run() {
 109       try {
 110         while(true) {
 111             Object tmp = buf.get();
 112         }
 113       } catch(InterruptedException e ){}
 114     }
 115   }
 116
 117   //--- the test driver
 118   public static void main(String [] args) {
 119     readArguments( args);
 120     //System.out.printf("running BoundedBuffer with buffer-size %d, %d producers and %d consumers\n", BUFFER_SIZE, N_PRODUCERS, N_CONSUMERS);
 121
 122     BoundedBuffer buf = new BoundedBuffer(BUFFER_SIZE);
 123
 124     for (int i=0; i<N_PRODUCERS; i++) {
 125       new Producer(buf).start();
 126     }
 127     for (int i=0; i<N_CONSUMERS; i++) {
 128       new Consumer(buf).start();
 129     }
 130   }
 131
 132   static void readArguments (String[] args){
 133     if (args.length > 0){
 134       BUFFER_SIZE = Integer.parseInt(args[0]);
 135     }
 136     if (args.length > 1){
 137       N_PRODUCERS = Integer.parseInt(args[1]);
 138     }
 139     if (args.length > 2){
 140       N_CONSUMERS = Integer.parseInt(args[2]);
 141     }
 142   }
 143 }