Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)

Paul E. McKenney
2023-01-15T05:20:15Z

On Sat, Jan 14, 2023 at 02:58:29PM -0500, Alan Stern wrote:
> On Sat, Jan 14, 2023 at 10:15:37AM -0800, Paul E. McKenney wrote:
> > > > 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().
>
> Yes it does. Grep for srcu_read_unlock in linux-kernel.def and you'll
> see two arguments.

Right you are! Too early this morning...

> > My guess is that the herd7
> > is noting the dependency that is being carried by the pointers to the
> > srcu_struct structures.
>
> That is not a dependency.

You are right, and apparently neither is the value returned by
srcu_read_lock() and passed to srcu_read_unlock().

> > 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().
>
> It shouldn't; that doesn't happen in the litmus test below. But the
> test does contain an srcu_read_lock() that doesn't match any instances
> of srcu_read_unlock(), so you should be getting an
> "unbalanced-srcu-locking" complaint -- and indeed, you mentioned above
> that this does happen.
>
> Also, your bell file doesn't contain a check for a lock matched with
> multiple unlocks, so there's no way for herd to complain about it.

Agreed!

> > The complaint comes from the different_values()
> > check, which presumably complains about any duplication in the domain
> > or range of the specified relation.
>
> No; different_values() holds when the values of the two events
> linked by srcu-rscs are different. It has nothing to do with
> duplication.

I removed the different_values() check and one of the complaints
went away, but yes, the other one did not.

> > 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);
> > }
>
> This has 3 locks and 2 unlocks. The first lock matches the the first
> unlock (r3 and s3), the second lock matches the second unlock (r4 and
> s2), and the third lock doesn't match any unlock (r5 and s2).

Thank you and fixed.

Thanx, Paul

> Alan
>
> >
> > 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)