diff options
| author | Alan Stern <stern@rowland.harvard.edu> | 2019-06-20 11:55:46 -0400 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@linux.ibm.com> | 2019-06-21 16:20:49 -0700 |
| commit | 15aa25cbf0ccc4bd63ed6f2a8065decb7f5e6f89 (patch) | |
| tree | e3a2ee56ed0089cb5795217eddf0dc3d503eb76a /tools/memory-model | |
| parent | f9de417121001879d92a86960647adb06b5b81bf (diff) | |
| download | linux-15aa25cbf0ccc4bd63ed6f2a8065decb7f5e6f89.tar.bz2 | |
tools/memory-model: Change definition of rcu-fence
The rcu-fence relation in the Linux Kernel Memory Model is not well
named. It doesn't act like any other fence relation, in that it does
not relate events before a fence to events after that fence. All it
does is relate certain RCU events to one another (those that are
ordered by the RCU Guarantee); this induces an actual
strong-fence-like relation linking events preceding the first RCU
event to those following the second.
This patch renames rcu-fence, now called rcu-order. It adds a new
definition of rcu-fence, something which should have been present all
along because it is used in the rb relation. And it modifies the
fence and strong-fence relations by making them incorporate the new
rcu-fence.
As a result of this change, there is no longer any need to define
full-fence in the section for detecting data races. It can simply be
replaced by the updated strong-fence relation.
This change should have no effect on the operation of the memory model.
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Diffstat (limited to 'tools/memory-model')
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 8b61218c99fd..ca2f4297b4e6 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -122,24 +122,28 @@ 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. + * critical sections (joined by rcu-link) induces order like a generalized + * inter-CPU strong fence. * Likewise for SRCU grace periods and read-side critical sections, provided * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same * struct srcu_struct location. *) -let rec rcu-fence = rcu-gp | srcu-gp | +let rec rcu-order = rcu-gp | srcu-gp | (rcu-gp ; rcu-link ; rcu-rscsi) | ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) | (rcu-rscsi ; rcu-link ; rcu-gp) | ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) | - (rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; rcu-fence ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; srcu-gp) & loc) | - (rcu-fence ; rcu-link ; rcu-fence) + (rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) | + ((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) | + (rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) | + ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) | + (rcu-order ; rcu-link ; rcu-order) +let rcu-fence = po ; rcu-order ; po? +let fence = fence | rcu-fence +let strong-fence = strong-fence | rcu-fence (* rb orders instructions just as pb does *) -let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb* ; [Marked] +let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked] irreflexive rb as rcu @@ -163,9 +167,8 @@ flag ~empty mixed-accesses as mixed-accesses (* Executes-before and visibility *) let xbstar = (hb | pb | rb)* -let full-fence = strong-fence | (po ; rcu-fence ; po?) let vis = cumul-fence* ; rfe? ; [Marked] ; - ((full-fence ; [Marked] ; xbstar) | (xbstar & int)) + ((strong-fence ; [Marked] ; xbstar) | (xbstar & int)) (* Boundaries for lifetimes of plain accesses *) let w-pre-bounded = [Marked] ; (addr | fence)? |