Received: by 2002:ac0:a581:0:0:0:0:0 with SMTP id m1-v6csp738266imm; Wed, 4 Jul 2018 05:14:08 -0700 (PDT) X-Google-Smtp-Source: AAOMgpezfEYe/XJ2JgBOppg15WRZX1ZSmEW4xxJcdoBA72VsGaXtZmxPYMG4AYjaUShu3HP48KDR X-Received: by 2002:a17:902:850b:: with SMTP id bj11-v6mr1877892plb.210.1530706448316; Wed, 04 Jul 2018 05:14:08 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1530706448; cv=none; d=google.com; s=arc-20160816; b=j68lBtGTiL8mnktXO8MLUm8Dzp0FAPP5zJvVqPJNzRIg9PByjCqdDsoKAHe4sg47Pd y3iGSuBiwdWZrzb9CPIFFiKknj3FBOH3TCgfhcQKZZdgHd9B34A5017Xy14q9bHGRGvb c+vZrD/llG8lqVOpSG6qt4lEh0+3S1SM+FkFojS4lCj990mvtZy59CYYQ+lg27e+f1vB NF4KR0GLAfhaLiEu3GzuADwxa7V+QBd/D7azK4SM434YuWIABpCjCSeBRNqeodcESkto 2sPCUCwR63bwshTQ/xCWAJ7e+vrTHw6yLeN/pywf9tO8BEIn7blb+Wom9INUml4nr9I1 nOKA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:sender:user-agent:in-reply-to :content-disposition:mime-version:references:message-id:subject:cc :to:from:date:arc-authentication-results; bh=5jTx89MbnBBjfyYp8Iwe8UI6N0seQowbCj2KRsZC4uI=; b=DYrD0TE4nKtMQ0/oYnz6X6R8wSAJtj5jWkB0ODvxdKo49l28ytGnFvrCo6BQKDZkwT IKurVuWm5yKrrKrXd4gW6235j1zu/6nOvqR23OkSm+XyTDmF4oJAT4UjYIKqPFZF/IGR gKyNObnU6P9D/nHpXm+6Xct4eMtpyQnUEmr3LQel1SiDmGZUb40THwzGBhEtHKcsMN+u on9jlHweynyPz9AvkWYHFnU8Djbm6ZSb3/TqTf3WaZcxUKUsKV9SuOPdLrcOBzDIKh8T UEokofi9bfzp4CMHphTpTtQomuUzm8VZbAhEany9AhUjKdkBXaB3SCifIaY70Lrc2cFX qmJA== ARC-Authentication-Results: i=1; mx.google.com; spf=pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Return-Path: Received: from vger.kernel.org (vger.kernel.org. [209.132.180.67]) by mx.google.com with ESMTP id c197-v6si3849924pfc.74.2018.07.04.05.13.53; Wed, 04 Jul 2018 05:14:08 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67; Authentication-Results: mx.google.com; spf=pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S934098AbeGDMNQ (ORCPT + 99 others); Wed, 4 Jul 2018 08:13:16 -0400 Received: from usa-sjc-mx-foss1.foss.arm.com ([217.140.101.70]:36372 "EHLO foss.arm.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S932997AbeGDMNP (ORCPT ); Wed, 4 Jul 2018 08:13:15 -0400 Received: from usa-sjc-imap-foss1.foss.arm.com (unknown [10.72.51.249]) by usa-sjc-mx-foss1.foss.arm.com (Postfix) with ESMTP id 23C6F18A; Wed, 4 Jul 2018 05:13:15 -0700 (PDT) Received: from edgewater-inn.cambridge.arm.com (usa-sjc-imap-foss1.foss.arm.com [10.72.51.249]) by usa-sjc-imap-foss1.foss.arm.com (Postfix) with ESMTPA id E8D183F5BA; Wed, 4 Jul 2018 05:13:14 -0700 (PDT) Received: by edgewater-inn.cambridge.arm.com (Postfix, from userid 1000) id D82081AE189D; Wed, 4 Jul 2018 13:13:54 +0100 (BST) Date: Wed, 4 Jul 2018 13:13:54 +0100 From: Will Deacon To: "Paul E. McKenney" Cc: Alan Stern , Andrea Parri , LKMM Maintainers -- Akira Yokosawa , Boqun Feng , David Howells , Jade Alglave , Luc Maranget , Nicholas Piggin , Peter Zijlstra , Kernel development list Subject: Re: [PATCH 2/2] tools/memory-model: Add write ordering by release-acquire and by locks Message-ID: <20180704121354.GC26941@arm.com> References: <20180625081920.GA5619@andrea> <20180704112852.GH3593@linux.vnet.ibm.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20180704112852.GH3593@linux.vnet.ibm.com> User-Agent: Mutt/1.5.23 (2014-03-12) Sender: linux-kernel-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Wed, Jul 04, 2018 at 04:28:52AM -0700, Paul E. McKenney wrote: > On Tue, Jul 03, 2018 at 01:28:17PM -0400, Alan Stern wrote: > > PS: Paul, is the patch which introduced rel-rf-acq-po currently present > > in any of your branches? I couldn't find it. > > It is not, I will add it back in. I misinterpreted your "drop this > patch" on 2/2 as "drop both patches". Please accept my apologies! > > Just to double-check, the patch below should be added, correct? Hang on, I'm not sure this patch is quite right either. We need to reach agreement on whether or not we want to support native RCpc acquire/release instructions before we work out what to do with this relation. Will > ------------------------------------------------------------------------ > > Date: Thu, 21 Jun 2018 13:26:49 -0400 (EDT) > From: Alan Stern > To: LKMM Maintainers -- Akira Yokosawa , Andrea Parri > , Boqun Feng > , David Howells , > Jade Alglave , Luc Maranget , > Nicholas Piggin , > "Paul E. McKenney" , Peter Zijlstra , > Will Deacon > cc: Kernel development list > Subject: [PATCH 1/2] tools/memory-model: Change rel-rfi-acq ordering to > (rel-rf-acq-po & int) > Message-ID: > > This patch changes the LKMM rule which says that an acquire which > reads from an earlier release must be executed after that release (in > other words, the release cannot be forwarded to the acquire). This is > not true on PowerPC, for example. > > What is true instead is that any instruction following the acquire > must be executed after the release. On some architectures this is > because a write-release cannot be forwarded to a read-acquire; on > others (including PowerPC) it is because the implementation of > smp_load_acquire() places a memory barrier immediately after the > load. > > This change to the model does not cause any change to the model's > predictions. This is because any link starting from a load must be an > instance of either po or fr. In the po case, the new rule will still > provide ordering. In the fr case, we also have ordering because there > must be a co link to the same destination starting from the > write-release. > > Signed-off-by: Alan Stern > > --- > > > [as1870] > > > tools/memory-model/Documentation/explanation.txt | 35 ++++++++++++----------- > tools/memory-model/linux-kernel.cat | 6 +-- > 2 files changed, 22 insertions(+), 19 deletions(-) > > Index: usb-4.x/tools/memory-model/linux-kernel.cat > =================================================================== > --- usb-4.x.orig/tools/memory-model/linux-kernel.cat > +++ usb-4.x/tools/memory-model/linux-kernel.cat > @@ -38,7 +38,7 @@ let strong-fence = mb | gp > (* Release Acquire *) > let acq-po = [Acquire] ; po ; [M] > let po-rel = [M] ; po ; [Release] > -let rfi-rel-acq = [Release] ; rfi ; [Acquire] > +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po > > (**********************************) > (* Fundamental coherence ordering *) > @@ -60,9 +60,9 @@ 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) | rfi-rel-acq > +let to-r = addr | (dep ; rfi) > let fence = strong-fence | wmb | po-rel | rmb | acq-po > -let ppo = to-r | to-w | fence > +let ppo = to-r | to-w | fence | (rel-rf-acq-po & int) > > (* Propagation: Ordering from release operations and strong fences. *) > let A-cumul(r) = rfe? ; r > Index: usb-4.x/tools/memory-model/Documentation/explanation.txt > =================================================================== > --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt > +++ usb-4.x/tools/memory-model/Documentation/explanation.txt > @@ -1067,27 +1067,30 @@ allowing out-of-order writes like this t > violating the write-write coherence rule by requiring the CPU not to > send the W write to the memory subsystem at all!) > > -There is one last example of preserved program order in the LKMM: when > -a load-acquire reads from an earlier store-release. For example: > +There is one last example of preserved program order in the LKMM; it > +applies to instructions po-after a load-acquire which reads from an > +earlier store-release. For example: > > smp_store_release(&x, 123); > r1 = smp_load_acquire(&x); > + WRITE_ONCE(&y, 246); > > If the smp_load_acquire() ends up obtaining the 123 value that was > -stored by the smp_store_release(), the LKMM says that the load must be > -executed after the store; the store cannot be forwarded to the load. > -This requirement does not arise from the operational model, but it > -yields correct predictions on all architectures supported by the Linux > -kernel, although for differing reasons. > - > -On some architectures, including x86 and ARMv8, it is true that the > -store cannot be forwarded to the load. On others, including PowerPC > -and ARMv7, smp_store_release() generates object code that starts with > -a fence and smp_load_acquire() generates object code that ends with a > -fence. The upshot is that even though the store may be forwarded to > -the load, it is still true that any instruction preceding the store > -will be executed before the load or any following instructions, and > -the store will be executed before any instruction following the load. > +written by the smp_store_release(), the LKMM says that the store to y > +must be executed after the store to x. In fact, the only way this > +could fail would be if the store-release was forwarded to the > +load-acquire; the LKMM says it holds even in that case. This > +requirement does not arise from the operational model, but it yields > +correct predictions on all architectures supported by the Linux > +kernel, although for differing reasons: > + > +On some architectures, including x86 and ARMv8, a store-release cannot > +be forwarded to a load-acquire. On others, including PowerPC and > +ARMv7, smp_load_acquire() generates object code that ends with a > +fence. The result is that even though the store-release may be > +forwarded to the load-acquire, it is still true that the store-release > +(and all preceding instructions) will be executed before any > +instruction following the load-acquire. > > > AND THEN THERE WAS ALPHA > >