Messages in this thread |  | | Date | Sat, 14 Jan 2023 10:15:37 -0800 | From | "Paul E. McKenney" <> | Subject | Re: 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)
|  |