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 <st...@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 > >
signature.asc
Description: PGP signature
