README

   1 ****************************************
   2 CDSChecker Readme
   3 ****************************************
   4
   5 Copyright (c) 2013 Regents of the University of California. All rights reserved.
   6
   7 CDSChecker is distributed under the GPL v2.
   8
   9 CDSChecker compiles as a dynamically-linked shared library by simply running
  10 'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM
  11 (clang/clang++) and GCC.
  12
  13 Test programs should use the standard C11/C++11 library headers
  14 (<atomic>/<stdatomic.h>, <mutex>, <condition_variable>, <thread.h>) and must
  15 name their main routine as user_main(int, char**) rather than main(int, char**).
  16 We only support C11 thread syntax (thrd_t, etc. from <thread.h>).
  17
  18 Test programs may also use our included happens-before race detector by
  19 including <librace.h> and utilizing the appropriate functions
  20 (store_{8,16,32,64}() and load_{8,16,32,64}()) for loading/storing data from/to
  21 from non-atomic shared memory.
  22
  23 Test programs should be compiled against our shared library (libmodel.so) using
  24 the headers in the include/ directory. Then the shared library must be made
  25 available to the dynamic linker, using the LD_LIBRARY_PATH environment
  26 variable, for instance.
  27
  28 Sample run instructions:
  29
  30 $ make
  31 $ export LD_LIBRARY_PATH=.
  32 $ ./test/userprog.o                   # Runs simple test program
  33 $ ./test/userprog.o -h                # Prints help information
  34 Copyright (c) 2013 Regents of the University of California. All rights reserved.
  35 Distributed under the GPLv2
  36 Written by Brian Norris and Brian Demsky
  37
  38 Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
  39
  40 MODLE-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments
  41 provided after the `--' (the PROGRAM ARGS) are passed to the user program.
  42
  43 Model-checker options:
  44 -h, --help                  Display this help message and exit
  45 -m, --liveness=NUM          Maximum times a thread can read from the same write
  46                               while other writes exist.
  47                               Default: 0
  48 -M, --maxfv=NUM             Maximum number of future values that can be sent to
  49                               the same read.
  50                               Default: 0
  51 -s, --maxfvdelay=NUM        Maximum actions that the model checker will wait for
  52                               a write from the future past the expected number
  53                               of actions.
  54                               Default: 6
  55 -S, --fvslop=NUM            Future value expiration sloppiness.
  56                               Default: 4
  57 -y, --yield                 Enable CHESS-like yield-based fairness support.
  58                               Default: disabled
  59 -Y, --yieldblock            Prohibit an execution from running a yield.
  60                               Default: disabled
  61 -f, --fairness=WINDOW       Specify a fairness window in which actions that are
  62                               enabled sufficiently many times should receive
  63                               priority for execution (not recommended).
  64                               Default: 0
  65 -e, --enabled=COUNT         Enabled count.
  66                               Default: 1
  67 -b, --bound=MAX             Upper length bound.
  68                               Default: 0
  69 -v, --verbose               Print verbose execution information.
  70 -u, --uninitialized=VALUE   Return VALUE any load which may read from an
  71                               uninitialized atomic.
  72                               Default: 0
  73 -c, --analysis              Use SC Trace Analysis.
  74  --                         Program arguments follow.
  75
  76
  77 Note that we also provide a series of benchmarks (distributed separately),
  78 which can be placed under the benchmarks/ directory. After building CDSChecker,
  79 you can build and run the benchmarks as follows:
  80
  81   cd benchmarks
  82   make
  83   ./run.sh barrier/barrier -y -m 2     # runs barrier test with fairness/memory liveness
  84   ./bench.sh                           # run all benchmarks twice, with timing results