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
From 1585255508732072548@xxx Mon Nov 27 21:17:43 +0000 2017
X-GM-THRID: 1585255508732072548
X-Gmail-Labels: Inbox,Category Forums,HistoricalUnread