CSE 128 Spring 2004
Concurrency
Problem 3.4: You need to come up with two specifications. The first one will have buf have m > n elements, and nxtC and nxtR will take on values from 0 to m - 1. The second one will have buf have n elements, and nxtC and nxtR will take on values from 0 to 2n - 1.

Problem 3.5:  We've put SemProducerConsumer.java on the web page for you to use. This is the code that is shown in Figure 3.5. You'll need to write a driver program that uses this class and your own class (say, BWProducerConsumer). The program will take as input the value N. It will create two threads, a producer thread and a consumer thread. They will produce and consume a fixed number of values C that is many times larger than N. Each will waste some time before producing or consuming again (you can do this by having them go into a loop). The producer should be faster than the consumer (you can have the producer count to some value X and have the consumer count to 2X). Measure how long it takes for the consumer thread to consume C values using SemProducerConsumer and how long it takes the consumer thread to consume C values using BWProducerConsumer. Do this experiment for several values of N.

You should find that the busy waiting-based version will run faster as N increases but the semaphore version will run at the same speed. Depending on the value of N and the time you have the producer and consumer run, you may find that the busy waiting-based version will stop running faster when you reach a certain value of N. If you run this by ssh into ieng9, you may see yet another behavior (isn't systems fun?) so you might want to run this from one of the lab machines.

Problem 3.7:  In finding the invariant, if you were to prove, say, that ListPCCall(v) implies PCCall(v) under your refinement mapping, what invariant would let you do that? Look at the conjuncts of ListPCCall(v) and those of PCCall(v) under refinement and see how you'd do the proof by hand.