typos
[cdsspec-compiler.git] / README
1 ****************************************
2 CDSChecker Readme
3 ****************************************
4
5 Copyright (c) 2013 Regents of the University of California. All rights reserved.
6
7 CDSChecker is distributed under the GPL v2.
8
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.
12
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>).
17
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.
22
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.
27
28 Sample run instructions:
29
30 $ make
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
37
38 Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
39
40 MODEL-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.
42
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.
47                               Default: 0
48 -M, --maxfv=NUM             Maximum number of future values that can be sent to
49                               the same read.
50                               Default: 0
51 -s, --maxfvdelay=NUM        Maximum actions that the model checker will wait for
52                               a write from the future past the expected number
53                               of actions.
54                               Default: 6
55 -S, --fvslop=NUM            Future value expiration sloppiness.
56                               Default: 4
57 -y, --yield                 Enable CHESS-like yield-based fairness support.
58                               Default: disabled
59 -Y, --yieldblock            Prohibit an execution from running a yield.
60                               Default: disabled
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).
64                               Default: 0
65 -e, --enabled=COUNT         Enabled count.
66                               Default: 1
67 -b, --bound=MAX             Upper length bound.
68                               Default: 0
69 -v, --verbose               Print verbose execution information.
70 -u, --uninitialized=VALUE   Return VALUE any load which may read from an
71                               uninitialized atomic.
72                               Default: 0
73 -c, --analysis              Use SC Trace Analysis.
74  --                         Program arguments follow.
75
76
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:
80
81   cd benchmarks
82   make
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