Commit | Line | Data |
---|---|---|
15553dcb LM |
1 | C MP+polockmbonce+poacquiresilsil |
2 | ||
3 | (* | |
4 | * Result: Never | |
5 | * | |
6 | * Do spinlocks combined with smp_mb__after_spinlock() provide order | |
7 | * to outside observers using spin_is_locked() to sense the lock-held | |
8 | * state, ordered by acquire? Note that when the first spin_is_locked() | |
9 | * returns false and the second true, we know that the smp_load_acquire() | |
10 | * executed before the lock was acquired (loosely speaking). | |
11 | *) | |
12 | ||
13 | { | |
1947bfcf PM |
14 | spinlock_t lo; |
15 | int x; | |
15553dcb LM |
16 | } |
17 | ||
b6ff3084 | 18 | P0(spinlock_t *lo, int *x) // Producer |
15553dcb LM |
19 | { |
20 | spin_lock(lo); | |
21 | smp_mb__after_spinlock(); | |
22 | WRITE_ONCE(*x, 1); | |
23 | spin_unlock(lo); | |
24 | } | |
25 | ||
b6ff3084 | 26 | P1(spinlock_t *lo, int *x) // Consumer |
15553dcb LM |
27 | { |
28 | int r1; | |
29 | int r2; | |
30 | int r3; | |
31 | ||
32 | r1 = smp_load_acquire(x); | |
33 | r2 = spin_is_locked(lo); | |
34 | r3 = spin_is_locked(lo); | |
35 | } | |
36 | ||
b6ff3084 | 37 | exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *) |