Re: [PATCH RFC tools/lkmm 10/12] tools/memory-model: Add a S lock-based external-view litmus test

[Peter Zijlstra]

On Thu, Feb 22, 2018 at 06:45:32PM +0800, Boqun Feng wrote:
> Maybe it's me who misunderstand Daniel's words. But my understanding is
> that riscv people are on a debate about whether their "RCpc" atomic
> instructions need to be more strict: release+acquire pair orders two
> writes. And I thought that atomics(including RmW atomics) in kernel only
> have purely RCpc semantics, which I needed to check with you guy. And if
> I'm right, it's cerntainly fine for riscv "RCpc" instruction to be
> purely RCpc.
> 
> Note that even on PPC, the release+acquire pair of atomics orders writes
> before and after, and on x86, writes are ordered since it's TSO. So
> strictly speaking, I think our current implementation of atomics are a
> little more strict than purely RCpc. If we think this is an requirement
> for implementation of atomic primitives, than the current version of
> riscv's "RCpc" atomics don't suffice.


So the question is:

P0()
{
	WRITE_ONCE(x, 1);
	smp_store_release(&y, 1);
	r0 = smp_load_acquire(&y);
	WRITE_ONCE(z, 1);
}

P1()
{
	r1 = READ_ONCE(z);
	smp_rmb();
	r2 = READ_ONCE(x);
}

exists: r0 == 1 /\ r1==1 /\ r2==0

Which per the current LKMM would be forbidden? How would strict RCpc
allow that? Due to a fwd from the release to the acquire and then
defeating the ordering or something like that?

My vote would go to disallowing this. Allowing this would be rather
subtle and unexpected IMO.