Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}

[Alan Stern]

On Wed, 28 Mar 2018, Paul E. McKenney wrote:

> On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote:
> > On Wed, 28 Mar 2018, Paul E. McKenney wrote:
> > 
> > > Hello!
> > > 
> > > The prototype patch shown below provides files required to allow herd7 to
> > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering
> > > provided by s390.  This patch should be viewed with great suspicion.
> > > It does what I expect it to do on SB (with and without barriers),
> > > IRIW without barriers, and Alan's SB with read-of-write added, but my
> > > expectations are quite likely faulty, and my test cases are very few
> > > in number.
> > > 
> > > Either way, this is the easy part.  The hard part (which I am happy
> > > to leave to others) is making litmus7 and klitmus7 able to do tests
> > > on actual hardware, as well as enabling herd to handle litmus tests
> > > containing BAL.  ;-)
> > > 
> > > Note that CPU architectures already supported by herd might well need
> > > only a .cfg file that refers to herd's pre-existing support.
> > > 
> > > Thoughts?
> > 
> > I don't quite see the point of this.  You're not suggesting that we
> > have one Linux Kernel Memory Consistency Model for s390 and another
> > one for all the other architectures, are you?
> 
> Certainly not for common code!
> 
> > If the idea is merely to provide a herd model for s390 then it should 
> > go into the DIY repository, not into the LKMM repository.
> 
> Makes sense.
> 
> In the meantime, does the cat file look to you like it correctly
> models the combination of TSO and multicopy atomicity?  Do the
> fences really work, or did I just get lucky with my choice of
> litmus tests?

You got lucky.  Try creating an SB litmus test where, instead of an
smp_mb() fence between the write and the read, each thread executes
some other kind of fence.

The acyclicity condition should have been written more like this:

let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W])

acyclic mfence | po_ghb | rf | fr | co as tso-mca

I don't know what the fence instruction is on s390; change the "mfence"
above accordingly.  The main difference between this and the
corresponding expression in x86tso.cat is that I replaced rfe with rf.

This doesn't account for atomic operations properly; see the "implied" 
term in x86tso.cat.

Alan