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

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



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.





[Index of Archives]     [Linux Kernel]     [Kernel Newbies]     [x86 Platform Driver]     [Netdev]     [Linux Wireless]     [Netfilter]     [Bugtraq]     [Linux Filesystems]     [Yosemite Discussion]     [MIPS Linux]     [ARM Linux]     [Linux Security]     [Linux RAID]     [Samba]     [Device Mapper]

  Powered by Linux