Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics

[Paul E. McKenney]

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
>