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 Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]
  35
  36 Options:
  37 -h                    Display this help message and exit
  38 -m                    Maximum times a thread can read from the same write
  39                       while other writes exist. Default: 0
  40 -M                    Maximum number of future values that can be sent to
  41                       the same read. Default: 0
  42 -s                    Maximum actions that the model checker will wait for
  43                       a write from the future past the expected number of
  44                       actions. Default: 100
  45 -S                    Future value expiration sloppiness. Default: 10
  46 -f                    Specify a fairness window in which actions that are
  47                       enabled sufficiently many times should receive
  48                       priority for execution. Default: 0
  49 -e                    Enabled count. Default: 1
  50 -b                    Upper length bound. Default: 0
  51 -v                    Print verbose execution information.
  52 -y                    CHESS like yield based fairness. Default: 0
  53 --                    Program arguments follow.
  54
  55
  56 Note that we also provide a series of benchmarks (distributed separately),
  57 which can be placed under the benchmarks/ directory. After building CDSChecker,
  58 you can build and run the benchmarks as follows:
  59
  60   cd benchmarks
  61   make
  62   ./run.sh barrier/barrier -f 10 -m 2  # runs barrier test with fairness/memory liveness
  63   ./bench.sh <dir>                     # run all benchmarks twice, with timing results; all logged to <dir>