Re: Unlock-lock questions and the Linux Kernel Memory Model

[Daniel Lustig <dlustig@nvidia.com>]

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