LKMM: Making RMW barriers explicit

Alan Stern
2024-05-16T01:43:24Z

Hernan and Jonas:

Can you explain more fully the changes you want to make to herd7 and/or
the LKMM? The goal is to make the memory barriers currently implicit in
RMW operations explicit, but I couldn't understand how you propose to do
this.

Are you going to change herd7 somehow, and if so, how? It seems like
you should want to provide sufficient information so that the .bell
and .cat files can implement the appropriate memory barriers associated
with each RMW operation. What additional information is needed? And
how (explained in English, not by quoting source code) will the .bell
and .cat files make use of this information?

Alan