Synchronization in work-stealing deque

[clef-men]

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.

[lyrm]

Thanks for reporting this ! I will have a look.

[polytypic]

Writes like

saturn/src/ws_deque.ml

Line 97 in f343045

q.tab <- a;

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.

[clef-men]

OCaml 5.4 will feature atomic record fields: ocaml/ocaml#13404. I imagine this will be a better alternative. In the meantime, I would suggest simply making .tab atomic.