Skip to content
  • 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: default avatarLuc Maranget <Luc.Maranget@inria.fr>
    Signed-off-by: default avatarPaul E. McKenney <paulmck@linux.ibm.com>
    [ paulmck: Apply Andrea Parri's off-list feedback. ]
    Acked-by: default avatarAlan Stern <stern@rowland.harvard.edu>
    dbb12fb0