§P415 Homework Assignment

This assignment is not more difficult than the first two SMV assignments; the modeling task is roughly the same as the Observer-Reporter problem. The goal here is to explore the complexity limits of model checking decision procedures.

The Thread Game

This problem is due to J Stother Moore, who described it to me at the TPHOLs Conference in 2001. Related information can be found in material for a more challenging problem involving unbounded concurrency.

The assignment:
       A. Model the system described below in SMV and demonstrate the truth of the CLAIM for various values of N. Use SMV to construct an answer. In other words, rather than simply proving that a given value of N is possible, use refutation to show how that value can arrive in G.

       B. Using increasing values of N, experimentally estimate the running time and memory requirements as a function of N.

CAUTION Do not run multiple smv sessions on departmental computers. Learn to use the nice command before attempting long background runs. Be reasonable about the size of N you attempt; that is, work up toward it. Good citizenship demands that you not attempt to solve this problem for an instance of N for which there is no hope of getting an answer. Bad citizenship may be penalized.

       C. Write a report presenting your results under the name report.ext with the appropriate extension. As always, P515 students must use LaTeX and include all files involved in generation of the document. P415 students may use any document preparation system but should include a .pdf, .txt, or .htm version of their report.

       D. (optional) Include a "rigorous" proof (i.e. mathematically precise, not logically formal) of the CLAIM in your report. Although you may be able to do this proof on your own, consider whether the SMV experimentation provides any insight into the proof discovery.

The system

Concurrent processes A and B have unprotected access to a common program variable, G, whose initial value is 1. Each is simply a cycle that repeatedly doubles the value of G,
Process A:
while true do G := G + G

Process B:
while true do G := G + G
A naive compiler translates these source statements to machine-level operations involving local ("register") variables Ai and Bj
Process A:       Process B:
Loop: A1 := G; Loop: B1 := G;
A2 := G; B2 := G;
A3 := A1 + A2; B3 := B1 + B2;
G := A3; G := B3;
go to Loop; go to Loop;

CLAIM: For any given integer N > 0, it is possible for G to acquire that value N at some time during an asynchronous concurrent execution of A and B.