WBW THEORY ASSIGNMENT	    		 Wed Mar 21 2001

The goal of this assignment is to prove that two-server
algorithms which might be selected for WBW work properly
in all appropriate circumstances, or to find failure
modes for these algorithms.  There are three different
algorithm approaches outlined in Draft 3a of the WBW
Storage System Specification, and, as part of this
assignment, additional (asymmetric) algorithms may be
proposed.

The method of this assignment is to have the class
produce a single document cooperatively.  This
document will prove various things about various
algorithms, and may introduce one or two new algorithms.

The procedure will be as follows:

1. Cooperatively produce an outline of the document.

2. Assign non-proof parts of the document (including
   statements of results to be proved) to author/editor
   pairs of students, and write first drafts of these.

3. Assign proofs to be included in the document to
   author/editor pairs of students.

4. Get everything done in final form.

5. Do some modest amount of rewriting under instructor
   supervision.

When part of a document is assigned to one student as
author and a second student as editor, the author is
to produce drafts of that document part, the editor
is to mark these up, and all drafts, including the
marked up ones, are to be turned in.

The circumstances in which the algorithm are to run
include the following.

A. There are 4 different two-server WBW operations,
   namely two-server open and three two-server link
   operations.

B. There may be race conditions between pairs of
   these operations being performed by different
   clients, or even by the same client.

C. Any of the processes involved in an operation may
   not be running when the operation is started.

D. Any of the processes involved in an operation may
   crash during the operation.

E. Any of the processes involved in an operation may
   be run by an evil person who is trying to crash or
   corrupt the other processes involved in the
   operation.

The algorithm properties to be investigated include:

I. Termination.

II.  Not doing any harm (includes agreement usually).

III. Efficiency.

Note:  Proofs can be `informal'.  An informal proof
should convince the knowledgeable reader that a formal
proof can be constructed.