termination of two concurrent threads with shared variables
-
16-10-2019 - |
Question
We're in a shared memory concurrency model where all reads and writes to integer variables are atomic.
do:
$S_1$in parallel with:
$S_2$ means to execute $S_1$ and $S_2$ in separate threads, concurrently.atomically(
$E$)
means to evaluate $E$ atomically, i.e. all other threads are stopped during the execution of $E$.
Consider the following program:
x = 0; y = 4
do: # thread T1
while x != y:
x = x + 1; y = y - 1
in parallel with: # thread T2
while not atomically (x == y): pass
x = 0; y = 2
Does the program always terminate? When it does terminate, what are the possible values for x
and y
?
Acknowledgement: this is a light rephrasing of exercise 2.19 in Foundations of Multithreaded, Parallel, and Distributed Programming by Gregory R. Andrews.
Solution
This trace is possible, in two separate threads T1 and T2. $state$ is $(x,y)$.
- T1:
...
$state=(0, 4)$ - T1:
x = x + 1; y = y - 1
$~~state=(1, 3)$ - T1:
x = x + 1; y = y - 1
$~~state=(2, 2)$ - T2:
x == y
evaluates to true,pass
and thenx = 0;
$~~state=(0, 2)$ - T1:
x != y
evaluates to true,x = x + 1; y = y - 1
$~~state=(1, 1)$ - T2:
y = 2
$~~state=(1, 2)$ - T1:
x != y
evaluates to true,x = x + 1; y = y - 1
$~~state=(2, 1)$ - $state=(3, 0)$
- $state=(4, -1)$
- ...
(Note that it works even if x = expr;
is atomic)
There are other possible interleavings. The point $(2,2)$ is common to all of them, where T1 has pending (logically) atomic instructions:
T1: push x; push y; eq ? stop : push(x + 1); pop@x; push(y - 1); pop@y; repeat
T2: (x != y) ? repeat : x = 0; y = 2;
In the first case, T1 proceeds to stop
and then T2 can only proceed and the final state is $(0,2)$.
If T2 finally skips the repeat and (T1:push x
) is run before (T2:x = 0
) then T1 will stop looping and the same final state is reached.
If T2 finally skips the repeat and (T1:push x
) is run after (T2:x = 0
) then T2 can proceed after the stop
independently of (T1:y = 2
).
state = (0, 2)
T1: push(x + 1); pop@x; push(y - 1); pop@y; ...
T2: y = 2;
If T2 is run now then it will loop as above, so T1 proceeds:
state = (1, 2); stack = 1
T1: pop@y; ...
T2: y = 2;
If T2 is run now, this will go to the final state $(1,1)$. Otherwise:
state = (1, 1)
T1: push x; push y; eq ? stop : push(x + 1); pop@x; push(y + 1); pop@y; repeat
T2: y = 2;
If T2 does not act before push y
, this will stop and go to the state $(1,2)$. If it does, then the state is $(1, 2)$ and this will loop into $(2,1)$, $(3,0)$, ...
To sum up the possible final states are $(0,2)$, $(1,1)$, $(1,2)$. I don't think it was worth the effort though, since I probably made mistakes.