termination of two concurrent threads with shared variables
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.