From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org X-Spam-Level: X-Spam-Status: No, score=-10.3 required=3.0 tests=BAYES_00, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,MENTIONS_GIT_HOSTING, SPF_HELO_NONE,SPF_PASS,USER_AGENT_SANE_1 autolearn=unavailable autolearn_force=no version=3.4.0 Received: from mail.kernel.org (mail.kernel.org [198.145.29.99]) by smtp.lore.kernel.org (Postfix) with ESMTP id 6367FC4320A for ; Fri, 30 Jul 2021 20:35:43 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 35B9760EE6 for ; Fri, 30 Jul 2021 20:35:43 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S230483AbhG3Ufr (ORCPT ); Fri, 30 Jul 2021 16:35:47 -0400 Received: from netrider.rowland.org ([192.131.102.5]:57291 "HELO netrider.rowland.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with SMTP id S230217AbhG3Ufr (ORCPT ); Fri, 30 Jul 2021 16:35:47 -0400 Received: (qmail 265720 invoked by uid 1000); 30 Jul 2021 16:35:41 -0400 Date: Fri, 30 Jul 2021 16:35:41 -0400 From: Alan Stern To: Jade Alglave Cc: Will Deacon , Peter Zijlstra , Linus Torvalds , Segher Boessenkool , "Paul E. McKenney" , Andrea Parri , Boqun Feng , Nick Piggin , David Howells , Luc Maranget , Akira Yokosawa , Linux Kernel Mailing List , linux-toolchains@vger.kernel.org, linux-arch Subject: Re: [RFC] LKMM: Add volatile_if() Message-ID: <20210730203541.GA262784@rowland.harvard.edu> References: <20210605145739.GB1712909@rowland.harvard.edu> <20210606001418.GH4397@paulmck-ThinkPad-P17-Gen-1> <20210606012903.GA1723421@rowland.harvard.edu> <20210606115336.GS18427@gate.crashing.org> <20210606182213.GA1741684@rowland.harvard.edu> <20210607115234.GA7205@willie-the-truck> <20210730172020.GA32396@knuckles.cs.ucl.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20210730172020.GA32396@knuckles.cs.ucl.ac.uk> User-Agent: Mutt/1.10.1 (2018-07-13) Precedence: bulk List-ID: X-Mailing-List: linux-toolchains@vger.kernel.org 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