Hacker News Reader

Comment by jprete | Hacker News Reader

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

View on HN

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.

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)'

Reply on news.ycombinator.com