Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20;
Date:   Fri, 15 Jul 2022 08:21:45 -0700
From:   "Paul E. McKenney" <paulmck@kernel.org>
To:     Alan Stern <stern@rowland.harvard.edu>
Cc:     Paul =?iso-8859-1?Q?Heidekr=FCger?= <Paul.Heidekrueger@in.tum.de>,
        clang-built-linux <llvm@lists.linux.dev>,
        linux-toolchains@vger.kernel.org,
        Andrea Parri <parri.andrea@gmail.com>,
        Will Deacon <will@kernel.org>,
        Peter Zijlstra <peterz@infradead.org>,
        Boqun Feng <boqun.feng@gmail.com>,
        Nicholas Piggin <npiggin@gmail.com>,
        David Howells <dhowells@redhat.com>,
        Jade Alglave <j.alglave@ucl.ac.uk>,
        Luc Maranget <luc.maranget@inria.fr>,
        Akira Yokosawa <akiyks@gmail.com>,
        Daniel Lustig <dlustig@nvidia.com>,
        Joel Fernandes <joel@joelfernandes.org>,
        Nathan Chancellor <nathan@kernel.org>,
        Nick Desaulniers <ndesaulniers@google.com>,
        Tom Rix <trix@redhat.com>, Palmer Dabbelt <palmer@dabbelt.com>,
        LKML <linux-kernel@vger.kernel.org>,
        linux-arch <linux-arch@vger.kernel.org>,
        Marco Elver <elver@google.com>,
        Charalampos Mainas <charalampos.mainas@gmail.com>,
        Pramod Bhatotia <pramod.bhatotia@in.tum.de>,
        Soham Chakraborty <s.s.chakraborty@tudelft.nl>,
        Martin Fink <martin.fink@in.tum.de>
Subject: Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition
Message-ID: <20220715152145.GZ1790663@paulmck-ThinkPad-P17-Gen-1>
Reply-To: paulmck@kernel.org
References: <20220615114330.2573952-1-paul.heidekrueger@in.tum.de>
 <YqnpshlsAHg7Uf9G@rowland.harvard.edu>
 <50B9D7C1-B11D-4583-9814-BFFF2C80D8CA@in.tum.de>
 <YrHUkfDWsexHRUKj@rowland.harvard.edu>
 <04B4DBD6-1262-4905-9E85-9466FC104895@in.tum.de>
 <YrnFCSjESpeQdciv@rowland.harvard.edu>
 <20F4C097-24B4-416B-95EE-AC11F5952B44@in.tum.de>
 <YtFrPoOARrL/etBu@rowland.harvard.edu>
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Disposition: inline
Content-Transfer-Encoding: 8bit
In-Reply-To: <YtFrPoOARrL/etBu@rowland.harvard.edu>
Precedence: bulk

On Fri, Jul 15, 2022 at 09:27:26AM -0400, Alan Stern wrote:
> On Fri, Jul 15, 2022 at 02:27:28PM +0200, Paul Heidekr?ger wrote:
> > I have just been thinking about how to word this patch; am I correct in
> > assuming that the LKMM does not deal with loop conditions? Or in other
> > words, there is no way for a loop condition to impose a ctrl dependency on
> > any WRITE_ONCE's in the loop body? It are only if and switch statements the
> > LKMM is concerned with in the case of ctrl dependencies?
> 
> In theory, the LKMM does say that a loop condition imposes a control 
> dependency on any memory accesses within the loop body.  However, the 
> herd7 tool has only very limited support for looping constructs, so in 
> practice it's not possible to create suitable litmus tests with loops.

And Alan isn't joking.  The closest simulation that I know of is to
combine limited loop unrolling with the "filter" clause.  The point of
the filter clause is to eliminate from consideration executions that
need the more iterations of the loop to be unrolled.

And that means that as far as LKMM is concerned, loop-based control
dependencies are similar to those for nested "if" statements.

							Thanx, Paul