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.
Instructions
-
Modify the Observer-Reporter problem
to model the Thread Game problem, described below.
Call this file tg.smv.
-
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.
-
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.
-
(Optional) Prove the Claim.
-
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.