threads icon indicating copy to clipboard operation
threads copied to clipboard

Missing docs on atomic nature of wait / notify

Open anuraaga opened this issue 11 months ago • 1 comments

wait and notify are probably inspired by futex APIs. However, currently they seem to be underspecified in terms of atomicity. When referring to futex docs

https://man7.org/linux/man-pages/man2/futex.2.html

       loading of the futex word's value, the comparison of that value
       with the expected value, and the actual blocking will happen
       atomically and will be totally ordered with respect to concurrent
       operations performed by other threads on the same futex word.
       Thus, the futex word is used to connect the synchronization in
       user space with the implementation of blocking by the kernel.

In other words, there should be no concurrent wait/notify operations for a given address.

Here, there is no such language, only sequential ordering and "Otherwise, the wait operation begins by performing an atomic load from the given address. If the loaded value is not equal to the expected value, the operator returns 1 ("not-equal"). If the values are equal, the agent is suspended. ", this latter note not mentioning that this all has to be atomic vs other operations on the given address. An implementation (like my first prototype :P) may not preserve this atomicity if only implementing based on the wording.

anuraaga avatar Sep 11 '23 06:09 anuraaga

The formal specification now documents this as a consequence of the relaxed memory model, but I think there's room to add further non-normative language clarifying this in plain English. I'll look into this shortly. Currently the note which comes closest to documenting this behaviour comes at the end of the relaxed memory model section:

All operations on the same location which change the state of that location’s wait queue are sequentially consistent and totally ordered by happens-before.

But this doesn't explicitly say that the read and "wait queue modifying" parts of the wait operation happen atomically (in the sense of simultaneously and indivisibly).

conrad-watt avatar Oct 11 '23 21:10 conrad-watt