CSE 128 Spring
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
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.