Re: LKMM: Making RMW barriers explicit

From: Andrea Parri
Date: Thu May 23 2024 - 05:04:33 EST


> It would be much simpler if
> one could find all the information to support lkmm in tools/memory-model/
> (in the form of the model + some comments or a .txt to cover those things we
> cannot move out of the tool implementation), rather than having to dive into
> herd7 code.

Got it. And I do find that very relatable to LKMM developers who, like me,
are definitely not fluent in OCaml. :-/

Let me draft some .txt to such effect, based on but expanding and hopefully
completing my previous remarks in

https://lore.kernel.org/lkml/ZjrSm119+IfIU9eU@andrea/

Having something like that "on paper" can also help evaluate future changes
to the tool and/or model.

Thank you for the suggestion.

Andrea