Re: [RFC PATCH] tools/memory-model: Remove (dep ; rfi) from ppo

On Wed, Feb 20, 2019 at 09:57:00AM +0000, Will Deacon wrote:

On Wed, Feb 20, 2019 at 10:26:04AM +0100, Peter Zijlstra wrote:

quoted

On Tue, Feb 19, 2019 at 06:01:17PM -0800, Paul E. McKenney wrote:

quoted

On Tue, Feb 19, 2019 at 11:57:37PM +0100, Andrea Parri wrote:

quoted

Remove this subtle (and, AFAICT, unused) ordering: we can add it back,
if necessary, but let us not encourage people to rely on this thing.

For example, the following "exists" clause can be satisfied with this
change:

C dep-rfi

{ }

P0(int *x, int *y)
{
	WRITE_ONCE(*x, 1);
	smp_store_release(y, 1);
}

P1(int *x, int *y, int *z)
{
	int r0;
	int r1;
	int r2;

	r0 = READ_ONCE(*y);
	WRITE_ONCE(*z, r0);
	r1 = smp_load_acquire(z);
	r2 = READ_ONCE(*x);
}

exists (1:r0=1 /\ 1:r2=0)

Any objections?  If I don't hear any in a couple days, I will apply this.

IIUC you cannot build hardware that allows the above, so why would we
allow it?

Agreed. Maybe the intention was to make the dependency between the read of
*y and the write of *z on P1 a control dependency instead? That's certainly
allowed on arm64.

No no, I did mean dep (= addr | data).  As you remarked, control dep.
aren't going to work here.  I expanded on this in my reply to peterz.

  Andrea

Will