Skip to content
  • Lance Roy's avatar
    rcutorture: Add CBMC-based formal verification for SRCU · 418b2977
    Lance Roy authored
    
    
    This commit creates a formal/srcu-cbmc directory containing scripts that
    pull SRCU in from the source code, filter it to remove things that CBMC
    cannot handle, and run a series of verifications on it.  This has a number
    of shortcomings:
    
    1.	It does not yet hook into the upper-level self-test Makefiles.
    2.	It tests only a single scenario, store buffering.
    3.	There is no gcc-based syntax-error prefiltering.
    
    Nevertheless, it does fully verify a piece of SRCU under a moderately
    weak memory model (PSO).
    
    Signed-off-by: default avatarLance Roy <ldr709@gmail.com>
    Signed-off-by: default avatarPaul E. McKenney <paulmck@linux.vnet.ibm.com>
    418b2977