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