ec10620166721e921b11a6dca286c27ca42f7e57
[cdsspec-compiler.git] / README.md
1 CDSChecker Readme
2 =================
3
4 Copyright © 2013 Regents of the University of California. All rights reserved.
5
6 CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
7
8 Overview
9 --------
10
11 CDSChecker is a model checker for C11/C++11 which exhaustively explores the
12 behaviors of code under the C/C++ memory model. It uses partial order reduction
13 as well as a few other novel techniques to eliminate time spent on redundant
14 execution behaviors and to significantly shrink the state space. The model
15 checking algorithm is described in more detail in this paper (published in
16 OOPSLA '13):
17
18   <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
19
20 It is designed to support unit tests on concurrent data structure written using
21 C/C++ atomics.
22
23 CDSChecker is constructed as a dynamically-linked shared library which
24 implements the C and C++ atomic types and portions of the other thread-support
25 libraries of C/C++ (e.g., std::atomic, std::mutex, etc.). Notably, we only
26 support the C version of threads (i.e., `thrd_t` and similar, from `<threads.h>`),
27 because C++ threads require features which are only available to a C++11
28 compiler (and we want to support others, at least for now).
29
30 CDSChecker should compile on Linux and Mac OSX with no dependencies and has been
31 tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX
32 flavors. We have not attempted to port to Windows.
33
34 You may also refer to the CDSChecker project page:
35
36   <http://demsky.eecs.uci.edu/c11modelchecker.php>
37
38 Getting Started
39 ---------------
40
41 If you haven't done so already, you may download CDSChecker using
42 [git](http://git-scm.com/):
43
44       git clone git://demsky.eecs.uci.edu/model-checker.git
45
46 Get the benchmarks (not required; distributed separately):
47
48       cd model-checker
49       git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks
50
51 Compile the model checker:
52
53       make
54
55 Compile the benchmarks:
56
57       make benchmarks
58
59 Run a simple example (the `run.sh` script does some very minimal processing for
60 you):
61
62       ./run.sh test/userprog.o
63
64 To see the help message on how to run CDSChecker, execute:
65
66       ./run.sh -h
67
68 Useful Options
69 --------------
70
71 `-m num`
72
73   > Controls the liveness of the memory system. Note that multithreaded programs
74   > often rely on memory liveness for termination, so this parameter is
75   > necessary for such programs.
76   >
77   > Liveness is controlled by `num`: the number of times a load is allowed to
78   > see the same store when a newer store exists---one that is ordered later in
79   > the modification order.
80
81 `-y`
82
83   > Turns on CHESS-like yield-based fairness support (requires `thrd_yield()`
84   > instrumentation in test program).
85
86 `-f num`
87
88   > Turns on alternative fairness support (less desirable than `-y`).
89
90 `-v`
91
92   > Verbose: show all executions and not just buggy ones.
93
94 `-s num`
95
96   > Constrain how long we will run to wait for a future value past when it is
97   > expected
98
99 `-u num`
100
101   > Value to provide to atomics loads from uninitialized memory locations. The
102   > default is 0, but this may cause some programs to throw exceptions
103   > (segfault) before the model checker prints a trace.
104
105 Suggested options:
106
107 >     -m 2 -y
108
109 or
110
111 >     -m 2 -f 10
112
113 Benchmarks
114 -------------------
115
116 Many simple tests are located in the `tests/` directory. You may also want to
117 try the larger benchmarks (distributed separately), which can be placed under
118 the `benchmarks/` directory. After building CDSChecker, you can build and run
119 the benchmarks as follows:
120
121 >     make benchmarks
122 >     cd benchmarks
123 >     ./run.sh barrier/barrier -y -m 2     # runs barrier test with fairness/memory liveness
124 >     ./bench.sh                           # run all benchmarks and provide timing results
125
126 Running your own code
127 ---------------------
128
129 You likely want to test your own code, not just our simple tests. To do so, you
130 need to perform a few steps.
131
132 First, because CDSChecker executes your program dozens (if not hundreds or
133 thousands) of times, you will have the most success if your code is written as a
134 unit test and not as a full-blown program.
135
136 Second, because CDSChecker must be able to manage your program for you, your
137 program should declare its main entry point as `user_main(int, char**)` rather
138 than `main(int, char**)`.
139
140 Third, test programs should use the standard C11/C++11 library headers
141 (`<atomic>`/`<stdatomic.h>`, `<mutex>`, `<condition_variable>`, `<thread.h>`).
142 As of now, we only support C11 thread syntax (`thrd_t`, etc. from
143 `<thread.h>`).
144
145 Test programs may also use our included happens-before race detector by
146 including <librace.h> and utilizing the appropriate functions
147 (`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for loading/storing data from/to
148 non-atomic shared memory.
149
150 CDSChecker can also check boolean assertions in your test programs. Just
151 include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
152 CDSChecker will report a bug in any possible execution in which the argument to
153 `MODEL_ASSERT()` evaluates to false (that is, 0).
154
155 Test programs should be compiled against our shared library (libmodel.so) using
156 the headers in the `include/` directory. Then the shared library must be made
157 available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
158 variable, for instance.
159
160 Reading an execution trace
161 --------------------------
162
163 When CDSChecker detects a bug in your program (or when run with the `--verbose`
164 flag), it prints the output of the program run (STDOUT) along with some summary
165 trace information for the execution in question. The trace is given as a
166 sequence of lines, where each line represents an operation in the execution
167 trace. These lines are ordered by the order in which they were run by CDSChecker
168 (i.e., the "execution order"), which does not necessarily align with the "order"
169 of the values observed (i.e., the modification order or the reads-from
170 relation).
171
172 The following list describes each of the columns in the execution trace output:
173
174  * \#: The sequence number within the execution. That is, sequence number "9"
175    means the operation was the 9th operation executed by CDSChecker. Note that
176    this represents the execution order, not necessarily any other order (e.g.,
177    modification order or reads-from).
178
179  * t: The thread number
180
181  * Action type: The type of operation performed
182
183  * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
184    `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
185
186  * Location: The memory location on which this operation is operating. This is
187    well-defined for atomic write/read/RMW, but other operations are subject to
188    CDSChecker implementation details.
189
190  * Value: For reads/writes/RMW, the value returned by the operation. Note that
191    for RMW, this is the value that is *read*, not the value that was *written*.
192    For other operations, 'value' may have some CDSChecker-internal meaning, or
193    it may simply be a don't-care (such as `0xdeadbeef`).
194
195  * Rf: For reads, the sequence number of the operation from which it reads.
196    [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
197    as printed during `--verbose` execution, reads may not be resolved and so may
198    have Rf=? or Rf=Px, where x is a promised future value.]
199
200  * CV: The clock vector, encapsulating the happens-before relation (see our
201    paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
202    similar to [1]. The "clock" is just the sequence number (#). The clock vector
203    can be read as follows:
204
205    Each entry is indexed as CV[i], where
206
207             i = 0, 1, 2, ..., <number of threads>
208
209    So for any thread i, we say CV[i] is the sequence number of the most recent
210    operation in thread i such that operation i happens-before this operation.
211    Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
212    operations.
213
214 See the following example trace:
215
216 <pre>
217 ------------------------------------------------------------------------------------
218 #    t    Action type     MO       Location         Value               Rf  CV
219 ------------------------------------------------------------------------------------
220 1    1    thread start    seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0,  1)
221 2    1    init atomic     relaxed        0x601068   0                       ( 0,  2)
222 3    1    init atomic     relaxed        0x60106c   0                       ( 0,  3)
223 4    1    thread create   seq_cst  0x7f68fe51c710   0x7f68fe51c6e0          ( 0,  4)
224 5    2    thread start    seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4,  5)
225 6    2    atomic read     relaxed        0x60106c   0                   3   ( 0,  4,  6)
226 7    1    thread create   seq_cst  0x7f68fe51c720   0x7f68fe51c6e0          ( 0,  7)
227 8    3    thread start    seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0,  8)
228 9    2    atomic write    relaxed        0x601068   0                       ( 0,  4,  9)
229 10   3    atomic read     relaxed        0x601068   0                   2   ( 0,  7,  0, 10)
230 11   2    thread finish   seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4, 11)
231 12   3    atomic write    relaxed        0x60106c   0x2a                    ( 0,  7,  0, 12)
232 13   1    thread join     seq_cst  0x7f68ff11ebc0   0x2                     ( 0, 13, 11)
233 14   3    thread finish   seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0, 14)
234 15   1    thread join     seq_cst  0x7f68ff11efc0   0x3                     ( 0, 15, 11, 14)
235 16   1    thread finish   seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0, 16, 11, 14)
236 HASH 4073708854
237 ------------------------------------------------------------------------------------
238 </pre>
239
240 Now consider, for example, operation 10:
241
242 This is the 10th operation in the execution order. It is an atomic read-relaxed
243 operation performed by thread 3 at memory address `0x601068`. It reads the value
244 "0", which was written by the 2nd operation in the execution order. Its clock
245 vector consists of the following values:
246
247         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
248
249
250 Other Notes
251 -----------
252
253 * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
254   following test program.
255
256   >     ./run.sh test/deadlock.o
257
258   Deadlock detection currently detects when a thread is about to step into a
259   deadlock, without actually including the final step in the trace. But you can
260   examine the program to see the next step.
261
262 * CDSChecker has to speculatively explore many execution behaviors due to the
263   relaxed memory model, and many of these turn out to be infeasible (that is,
264   they cannot be legally produced by the memory model). CDSChecker discards
265   these executions as soon as it identifies them (see the "Number of infeasible
266   executions" statistic); however, the speculation can occasionally cause
267   CDSChecker to hit unexpected parts of the unit test program (causing a
268   division by 0, for instance). In such programs, you might consider running
269   CDSChecker with the `-u num` option.
270
271
272 Contact
273 -------
274
275 Please feel free to contact us for more information. Bug reports are welcome,
276 and we are happy to hear from our users. We are also very interested to know if
277 CDSChecker catches bugs in your programs.
278
279 Contact Brian Norris at <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
280
281
282 References
283 ----------
284
285 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
286     system. CACM, 21(7):558-565, July 1978.