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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Date:   Wed, 28 Mar 2018 14:04:07 -0400 (EDT)
From:   Alan Stern <stern@...land.harvard.edu>
To:     "Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>
cc:     schwidefsky@...ibm.com, <borntraeger@...ibm.com>,
        <linux-kernel@...r.kernel.org>, <linux-arch@...r.kernel.org>,
        <parri.andrea@...il.com>, <will.deacon@....com>,
        <peterz@...radead.org>, <boqun.feng@...il.com>,
        <npiggin@...il.com>, <dhowells@...hat.com>, <j.alglave@....ac.uk>,
        <luc.maranget@...ia.fr>, <akiyks@...il.com>
Subject: Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}

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