Commit | Line | Data |
---|---|---|
1c27b644 PM |
1 | C MP+polocks |
2 | ||
8f32543b PM |
3 | (* |
4 | * Result: Never | |
5 | * | |
6 | * This litmus test demonstrates how lock acquisitions and releases can | |
7 | * stand in for smp_load_acquire() and smp_store_release(), respectively. | |
8 | * In other words, when holding a given lock (or indeed after releasing a | |
9 | * given lock), a CPU is not only guaranteed to see the accesses that other | |
10 | * CPUs made while previously holding that lock, it is also guaranteed | |
11 | * to see all prior accesses by those other CPUs. | |
12 | *) | |
13 | ||
5c587f9b | 14 | {} |
1c27b644 | 15 | |
b6ff3084 | 16 | P0(int *buf, int *flag, spinlock_t *mylock) // Producer |
1c27b644 | 17 | { |
acc4bdc5 | 18 | WRITE_ONCE(*buf, 1); |
1c27b644 | 19 | spin_lock(mylock); |
acc4bdc5 | 20 | WRITE_ONCE(*flag, 1); |
1c27b644 PM |
21 | spin_unlock(mylock); |
22 | } | |
23 | ||
b6ff3084 | 24 | P1(int *buf, int *flag, spinlock_t *mylock) // Consumer |
1c27b644 PM |
25 | { |
26 | int r0; | |
27 | int r1; | |
28 | ||
29 | spin_lock(mylock); | |
acc4bdc5 | 30 | r0 = READ_ONCE(*flag); |
1c27b644 | 31 | spin_unlock(mylock); |
acc4bdc5 | 32 | r1 = READ_ONCE(*buf); |
1c27b644 PM |
33 | } |
34 | ||
b6ff3084 | 35 | exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *) |