On Mon, May 27, 2024 at 02:25:01PM +0200, Hernan Ponce de Leon wrote: > On 5/24/2024 6:00 PM, Andrea Parri wrote: > > > What's the difference between R and R*, or between W and W*? > > > > AFAIU, herd7 uses such notation, "*", to denote a load or a store which > > is also in RMW. > > I also got confused with this. What about the following notation? > > R[once,RMW] ->rmw W[once,RMW] I'll add a (minimal) legenda describing this and some other notations in the next version. As Jonas remarked in his reply, * is what you would currently find in herd7-generated graphs, so I'd stick to it for the moment. Andrea