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 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
38 Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
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.
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.
48 -M, --maxfv=NUM Maximum number of future values that can be sent to
51 -s, --maxfvdelay=NUM Maximum actions that the model checker will wait for
52 a write from the future past the expected number
55 -S, --fvslop=NUM Future value expiration sloppiness.
57 -y, --yield Enable CHESS-like yield-based fairness support.
59 -Y, --yieldblock Prohibit an execution from running a yield.
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).
65 -e, --enabled=COUNT Enabled count.
67 -b, --bound=MAX Upper length bound.
69 -v, --verbose Print verbose execution information.
70 -u, --uninitialized=VALUE Return VALUE any load which may read from an
73 -c, --analysis Use SC Trace Analysis.
74 -- Program arguments follow.
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:
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