Messages in this thread | | | From | John Ogness <> | Subject | Re: [PATCH next v2 2/2] printk: fix cpu lock ordering | Date | Thu, 10 Jun 2021 16:44:47 +0200 |
| |
On 2021-06-08, Petr Mladek <pmladek@suse.com> wrote: >> /* >> * Guarantee loads and stores from this CPU when it is the lock owner >> * are _not_ visible to the previous lock owner. This pairs with >> * cpu_unlock:B. >> * >> * Memory barrier involvement: >> * >> * If cpu_lock:A reads from cpu_unlock:B, then cpu_unlock:A can never >> * read from cpu_lock:B. >> * >> * Relies on: >> * >> * RELEASE from cpu_unlock:A to cpu_unlock:B >> * matching >> * ACQUIRE from cpu_lock:A to cpu_lock:B >> */ > > I can't check this so I believe you ;-)
I appreciate your confidence in me, but for the record, we should operate on proofs. Here is a litmus test for this case that is only using the 2 memory barriers described in the coments. I also added commented out non-memory-barrier variants so you can quickly check what happens if either memory barrier is removed.
-------- BEGIN prevent_backwards_leak.litmus -------- C prevent_backwards_leak
(* * Guarantee a previous CPU (P0) in the critical section cannot * see data stored by the next CPU (P1) in the critical section. * * RELEASE in P0 matches ACQUIRE in P1 *)
{ }
P0(int *lck, int *var) { int old; int val;
old = atomic_cmpxchg_relaxed(lck, 0, 1); if (old == 0) { val = *var; atomic_set_release(lck, 2); //atomic_set(lck, 2); } }
P1(int *lck, int *var) { int old;
old = atomic_cmpxchg_acquire(lck, 2, 3); //old = atomic_cmpxchg_relaxed(lck, 2, 3); if (old == 2) { *var = 1; atomic_set(lck, 3); } }
exists (1:old=2 /\ 0:val=1) -------- END prevent_backwards_leak.litmus --------
And running it shows:
$ herd7 -conf linux-kernel.cfg prevent_backwards_leak.litmus Test prevent_backwards_leak Allowed States 3 0:val=0; 1:old=0; 0:val=0; 1:old=1; 0:val=0; 1:old=2; No Witnesses Positive: 0 Negative: 3 Condition exists (1:old=2 /\ 0:val=1) Observation prevent_backwards_leak Never 0 3 Time prevent_backwards_leak 0.01 Hash=a83f3a63382111d7f61810639fa38ad4
If either of the two memory barriers are removed, the results will show that @val in first CPU (P0) can be 1 (0:val=1), which was the value set by the following CPU (P1) in the critical section.
>> /* >> * Guarantee loads and stores from this CPU when it was the >> * lock owner are visible to the next lock owner. This pairs >> * with cpu_lock:A. >> * >> * Memory barrier involvement: >> * >> * If cpu_lock:A reads from cpu_unlock:B, then cpu_lock:B >> * reads from cpu_unlock:A. >> * >> * Relies on: >> * >> * RELEASE from cpu_unlock:A to cpu_unlock:B >> * matching >> * ACQUIRE from cpu_lock:A to cpu_lock:B >> */ > > Same as for acquire ;-)
And here is the litmus test for this case, also with extra commented out non-memory-barrier variants.
-------- BEGIN guarantee_forward_visibility.litmus -------- C guarantee_forward_visibility
(* * Guarantee data stored by a previous CPU (P0) in the critical * section is always visible to the next CPU (P1) in the critical * section. * * RELEASE in P0 matches ACQUIRE in P1 *)
{ }
P0(int *lck, int *var) { int old;
old = atomic_cmpxchg_relaxed(lck, 0, 1); if (old == 0) { *var = 1; atomic_set_release(lck, 2); //atomic_set(lck, 2); } }
P1(int *lck, int *var) { int old; int val;
old = atomic_cmpxchg_acquire(lck, 2, 3); //old = atomic_cmpxchg_relaxed(lck, 2, 3); if (old == 2) { val = *var; atomic_set(lck, 3); } }
exists (1:old=2 /\ 1:val=0 ) -------- END guarantee_forward_visibility.litmus --------
$ herd7 -conf linux-kernel.cfg guarantee_forward_visibility.litmus Test guarantee_forward_visibility Allowed States 3 1:old=0; 1:val=0; 1:old=1; 1:val=0; 1:old=2; 1:val=1; No Witnesses Positive: 0 Negative: 3 Condition exists (1:old=2 /\ 1:val=0) Observation guarantee_forward_visibility Never 0 3 Time guarantee_forward_visibility 0.00 Hash=fad189f07da06da99b97a7ab1215a5dc
Also here, if either of the memory barriers are removed, @val in the later CPU (P1) can be 0 (1:val=0). Meaning that the a following CPU in the critical section would not see a value set by the previous CPU in the critical section.
John Ogness
| |