[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <73ff21ef-44fa-2dbf-cae0-f74077875502@gmail.com>
Date: Wed, 18 Jan 2023 20:57:22 +0100
From: Jonas Oberhauser <s9joober@...il.com>
To: paulmck@...nel.org, Alan Stern <stern@...land.harvard.edu>
Cc: Andrea Parri <parri.andrea@...il.com>,
Jonas Oberhauser <jonas.oberhauser@...wei.com>,
Peter Zijlstra <peterz@...radead.org>, will <will@...nel.org>,
"boqun.feng" <boqun.feng@...il.com>, npiggin <npiggin@...il.com>,
dhowells <dhowells@...hat.com>,
"j.alglave" <j.alglave@....ac.uk>,
"luc.maranget" <luc.maranget@...ia.fr>, akiyks <akiyks@...il.com>,
dlustig <dlustig@...dia.com>, joel <joel@...lfernandes.org>,
urezki <urezki@...il.com>,
quic_neeraju <quic_neeraju@...cinc.com>,
frederic <frederic@...nel.org>,
Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus
test)
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 :) :( :)).
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.
Powered by blists - more mailing lists