On Mon, 2 Apr 2018, Paul E. McKenney wrote: > > > I will look at this more later, reaching end of both battery and useful > > > attention span... > > Like the following, perhaps? > > Thanx, Paul > > ------------------------------------------------------------------------ > > s390 > > include "fences.cat" > include "cos.cat" > > (* Fundamental coherence ordering *) > let com = rf | co | fr > acyclic po-loc | com as coherence > > (* Atomic *) > empty rmw & (fre;coe) as atom > > (* Fences *) > let mb = [M] ; fencerel(Mb) ; [M] > > (* TSO with multicopy atomicity *) > let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > acyclic mb | po-ghb | fr | rf | co as sc Yes, that should work okay (apart from issues related to ordering of atomic accesses). By the way, what does that last "sc" stand for? Surely not Sequential Consistency! You might consider renaming it to "tso-mca". Alan