linux-kernel - Re: [PATCH 2/2 v2 RFC] tools/memory-model: redefine rb in terms of rcu-fence

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]

Message-ID: <Pine.LNX.4.44L0.1803011027120.1394-100000@iolanthe.rowland.org>
Date:   Thu, 1 Mar 2018 10:49:05 -0500 (EST)
From:   Alan Stern <stern@...land.harvard.edu>
To:     Boqun Feng <boqun.feng@...il.com>
cc:     LKMM Maintainers -- Akira Yokosawa <akiyks@...il.com>,
        Andrea Parri <parri.andrea@...il.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        Luc Maranget <luc.maranget@...ia.fr>,
        Nicholas Piggin <npiggin@...il.com>,
        "Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>,
        Peter Zijlstra <peterz@...radead.org>,
        Will Deacon <will.deacon@....com>,
        Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: [PATCH 2/2 v2 RFC] tools/memory-model: redefine rb in terms of
 rcu-fence

On Thu, 1 Mar 2018, Boqun Feng wrote:

> > +let rec rcu-fence = gp |
> > +	(gp ; rcu-link ; rscs) |
> > +	(rscs ; rcu-link ; gp) |
> > +	(gp ; rcu-link ; rcu-fence ; rcu-link ; rscs) |
> > +	(rscs ; rcu-link ; rcu-fence ; rcu-link ; gp) |
> > +	(rcu-fence ; rcu-link ; rcu-fence)
> > +
> > +(* rb orders instructions just as pb does *)
> > +let rb = prop ; rcu-fence ; hb* ; pb*
> >  
> >  irreflexive rb as rcu
> 
> I wonder whether we can simplify things as:
> 
> 	let rec rcu-fence =
> 	    (gp; rcu-link; rscs) |
> 	    (rscs; rcu-link; gp) |
> 	    (gp; rcu-link; rcu-fence; rcu-link; rscs) |
> 	    (rscs; rcu-link; rcu-fence; rcu-link; gp)
> 	
> 	(* gp and rcu-fence; rcu-link; rcu-fence removed *)
> 	
> 	let rb = prop; rcu-fence; hb*; pb*
> 
> 	acycle rb as rcu
> 
> In this way, "rcu-fence" is defined as "any sequence containing as many
> grace periods as RCU read-side critical sections (joined by rcu-link)."
> Note that "rcu-link" contains "gp", so we don't miss the case where
> there are more grace periods. And since we use "acycle" now, so we don't
> need "rcu-fence; rcu-link; rcu-fence" to build "rcu-fence" recursively.

Would this definition of rcu-fence work for a sequence such as (leaving
out the intermediate rcu-link parts):

	gp gp gp rscs rscs gp rscs rscs

?  I don't think it would.  Yes, if you had a cycle of that form then 
your "rcu" axiom would detect it, but at some point we might want to 
use rcu-fence for some other purpose, one that doesn't involve cycles.

> I prefer this because we already treat "gp" as "strong-fence", which
> already is a "rcu-link".

That's a good point; it had not occurred to me.

>  Also, recurisively extending rcu-fence with
> itself is exactly calculating the transitive closure, which we can avoid
> by using a "acycle" rule. Besides, it looks more consistent with hb and
> pb.

That _had_ occurred to me.  But I couldn't see any way to do it while 
still defining rcu-fence correctly.

Alan