**************************************** CDSChecker Readme **************************************** Copyright (c) 2013 Regents of the University of California. All rights reserved. CDSChecker is distributed under the GPL v2. CDSChecker compiles as a dynamically-linked shared library by simply running 'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM (clang/clang++) and GCC. Test programs should use the standard C11/C++11 library headers (/, , , ) and must name their main routine as user_main(int, char**) rather than main(int, char**). We only support C11 thread syntax (thrd_t, etc. from ). Test programs may also use our included happens-before race detector by including and utilizing the appropriate functions (store_{8,16,32,64}() and load_{8,16,32,64}()) for loading/storing data from/to from non-atomic shared memory. Test programs should be compiled against our shared library (libmodel.so) using the headers in the include/ directory. Then the shared library must be made available to the dynamic linker, using the LD_LIBRARY_PATH environment variable, for instance. Sample run instructions: $ make $ export LD_LIBRARY_PATH=. $ ./test/userprog.o # Runs simple test program $ ./test/userprog.o -h # Prints help information Copyright (c) 2013 Regents of the University of California. All rights reserved. Distributed under the GPLv2 Written by Brian Norris and Brian Demsky Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS] MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments provided after the `--' (the PROGRAM ARGS) are passed to the user program. Model-checker options: -h, --help Display this help message and exit -m, --liveness=NUM Maximum times a thread can read from the same write while other writes exist. Default: 0 -M, --maxfv=NUM Maximum number of future values that can be sent to the same read. Default: 0 -s, --maxfvdelay=NUM Maximum actions that the model checker will wait for a write from the future past the expected number of actions. Default: 6 -S, --fvslop=NUM Future value expiration sloppiness. Default: 4 -y, --yield Enable CHESS-like yield-based fairness support. Default: disabled -Y, --yieldblock Prohibit an execution from running a yield. Default: disabled -f, --fairness=WINDOW Specify a fairness window in which actions that are enabled sufficiently many times should receive priority for execution (not recommended). Default: 0 -e, --enabled=COUNT Enabled count. Default: 1 -b, --bound=MAX Upper length bound. Default: 0 -v, --verbose Print verbose execution information. -u, --uninitialized=VALUE Return VALUE any load which may read from an uninitialized atomic. Default: 0 -c, --analysis Use SC Trace Analysis. -- Program arguments follow. Note that we also provide a series of benchmarks (distributed separately), which can be placed under the benchmarks/ directory. After building CDSChecker, you can build and run the benchmarks as follows: cd benchmarks make ./run.sh barrier/barrier -y -m 2 # runs barrier test with fairness/memory liveness ./bench.sh # run all benchmarks twice, with timing results