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

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

[Alan Stern]

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
 
 (*
  * 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
 

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

[Boqun Feng]

[-- 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 --]

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

[Alan Stern]

On Fri, 16 Nov 2018, Boqun Feng wrote:

> > -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?

It's a matter of personal preference.  I prefer to store the inverse
relation in a separate variable rather than recomputing it multiple
times.  (Maybe OCaml is smart enough to recognize when a value has 
already been computed and avoid computing it again; I don't know.)

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

In the end this probably doesn't make much difference.

Alan