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

[Boqun Feng <boqun.feng@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3321 bytes --]

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@rowland.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
>  
> 

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]