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

[Paul E. McKenney]

On Tue, Feb 19, 2019 at 11:57:37PM +0100, 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)

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

							Thanx, Paul

> 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
>  
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 8dcb37835b613..6b9e3bb4e397f 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -62,7 +62,7 @@ let dep = addr | data
>  let rwdep = (dep | ctrl) ; [W]
>  let overwrite = co | fr
>  let to-w = rwdep | (overwrite & int)
> -let to-r = addr | (dep ; rfi)
> +let to-r = addr ; [R]
>  let fence = strong-fence | wmb | po-rel | rmb | acq-po
>  let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
>  
> -- 
> 2.7.4
>