Messages in this thread | | | Subject | Re: Unlock-lock questions and the Linux Kernel Memory Model | From | Daniel Lustig <> | Date | Mon, 27 Nov 2017 15:28:03 -0800 |
| |
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
| |