Messages in this thread |  | | Date | Sat, 14 Jan 2023 21:19:58 -0800 | From | "Paul E. McKenney" <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
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)
|  |