lkml.org 
[lkml]   [2018]   [Nov]   [15]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [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@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
>
>
[unhandled content-type:application/pgp-signature]
\
 
 \ /
  Last update: 2018-11-15 18:48    [W:0.077 / U:22.096 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site