• Alan Stern's avatar
    tools/memory-model: Add SRCU support · a3f600d9
    Alan Stern authored
    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: default avatarAlan Stern <stern@rowland.harvard.edu>
    CC: Luc Maranget <luc.maranget@inria.fr>
    Signed-off-by: default avatarPaul E. McKenney <paulmck@linux.ibm.com>
    Tested-by: default avatarAndrea Parri <andrea.parri@amarulasolutions.com>
    a3f600d9
linux-kernel.def 4.51 KB