Clarifications for Problem Set 5

Some problems in this problem set require establishing
whether a system can deadlock or not.

In general, to show that a system *can* deadlock, describe a
reachable state where the system can make no progress (there
are no further transitions possible).

In general, to show that a system *cannot* deadlock, show
that in every reachable state there is a transition that the
system can make.

The arguments for deadlocks should be precise and detailed,
although they need not be formal.  To describe particular
states you can label program points and talk about certain
thread being at certain program point in its execution.

Problem 1
---------

"Replace the knife and fork" means that each gourmand puts
the knife and fork back to the same position at table where
she took them from.

In the part a) you should just write in Spec the
implementation that matches the problem.  You may use the
synchronization primitives that we introduced in the class
(like locks and condition variables).

The program will probably be clearer if you write it so that
it works for any even number of gourmands and not just 6.

In part b) you should check whether your program can
deadlock or not.  My solution is 1/4 of a page 10pt font.

Problem 2
---------

The guard in the definition of Consume applies to the entire
sequence of statements that follows it (that follows from
the syntax of Spec).  This means that Consume won't execute
if the buffer is empty.

When writing part a) I suggest you name your implementation
BoundBufferImpl.

You can make the effective size of your buffer be N-1 and
not N (clearly it is less than 1/1000 of difference for the
given value of N).

For part b), you may want to look at page 24 of the Handout
17 on formal concurrency for a proof that BufferImpl
implements Buffer.  You may also use the rules for
increasing the atomicity of the region if you explain why
you may do it (see page 6 of the Handout 17).

My solution for b) makes atomic actions larger using
properties of locks (and explains why that is okay), and
then performs pretty much standard proof using a simulation
relation to show the correspondence of operations on my data
structure with operations in the specification.

For property c), "system always makes progress" here means
that it *completes* some Consume or Produce actions.  Merely
starting actions without possibility for any of them to
complete is not a good notion of progress in this problem.
The assumption on the environment that you are allowed to
make is:

 If you wait long enough, a Consume action will be initiated, and
 if you wait long enough, a Produce action will be initiated.

The property that you need to show is "if you wait long
enough, then some action will complete".

Assume that the scheduler has the following property: it
never produces an infinite trace with the property that: an
action inside Produce or Consume remains enabled infinitely
many times, but never executes.

I used this property to argue that operations eventually
complete.  I believe my argument is precise enough (although
I used English) and it still fits in about 1/3 of a
full-width 10pt page.

Problem 3
---------

If you read the handout and understand the problem the
problem should not be too difficult.

For part c) you may find it useful to use techniques similar
to those used in Problem 3 of the Problem Set 1.