Date:   Tue, 24 Jan 2023 14:54:49 -0800
From:   "Paul E. McKenney" <paulmck@kernel.org>
To:     Alan Stern <stern@rowland.harvard.edu>
Cc:     Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>,
        Andrea Parri <parri.andrea@gmail.com>,
        Jonas Oberhauser <jonas.oberhauser@huawei.com>,
        Peter Zijlstra <peterz@infradead.org>, will <will@kernel.org>,
        "boqun.feng" <boqun.feng@gmail.com>, npiggin <npiggin@gmail.com>,
        dhowells <dhowells@redhat.com>,
        "j.alglave" <j.alglave@ucl.ac.uk>,
        "luc.maranget" <luc.maranget@inria.fr>, akiyks <akiyks@gmail.com>,
        dlustig <dlustig@nvidia.com>, joel <joel@joelfernandes.org>,
        urezki <urezki@gmail.com>,
        quic_neeraju <quic_neeraju@quicinc.com>,
        frederic <frederic@kernel.org>,
        Kernel development list <linux-kernel@vger.kernel.org>
Subject: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus
 test)
Message-ID: <20230124225449.GY2948950@paulmck-ThinkPad-P17-Gen-1>
Reply-To: paulmck@kernel.org
References: <20230124040611.GD2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y8+8fH52iqQABYs2@andrea>
 <20230124145423.GI2948950@paulmck-ThinkPad-P17-Gen-1>
 <8cc799ab-ffa1-47f7-6e1d-97488a210f14@huaweicloud.com>
 <20230124162253.GL2948950@paulmck-ThinkPad-P17-Gen-1>
 <3e5020c2-0dd3-68a6-9b98-5a7f57ed7733@huaweicloud.com>
 <20230124172647.GN2948950@paulmck-ThinkPad-P17-Gen-1>
 <2788294a-972e-acbc-84ce-25d2bb4d26d6@huaweicloud.com>
 <20230124221524.GV2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y9BdNVk2LQiUYABS@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: <Y9BdNVk2LQiUYABS@rowland.harvard.edu>
Precedence: bulk

On Tue, Jan 24, 2023 at 05:35:33PM -0500, Alan Stern wrote:
> On Tue, Jan 24, 2023 at 02:15:24PM -0800, Paul E. McKenney wrote:
> > > Ah, looking at the model now. Indeed it's forbidden, because in order to say
> > > that something is in co, there must not be a (resulting) cycle of co and
> > > barriers. But you'd get that here.? In the axiomatic model, this corresponds
> > > to saying Power's "prop | co" is acyclic. The same isn't true in LKMM. So
> > > that's probably why.
> > 
> > Which means that the RCU and SRCU implementations need to make (admittedly
> > small) guarantees that cannot be expressed in LKMM.  Which is in fact
> > what I was remembering, so I feel better now.
> > 
> > Not sure about the rest of you, though.  ;-)
> 
> Can you be more explicit?  Exactly what guarantees does the kernel 
> implementation make that can't be expressed in LKMM?

I doubt that I will be able to articulate it very well, but here goes.

Within the Linux kernel, the rule for a given RCU "domain" is that if
an event follows a grace period in pretty much any sense of the word,
then that event sees the effects of all events in all read-side critical
sections that began prior to the start of that grace period.

Here the senses of the word "follow" include combinations of rf, fr,
and co, combined with the various acyclic and irreflexive relations
defined in LKMM.

> And are these anything the memory model needs to worry about?

Given that several people, yourself included, are starting to use LKMM
to analyze the Linux-kernel RCU implementations, maybe it does.

Me, I am happy either way.

							Thanx, Paul