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
