Messages in this thread | | | Date | Wed, 18 Jan 2023 12:08:34 -0500 | From | Alan Stern <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
On Wed, Jan 18, 2023 at 08:59:55AM -0800, Boqun Feng wrote: > On Wed, Jan 18, 2023 at 11:03:35AM -0500, Alan Stern wrote: > > On Tue, Jan 17, 2023 at 09:17:04PM -0800, Paul E. McKenney wrote: > > > On Tue, Jan 17, 2023 at 09:15:15PM -0500, Alan Stern wrote: > > > > Maybe we don't. Please test the patch below; I think it will do what > > > > you want -- and it doesn't rule out nesting. > > > > > > It works like a champ on manual/kernel/C-srcu*.litmus in the litmus > > > repository on github, good show and thank you!!! > > > > > > I will make more tests, and am checking this against the rest of the > > > litmus tests in the repo, but in the meantime would you be willing to > > > have me add your Signed-off-by? > > > > I'll email a real patch submission in the not-too-distant future, > > assuming you don't find any problems with the new code. > > I haven't tested the following, but I think we also need it to avoid > (although rare) mixing srcu_struct with normal memory access? > > Since you are working on a patch, I think I better mention this ;-) > > Regards, > Boqun > > diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat > index 6b52f365d73a..c134c2027224 100644 > --- a/tools/memory-model/lock.cat > +++ b/tools/memory-model/lock.cat > @@ -37,7 +37,7 @@ let RU = try RU with emptyset > let LF = LF | RL > > (* There should be no ordinary R or W accesses to spinlocks *) > -let ALL-LOCKS = LKR | LKW | UL | LF | RU > +let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock > flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses > > (* Link Lock-Reads to their RMW-partner Lock-Writes *)
Great point! I'll at this to the patch, thanks.
Alan
| |