next = next + 1 does not obey the At-Most-Once property becuase it
contains a critical reference and it writes a variable that is read in another
computation. Concurrent execution of the statement could produce results not
consistent with some sequential interleaving.
Suppose that computations i and j (i != j) both execute
next = next + 1
"at the same time". Notice that each computation has to be in the critical
region to do so. By the next-ticket property of the global invariant, it must
be the case that turn[i] == next and turn[j] == next, that is,
turn[j] == turn[i].
However, by the unique-ticket property of the global invariant, if i != j,
then turn[i] != turn[j], a contradiction. It is not possible for two
computations to execute
next = next + 1
at the same time, and the statement is effectively atomic even though it doesn't obey the At-Most-Once property.
This page last modified on 19 June 2003.