Avoid re-using register in ticketlock

[hernanponcedeleon]

The idea of the final condition is to check that each lock reads a different ticket. While I think in a correct implementation, we would still check original-read-r1-T0 + != original-read-r1-T1, I don't think this is guaranteed if the mutual exclusion does not hold.

This PR solves the issue by simply using a fresh register for the release store.

[ThomasHaas]

I don't really see a big difference in the new and the old code. In both cases, 0:r1 != 1:r1 simply by atomicity of the RMW instructions (i.e., you do not even need to care about proper synchronisation). So the condition that both are different is trivially satisfied I would say.
Anyway, that means this PR is fine :)

[hernanponcedeleon]

You are right that the first two conditions are trivially satisfied. I now know what confused me. Initially I only had the conditions about the critical sections and even the correct code was failing. This is because one thread could acquire the lock and the other fails. Since the initial code of registers matches what I was expecting not to be read from x, then it was possible to match the final state.

I added these extra conditions to try to force that each lock acquire succeeds (this could also be solved if the initial value of x would be different than the initial value of registers), but the condition is wrong.
The correct query should be exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0).

I will update this.

[ThomasHaas]

I see. I think this is because we evaluate litmus assertions even for executions that do not terminate properly.
I guess the way litmus assertions are intended, they should never get evaluated for incomplete executions, i.e., those that hit bound events or are stuck in spinloops.
We could modify our assertion encoding for litmus so as to only consider complete executions and then you wouldn't need to those lock acquisition conditions anymore.

[hernanponcedeleon]

That is orthogonal to the changes in here. I'll tackle that problem in a different PR.

[ThomasHaas]

Of course. You can go ahead and merge.