Messages in this thread Patch in this message | | | Date | Wed, 18 Jan 2023 08:59:55 -0800 | From | Boqun Feng <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
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 *) > > Alan
| |