On Thu, Jan 26, 2023 at 12:30:14PM +0100, Jonas Oberhauser wrote:
I'll let Paul answer this.
On 1/25/2023 11:52 PM, Alan Stern wrote:
On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote:I don't think they're necessarily implemented in a compatible way, so
On 1/25/2023 9:21 PM, Alan Stern wrote:Why invent new classes for them? They are literally the same operation
(* Validate nesting *)[...]
flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock
flag ~empty Srcu-unlock \ range(srcu-rscs) as unmatched-srcu-unlock
+flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-matches
// SRCUHow do you feel about introducing Srcu-up and Srcu-down with this patch?
-srcu_read_lock(X) __srcu{srcu-lock}(X)
-srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
+srcu_read_lock(X) __load{srcu-lock}(*X)
+srcu_read_unlock(X,Y) { __store{srcu-unlock}(*X,Y); }
+srcu_down_read(X) __load{srcu-lock}(*X)
+srcu_up_read(X,Y) { __store{srcu-unlock}(*X,Y); }
as Srcu-lock and Srcu-unlock; the only difference is how the kernel's
lockdep checker treats them.
r = srcu_lock(s);
srcu_up(s,r);
might not actually work, but would currently be ok'ed by LKMM.
WithBear in mind that the herd7 model is not obliged to find and warn about
different classes you could state
flag ~empty [Srcu-lock];srcu-rscs;[Srcu-up] as srcu-mismatch-lock-to-up
flag ~empty [Srcu-down];srcu-rscs;[Srcu-unlock] as
srcu-mismatch-down-to-unlock
I think with the current implementation this code might work, but I don't
feel like this is inherently true.
You could then also go ahead and define the "same CPU" requirement as a flag
for lock and unlock specifically, like
flag ~empty [Srcu-lock];srcu-rscs & ext as srcu-lock-unlock-mismatch-CPU
or so.
all possible bugs in a litmus test. Especially if the same code would
generate a warning or error when run in the kernel.