projects / linux-block.git / blame
| Commit | Line | Data |
|---|---|---|
| 1c27b644 PM |
1 | // SPDX-License-Identifier: GPL-2.0+ |
| 2 | (* | |
| 3 | * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>, | |
| 4 | * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria | |
| 5 | * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>, | |
| 6 | * Andrea Parri <parri.andrea@gmail.com> | |
| 7 | * | |
| 8 | * An earlier version of this file appears in the companion webpage for | |
| 9 | * "Frightening small children and disconcerting grown-ups: Concurrency | |
| 10 | * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern, | |
| 11 | * which is to appear in ASPLOS 2018. | |
| 12 | *) | |
| 13 | ||
| 48d44d4e | 14 | "Linux-kernel memory consistency model" |
| 1c27b644 PM |
15 | |
| 16 | enum Accesses = 'once (*READ_ONCE,WRITE_ONCE,ACCESS_ONCE*) || | |
| 17 | 'release (*smp_store_release*) || | |
| 18 | 'acquire (*smp_load_acquire*) || | |
| 19 | 'noreturn (* R of non-return RMW *) | |
| 20 | instructions R[{'once,'acquire,'noreturn}] | |
| 21 | instructions W[{'once,'release}] | |
| 22 | instructions RMW[{'once,'acquire,'release}] | |
| 23 | ||
| 24 | enum Barriers = 'wmb (*smp_wmb*) || | |
| 25 | 'rmb (*smp_rmb*) || | |
| 26 | 'mb (*smp_mb*) || | |
| 1c27b644 PM |
27 | 'rcu-lock (*rcu_read_lock*) || |
| 28 | 'rcu-unlock (*rcu_read_unlock*) || | |
| 29 | 'sync-rcu (*synchronize_rcu*) || | |
| cac79a39 PM |
30 | 'before-atomic (*smp_mb__before_atomic*) || |
| 31 | 'after-atomic (*smp_mb__after_atomic*) || | |
| 32 | 'after-spinlock (*smp_mb__after_spinlock*) | |
| 1c27b644 PM |
33 | instructions F[Barriers] |
| 34 | ||
| 35 | (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) | |
| 36 | let matched = let rec | |
| 37 | unmatched-locks = Rcu-lock \ domain(matched) | |
| 38 | and unmatched-unlocks = Rcu-unlock \ range(matched) | |
| 39 | and unmatched = unmatched-locks | unmatched-unlocks | |
| 40 | and unmatched-po = [unmatched] ; po ; [unmatched] | |
| 41 | and unmatched-locks-to-unlocks = | |
| 42 | [unmatched-locks] ; po ; [unmatched-unlocks] | |
| 43 | and matched = matched | (unmatched-locks-to-unlocks \ | |
| 44 | (unmatched-po ; unmatched-po)) | |
| 45 | in matched | |
| 46 | ||
| 47 | (* Validate nesting *) | |
| 48 | flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking | |
| 49 | flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking | |
| 50 | ||
| 51 | (* Outermost level of nesting only *) | |
| 52 | let crit = matched \ (po^-1 ; matched ; po^-1) |