2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
20 * concurrency example with deadlock
21 * adapted from "Concurrency: State Models & Java Programs", Jeff Magee & Jeff Kramer
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
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
32 public class BoundedBuffer {
34 static int BUFFER_SIZE = 1;
35 static int N_PRODUCERS = 4;
36 static int N_CONSUMERS = 4;
38 static Object DATA = "fortytwo";
40 //--- the bounded buffer implementation
41 protected Object[] buf;
44 protected int count= 0;
47 public BoundedBuffer(int size) {
49 buf = new Object[size];
52 public synchronized void put(Object o) throws InterruptedException {
53 while (count == size) {
57 //System.out.println("PUT from " + Thread.currentThread().getName());
60 notify(); // if this is not a notifyAll() we might notify the wrong waiter
63 public synchronized Object get() throws InterruptedException {
69 //System.out.println("GET from " + Thread.currentThread().getName());
71 out = (out + 1) % size;
72 notify(); // if this is not a notifyAll() we might notify the wrong waiter
77 static class Producer extends Thread {
78 static int nProducers = 1;
81 Producer(BoundedBuffer b) {
83 setName("P" + nProducers++);
90 // to ease state matching, we don't put different objects in the buffer
93 } catch (InterruptedException e){}
98 static class Consumer extends Thread {
99 static int nConsumers = 1;
102 Consumer(BoundedBuffer b) {
104 setName( "C" + nConsumers++);
111 Object tmp = buf.get();
113 } catch(InterruptedException e ){}
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);
122 BoundedBuffer buf = new BoundedBuffer(BUFFER_SIZE);
124 for (int i=0; i<N_PRODUCERS; i++) {
125 new Producer(buf).start();
127 for (int i=0; i<N_CONSUMERS; i++) {
128 new Consumer(buf).start();
132 static void readArguments (String[] args){
133 if (args.length > 0){
134 BUFFER_SIZE = Integer.parseInt(args[0]);
136 if (args.length > 1){
137 N_PRODUCERS = Integer.parseInt(args[1]);
139 if (args.length > 2){
140 N_CONSUMERS = Integer.parseInt(args[2]);