mirror of
https://github.com/torvalds/linux.git
synced 2026-01-25 07:47:50 +00:00
fafa180683
A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7 behavior of simply ignoring any softcoded tags in the .def and .bell files. We port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg and reporting an error if the LKMM is used without this switch. To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic RMW which do not return a value and define atomic_add_unless with an Mb tag in linux-kernel.def. We update the herd-representation.txt accordingly and clarify some of the resulting combinations. Co-developed-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org> Reviewed-by: Boqun Feng <boqun.feng@gmail.com> Tested-by: Boqun Feng <boqun.feng@gmail.com> Tested-by: Akira Yokosawa <akiyks@gmail.com> # herdtools7.7.58
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 | domain(rmw) | range(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
|