Add SRCU support to the LKMM
On Tue, 13 Nov 2018, Paul E. McKenney wrote:
> But on -rcu, I get the following:
>
> $ git am -s /tmp/stern.patch
> Applying: rename some RCU relations
> Applying: Refactor some RCU definitions
> Applying: Add SRCU support to the LKMM
> error: patch failed: tools/memory-model/linux-kernel.bell:32
> error: tools/memory-model/linux-kernel.bell: patch does not apply
> error: patch failed: tools/memory-model/linux-kernel.cat:31
> error: tools/memory-model/linux-kernel.cat: patch does not apply
> Patch failed at 0003 Add SRCU support to the LKMM
> Use 'git am --show-current-patch' to see the failed patch
> When you have resolved this problem, run "git am --continue".
> If you prefer to skip this patch, run "git am --skip" instead.
> To restore the original branch and stop patching, run "git am --abort".
Here's the updated patch.
Alan
--------------------------------------------------------------------------
Add support for SRCU. Herd creates srcu events and linux-kernel.def
associates them with three possible annotations (srcu-lock,
srcu-unlock, and sync-srcu) corresponding to the API routines
srcu_read_lock(), srcu_read_unlock(), and synchronize_srcu().
The linux-kernel.bell file now declares the annotations
and determines matching lock/unlock pairs delimiting SRCU read-side
critical sections, and it also checks for synchronize_srcu() calls
inside an RCU critical section (which would generate a "sleeping in
atomic context" error in real kernel code). The linux-kernel.cat file
now adds SRCU-induced ordering, analogous to the existing RCU-induced
ordering, to the gp and rcu-fence relations.
Curiously enough, these small changes to the model's .cat code are all
that is needed to describe SRCU.
Portions of this patch (linux-kernel.def and the first hunk in
linux-kernel.bell) were written by Luc Maranget.
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
CC: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
3 files changed
