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