CSCI P415/515 Wed Mar 21 15:53:54 EDT 2012 [SDJ]

The Thread Game

The Thread Game problem is due to J Strother Moore, who described it to me in a bar in Edinborough, Scotland during the TPHOLs Conference in 2001.


  1. Modify the Observer-Reporter problem to model the Thread Game problem, described below. Call this file tg.smv.
  2. Using vw make SMV demonstrate the Claim for small values of N. Formulate the Claim in such a way that SMV shows you how the given value of N is computed.
  3. Plot a graph showing the computational effort (either time or space) for N = 1, 2, 3, ... . Note: proceed incrementally until you see a clear trend indicating complexity.
  4. (Optional) Prove the Claim.
  5. Write a report, report.pdf, explaining your results.

The Thread Game

Identical concurrent processes A and B have unprotected access to a common program variable, G, whose initial value is 1. Each process 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;
Note: The model above was the one Moore presented to me. In model checking, it is important to keep the models as small as possible. Toward this end, I recommend replacing local "registers" A3 and B3 with A2 and B2. This is allowed under the machine-level instruction set we are using.

Claim: For any 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.