I get your point, and my first question was "what operations are even atomic here for this problem to be well-defined?".
But I think "language operations are atomic and everything else isn't" is a reasonable inference for a puzzle.
I'm also intrigued by locking being done through atomic assignments; I thought it required at least something like "write if equal to value" or "write new value and return old".
I think that the following PROMELA code proofs it:
byte n = 0
byte A = 0
byte B = 0
proctype Client(byte id)
{
do
:: (A == 0) -> B = id
:: (A == id) ->
n = n + 1;
assert (n <= 1);
n = n - 1;
A = 0
od
}
proctype LockServer()
{
do
:: (A == 0) -> A = B
od
}
init {
atomic {
run LockServer();
run Client(1);
run Client(2);
run Client(3);
}
}
The idea is that there is one task that does the locking. It does so by copying a value from a memory location A to B, when B is equal 0 (the initial value) at regular intervals. Any task that wants to get the lock, writes a unique task identifier (unequal to 0) to memory location A and starts polling B. When it becomes equal to its task identifier, it did get the lock. To release the lock, it writes 0 to B. If it did not get the lock and sees that B has become zero, and A is different, it may overwrite A with its own task identifier.
This locking is 'slow' and has 'unfair' behavior.