mirror of
https://git.kernel.org/pub/scm/linux/kernel/git/next/linux-next.git
synced 2025-01-15 21:23:23 +00:00
9049cf9a20
Not all annotated accesses provide the semantics their syntactic tags would imply. For example, an 'acquire tag on a write does not imply that the write is finally in the Acquire set and provides acquire ordering. To distinguish in those cases between the syntactic tags and actual sets, we capitalize the former, so 'ACQUIRE tags may be present on both reads and writes, but only reads will appear in the Acquire set. For tags where the two concepts are the same we do not use specific capitalization to make this distinction. Reported-by: Boqun Feng <boqun.feng@gmail.com> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> Reviewed-by: Boqun Feng <boqun.feng@gmail.com> Tested-by: Boqun Feng <boqun.feng@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
100 lines
3.5 KiB
Plaintext
100 lines
3.5 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"
|
|
|
|
enum Accesses = 'ONCE (*READ_ONCE,WRITE_ONCE*) ||
|
|
'RELEASE (*smp_store_release*) ||
|
|
'ACQUIRE (*smp_load_acquire*) ||
|
|
'NORETURN (* R of non-return RMW *) ||
|
|
'MB (*xchg(),cmpxchg(),...*)
|
|
instructions R[Accesses]
|
|
instructions W[Accesses]
|
|
instructions RMW[Accesses]
|
|
|
|
enum Barriers = 'wmb (*smp_wmb*) ||
|
|
'rmb (*smp_rmb*) ||
|
|
'MB (*smp_mb*) ||
|
|
'barrier (*barrier*) ||
|
|
'rcu-lock (*rcu_read_lock*) ||
|
|
'rcu-unlock (*rcu_read_unlock*) ||
|
|
'sync-rcu (*synchronize_rcu*) ||
|
|
'before-atomic (*smp_mb__before_atomic*) ||
|
|
'after-atomic (*smp_mb__after_atomic*) ||
|
|
'after-spinlock (*smp_mb__after_spinlock*) ||
|
|
'after-unlock-lock (*smp_mb__after_unlock_lock*) ||
|
|
'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*)
|
|
instructions F[Barriers]
|
|
|
|
|
|
(*
|
|
* Filter out syntactic annotations that do not provide the corresponding
|
|
* semantic ordering, such as Acquire on a store or Mb on a failed RMW.
|
|
*)
|
|
let FailedRMW = RMW \ (domain(rmw) | range(rmw))
|
|
let Acquire = ACQUIRE \ W \ FailedRMW
|
|
let Release = RELEASE \ R \ FailedRMW
|
|
let Mb = MB \ FailedRMW
|
|
let Noreturn = NORETURN \ W
|
|
|
|
(* SRCU *)
|
|
enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu
|
|
instructions SRCU[SRCU]
|
|
(* All srcu events *)
|
|
let Srcu = Srcu-lock | Srcu-unlock | Sync-srcu
|
|
|
|
(* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
|
|
let rcu-rscs = let rec
|
|
unmatched-locks = Rcu-lock \ domain(matched)
|
|
and unmatched-unlocks = Rcu-unlock \ range(matched)
|
|
and unmatched = unmatched-locks | unmatched-unlocks
|
|
and unmatched-po = [unmatched] ; po ; [unmatched]
|
|
and unmatched-locks-to-unlocks =
|
|
[unmatched-locks] ; po ; [unmatched-unlocks]
|
|
and matched = matched | (unmatched-locks-to-unlocks \
|
|
(unmatched-po ; unmatched-po))
|
|
in matched
|
|
|
|
(* Validate nesting *)
|
|
flag ~empty Rcu-lock \ domain(rcu-rscs) as unmatched-rcu-lock
|
|
flag ~empty Rcu-unlock \ range(rcu-rscs) as unmatched-rcu-unlock
|
|
|
|
(* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
|
|
let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*
|
|
let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc
|
|
|
|
(* Validate nesting *)
|
|
flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock
|
|
flag ~empty Srcu-unlock \ range(srcu-rscs) as unmatched-srcu-unlock
|
|
flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-matches
|
|
|
|
(* Check for use of synchronize_srcu() inside an RCU critical section *)
|
|
flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
|
|
|
|
(* Validate SRCU dynamic match *)
|
|
flag ~empty different-values(srcu-rscs) as srcu-bad-value-match
|
|
|
|
(* Compute marked and plain memory accesses *)
|
|
let Marked = (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | RMW |
|
|
LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock
|
|
let Plain = M \ Marked
|
|
|
|
(* Redefine dependencies to include those carried through plain accesses *)
|
|
let carry-dep = (data ; [~ Srcu-unlock] ; rfi)*
|
|
let addr = carry-dep ; addr
|
|
let ctrl = carry-dep ; ctrl
|
|
let data = carry-dep ; data
|
|
|
|
flag ~empty (if "lkmmv2" then 0 else _)
|
|
as this-model-requires-variant-higher-than-lkmmv1
|