Messages in this thread | ![/](/images/icornerl.gif) | | Date | Wed, 25 Jan 2023 13:58:18 -0800 | From | "Paul E. McKenney" <> | Subject | Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics |
| |
On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote: > On 1/25/2023 9:21 PM, Alan Stern wrote: > > LKMM has long provided only approximate handling of SRCU read-side > > critical sections. This has not been a pressing problem because LKMM's > > traditional handling is correct for the common cases of non-overlapping > > and properly nested critical sections. However, LKMM's traditional > > handling of partially overlapping critical sections incorrectly fuses > > them into one large critical section.
[ . . . ]
> > synchronize_srcu(X) { __srcu{sync-srcu}(X); } > > synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); } > > Index: usb-devel/tools/memory-model/lock.cat > > =================================================================== > > --- usb-devel.orig/tools/memory-model/lock.cat > > +++ usb-devel/tools/memory-model/lock.cat > > @@ -36,9 +36,9 @@ let RU = try RU with emptyset > > (* Treat RL as a kind of LF: a read with no ordering properties *) > > let LF = LF | RL > > -(* There should be no ordinary R or W accesses to spinlocks *) > > -let ALL-LOCKS = LKR | LKW | UL | LF | RU > > -flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses > > +(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *) > > +let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu > > +flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses > > Since this was pointed out by Boqun, would it be appropriate to mention him > in the patch somehow?
Would you be willing to list who contributed what? Once you and Alan come to agreement on the list, I would be happy to wordsmith a version into the commit log.
Thanx, Paul
> > (* Link Lock-Reads to their RMW-partner Lock-Writes *) > > let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) > > Thanks for your patience, > jonas >
| ![\](/images/icornerr.gif) |