12a02ff0add089fc1234ba78a6f1e48ef971a911
[c11tester.git] / README
1 ****************************************
2 CDSChecker Readme
3 ****************************************
4
5 This is an evaluation-only version of CDSChecker. Please do not distribute.
6
7 CDSChecker compiles as a dynamically-linked shared library by simply running
8 'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM
9 (clang/clang++) and GCC.
10
11 Test programs should use the standard C11/C++11 library headers
12 (<atomic>/<stdatomic.h>, <mutex>, <condition_variable>, <thread.h>) and must
13 name their main routine as user_main(int, char**) rather than main(int, char**).
14 We only support C11 thread syntax (thrd_t, etc. from <thread.h>).
15
16 Test programs may also use our included happens-before race detector by
17 including <librace.h> and utilizing the appropriate functions
18 (store_{8,16,32,64}() and load_{8,16,32,64}()) for loading/storing data from/to
19 from non-atomic shared memory.
20
21 Test programs should be compiled against our shared library (libmodel.so) using
22 the headers in the include/ directory. Then the shared library must be made
23 available to the dynamic linker, using the LD_LIBRARY_PATH environment
24 variable, for instance.
25
26 Sample run instructions:
27
28 $ make
29 $ export LD_LIBRARY_PATH=.
30 $ ./test/userprog.o                   # Runs simple test program
31 $ ./test/userprog.o -h                # Prints help information
32 Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]
33
34 Options:
35 -h                    Display this help message and exit
36 -m                    Maximum times a thread can read from the same write
37                       while other writes exist. Default: 0
38 -M                    Maximum number of future values that can be sent to
39                       the same read. Default: 0
40 -s                    Maximum actions that the model checker will wait for
41                       a write from the future past the expected number of
42                       actions. Default: 100
43 -S                    Future value expiration sloppiness. Default: 10
44 -f                    Specify a fairness window in which actions that are
45                       enabled sufficiently many times should receive
46                       priority for execution. Default: 0
47 -e                    Enabled count. Default: 1
48 -b                    Upper length bound. Default: 0
49 --                    Program arguments follow.
50
51
52 Note that we also provide a series of benchmarks (distributed separately),
53 which can be placed under the benchmarks/ directory. After building CDSChecker,
54 you can build and run the benchmarks as follows:
55
56   cd benchmarks
57   make
58   ./run.sh barrier/barrier -f 10 -m 2  # runs barrier test with fairness/memory liveness
59   ./bench.sh <dir>                     # run all benchmarks twice, with timing results; all logged to <dir>