lkml.org 
[lkml]   [2017]   [Nov]   [27]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
SubjectRe: Unlock-lock questions and the Linux Kernel Memory Model
From
Date
On 11/27/2017 1:16 PM, Alan Stern wrote:> C rel-acq-write-ordering-3
>
> {}
>
> P0(int *x, int *s, int *y)
> {
> WRITE_ONCE(*x, 1);
> smp_store_release(s, 1);
> r1 = smp_load_acquire(s);
> WRITE_ONCE(*y, 1);
> }
>
> P1(int *x, int *y)
> {
> r2 = READ_ONCE(*y);
> smp_rmb();
> r3 = READ_ONCE(*x);
> }
>
> exists (1:r2=1 /\ 1:r3=0)
>
<snip>
>
> And going to extremes...

Sorry if I'm missing something obvious, but before going to extremes...
what about this one?

"SB+rel-acq" (or please rename if you have a different scheme)

{}

P0(int *x, int *s, int *y)
{
WRITE_ONCE(*x, 1);
smp_store_release(s, 1);
r1 = smp_load_acquire(s);
r2 = READ_ONCE(*y);
}

P1(int *x, int *y)
{
WRITE_ONCE(*y, 1);
smp_store_release(s, 2);
r3 = smp_load_acquire(s);
r4 = READ_ONCE(*x);
}

exists (1:r2=0 /\ 1:r4=0)

If smp_store_release() and smp_load_acquire() map to normal TSO loads
and stores on x86, then this test can't be forbidden, can it?

Similar question for the other tests, but this is probably the
easiest one to analyze.

Dan

\
 
 \ /
  Last update: 2017-11-28 00:28    [W:0.142 / U:0.028 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site