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

[Paul E. McKenney]

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)