> 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
