name mode size
doc 040000
include 040000
test 040000
.dir-locals.el 100644 0 kb
.gitignore 100644 0 kb
DEBUGGINGNOTES.txt 100644 0 kb
Doxyfile 100644 75 kb
Makefile 100644 2 kb
README 100644 3 kb
action.cc 100644 12 kb
action.h 100644 5 kb
clockvector.cc 100644 3 kb
clockvector.h 100644 1 kb
cmodelint.cc 100644 1 kb
common.cc 100644 1 kb
common.h 100644 1 kb
common.mk 100644 0 kb
conditionvariable.cc 100644 1 kb
config.h 100644 1 kb
cyclegraph.cc 100644 8 kb
cyclegraph.h 100644 2 kb
datarace.cc 100644 11 kb
datarace.h 100644 2 kb
hashtable.h 100644 8 kb
impatomic.cc 100644 1 kb
librace.cc 100644 3 kb
libthreads.cc 100644 1 kb
main.cc 100644 4 kb
malloc.c 100644 215 kb
model.cc 100644 69 kb
model.h 100644 8 kb
mutex.cc 100644 1 kb
mymemory.cc 100644 5 kb
mymemory.h 100644 7 kb
nodestack.cc 100644 14 kb
nodestack.h 100644 5 kb
promise.cc 100644 1 kb
promise.h 100644 1 kb
run.sh 100755 0 kb
schedule.cc 100644 5 kb
schedule.h 100644 1 kb
snapshot-interface.cc 100644 4 kb
snapshot-interface.h 100644 1 kb
snapshot.cc 100644 13 kb
snapshot.h 100644 0 kb
snapshotimp.h 100644 2 kb
stacktrace.h 100644 2 kb
threads-model.h 100644 4 kb
threads.cc 100644 4 kb
workqueue.h 100644 3 kb
README
**************************************** CDSChecker Readme **************************************** This is an evaluation-only version of CDSChecker. Please do not distribute. 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 (<atomic>/<stdatomic.h>, <mutex>, <condition_variable>, <thread.h>) 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 <thread.h>). Test programs may also use our included happens-before race detector by including <librace.h> 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 Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS] Options: -h Display this help message and exit -m Maximum times a thread can read from the same write while other writes exist. Default: 0 -M Maximum number of future values that can be sent to the same read. Default: 0 -s Maximum actions that the model checker will wait for a write from the future past the expected number of actions. Default: 100 -S Future value expiration sloppiness. Default: 10 -f Specify a fairness window in which actions that are enabled sufficiently many times should receive priority for execution. Default: 0 -e Enabled count. Default: 1 -b Upper length bound. Default: 0 -- Program arguments follow. Note that we also provide a series of benchmarks, placed under the benchmarks/ directory. After building CDSChecker, you can build and run the benchmarks as follows: cd benchmarks make ./run.sh barrier/barrier -f 10 -m 2 # runs barrier test with fairness/memory liveness ./bench.sh <dir> # run all benchmarks twice, with timing results; all logged to <dir>