Date: Tue, 19 Dec 2017 14:06:50 +0530
From: afzal mohammed <afzal.mohd.ma@gmail.com>
To: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Cc: Alan Stern <stern@rowland.harvard.edu>,
        Peter Zijlstra <peterz@infradead.org>, parri.andrea@gmail.com,
        will.deacon@arm.com, boqun.feng@gmail.com, npiggin@gmail.com,
        dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
        linux-kernel@vger.kernel.org, elena.reshetova@intel.com
Subject: Re: Prototype patch for Linux-kernel memory model
Message-ID: <20171219083650.GA10215@afzalpc>
References: <20171114075925.apzztfksn4f4y5ue@hirez.programming.kicks-ass.net>
 <Pine.LNX.4.44L0.1711141016340.1796-100000@iolanthe.rowland.org>
 <20171114171505.GS3624@linux.vnet.ibm.com>
 <20171115163749.GA8555@linux.vnet.ibm.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20171115163749.GA8555@linux.vnet.ibm.com>
User-Agent: Mutt/1.5.24 (2015-08-30)
Sender: linux-kernel-owner@vger.kernel.org
Content-Length: 2143
Lines: 61

Hi,

A trivial & late (sorry) comment,

On Wed, Nov 15, 2017 at 08:37:49AM -0800, Paul E. McKenney wrote:

> +THE HAPPENS-BEFORE RELATION: hb
> +-------------------------------

> +Less trivial examples of prop all involve fences.  Unlike the simple
> +examples above, they can require that some instructions are executed
> +out of program order.  This next one should look familiar:
> +
> +	int buf = 0, flag = 0;
> +
> +	P0()
> +	{
> +		WRITE_ONCE(buf, 1);
> +		smp_wmb();
> +		WRITE_ONCE(flag, 1);
> +	}
> +
> +	P1()
> +	{
> +		int r1;
> +		int r2;
> +
> +		r1 = READ_ONCE(flag);
> +		r2 = READ_ONCE(buf);
> +	}
> +
> +This is the MP pattern again, with an smp_wmb() fence between the two
> +stores.  If r1 = 1 and r2 = 0 at the end then there is a prop link
> +from P1's second load to its first (backwards!).  The reason is
> +similar to the previous examples: The value P1 loads from buf gets
> +overwritten by P1's store to buf,

                  P0's store to buf

afzal

> the fence guarantees that the store
> +to buf will propagate to P1 before the store to flag does, and the
> +store to flag propagates to P1 before P1 reads flag.
> +
> +The prop link says that in order to obtain the r1 = 1, r2 = 0 result,
> +P1 must execute its second load before the first.  Indeed, if the load
> +from flag were executed first, then the buf = 1 store would already
> +have propagated to P1 by the time P1's load from buf executed, so r2
> +would have been 1 at the end, not 0.  (The reasoning holds even for
> +Alpha, although the details are more complicated and we will not go
> +into them.)
> +
> +But what if we put an smp_rmb() fence between P1's loads?  The fence
> +would force the two loads to be executed in program order, and it
> +would generate a cycle in the hb relation: The fence would create a ppo
> +link (hence an hb link) from the first load to the second, and the
> +prop relation would give an hb link from the second load to the first.
> +Since an instruction can't execute before itself, we are forced to
> +conclude that if an smp_rmb() fence is added, the r1 = 1, r2 = 0
> +outcome is impossible -- as it should be.