Messages in this thread | | | Date | Wed, 18 Jan 2023 20:57:22 +0100 | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) | From | Jonas Oberhauser <> |
| |
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.
| |