Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Missing docs on atomic nature of wait / notify #211

Open
anuraaga opened this issue Sep 11, 2023 · 1 comment
Open

Missing docs on atomic nature of wait / notify #211

anuraaga opened this issue Sep 11, 2023 · 1 comment

Comments

@anuraaga
Copy link

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.

@conrad-watt
Copy link
Collaborator

conrad-watt commented Oct 11, 2023

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants