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

[Alan Stern]

On Tue, Jan 17, 2023 at 09:43:08AM -0800, Paul E. McKenney wrote:
> On Tue, Jan 17, 2023 at 10:56:34AM -0500, Alan Stern wrote:

> > Isn't it true that the current code will flag srcu-bad-nesting if a 
> > litmus test has non-nested overlapping SRCU read-side critical sections?
> 
> Now that you mention it, it does indeed, flagging srcu-bad-nesting.
> 
> Just to see if I understand, different-values yields true if the set
> contains multiple elements with the same value mapping to different
> values.  Or, to put it another way, if the relation does not correspond
> to a function.
> 
> Or am I still missing something?
> 
> > And if it is true, is there any need to change the memory model at this 
> > point?
> > 
> > (And if it's not true, that's most likely due to a bug in herd7.)
> 
> Agreed, changes must wait for SRCU support in herd7.

Maybe we don't.  Please test the patch below; I think it will do what 
you want -- and it doesn't rule out nesting.

Alan



Index: usb-devel/tools/memory-model/linux-kernel.bell
===================================================================
--- usb-devel.orig/tools/memory-model/linux-kernel.bell
+++ usb-devel/tools/memory-model/linux-kernel.bell
@@ -57,20 +57,12 @@ flag ~empty Rcu-lock \ domain(rcu-rscs)
 flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking
 
 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
-let srcu-rscs = let rec
-	    unmatched-locks = Srcu-lock \ domain(matched)
-	and unmatched-unlocks = Srcu-unlock \ range(matched)
-	and unmatched = unmatched-locks | unmatched-unlocks
-	and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc
-	and unmatched-locks-to-unlocks =
-		([unmatched-locks] ; po ; [unmatched-unlocks]) & loc
-	and matched = matched | (unmatched-locks-to-unlocks \
-		(unmatched-po ; unmatched-po))
-	in matched
+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
+flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-unlocking
+flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-unlocks
 
 (* Check for use of synchronize_srcu() inside an RCU critical section *)
 flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
@@ -80,11 +72,11 @@ flag ~empty different-values(srcu-rscs)
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
-		LKR | LKW | UL | LF | RL | RU
+ 		LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock
 let Plain = M \ Marked
 
 (* Redefine dependencies to include those carried through plain accesses *)
-let carry-dep = (data ; rfi)*
+let carry-dep = (data ; rfi ; [~Srcu-lock])*
 let addr = carry-dep ; addr
 let ctrl = carry-dep ; ctrl
 let data = carry-dep ; data
Index: usb-devel/tools/memory-model/linux-kernel.def
===================================================================
--- usb-devel.orig/tools/memory-model/linux-kernel.def
+++ usb-devel/tools/memory-model/linux-kernel.def
@@ -49,8 +49,8 @@ synchronize_rcu() { __fence{sync-rcu}; }
 synchronize_rcu_expedited() { __fence{sync-rcu}; }
 
 // SRCU
-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); }
 synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
 synchronize_srcu_expedited(X)  { __srcu{sync-srcu}(X); }