ocaml-multicore
Synchronization in work-stealing deque
In src/ws_deque.ml, the tab field is not atomic, contrary to the reference implementation in relaxed memory (Correct and Efficient Work-Stealing for Weak Memory Models). Furthermore, there is no synchronization before writing to this field in push and pop_as. Therefore, in my understanding, there is no guarantee that the thieves do not read Obj.magic () (from realloc) when accessing tab in steal_as (same scenario as https://fzn.fr/readings/errata-ppopp207-le.txt).
Are you sure it is correct? Maybe it relies on a synchronization mechanism I am not aware of.
Writes like https://github.com/ocaml-multicore/saturn/blob/f343045c0547fca9ab9ed6dfaf4dbe59d8f3926e/src/ws_deque.ml#L97 generate calls to caml_modify, which uses atomic_store_release.
A store with a release fence does not allow preceding reads or writes to be moved after it.
However, the OCaml memory model does not prevent non-atomic writes from being reordered.
Instead of making .tab an atomic and adding an indirection, another alternative would be to add an atomic write, e.g. Multicore_magic.fence q.bottom, just before writing q.tab <- a.
OCaml 5.4 will feature atomic record fields: https://github.com/ocaml/ocaml/pull/13404. I imagine this will be a better alternative. In the meantime, I would suggest simply making .tab atomic.