1 ****************************************
3 ****************************************
5 Copyright (c) 2013 Regents of the University of California. All rights reserved.
7 CDSChecker is distributed under the GPL v2.
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.
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>).
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.
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.
28 Sample run instructions:
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]
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
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.
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:
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>