Re: [RFC] LKMM: Add volatile_if()

From: Alan Stern <stern@rowland.harvard.edu>
To: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Will Deacon <will@kernel.org>,
	Peter Zijlstra <peterz@infradead.org>,
	Linus Torvalds <torvalds@linux-foundation.org>,
	Segher Boessenkool <segher@kernel.crashing.org>,
	"Paul E. McKenney" <paulmck@kernel.org>,
	Andrea Parri <parri.andrea@gmail.com>,
	Boqun Feng <boqun.feng@gmail.com>,
	Nick Piggin <npiggin@gmail.com>,
	David Howells <dhowells@redhat.com>,
	Luc Maranget <luc.maranget@inria.fr>,
	Akira Yokosawa <akiyks@gmail.com>,
	Linux Kernel Mailing List <linux-kernel@vger.kernel.org>,
	linux-toolchains@vger.kernel.org,
	linux-arch <linux-arch@vger.kernel.org>
Subject: Re: [RFC] LKMM: Add volatile_if()
Date: Fri, 30 Jul 2021 16:35:41 -0400	[thread overview]
Message-ID: <20210730203541.GA262784@rowland.harvard.edu> (raw)
In-Reply-To: <20210730172020.GA32396@knuckles.cs.ucl.ac.uk>

On Fri, Jul 30, 2021 at 06:20:22PM +0100, Jade Alglave wrote:
> Dear all,

> Sincere apologies in taking so long to reply. I attach a technical
> report which describes the status of dependencies in the Arm memory
> model. 
> 
> I have also released the corresponding cat files and a collection of
> interesting litmus tests over here:
> https://github.com/herd/herdtools7/commit/f80bd7c2e49d7d3adad22afc62ff4768d65bf830
> 
> I hope this material can help inform this conversation and I would love
> to hear your thoughts.

Jade:

Here are a few very preliminary reactions (I haven't finished reading the 
entire paper yet).

P.2: Typo: "the register X1 contains the address x" should be "the 
register X1 contains the address of x".

P.4 and later: Several complicated instructions (including CSEL, CAS, and 
SWP) are mentioned but not explained; the text assumes that the reader 
already understands what these instructions do.  A brief description of 
their effects would help readers like me who aren't very familiar with the 
ARM instruction set.

P.4: The text describing Instrinsic dependencies in CSEL instructions says 
that if cond is true then there is an Intrinsic control dependencies from 
the read of PSTATE.NZCV to the read of Xm.  Why is this so?  Can't the CPU 
read Xm unconditionally before it knows whether the value will be used?

P.17: The definition of "Dependency through registers" uses the acronym 
"PE", but the acronym isn't defined anywhere.

P.14: In the description of Figure 18, I wasn't previously aware -- 
although perhaps I should have been -- that ARM could speculatively place 
a Store in a local store buffer, allowing it to be forwarded to a po-later 
Read.  Why doesn't the same mechanism apply to Figure 20, allowing the 
Store in D to be speculatively placed in a local store buffer and 
forwarded to E?  Is this because conditional branches are predicted but 
loads aren't?  If so, that is a significant difference.

More to come...

Alan