Back
public class BBDriver {
public static void main (String [] args) {
BoundedBuffer b1 = new BoundedBuffer(3);
BoundedBuffer b2 = new BoundedBuffer(3);
b1.add(new Element());
b1.add(new Element());
(new InOut1(b1,b2)).start();
(new InOut2(b2,b1)).start();
}
}
class Element {
}
/**
* @observable
* EXP Full: (head_ == tail_);
* EXP IndexRange: (head_ >= 0 && tail_ >= 0 && head_ < bound_ && tail_ < bound_);
*/
class BoundedBuffer {
Element [] buffer_;
int bound_;
int head_, tail_;
/**
* @assert
* PRE PositiveBound: (b > 0);
*/
public BoundedBuffer(int b) {
bound_ = b;
buffer_ = new Element[bound_];
head_ = 0;
tail_ = bound_-1;
}
/**
* @assert
* POST addPost: (head_==0) ? buffer_[bound_-1]==o : buffer_[head_-1]==o;
* @observable
* INVOKE addInvoke;
*/
public synchronized void add(Element o) {
while ( tail_ == head_ )
try { wait(); } catch ( InterruptedException ex) {}
buffer_[head_] = o;
head_ = (head_+1) % bound_;
notifyAll();
}
/**
* @observable
* RETURN takeReturn;
*/
public synchronized Element take() {
while ( head_ == ((tail_+1) % bound_) )
try { wait(); } catch ( InterruptedException ex) {}
tail_ = (tail_+1) % bound_;
notifyAll();
return buffer_[tail_];
}
/**
* @observable
* RETURN isEmptyReturnTrue: ($ret == true);
*/
public synchronized boolean isEmpty() { return head_ == ((tail_+1) % bound_); }
}
class InOut1 extends Thread {
BoundedBuffer in_,out_;
public InOut1(BoundedBuffer in, BoundedBuffer out) {
in_ = in;
out_ = out;
}
public void run() {
Element tmp;
while(true) {
tmp = in_.take();
System.out.println("Take 1");
out_.add(tmp);
System.out.println("Put 1");
}
}
}
class InOut2 extends Thread {
BoundedBuffer in_,out_;
public InOut2(BoundedBuffer in, BoundedBuffer out) {
in_ = in;
out_ = out;
}
public void run() {
Element tmp;
while(true) {
tmp = in_.take();
System.out.println("Take 2");
out_.add(tmp);
System.out.println("Put 2");
}
}
}
Back