linux-kernel - Re: [PATCH 2/3] tools/memory-model: Refactor some RCU relations

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: <20181115175420.GA3227@tardis>
Date:   Fri, 16 Nov 2018 01:54:20 +0800
From:   Boqun Feng <boqun.feng@...il.com>
To:     Alan Stern <stern@...land.harvard.edu>
Cc:     "Paul E. McKenney" <paulmck@...ux.ibm.com>,
        LKMM Maintainers -- Akira Yokosawa <akiyks@...il.com>,
        Andrea Parri <andrea.parri@...rulasolutions.com>,
        Daniel Lustig <dlustig@...dia.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        Luc Maranget <luc.maranget@...ia.fr>,
        Nicholas Piggin <npiggin@...il.com>,
        Peter Zijlstra <peterz@...radead.org>,
        Will Deacon <will.deacon@....com>,
        Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: [PATCH 2/3] tools/memory-model: Refactor some RCU relations

Hi Alan,

On Thu, Nov 15, 2018 at 11:19:58AM -0500, Alan Stern wrote:
> In preparation for adding support for SRCU, refactor the definitions
> of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po?
> terms from the first two to the second two.  An rcu-gp relation is
> added; it is equivalent to gp with the po and po? terms removed.
> 
> This is necessary because for SRCU, we will have to use the loc
> relation to check that the terms at the start and end of each disjunct
> in the definition of rcu-fence refer to the same srcu_struct
> location.  If these terms are hidden behind po and po?, there's no way
> to carry out this check.
> 
> Signed-off-by: Alan Stern <stern@...land.harvard.edu>
> 
> ---
> 
> 
>  tools/memory-model/linux-kernel.cat |   25 +++++++++++++++----------
>  1 file changed, 15 insertions(+), 10 deletions(-)
> 
> Index: usb-4.x/tools/memory-model/linux-kernel.cat
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/linux-kernel.cat
> +++ usb-4.x/tools/memory-model/linux-kernel.cat
> @@ -91,32 +91,37 @@ acyclic pb as propagation
>  (*******)
>  
>  (*
> - * Effect of read-side critical section proceeds from the rcu_read_lock()
> - * onward on the one hand and from the rcu_read_unlock() backwards on the
> + * Effects of read-side critical sections proceed from the rcu_read_unlock()
> + * backwards on the one hand, and from the rcu_read_lock() forwards on the
>   * other hand.
> + *
> + * In the definition of rcu-fence below, the po term at the left-hand side
> + * of each disjunct and the po? term at the right-hand end have been factored
> + * out.  They have been moved into the definitions of rcu-link and rb.
>   *)
> -let rcu-rscsi = po ; rcu-rscs^-1 ; po?
> +let rcu-gp = [Sync-rcu]		(* Compare with gp *)
> +let rcu-rscsi = rcu-rscs^-1

Isn't it more straight-forward to use "rcu-rscs^-1" other than
"rcu-rscsi" in the definition of "rcu-fence", is it?

The introduction of "rcu-rscsi" makes sense in the first patch, but with
this refactoring, I think it's better we just don't use it.

Regards,
Boqun

>  
>  (*
>   * The synchronize_rcu() strong fence is special in that it can order not
>   * one but two non-rf relations, but only in conjunction with an RCU
>   * read-side critical section.
>   *)
> -let rcu-link = hb* ; pb* ; prop
> +let rcu-link = po? ; hb* ; pb* ; prop ; po
>  
>  (*
>   * Any sequence containing at least as many grace periods as RCU read-side
>   * critical sections (joined by rcu-link) acts as a generalized strong fence.
>   *)
> -let rec rcu-fence = gp |
> -	(gp ; rcu-link ; rcu-rscsi) |
> -	(rcu-rscsi ; rcu-link ; gp) |
> -	(gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
> -	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; gp) |
> +let rec rcu-fence = rcu-gp |
> +	(rcu-gp ; rcu-link ; rcu-rscsi) |
> +	(rcu-rscsi ; rcu-link ; rcu-gp) |
> +	(rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
> +	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) |
>  	(rcu-fence ; rcu-link ; rcu-fence)
>  
>  (* rb orders instructions just as pb does *)
> -let rb = prop ; rcu-fence ; hb* ; pb*
> +let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb*
>  
>  irreflexive rb as rcu
>  
> 

Download attachment "signature.asc" of type "application/pgp-signature" (489 bytes)