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

[Alan Stern]

On Tue, 19 Feb 2019, Andrea Parri wrote:

> 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)
> 
> Signed-off-by: Andrea Parri <andrea.parri@xxxxxxxxxxxxxxxxxxxx>
> Cc: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> Cc: Will Deacon <will.deacon@xxxxxxx>
> Cc: Peter Zijlstra <peterz@xxxxxxxxxxxxx>
> Cc: Boqun Feng <boqun.feng@xxxxxxxxx>
> Cc: Nicholas Piggin <npiggin@xxxxxxxxx>
> Cc: David Howells <dhowells@xxxxxxxxxx>
> Cc: Jade Alglave <j.alglave@xxxxxxxxx>
> Cc: Luc Maranget <luc.maranget@xxxxxxxx>
> Cc: "Paul E. McKenney" <paulmck@xxxxxxxxxxxxx>
> Cc: Akira Yokosawa <akiyks@xxxxxxxxx>
> Cc: Daniel Lustig <dlustig@xxxxxxxxxx>
> ---
>  tools/memory-model/Documentation/explanation.txt | 28 ------------------------
>  tools/memory-model/linux-kernel.cat              |  2 +-
>  2 files changed, 1 insertion(+), 29 deletions(-)
> 
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index 68caa9a976d0c..965e11744d090 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -1019,34 +1019,6 @@ section for more details).  The kernel includes a workaround for this
>  problem when the loads come from READ_ONCE(), and therefore the LKMM
>  includes address dependencies to loads in the ppo relation.
>  
> -On the other hand, dependencies can indirectly affect the ordering of
> -two loads.  This happens when there is a dependency from a load to a
> -store and a second, po-later load reads from that store:
> -
> -	R ->dep W ->rfi R',
> -
> -where the dep link can be either an address or a data dependency.  In
> -this situation we know it is possible for the CPU to execute R' before
> -W, because it can forward the value that W will store to R'.  But it
> -cannot execute R' before R, because it cannot forward the value before
> -it knows what that value is, or that W and R' do access the same
> -location.  However, if there is merely a control dependency between R
> -and W then the CPU can speculatively forward W to R' before executing
> -R; if the speculation turns out to be wrong then the CPU merely has to
> -restart or abandon R'.
> -
> -(In theory, a CPU might forward a store to a load when it runs across
> -an address dependency like this:
> -
> -	r1 = READ_ONCE(ptr);
> -	WRITE_ONCE(*r1, 17);
> -	r2 = READ_ONCE(*r1);
> -
> -because it could tell that the store and the second load access the
> -same location even before it knows what the location's address is.
> -However, none of the architectures supported by the Linux kernel do
> -this.)
> -
>  Two memory accesses of the same location must always be executed in
>  program order if the second access is a store.  Thus, if we have

If we do decide to remove the (dep;rfi) term, I would prefer not to
erase this discussion from explanation.txt completely.  Instead, we
should explain that the operational model predicts this ordering but it
has been left out of the LKMM for practical (not technical) reasons.

Alan