4 ms·
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
by fjfaase 2y ago
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 2y agoI 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)'