lkml.org 
[lkml]   [2023]   [Jan]   [18]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    SubjectRe: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)
    From


    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.



    \
     
     \ /
      Last update: 2023-03-26 23:46    [W:2.541 / U:0.020 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site