de8c3ef5c18699cf6d1b499b32c16c38ac920c5c
[c11tester.git] / README.md
1 CDSChecker: A Model Checker for C11 and C++11 Atomics
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
9 Overview
10 --------
11
12 CDSChecker is a model checker for C11/C++11 which exhaustively explores the
13 behaviors of code under the C/C++ memory model. It uses partial order reduction
14 as well as a few other novel techniques to eliminate time spent on redundant
15 execution behaviors and to significantly shrink the state space. The model
16 checking algorithm is described in more detail in this paper (published in
17 OOPSLA '13):
18
19 >   <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
20
21 It is designed to support unit tests on concurrent data structure written using
22 C/C++ atomics.
23
24 CDSChecker is constructed as a dynamically-linked shared library which
25 implements the C and C++ atomic types and portions of the other thread-support
26 libraries of C/C++ (e.g., std::atomic, std::mutex, etc.). Notably, we only
27 support the C version of threads (i.e., `thrd_t` and similar, from `<threads.h>`),
28 because C++ threads require features which are only available to a C++11
29 compiler (and we want to support others, at least for now).
30
31 CDSChecker should compile on Linux and Mac OSX with no dependencies and has been
32 tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX
33 flavors. We have not attempted to port to Windows.
34
35
36 Getting Started
37 ---------------
38
39 If you haven't done so already, you may download CDSChecker using
40 [git](http://git-scm.com/) (for those without git, snapshots can be found at the
41 Gitweb URLs below):
42
43       git clone git://demsky.eecs.uci.edu/model-checker.git
44
45 Get the benchmarks (not required; distributed separately):
46
47       cd model-checker
48       git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks
49
50 Compile the model checker:
51
52       make
53
54 Compile the benchmarks:
55
56       make benchmarks
57
58 Run a simple example (the `run.sh` script does some very minimal processing for
59 you):
60
61       ./run.sh test/userprog.o
62
63 To see the help message on how to run CDSChecker, execute:
64
65       ./run.sh -h
66
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
114 Benchmarks
115 -------------------
116
117 Many simple tests are located in the `tests/` directory. You may also want to
118 try the larger benchmarks (distributed separately), which can be placed under
119 the `benchmarks/` directory. After building CDSChecker, you can build and run
120 the benchmarks as follows:
121
122 >     make benchmarks
123 >     cd benchmarks
124 >
125 >     # run barrier test with fairness/memory liveness
126 >     ./run.sh barrier/barrier -y -m 2
127 >
128 >     # Linux reader/write lock test with fairness/memory liveness
129 >     ./run.sh linuxrwlocks/linuxrwlocks -y -m 2
130 >
131 >     # run all benchmarks and provide timing results
132 >     ./bench.sh
133
134
135 Running your own code
136 ---------------------
137
138 You likely want to test your own code, not just our simple tests. To do so, you
139 need to perform a few steps.
140
141 First, because CDSChecker executes your program dozens (if not hundreds or
142 thousands) of times, you will have the most success if your code is written as a
143 unit test and not as a full-blown program.
144
145 Second, because CDSChecker must be able to manage your program for you, your
146 program should declare its main entry point as `user_main(int, char**)` rather
147 than `main(int, char**)`.
148
149 Third, test programs must use the standard C11/C++11 library headers (see below
150 for supported APIs) and must compile against the versions provided in
151 CDSChecker's `include/` directory. Notably, we only support C11 thread syntax
152 (`thrd_t`, etc. from `<thread.h>`).
153
154 Test programs may also use our included happens-before race detector by
155 including <librace.h> and utilizing the appropriate functions
156 (`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for storing/loading data
157 to/from non-atomic shared memory.
158
159 CDSChecker can also check boolean assertions in your test programs. Just
160 include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
161 CDSChecker will report a bug in any possible execution in which the argument to
162 `MODEL_ASSERT()` evaluates to false (that is, 0).
163
164 Test programs should be compiled against our shared library (libmodel.so) using
165 the headers in the `include/` directory. Then the shared library must be made
166 available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
167 variable, for instance.
168
169
170 ### Supported C11/C++11 APIs ###
171
172 To model-check multithreaded code properly, CDSChecker needs to instrument any
173 concurrency-related API calls made in your code. Currently, we support parts of
174 the following thread-support libraries. The C versions can be used in either C
175 or C++.
176
177 * `<atomic>`, `<cstdatomic>`, `<stdatomic.h>`
178 * `<condition_variable>`
179 * `<mutex>`
180 * `<threads.h>`
181
182 Because we want to extend support to legacy (i.e., non-C++11) compilers, we do
183 not support some new C++11 features that can't be implemented in C++03 (e.g.,
184 C++ `<thread>`).
185
186 Reading an execution trace
187 --------------------------
188
189 When CDSChecker detects a bug in your program (or when run with the `--verbose`
190 flag), it prints the output of the program run (STDOUT) along with some summary
191 trace information for the execution in question. The trace is given as a
192 sequence of lines, where each line represents an operation in the execution
193 trace. These lines are ordered by the order in which they were run by CDSChecker
194 (i.e., the "execution order"), which does not necessarily align with the "order"
195 of the values observed (i.e., the modification order or the reads-from
196 relation).
197
198 The following list describes each of the columns in the execution trace output:
199
200  * \#: The sequence number within the execution. That is, sequence number "9"
201    means the operation was the 9th operation executed by CDSChecker. Note that
202    this represents the execution order, not necessarily any other order (e.g.,
203    modification order or reads-from).
204
205  * t: The thread number
206
207  * Action type: The type of operation performed
208
209  * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
210    `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
211
212  * Location: The memory location on which this operation is operating. This is
213    well-defined for atomic write/read/RMW, but other operations are subject to
214    CDSChecker implementation details.
215
216  * Value: For reads/writes/RMW, the value returned by the operation. Note that
217    for RMW, this is the value that is *read*, not the value that was *written*.
218    For other operations, 'value' may have some CDSChecker-internal meaning, or
219    it may simply be a don't-care (such as `0xdeadbeef`).
220
221  * Rf: For reads, the sequence number of the operation from which it reads.
222    [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
223    as printed during `--verbose` execution, reads may not be resolved and so may
224    have Rf=? or Rf=Px, where x is a promised future value.]
225
226  * CV: The clock vector, encapsulating the happens-before relation (see our
227    paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
228    similar to [1]. The "clock" is just the sequence number (#). The clock vector
229    can be read as follows:
230
231    Each entry is indexed as CV[i], where
232
233             i = 0, 1, 2, ..., <number of threads>
234
235    So for any thread i, we say CV[i] is the sequence number of the most recent
236    operation in thread i such that operation i happens-before this operation.
237    Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
238    operations.
239
240 See the following example trace:
241
242 <pre>
243 ------------------------------------------------------------------------------------
244 #    t    Action type     MO       Location         Value               Rf  CV
245 ------------------------------------------------------------------------------------
246 1    1    thread start    seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0,  1)
247 2    1    init atomic     relaxed        0x601068   0                       ( 0,  2)
248 3    1    init atomic     relaxed        0x60106c   0                       ( 0,  3)
249 4    1    thread create   seq_cst  0x7f68fe51c710   0x7f68fe51c6e0          ( 0,  4)
250 5    2    thread start    seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4,  5)
251 6    2    atomic read     relaxed        0x60106c   0                   3   ( 0,  4,  6)
252 7    1    thread create   seq_cst  0x7f68fe51c720   0x7f68fe51c6e0          ( 0,  7)
253 8    3    thread start    seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0,  8)
254 9    2    atomic write    relaxed        0x601068   0                       ( 0,  4,  9)
255 10   3    atomic read     relaxed        0x601068   0                   2   ( 0,  7,  0, 10)
256 11   2    thread finish   seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4, 11)
257 12   3    atomic write    relaxed        0x60106c   0x2a                    ( 0,  7,  0, 12)
258 13   1    thread join     seq_cst  0x7f68ff11ebc0   0x2                     ( 0, 13, 11)
259 14   3    thread finish   seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0, 14)
260 15   1    thread join     seq_cst  0x7f68ff11efc0   0x3                     ( 0, 15, 11, 14)
261 16   1    thread finish   seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0, 16, 11, 14)
262 HASH 4073708854
263 ------------------------------------------------------------------------------------
264 </pre>
265
266 Now consider, for example, operation 10:
267
268 This is the 10th operation in the execution order. It is an atomic read-relaxed
269 operation performed by thread 3 at memory address `0x601068`. It reads the value
270 "0", which was written by the 2nd operation in the execution order. Its clock
271 vector consists of the following values:
272
273         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
274
275 End of Execution Summary
276 ------------------------
277
278 CDSChecker prints summary statistics at the end of each execution. These
279 summaries are based off of a few different properties of an execution, which we
280 will break down here:
281
282 * An _infeasible_ execution is an execution which is not consistent with the
283   memory model. Such an execution can be considered overhead for the
284   model-checker, since it should never appear in practice.
285
286 * A _buggy_ execution is an execution in which CDSChecker has found a real
287   bug: a data race, a deadlock, failure of a user-provided assertion, or an
288   uninitialized load, for instance. CDSChecker will only report bugs in feasible
289   executions.
290
291 * A _redundant_ execution is a feasible execution that is exploring the same
292   state space explored by a previous feasible execution. Such exploration is
293   another instance of overhead, so CDSChecker terminates these executions as
294   soon as they are detected. CDSChecker is mostly able to avoid such executions
295   but may encounter them if a fairness option is enabled.
296
297 Now, we can examine the end-of-execution summary of one test program:
298
299     $ ./run.sh test/rmwprog.o
300     + test/rmwprog.o
301     ******* Model-checking complete: *******
302     Number of complete, bug-free executions: 6
303     Number of redundant executions: 0
304     Number of buggy executions: 0
305     Number of infeasible executions: 29
306     Total executions: 35
307
308 * _Number of complete, bug-free executions:_ these are feasible, non-buggy, and
309   non-redundant executions. They each represent different, legal behaviors you
310   can expect to see in practice.
311
312 * _Number of redundant executions:_ these are feasible but redundant executions
313   that were terminated as soon as CDSChecker noticed the redundancy.
314
315 * _Number of buggy executions:_ these are feasible, buggy executions. These are
316   the trouble spots where your program is triggering a bug or assertion.
317   Ideally, this number should be 0.
318
319 * _Number of infeasible executions:_ these are infeasible executions,
320   representing some of the overhead of model-checking.
321
322 * _Total executions:_ the total number of executions explored by CDSChecker.
323   Should be the sum of the above categories, since they are mutually exclusive.
324
325
326 Other Notes and Pitfalls
327 ------------------------
328
329 * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
330   following test program.
331
332   >     ./run.sh test/deadlock.o
333
334   Deadlock detection currently detects when a thread is about to step into a
335   deadlock, without actually including the final step in the trace. But you can
336   examine the program to see the next step.
337
338 * CDSChecker has to speculatively explore many execution behaviors due to the
339   relaxed memory model, and many of these turn out to be infeasible (that is,
340   they cannot be legally produced by the memory model). CDSChecker discards
341   these executions as soon as it identifies them (see the "Number of infeasible
342   executions" statistic); however, the speculation can occasionally cause
343   CDSChecker to hit unexpected parts of the unit test program (causing a
344   division by 0, for instance). In such programs, you might consider running
345   CDSChecker with the `-u num` option.
346
347 * Related to the previous point, CDSChecker may report more than one bug for a
348   particular candidate execution. This is because some bugs may not be
349   reportable until CDSChecker has explored more of the program, and in the
350   time between initial discovery and final assessment of the bug, CDSChecker may
351   discover another bug.
352
353 * Data races may be reported as multiple bugs, one for each byte-address of the
354   data race in question. See, for example, this run:
355
356         $ ./run.sh test/releaseseq.o
357         ...
358         Bug report: 4 bugs detected
359           [BUG] Data race detected @ address 0x601078:
360             Access 1: write in thread  2 @ clock   4
361             Access 2:  read in thread  3 @ clock   9
362           [BUG] Data race detected @ address 0x601079:
363             Access 1: write in thread  2 @ clock   4
364             Access 2:  read in thread  3 @ clock   9
365           [BUG] Data race detected @ address 0x60107a:
366             Access 1: write in thread  2 @ clock   4
367             Access 2:  read in thread  3 @ clock   9
368           [BUG] Data race detected @ address 0x60107b:
369             Access 1: write in thread  2 @ clock   4
370             Access 2:  read in thread  3 @ clock   9
371
372
373 See Also
374 --------
375
376 The CDSChecker project page:
377
378 >   <http://demsky.eecs.uci.edu/c11modelchecker.php>
379
380 The CDSChecker source and accompanying benchmarks on Gitweb:
381
382 >   <http://demsky.eecs.uci.edu/git/?p=model-checker.git>
383 >
384 >   <http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git>
385
386
387 Contact
388 -------
389
390 Please feel free to contact us for more information. Bug reports are welcome,
391 and we are happy to hear from our users. We are also very interested to know if
392 CDSChecker catches bugs in your programs.
393
394 Contact Brian Norris at <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
395
396
397 References
398 ----------
399
400 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
401     system. CACM, 21(7):558-565, July 1978.