0001 // SPDX-License-Identifier: GPL-2.0+
0002 (*
0003 * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
0004 * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
0005 * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
0006 * Andrea Parri <parri.andrea@gmail.com>
0007 *
0008 * An earlier version of this file appeared in the companion webpage for
0009 * "Frightening small children and disconcerting grown-ups: Concurrency
0010 * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern,
0011 * which appeared in ASPLOS 2018.
0012 *)
0013
0014 "Linux-kernel memory consistency model"
0015
0016 enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) ||
0017 'release (*smp_store_release*) ||
0018 'acquire (*smp_load_acquire*) ||
0019 'noreturn (* R of non-return RMW *)
0020 instructions R[{'once,'acquire,'noreturn}]
0021 instructions W[{'once,'release}]
0022 instructions RMW[{'once,'acquire,'release}]
0023
0024 enum Barriers = 'wmb (*smp_wmb*) ||
0025 'rmb (*smp_rmb*) ||
0026 'mb (*smp_mb*) ||
0027 'barrier (*barrier*) ||
0028 'rcu-lock (*rcu_read_lock*) ||
0029 'rcu-unlock (*rcu_read_unlock*) ||
0030 'sync-rcu (*synchronize_rcu*) ||
0031 'before-atomic (*smp_mb__before_atomic*) ||
0032 'after-atomic (*smp_mb__after_atomic*) ||
0033 'after-spinlock (*smp_mb__after_spinlock*) ||
0034 'after-unlock-lock (*smp_mb__after_unlock_lock*)
0035 instructions F[Barriers]
0036
0037 (* SRCU *)
0038 enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu
0039 instructions SRCU[SRCU]
0040 (* All srcu events *)
0041 let Srcu = Srcu-lock | Srcu-unlock | Sync-srcu
0042
0043 (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
0044 let rcu-rscs = let rec
0045 unmatched-locks = Rcu-lock \ domain(matched)
0046 and unmatched-unlocks = Rcu-unlock \ range(matched)
0047 and unmatched = unmatched-locks | unmatched-unlocks
0048 and unmatched-po = [unmatched] ; po ; [unmatched]
0049 and unmatched-locks-to-unlocks =
0050 [unmatched-locks] ; po ; [unmatched-unlocks]
0051 and matched = matched | (unmatched-locks-to-unlocks \
0052 (unmatched-po ; unmatched-po))
0053 in matched
0054
0055 (* Validate nesting *)
0056 flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking
0057 flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking
0058
0059 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
0060 let srcu-rscs = let rec
0061 unmatched-locks = Srcu-lock \ domain(matched)
0062 and unmatched-unlocks = Srcu-unlock \ range(matched)
0063 and unmatched = unmatched-locks | unmatched-unlocks
0064 and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc
0065 and unmatched-locks-to-unlocks =
0066 ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc
0067 and matched = matched | (unmatched-locks-to-unlocks \
0068 (unmatched-po ; unmatched-po))
0069 in matched
0070
0071 (* Validate nesting *)
0072 flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking
0073 flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
0074
0075 (* Check for use of synchronize_srcu() inside an RCU critical section *)
0076 flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
0077
0078 (* Validate SRCU dynamic match *)
0079 flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
0080
0081 (* Compute marked and plain memory accesses *)
0082 let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
0083 LKR | LKW | UL | LF | RL | RU
0084 let Plain = M \ Marked
