4 ms·

This implicitely assumes atomic assignments, meaning that during an assignment all bits representing a value are transfered in one atomic unit. This sounds a bi

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.

bcoates 2y ago
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 2y ago
  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.
jprete 2y ago
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 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 ago
    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 2y ago
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 2y ago

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 2y ago
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.

jprete 2y ago

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 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 ago
  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 2y ago

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.