Orange Pi5 kernel

^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  1) // SPDX-License-Identifier: GPL-2.0+
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  2) (*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  3)  * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  4)  * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  5)  * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  6)  *                    Andrea Parri <parri.andrea@gmail.com>
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  7)  *
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  8)  * An earlier version of this file appeared in the companion webpage for
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  9)  * "Frightening small children and disconcerting grown-ups: Concurrency
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 10)  * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 11)  * which appeared in ASPLOS 2018.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 12)  *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 13) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 14) "Linux-kernel memory consistency model"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 15) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 16) enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 17) 		'release (*smp_store_release*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 18) 		'acquire (*smp_load_acquire*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 19) 		'noreturn (* R of non-return RMW *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 20) instructions R[{'once,'acquire,'noreturn}]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 21) instructions W[{'once,'release}]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 22) instructions RMW[{'once,'acquire,'release}]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 23) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 24) enum Barriers = 'wmb (*smp_wmb*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 25) 		'rmb (*smp_rmb*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 26) 		'mb (*smp_mb*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 27) 		'barrier (*barrier*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 28) 		'rcu-lock (*rcu_read_lock*)  ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 29) 		'rcu-unlock (*rcu_read_unlock*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 30) 		'sync-rcu (*synchronize_rcu*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 31) 		'before-atomic (*smp_mb__before_atomic*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 32) 		'after-atomic (*smp_mb__after_atomic*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 33) 		'after-spinlock (*smp_mb__after_spinlock*) ||
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 34) 		'after-unlock-lock (*smp_mb__after_unlock_lock*)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 35) instructions F[Barriers]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 36) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 37) (* SRCU *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 38) enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 39) instructions SRCU[SRCU]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 40) (* All srcu events *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 41) let Srcu = Srcu-lock | Srcu-unlock | Sync-srcu
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 42) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 43) (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 44) let rcu-rscs = let rec
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 45) 	    unmatched-locks = Rcu-lock \ domain(matched)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 46) 	and unmatched-unlocks = Rcu-unlock \ range(matched)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 47) 	and unmatched = unmatched-locks | unmatched-unlocks
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 48) 	and unmatched-po = [unmatched] ; po ; [unmatched]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 49) 	and unmatched-locks-to-unlocks =
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 50) 		[unmatched-locks] ; po ; [unmatched-unlocks]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 51) 	and matched = matched | (unmatched-locks-to-unlocks \
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 52) 		(unmatched-po ; unmatched-po))
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 53) 	in matched
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 54) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 55) (* Validate nesting *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 56) flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 57) flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 58) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 59) (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 60) let srcu-rscs = let rec
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 61) 	    unmatched-locks = Srcu-lock \ domain(matched)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 62) 	and unmatched-unlocks = Srcu-unlock \ range(matched)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 63) 	and unmatched = unmatched-locks | unmatched-unlocks
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 64) 	and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 65) 	and unmatched-locks-to-unlocks =
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 66) 		([unmatched-locks] ; po ; [unmatched-unlocks]) & loc
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 67) 	and matched = matched | (unmatched-locks-to-unlocks \
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 68) 		(unmatched-po ; unmatched-po))
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 69) 	in matched
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 70) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 71) (* Validate nesting *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 72) flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 73) flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 74) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 75) (* Check for use of synchronize_srcu() inside an RCU critical section *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 76) flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 77) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 78) (* Validate SRCU dynamic match *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 79) flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 80) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 81) (* Compute marked and plain memory accesses *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 82) let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 83) 		LKR | LKW | UL | LF | RL | RU
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 84) let Plain = M \ Marked