1. 09 6月, 2017 9 次提交
  2. 08 6月, 2017 13 次提交
  3. 20 4月, 2017 1 次提交
    • P
      torture: Use correct path for Kconfig fragment for duplicates · 6bb7ff17
      Paul E. McKenney 提交于
      Currently, the rcutorture scripting will give an error message if
      running a duplicate scenario that happens also to have a non-existent
      build directory (b1, b2, ... in the rcutorture directory).  Worse yet, if
      the build directory has already been created and used for a real build,
      the script will silently grab the wrong Kconfig fragment, which could
      cause confusion to the poor sap (me) analyzing old test results.  At
      least the actual test runs correctly...
      
      This commit therefore accesses the Kconfig fragment from the results
      directory corresponding to the first of the duplicate scenarios, for
      which a build was actually carried out.  This prevents both the messages
      and at least one form of later confusion.
      Signed-off-by: NPaul E. McKenney <paulmck@linux.vnet.ibm.com>
      6bb7ff17
  4. 26 1月, 2017 1 次提交
    • L
      rcutorture: Add CBMC-based formal verification for SRCU · 418b2977
      Lance Roy 提交于
      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: NLance Roy <ldr709@gmail.com>
      Signed-off-by: NPaul E. McKenney <paulmck@linux.vnet.ibm.com>
      418b2977
  5. 15 1月, 2017 8 次提交
  6. 14 1月, 2017 1 次提交
  7. 15 11月, 2016 2 次提交
  8. 15 6月, 2016 5 次提交