On Sat, Feb 04, 2023 at 02:24:11PM -0800, Paul E. McKenney wrote:
> On Sat, Feb 04, 2023 at 09:58:12AM -0500, Alan Stern wrote:
> > On Fri, Feb 03, 2023 at 05:49:41PM -0800, Paul E. McKenney wrote:
> > > On Fri, Feb 03, 2023 at 08:28:35PM -0500, Alan Stern wrote:
> > > > On Fri, Feb 03, 2023 at 04:48:43PM -0800, Paul E. McKenney wrote:
> > > > > Hello!
> > > > >
> > > > > Here is what I currently have for LKMM patches:
> > > > >
> > > > > 289e1c89217d4 ("locking/memory-barriers.txt: Improve documentation for writel() example")
> > > > > ebd50e2947de9 ("tools: memory-model: Add rmw-sequences to the LKMM")
> > > > > aae0c8a50d6d3 ("Documentation: Fixed a typo in atomic_t.txt")
> > > > > 9ba7d3b3b826e ("tools: memory-model: Make plain accesses carry dependencies")
> > > > >
> > > > > Queued for the upcoming (v6.3) merge window.
> > > > >
> > > > > c7637e2a8a27 ("tools/memory-model: Update some warning labels")
> > > > > 7862199d4df2 ("tools/memory-model: Unify UNLOCK+LOCK pairings to po-unlock-lock-")
> > > > >
> > > > > Are ready for the next (v6.4) merge window. If there is some
> > > > > reason that they should instead go into v6.3, please let us
> > > > > all know.
> > > > >
> > > > > a6cd5214b5ba ("tools/memory-model: Document LKMM test procedure")
> > > > >
> > > > > This goes onto the lkmm-dev pile because it is documenting how
> > > > > to use those scripts.
> > > > >
> > > > > https://lore.kernel.org/lkml/Y9GPVnK6lQbY6vCK@xxxxxxxxxxxxxxxxxxx/
> > > > > https://lore.kernel.org/lkml/20230126134604.2160-3-jonas.oberhauser@xxxxxxxxxxxxxxx
> > > > > https://lore.kernel.org/lkml/20230203201913.2555494-1-joel@xxxxxxxxxxxxxxxxx/
> > > > > 5d871b280e7f ("tools/memory-model: Add smp_mb__after_srcu_read_unlock()")
> > > > >
> > > > > These need review and perhaps further adjustment.
> > > > >
> > > > > So, am I missing any? Are there any that need to be redirected?
> > > >
> > > > The "Provide exact semantics for SRCU" patch should have:
> > > >
> > > > Portions suggested by Boqun Feng and Jonas Oberhauser.
> > > >
> > > > added at the end, together with your Reported-by: tag. With that, I
> > > > think it can be queued for 6.4.
> > >
> > > Thank you! Does the patch shown below work for you?
> > >
> > > (I have tentatively queued this, but can easily adjust or replace it.)
> >
> > It looks fine.
>
> Very good, thank you for looking it over! I pushed it out on branch
> stern.2023.02.04a.
>
> Would anyone like to ack/review/whatever this one?
Would it be possible to add comments, something like the following? Apologies
if it is missing some ideas. I will try to improve it later.
thanks!
- Joel
---8<-----------------------
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index ce068700939c..0a16177339bc 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -57,7 +57,23 @@ let rcu-rscs = let rec
flag ~empty Rcu-lock \ domain(rcu-rscs) as unmatched-rcu-lock
flag ~empty Rcu-unlock \ range(rcu-rscs) as unmatched-rcu-unlock
+(***************************************************************)
(* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
+(***************************************************************)
+(*
+ * carry-srcu-data: To handle the case of the SRCU critical section split
+ * across CPUs, where the idx is used to communicate the SRCU index across CPUs
+ * (say CPU0 and CPU1), data is between the R[srcu-lock] to W[once][idx] on
+ * CPU0, which is sequenced with the ->rf is between the W[once][idx] and the
+ * R[once][idx] on CPU1. The carry-srcu-data is made to exclude Srcu-unlock
+ * events to prevent capturing accesses across back-to-back SRCU read-side
+ * critical sections.
+ *
+ * srcu-rscs: Putting everything together, the carry-srcu-data is sequenced with
+ * a data relation, which is the data dependency between R[once][idx] on CPU1
+ * and the srcu-unlock store, and loc ensures the relation is unique for a
+ * specific lock.
+ *)
let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*
let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc
