Re: LKMM: Making RMW barriers explicit

Andrea Parri
2024-05-24T03:30:29Z

> Do you mean the one example in Table 3?
> What about cmpxchg() or cmpxchg_acquire()?

Yes, Table 3.

The cmpxchg*() primitives were not discussed in the paper. IIRC, their
representation has not changed since at least 1c27b644c0fd.

> We're definitely getting rid of some lines in herd7, that have been added
> solely for dealing with this specific case of LKMM.

Good. If the herd7 maintainers are "tired" of dealing with those lines,
that's definitely a big fat "why" to put in a changelog.

> Deal with what, no longer having to learn OCaml to be sure that the LKMM's
> formal definition matches the description in memory_barriers.txt?

Nope. ;-) Dealing with the review, testing, and maintainance of a new
representation.

> - it makes it easier to maintain the LKMM in the future, because you don't
> have to work around hidden transformations inside herd7
> - it makes implicit behavior explicit
> - it makes it easier to understand that the formalization matches the
> intention
> - it makes it easier to learn the LKMM from the formalization without having
> to cross-reference every bit with the informal documentation to avoid
> misunderstandings

Jonas - You write "less hidden", "less implicit", but I keep reading "a
representation I/some people would expect". We've already acknowledged
that's no deciding factor to abandon the current seasoned representation.

Andrea