.. | .. |
---|
24 | 24 | enum Barriers = 'wmb (*smp_wmb*) || |
---|
25 | 25 | 'rmb (*smp_rmb*) || |
---|
26 | 26 | 'mb (*smp_mb*) || |
---|
| 27 | + 'barrier (*barrier*) || |
---|
27 | 28 | 'rcu-lock (*rcu_read_lock*) || |
---|
28 | 29 | 'rcu-unlock (*rcu_read_unlock*) || |
---|
29 | 30 | 'sync-rcu (*synchronize_rcu*) || |
---|
30 | 31 | 'before-atomic (*smp_mb__before_atomic*) || |
---|
31 | 32 | 'after-atomic (*smp_mb__after_atomic*) || |
---|
32 | | - 'after-spinlock (*smp_mb__after_spinlock*) |
---|
| 33 | + 'after-spinlock (*smp_mb__after_spinlock*) || |
---|
| 34 | + 'after-unlock-lock (*smp_mb__after_unlock_lock*) |
---|
33 | 35 | instructions F[Barriers] |
---|
34 | 36 | |
---|
| 37 | +(* SRCU *) |
---|
| 38 | +enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu |
---|
| 39 | +instructions SRCU[SRCU] |
---|
| 40 | +(* All srcu events *) |
---|
| 41 | +let Srcu = Srcu-lock | Srcu-unlock | Sync-srcu |
---|
| 42 | + |
---|
35 | 43 | (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) |
---|
36 | | -let matched = let rec |
---|
| 44 | +let rcu-rscs = let rec |
---|
37 | 45 | unmatched-locks = Rcu-lock \ domain(matched) |
---|
38 | 46 | and unmatched-unlocks = Rcu-unlock \ range(matched) |
---|
39 | 47 | and unmatched = unmatched-locks | unmatched-unlocks |
---|
.. | .. |
---|
45 | 53 | in matched |
---|
46 | 54 | |
---|
47 | 55 | (* Validate nesting *) |
---|
48 | | -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking |
---|
49 | | -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking |
---|
| 56 | +flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking |
---|
| 57 | +flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking |
---|
50 | 58 | |
---|
51 | | -(* Outermost level of nesting only *) |
---|
52 | | -let crit = matched \ (po^-1 ; matched ; po^-1) |
---|
| 59 | +(* Compute matching pairs of nested Srcu-lock and Srcu-unlock *) |
---|
| 60 | +let srcu-rscs = let rec |
---|
| 61 | + unmatched-locks = Srcu-lock \ domain(matched) |
---|
| 62 | + and unmatched-unlocks = Srcu-unlock \ range(matched) |
---|
| 63 | + and unmatched = unmatched-locks | unmatched-unlocks |
---|
| 64 | + and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc |
---|
| 65 | + and unmatched-locks-to-unlocks = |
---|
| 66 | + ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc |
---|
| 67 | + and matched = matched | (unmatched-locks-to-unlocks \ |
---|
| 68 | + (unmatched-po ; unmatched-po)) |
---|
| 69 | + in matched |
---|
| 70 | + |
---|
| 71 | +(* Validate nesting *) |
---|
| 72 | +flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking |
---|
| 73 | +flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking |
---|
| 74 | + |
---|
| 75 | +(* Check for use of synchronize_srcu() inside an RCU critical section *) |
---|
| 76 | +flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep |
---|
| 77 | + |
---|
| 78 | +(* Validate SRCU dynamic match *) |
---|
| 79 | +flag ~empty different-values(srcu-rscs) as srcu-bad-nesting |
---|
| 80 | + |
---|
| 81 | +(* Compute marked and plain memory accesses *) |
---|
| 82 | +let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | |
---|
| 83 | + LKR | LKW | UL | LF | RL | RU |
---|
| 84 | +let Plain = M \ Marked |
---|