• Luc Maranget's avatar
    tools/memory-model: Dynamically check SRCU lock-to-unlock matching · dbb12fb0
    Luc Maranget authored
    This commit checks that the return value of srcu_read_lock() is passed
    to the matching srcu_read_unlock(), where "matching" is determined by
    nesting.  This check operates as follows:
    
       1. srcu_read_lock() creates an integer token, which is stored into
          the generated events.
       2. srcu_read_unlock() records its second (token) argument into the
          generated event.
       3. A new herd primitive 'different-values' filters out pairs of events
          with identical values from the relation passed as its argument.
       4. The bell file applies the above primitive to the (srcu)
          read-side-critical-section relation 'srcu-rscs' and flags non-empty
          results.
    
    BEWARE: Works only with herd version 7.51+6 and onwards.
    Signed-off-by: 's avatarLuc Maranget <Luc.Maranget@inria.fr>
    Signed-off-by: 's avatarPaul E. McKenney <paulmck@linux.ibm.com>
    [ paulmck: Apply Andrea Parri's off-list feedback. ]
    Acked-by: 's avatarAlan Stern <stern@rowland.harvard.edu>
    dbb12fb0
Name
Last commit
Last update
..
Documentation Loading commit data...
litmus-tests Loading commit data...
scripts Loading commit data...
.gitignore Loading commit data...
README Loading commit data...
linux-kernel.bell Loading commit data...
linux-kernel.cat Loading commit data...
linux-kernel.cfg Loading commit data...
linux-kernel.def Loading commit data...
lock.cat Loading commit data...