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 | * | |
1a00b455 | 8 | * An earlier version of this file appeared in the companion webpage for |
1c27b644 PM |
9 | * "Frightening small children and disconcerting grown-ups: Concurrency |
10 | * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern, | |
1a00b455 | 11 | * which appeared in ASPLOS 2018. |
1c27b644 PM |
12 | *) |
13 | ||
48d44d4e | 14 | "Linux-kernel memory consistency model" |
1c27b644 | 15 | |
af41db5e | 16 | enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) || |
1c27b644 PM |
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*) || | |
0031e38a | 27 | 'barrier (*barrier*) || |
1c27b644 PM |
28 | 'rcu-lock (*rcu_read_lock*) || |
29 | 'rcu-unlock (*rcu_read_unlock*) || | |
30 | 'sync-rcu (*synchronize_rcu*) || | |
cac79a39 PM |
31 | 'before-atomic (*smp_mb__before_atomic*) || |
32 | 'after-atomic (*smp_mb__after_atomic*) || | |
5b735eb1 | 33 | 'after-spinlock (*smp_mb__after_spinlock*) || |
02bae7a2 PM |
34 | 'after-unlock-lock (*smp_mb__after_unlock_lock*) || |
35 | 'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*) | |
1c27b644 PM |
36 | instructions F[Barriers] |
37 | ||
a3f600d9 AS |
38 | (* SRCU *) |
39 | enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu | |
40 | instructions SRCU[SRCU] | |
41 | (* All srcu events *) | |
42 | let Srcu = Srcu-lock | Srcu-unlock | Sync-srcu | |
43 | ||
1c27b644 | 44 | (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) |
0172d9e3 | 45 | let rcu-rscs = let rec |
1c27b644 PM |
46 | unmatched-locks = Rcu-lock \ domain(matched) |
47 | and unmatched-unlocks = Rcu-unlock \ range(matched) | |
48 | and unmatched = unmatched-locks | unmatched-unlocks | |
49 | and unmatched-po = [unmatched] ; po ; [unmatched] | |
50 | and unmatched-locks-to-unlocks = | |
51 | [unmatched-locks] ; po ; [unmatched-unlocks] | |
52 | and matched = matched | (unmatched-locks-to-unlocks \ | |
53 | (unmatched-po ; unmatched-po)) | |
54 | in matched | |
55 | ||
56 | (* Validate nesting *) | |
627c9ad0 AS |
57 | flag ~empty Rcu-lock \ domain(rcu-rscs) as unmatched-rcu-lock |
58 | flag ~empty Rcu-unlock \ range(rcu-rscs) as unmatched-rcu-unlock | |
a3f600d9 AS |
59 | |
60 | (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *) | |
614e40fa AS |
61 | let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)* |
62 | let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc | |
a3f600d9 AS |
63 | |
64 | (* Validate nesting *) | |
627c9ad0 AS |
65 | flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock |
66 | flag ~empty Srcu-unlock \ range(srcu-rscs) as unmatched-srcu-unlock | |
614e40fa | 67 | flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-matches |
a3f600d9 AS |
68 | |
69 | (* Check for use of synchronize_srcu() inside an RCU critical section *) | |
70 | flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep | |
9393998e LM |
71 | |
72 | (* Validate SRCU dynamic match *) | |
627c9ad0 | 73 | flag ~empty different-values(srcu-rscs) as srcu-bad-value-match |
d1a84ab1 AS |
74 | |
75 | (* Compute marked and plain memory accesses *) | |
76 | let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | | |
614e40fa | 77 | LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock |
d1a84ab1 | 78 | let Plain = M \ Marked |
9ba7d3b3 JO |
79 | |
80 | (* Redefine dependencies to include those carried through plain accesses *) | |
614e40fa | 81 | let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* |
9ba7d3b3 JO |
82 | let addr = carry-dep ; addr |
83 | let ctrl = carry-dep ; ctrl | |
84 | let data = carry-dep ; data |