2
0
mirror of https://github.com/edk2-porting/linux-next.git synced 2024-12-29 15:43:59 +08:00
linux-next/tools/memory-model/linux-kernel.cat
Alan Stern 4289ee7d5a tools/memory-model: Improve data-race detection
Herbert Xu recently reported a problem concerning RCU and compiler
barriers.  In the course of discussing the problem, he put forth a
litmus test which illustrated a serious defect in the Linux Kernel
Memory Model's data-race-detection code [1].

The defect was that the LKMM assumed visibility and executes-before
ordering of plain accesses had to be mediated by marked accesses.  In
Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
test was allowed and contained a data race although neither is true.

In fact, plain accesses can be ordered by fences even in the absence
of marked accesses.  In most cases this doesn't matter, because most
fences only order accesses within a single thread.  But the rcu-fence
relation is different; it can order (and induce visibility between)
accesses in different threads -- events which otherwise might be
concurrent.  This makes it relevant to data-race detection.

This patch makes two changes to the memory model to incorporate the
new insight:

	If a store is separated by a fence from another access,
	the store is necessarily visible to the other access (as
	reflected in the ww-vis and wr-vis relations).  Similarly,
	if a load is separated by a fence from another access then
	the load necessarily executes before the other access (as
	reflected in the rw-xbstar relation).

	If a store is separated by a strong fence from a marked access
	then it is necessarily visible to any access that executes
	after the marked access (as reflected in the ww-vis and wr-vis
	relations).

With these changes, the LKMM gives the desired result for Herbert's
litmus test and other related ones [2].

[1]	https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/

[2]	https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-1.litmus
	https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
	https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-3.litmus
	https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-4.litmus
	https://github.com/paulmckrcu/litmus/blob/master/manual/plain/strong-vis.litmus

Reported-by: Herbert Xu <herbert@gondor.apana.org.au>
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>
Tested-by: Akira Yokosawa <akiyks@gmail.com>
2019-06-24 09:08:54 -07:00

204 lines
7.0 KiB
Plaintext

// SPDX-License-Identifier: GPL-2.0+
(*
* Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
* Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
* Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
* Andrea Parri <parri.andrea@gmail.com>
*
* An earlier version of this file appeared in the companion webpage for
* "Frightening small children and disconcerting grown-ups: Concurrency
* in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern,
* which appeared in ASPLOS 2018.
*)
"Linux-kernel memory consistency model"
(*
* File "lock.cat" handles locks and is experimental.
* It can be replaced by include "cos.cat" for tests that do not use locks.
*)
include "lock.cat"
(*******************)
(* Basic relations *)
(*******************)
(* Release Acquire *)
let acq-po = [Acquire] ; po ; [M]
let po-rel = [M] ; po ; [Release]
let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
(* Fences *)
let R4rmb = R \ Noreturn (* Reads for which rmb works *)
let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb]
let wmb = [W] ; fencerel(Wmb) ; [W]
let mb = ([M] ; fencerel(Mb) ; [M]) |
([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
([M] ; po ; [UL] ; (co | po) ; [LKW] ;
fencerel(After-unlock-lock) ; [M])
let gp = po ; [Sync-rcu | Sync-srcu] ; po?
let strong-fence = mb | gp
let nonrw-fence = strong-fence | po-rel | acq-po
let fence = nonrw-fence | wmb | rmb
let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu |
Before-atomic | After-atomic | Acquire | Release |
Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) |
(po ; [Release]) | ([Acquire] ; po)
(**********************************)
(* Fundamental coherence ordering *)
(**********************************)
(* Sequential Consistency Per Variable *)
let com = rf | co | fr
acyclic po-loc | com as coherence
(* Atomic Read-Modify-Write *)
empty rmw & (fre ; coe) as atomic
(**********************************)
(* Instruction execution ordering *)
(**********************************)
(* Preserved Program Order *)
let dep = addr | data
let rwdep = (dep | ctrl) ; [W]
let overwrite = co | fr
let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
let to-r = addr | (dep ; [Marked] ; rfi)
let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
(* Propagation: Ordering from release operations and strong fences. *)
let A-cumul(r) = (rfe ; [Marked])? ; r
let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
po-unlock-rf-lock-po) ; [Marked]
let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
[Marked] ; rfe? ; [Marked]
(*
* Happens Before: Ordering from the passage of time.
* No fences needed here for prop because relation confined to one process.
*)
let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked]
acyclic hb as happens-before
(****************************************)
(* Write and fence propagation ordering *)
(****************************************)
(* Propagation: Each non-rf link needs a strong fence. *)
let pb = prop ; strong-fence ; hb* ; [Marked]
acyclic pb as propagation
(*******)
(* RCU *)
(*******)
(*
* Effects of read-side critical sections proceed from the rcu_read_unlock()
* or srcu_read_unlock() backwards on the one hand, and from the
* rcu_read_lock() or srcu_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.
* This was necessary in order to apply the "& loc" tests correctly.
*)
let rcu-gp = [Sync-rcu] (* Compare with gp *)
let srcu-gp = [Sync-srcu]
let rcu-rscsi = rcu-rscs^-1
let srcu-rscsi = srcu-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 = po? ; hb* ; pb* ; prop ; po
(*
* Any sequence containing at least as many grace periods as RCU read-side
* 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-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-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 ; rcu-fence ; hb* ; pb* ; [Marked]
irreflexive rb as rcu
(*
* The happens-before, propagation, and rcu constraints are all
* expressions of temporal ordering. They could be replaced by
* a single constraint on an "executes-before" relation, xb:
*
* let xb = hb | pb | rb
* acyclic xb as executes-before
*)
(*********************************)
(* Plain accesses and data races *)
(*********************************)
(* Warn about plain writes and marked accesses in the same region *)
let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) |
([Marked] ; (po-loc \ barrier) ; [Plain & W])
flag ~empty mixed-accesses as mixed-accesses
(* Executes-before and visibility *)
let xbstar = (hb | pb | rb)*
let vis = cumul-fence* ; rfe? ; [Marked] ;
((strong-fence ; [Marked] ; xbstar) | (xbstar & int))
(* Boundaries for lifetimes of plain accesses *)
let w-pre-bounded = [Marked] ; (addr | fence)?
let r-pre-bounded = [Marked] ; (addr | nonrw-fence |
([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))?
let w-post-bounded = fence? ; [Marked]
let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ;
[Marked]
(* Visibility and executes-before for plain accesses *)
let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) |
(w-post-bounded ; vis ; w-pre-bounded)
let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) |
(w-post-bounded ; vis ; r-pre-bounded)
let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded)
(* Potential races *)
let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain))
(* Coherence requirements for plain accesses *)
let wr-incoh = pre-race & rf & rw-xbstar^-1
let rw-incoh = pre-race & fr & wr-vis^-1
let ww-incoh = pre-race & co & ww-vis^-1
empty (wr-incoh | rw-incoh | ww-incoh) as plain-coherence
(* Actual races *)
let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis)
let ww-race = (pre-race & co) \ ww-nonrace
let wr-race = (pre-race & (co? ; rf)) \ wr-vis
let rw-race = (pre-race & fr) \ rw-xbstar
flag ~empty (ww-race | wr-race | rw-race) as data-race