[PATCH 1/2] tools/memory-model: Fix bug in lock.cat

[PATCH 1/2] tools/memory-model: Fix bug in lock.cat

[Alan Stern]

Andrea reported that the following innocuous litmus test:

C T

{}

P0(spinlock_t *x)
{
	int r0;

	spin_lock(x);
	spin_unlock(x);
	r0 = spin_is_locked(x);
}

gives rise to a nonsensical empty result with no executions:

$ herd7 -conf linux-kernel.cfg T.litmus
Test T Required
States 0
Ok
Witnesses
Positive: 0 Negative: 0
Condition forall (true)
Observation T Never 0 0
Time T 0.00
Hash=6fa204e139ddddf2cb6fa963bad117c0

The problem is caused by a bug in the lock.cat part of the LKMM.  Its
computation of the rf relation for RU (read-unlocked) events is
faulty; it implicitly assumes that every RU event must read from
either a UL (unlock) event in another thread or from the lock's
initial state.  Neither is true in the litmus test above, so the
computation yields no possible executions.

The lock.cat code tries to make up for this deficiency by allowing RU
events outside of critical sections to read from the last po-previous
UL event.  But it does this incorrectly, trying to keep these rfi links
separate from the rfe links that might also be needed, and passing only
the latter to herd7's cross() macro.

The problem is fixed by merging the two sets of possible rf links for
RU events and using them all in the call to cross().

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Reported-and-tested-by: Andrea Parri <parri.andrea@gmail.com>
Closes: https://lore.kernel.org/linux-arch/ZlC0IkzpQdeGj+a3@andrea/
Fixes: 15553dcbca06 ("tools/memory-model: Add model support for spin_is_locked()")
CC: <stable@vger.kernel.org>

---

 tools/memory-model/lock.cat |   20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

Index: usb-devel/tools/memory-model/lock.cat
===================================================================
--- usb-devel.orig/tools/memory-model/lock.cat
+++ usb-devel/tools/memory-model/lock.cat
@@ -102,19 +102,19 @@ let rf-lf = rfe-lf | rfi-lf
  * within one of the lock's critical sections returns False.
  *)
 
-(* rfi for RU events: an RU may read from the last po-previous UL *)
-let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
-
-(* rfe for RU events: an RU may read from an external UL or the initial write *)
-let all-possible-rfe-ru =
-	let possible-rfe-ru r =
+(*
+ * rf for RU events: an RU may read from an external UL or the initial write,
+ * or from the last po-previous UL
+ *)
+let all-possible-rf-ru =
+	let possible-rf-ru r =
 		let pair-to-relation p = p ++ 0
-		in map pair-to-relation (((UL | IW) * {r}) & loc & ext)
-	in map possible-rfe-ru RU
+		in map pair-to-relation ((((UL | IW) * {r}) & loc & ext) |
+			(((UL * {r}) & po-loc) \ ([UL] ; po-loc ; [LKW] ; po-loc)))
+	in map possible-rf-ru RU
 
 (* Generate all rf relations for RU events *)
-with rfe-ru from cross(all-possible-rfe-ru)
-let rf-ru = rfe-ru | rfi-ru
+with rf-ru from cross(all-possible-rf-ru)
 
 (* Final rf relation *)
 let rf = rf | rf-lf | rf-ru

[PATCH 2/2] tools/memory-model: Code reorganization in lock.cat

[Alan Stern]

Code reorganization for the lock.cat file in tools/memory-model:

Improve the efficiency by ruling out right at the start RU events
(spin_is_locked() calls that return False) inside a critical section
for the same lock.

Improve the organization of the code for handling LF and RU events by
pulling the definitions of the pair-to-relation macro out from two
different complicated compound expressions, using a single standalone
definition instead.

Rewrite the calculations of the rf relation for LF and RU events, for
greater clarity.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>

---

 tools/memory-model/lock.cat |   56 +++++++++++++++++++++++++++-----------------
 1 file changed, 35 insertions(+), 21 deletions(-)

Index: usb-devel/tools/memory-model/lock.cat
===================================================================
--- usb-devel.orig/tools/memory-model/lock.cat
+++ usb-devel/tools/memory-model/lock.cat
@@ -54,6 +54,12 @@ flag ~empty LKR \ domain(lk-rmw) as unpa
  *)
 empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
 
+(*
+ * In the same way, spin_is_locked() inside a critical section must always
+ * return True (no RU events can be in a critical section for the same lock).
+ *)
+empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked
+
 (* The final value of a spinlock should not be tested *)
 flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
 
@@ -79,39 +85,47 @@ empty ([UNMATCHED-LKW] ; loc ; [UNMATCHE
 (* rfi for LF events: link each LKW to the LF events in its critical section *)
 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
 
-(* rfe for LF events *)
+(* Utility macro to convert a single pair to a single-edge relation *)
+let pair-to-relation p = p ++ 0
+
+(*
+ * If a given LF event e is outside a critical section, it cannot read
+ * internally but it may read from an LKW event in another thread.
+ * Compute the relation containing these possible edges.
+ *)
+let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext
+
+(* Compute set of sets of possible rfe edges for LF events *)
 let all-possible-rfe-lf =
 	(*
-	 * Given an LF event r, compute the possible rfe edges for that event
-	 * (all those starting from LKW events in other threads),
-	 * and then convert that relation to a set of single-edge relations.
+	 * Convert the possible-rfe-noncrit-lf relation for e
+	 * to a set of single edges
 	 *)
-	let possible-rfe-lf r =
-		let pair-to-relation p = p ++ 0
-		in map pair-to-relation ((LKW * {r}) & loc & ext)
-	(* Do this for each LF event r that isn't in rfi-lf *)
-	in map possible-rfe-lf (LF \ range(rfi-lf))
+	let set-of-singleton-rfe-lf e =
+			map pair-to-relation (possible-rfe-noncrit-lf e)
+	(* Do this for each LF event e that isn't in rfi-lf *)
+	in map set-of-singleton-rfe-lf (LF \ range(rfi-lf))
 
 (* Generate all rf relations for LF events *)
 with rfe-lf from cross(all-possible-rfe-lf)
 let rf-lf = rfe-lf | rfi-lf
 
 (*
- * RU, i.e., spin_is_locked() returning False, is slightly different.
- * We rely on the memory model to rule out cases where spin_is_locked()
- * within one of the lock's critical sections returns False.
+ * A given RU event e may read internally from the last po-previous UL,
+ * or it may read from a UL event in another thread or the initial write.
+ * Compute the relation containing these possible edges.
  *)
+let possible-rf-ru e = (((UL * {e}) & po-loc) \
+			([UL] ; po-loc ; [UL] ; po-loc)) |
+		(((UL | IW) * {e}) & loc & ext)
 
-(*
- * rf for RU events: an RU may read from an external UL or the initial write,
- * or from the last po-previous UL
- *)
+(* Compute set of sets of possible rf edges for RU events *)
 let all-possible-rf-ru =
-	let possible-rf-ru r =
-		let pair-to-relation p = p ++ 0
-		in map pair-to-relation ((((UL | IW) * {r}) & loc & ext) |
-			(((UL * {r}) & po-loc) \ ([UL] ; po-loc ; [LKW] ; po-loc)))
-	in map possible-rf-ru RU
+	(* Convert the possible-rf-ru relation for e to a set of single edges *)
+	let set-of-singleton-rf-ru e =
+		map pair-to-relation (possible-rf-ru e)
+	(* Do this for each RU event e *)
+	in map set-of-singleton-rf-ru RU
 
 (* Generate all rf relations for RU events *)
 with rf-ru from cross(all-possible-rf-ru)

Re: [PATCH 1/2] tools/memory-model: Fix bug in lock.cat

[Andrea Parri]

On Thu, Jun 06, 2024 at 09:57:55AM -0400, Alan Stern wrote:
> Andrea reported that the following innocuous litmus test:
> 
> C T
> 
> {}
> 
> P0(spinlock_t *x)
> {
> 	int r0;
> 
> 	spin_lock(x);
> 	spin_unlock(x);
> 	r0 = spin_is_locked(x);
> }
> 
> gives rise to a nonsensical empty result with no executions:
> 
> $ herd7 -conf linux-kernel.cfg T.litmus
> Test T Required
> States 0
> Ok
> Witnesses
> Positive: 0 Negative: 0
> Condition forall (true)
> Observation T Never 0 0
> Time T 0.00
> Hash=6fa204e139ddddf2cb6fa963bad117c0
> 
> The problem is caused by a bug in the lock.cat part of the LKMM.  Its
> computation of the rf relation for RU (read-unlocked) events is
> faulty; it implicitly assumes that every RU event must read from
> either a UL (unlock) event in another thread or from the lock's
> initial state.  Neither is true in the litmus test above, so the
> computation yields no possible executions.
> 
> The lock.cat code tries to make up for this deficiency by allowing RU
> events outside of critical sections to read from the last po-previous
> UL event.  But it does this incorrectly, trying to keep these rfi links
> separate from the rfe links that might also be needed, and passing only
> the latter to herd7's cross() macro.
> 
> The problem is fixed by merging the two sets of possible rf links for
> RU events and using them all in the call to cross().
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Reported-and-tested-by: Andrea Parri <parri.andrea@gmail.com>
> Closes: https://lore.kernel.org/linux-arch/ZlC0IkzpQdeGj+a3@andrea/
> Fixes: 15553dcbca06 ("tools/memory-model: Add model support for spin_is_locked()")

Acked-by: Andrea Parri <parri.andrea@gmail.com>

  Andrea

Re: [PATCH 2/2] tools/memory-model: Code reorganization in lock.cat

[Andrea Parri]

(... Reorganize code in lock.cat)

On Thu, Jun 06, 2024 at 09:59:01AM -0400, Alan Stern wrote:
> Code reorganization for the lock.cat file in tools/memory-model:
> 
> Improve the efficiency by ruling out right at the start RU events
> (spin_is_locked() calls that return False) inside a critical section
> for the same lock.
> 
> Improve the organization of the code for handling LF and RU events by
> pulling the definitions of the pair-to-relation macro out from two
> different complicated compound expressions, using a single standalone
> definition instead.
> 
> Rewrite the calculations of the rf relation for LF and RU events, for
> greater clarity.
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>

Tested-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>

  Andrea

Re: [PATCH 2/2] tools/memory-model: Code reorganization in lock.cat

[Paul E. McKenney]

On Thu, Jun 06, 2024 at 06:16:27PM +0200, Andrea Parri wrote:
> (... Reorganize code in lock.cat)
> 
> On Thu, Jun 06, 2024 at 09:59:01AM -0400, Alan Stern wrote:
> > Code reorganization for the lock.cat file in tools/memory-model:
> > 
> > Improve the efficiency by ruling out right at the start RU events
> > (spin_is_locked() calls that return False) inside a critical section
> > for the same lock.
> > 
> > Improve the organization of the code for handling LF and RU events by
> > pulling the definitions of the pair-to-relation macro out from two
> > different complicated compound expressions, using a single standalone
> > definition instead.
> > 
> > Rewrite the calculations of the rf relation for LF and RU events, for
> > greater clarity.
> > 
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> 
> Tested-by: Andrea Parri <parri.andrea@gmail.com>
> Acked-by: Andrea Parri <parri.andrea@gmail.com>

I queued them both, and thank you both!

							Thanx, Paul