termination of two concurrent threads with shared variables

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.

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 then x = 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.

StackExchange Computer Science Q#443, answer score: 4