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 <[email protected]>
> Cc: Alan Stern <[email protected]>
> Cc: Will Deacon <[email protected]>
> Cc: Peter Zijlstra <[email protected]>
> Cc: Boqun Feng <[email protected]>
> Cc: Nicholas Piggin <[email protected]>
> Cc: David Howells <[email protected]>
> Cc: Jade Alglave <[email protected]>
> Cc: Luc Maranget <[email protected]>
> Cc: "Paul E. McKenney" <[email protected]>
> Cc: Akira Yokosawa <[email protected]>
> Cc: Daniel Lustig <[email protected]>
> ---
> 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
>
