Take-home exam

Consider the following procedures which are meant to be used to manage a disk by accessing
its tracks (numbered 0..N) in order.

initially
    pos := -2
    c := 0
    b := 1
    args := 0
    results := 0
    s[0], s[1], stored, saved, done are all empty
    arg, buf are not initialized

procedure use (k, in, out)
    // Called by users to read or write from/to the disk on track k
    if pos = -1 then pos := k
    else if k > pos then wait(s[c],k)
    else wait(s[b],k)
    arg := in
    args := args+1
    signal(stored)
    while results = 0 do wait(saved,0)
    out := buf
    results := results-1
    signal(done)

procedure get (in)
    // Called by disk driver when it is ready to read/write
    if not empty?(s[c]) then pos := next(s[c])
    else if empty?(s[b]) then pos := -1
    else t :=c; c := b; b := t; pos := next(s[c])
    signal(s[c])
    while args = 0 do wait(stored,0)
    in := arg
    args := args-1

procedure finished (out)
    // Called by disk driver when it is done reading/writing
    buf := out
    results := results+1
    signal(saved)
    while results > 0 do wait(done,0)

The synchronization commands have the following effects:
wait(s,n) -- put this process on the queue of s with index n and relinquish control
signal(s) -- awaken the favorite process on s but don't stop this execution
empty?(s) -- test if s is empty
next(s) -- return the index of favorite process on s

Notes: Any fixed number q of processes may be trying to use the disk at the same time.
The global variables mentioned in the programs are only accessible via the above instructions.
Furthermore, the system will ensure that only one of the procedures executes at any given time.
The "favorite" is the oldest of those having the smallest index.
An awakened process still needs to wait for the current procedure to terminate before it can acquire access.
If the queue is empty, then signal acts like skip.

Your tasks are to:

1. Express formally all the requirements placed on the many users and on the single driver.
2. Express formally all the desired properties of these procedures.
3. For each property, provide enough details (and no more) so that all that remains to verify the property (or of its absence) can be left to an automated theorem-prover, i.e. the formula is correct and semi-decidable (= recursively enumerable).

Warning: You may not communicate with anyone regarding this exam until the deadline has elapsed.
Blessing: behatzlahah!