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:   Wed, 18 Jan 2023 13:06:41 -0800
From:   "Paul E. McKenney" <paulmck@kernel.org>
To:     Jonas Oberhauser <s9joober@gmail.com>
Cc:     Alan Stern <stern@rowland.harvard.edu>,
        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: <20230118210641.GK2948950@paulmck-ThinkPad-P17-Gen-1>
Reply-To: paulmck@kernel.org
References: <20230116190652.GZ2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y8WjmTFnqbAnS1Pz@rowland.harvard.edu>
 <20230116221357.GA2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y8aKlNY4Z0z2Yqs0@andrea>
 <20230117151416.GI2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y8bFMgDSUZymXUsS@rowland.harvard.edu>
 <20230117174308.GK2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y8cBypKx4gM3wBJa@rowland.harvard.edu>
 <20230118035041.GQ2948950@paulmck-ThinkPad-P17-Gen-1>
 <73ff21ef-44fa-2dbf-cae0-f74077875502@gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Disposition: inline
Content-Transfer-Encoding: 8bit
In-Reply-To: <73ff21ef-44fa-2dbf-cae0-f74077875502@gmail.com>
Precedence: bulk

On Wed, Jan 18, 2023 at 08:57:22PM +0100, Jonas Oberhauser wrote:
> 
> 
> On 1/18/2023 4:50 AM, Paul E. McKenney wrote:
> > On Tue, Jan 17, 2023 at 03:15:06PM -0500, Alan Stern wrote:
> > > On Tue, Jan 17, 2023 at 09:43:08AM -0800, Paul E. McKenney wrote:
> > > > On Tue, Jan 17, 2023 at 10:56:34AM -0500, Alan Stern wrote:
> > > > > Isn't it true that the current code will flag srcu-bad-nesting if a
> > > > > litmus test has non-nested overlapping SRCU read-side critical sections?
> > > > Now that you mention it, it does indeed, flagging srcu-bad-nesting.
> > > > 
> > > > Just to see if I understand, different-values yields true if the set
> > > > contains multiple elements with the same value mapping to different
> > > > values.  Or, to put it another way, if the relation does not correspond
> > > > to a function.
> > > As I understand it, given a relation r (i.e., a set of pairs of events),
> > > different-values(r) returns the sub-relation consisting of those pairs
> > > in r for which the value associated with the first event of the pair is
> > > different from the value associated with the second event of the pair.
> > OK, so different-values(r) is different than (r \ id) because the
> > former operates on values and the latter on events?
> 
> I think you can say that (if you allow yourself to be a little bit loose
> with words, as I allow myself to be, much to the chagrin of Alan :) :( :)).

Well, Alan's insistance on rigor has keep LKMM out of trouble more times
than I can count.  ;-)

> If you had a .value functional relation that relates every event to the
> value of that event, then
> ?? different-values(r) = r \ .value ; .value^-1
> i.e., it relates events x and y iff: 1) r relates x and y, and 2) the value
> of x is not equal to the value of y.
> 
> You could write this as
> ?? different-values(r) = r \ .value ; value-id ; .value^-1
> where value-id is like id but for values, i.e., relates every value v to
> itself.
> 
> You could say that this difference operates on the values of the events,
> rather than on the events itself.
> In contrast,
> ??? r \ id
> works directly on the events and relates x and y iff: 1) r relates x and y,
> and 2) the event x is not equal to the event y.
> 
> In this sense I think your characterization is appropriate.

It looks to be "different domain values", but maybe I should just run
some experiments.  ;-)

							Thanx, Paul