[fjfaase]

This implicitely assumes atomic assignments, meaning that during an assignment all bits representing a value are transfered in one atomic unit. This sounds a bit trivial, but if one would be working with large integers that are stored in multiple memory words, it is less trivial.

I think it is possible to implement locking with only atomic assigments.

[jprete]

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".

[fjfaase]

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.

[fjfaase]

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);
        }
    }

It fails when two 'Client(2)' is replaced by 'Client(1)'

[yencabulator]

You can replace the read and store with atomic operations and n==2 is still possible. As far as I can tell, the model being verified already uses atomic operations.

[bcoates]

Yeah, looking at the code my 'intuition' was "this is a classic data race, the program is broken" not "somewhere between 10 and 20".

I suppose if you assume all global accesses are atomic, it's a good demonstration that atomic operations don’t compose atomically (even in trivial cases) and aren't particularly useful as concurrency primitives.

[Salgat]

The question is more testing your full understanding of why this is a race condition, including understanding the possible side effects, since that's the only thing you start out with when someone sends in a bug report.