lkml.org 
[lkml]   [2023]   [Jan]   [14]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    From
    SubjectRe: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)
    On Sat, Jan 14, 2023 at 09:53:43AM -0800, Paul E. McKenney wrote:
    > On Fri, Jan 13, 2023 at 08:43:42PM +0000, Jonas Oberhauser wrote:
    > >
    > >
    > > -----Original Message-----
    > > From: Paul E. McKenney [mailto:paulmck@kernel.org]
    > >
    > > > (* Compute matching pairs of Srcu-lock and Srcu-unlock *) let srcu-rscs = ([Srcu-lock] ; rfi ; [Srcu-unlock]) & loc
    > >
    > > How does the Srcu-unlock read from the Srcu-lock? Is there something in your model or in herd that lets it understand lock and unlock should be treated as writes resp. reads from that specific location?
    > >
    > > Or do you mean that value given to Srcu-unlock should be the value produced by Srcu-lock?
    >
    > Yes, and in the Linux kernel one does something like this:
    >
    > idx = srcu_read_lock(&mysrcu);
    > // critical section
    > srcu_read_unlock(&mysrcu, idx);
    >
    > > Perhaps the closest to what you want is to express that as a data dependency if you know how to teach herd that Srcu-unlock is a read and Srcu-lock depends on its second input :D (I have no idea how to do that, hence the questions above)
    >
    > Given that both you and Alan suggested it, I must try it. ;-)

    And it works as desired on these litmus tests:

    manual/kernel/C-srcu-nest-*.litmus

    In this repository:

    https://github.com/paulmckrcu/litmus

    However, this has to be dumb luck because herd7 does not yet provide
    the second argument to srcu_read_unlock(). My guess is that the herd7
    is noting the dependency that is being carried by the pointers to the
    srcu_struct structures. This guess stems in part from the fact that
    I get "Flag unbalanced-srcu-locking" when I have one SRCU read-side
    critical section following another in the same process, both using the
    same srcu_struct structure.

    Nevertheless, here is the resulting .bell fragment:

    ------------------------------------------------------------------------

    (* Compute matching pairs of Srcu-lock and Srcu-unlock *)
    let srcu-rscs = ([Srcu-lock] ; data ; [Srcu-unlock]) & loc

    (* Validate nesting *)
    flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking
    flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking

    (* Check for use of synchronize_srcu() inside an RCU critical section *)
    flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep

    (* Validate SRCU dynamic match *)
    flag ~empty different-values(srcu-rscs) as srcu-bad-nesting

    ------------------------------------------------------------------------

    I also created a C-srcu-nest-*.litmus as shown below, and LKMM does
    complain about one srcu_read_lock() feeding into multiple instances of
    srcu_read_unlock(). The complaint comes from the different_values()
    check, which presumably complains about any duplication in the domain
    or range of the specified relation.

    But still working by accident! ;-)

    Thanx, Paul

    ------------------------------------------------------------------------

    C C-srcu-nest-3

    (*
    * Result: Flag srcu-bad-nesting
    *
    * This demonstrates erroneous matching of a single srcu_read_lock()
    * with multiple srcu_read_unlock() instances.
    *)

    {}

    P0(int *x, int *y, struct srcu_struct *s1, struct srcu_struct *s2)
    {
    int r1;
    int r2;
    int r3;
    int r4;

    r3 = srcu_read_lock(s1);
    r2 = READ_ONCE(*y);
    r4 = srcu_read_lock(s2);
    r5 = srcu_read_lock(s2);
    srcu_read_unlock(s1, r3);
    r1 = READ_ONCE(*x);
    srcu_read_unlock(s2, r4);
    }

    P1(int *x, int *y, struct srcu_struct *s2)
    {
    WRITE_ONCE(*y, 1);
    synchronize_srcu(s2);
    WRITE_ONCE(*x, 1);
    }

    locations [0:r1]
    exists (0:r1=1 /\ 0:r2=0)

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