1 CDSChecker: A Model Checker for C11 and C++11 Atomics
2 =====================================================
4 CDSChecker is a model checker for C11/C++11 which exhaustively explores the
5 behaviors of code under the C/C++ memory model. It uses partial order reduction
6 as well as a few other novel techniques to eliminate time spent on redundant
7 execution behaviors and to significantly shrink the state space. The model
8 checking algorithm is described in more detail in this paper (published in
11 > <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
13 It is designed to support unit tests on concurrent data structure written using
16 CDSChecker is constructed as a dynamically-linked shared library which
17 implements the C and C++ atomic types and portions of the other thread-support
18 libraries of C/C++ (e.g., std::atomic, std::mutex, etc.). Notably, we only
19 support the C version of threads (i.e., `thrd_t` and similar, from `<threads.h>`),
20 because C++ threads require features which are only available to a C++11
21 compiler (and we want to support others, at least for now).
23 CDSChecker should compile on Linux and Mac OSX with no dependencies and has been
24 tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX
25 flavors. We have not attempted to port to Windows.
31 If you haven't done so already, you may download CDSChecker using
32 [git](http://git-scm.com/):
34 git clone git://demsky.eecs.uci.edu/model-checker.git
36 Source code can also be downloaded via the snapshot links on Gitweb (found in
37 the __See Also__ section).
39 Get the benchmarks (not required; distributed separately), placing them as a
40 subdirectory under the `model-checker` directory:
43 git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks
45 Compile the model checker:
49 Compile the benchmarks:
53 Run a simple example (the `run.sh` script does some very minimal processing for
56 ./run.sh test/userprog.o
58 To see the help message on how to run CDSChecker, execute:
68 > Controls the liveness of the memory system. Note that multithreaded programs
69 > often rely on memory liveness for termination, so this parameter is
70 > necessary for such programs.
72 > Liveness is controlled by `num`: the number of times a load is allowed to
73 > see the same store when a newer store exists---one that is ordered later in
74 > the modification order.
78 > Turns on CHESS-like yield-based fairness support (requires `thrd_yield()`
79 > instrumentation in test program).
83 > Turns on alternative fairness support (less desirable than `-y`). A
84 > necessary alternative for some programs that do not support yield-based
89 > Verbose: show all executions and not just buggy ones.
93 > Constrain how long we will run to wait for a future value past when it is
98 > Value to provide to atomics loads from uninitialized memory locations. The
99 > default is 0, but this may cause some programs to throw exceptions
100 > (segfault) before the model checker prints a trace.
114 Many simple tests are located in the `tests/` directory. You may also want to
115 try the larger benchmarks (distributed separately), which can be placed under
116 the `benchmarks/` directory. After building CDSChecker, you can build and run
117 the benchmarks as follows:
122 > # run barrier test with fairness/memory liveness
123 > ./run.sh barrier/barrier -y -m 2
125 > # Linux reader/write lock test with fairness/memory liveness
126 > ./run.sh linuxrwlocks/linuxrwlocks -y -m 2
128 > # run all benchmarks and provide timing results
132 Running your own code
133 ---------------------
135 You likely want to test your own code, not just our simple tests. To do so, you
136 need to perform a few steps.
138 First, because CDSChecker executes your program dozens (if not hundreds or
139 thousands) of times, you will have the most success if your code is written as a
140 unit test and not as a full-blown program.
142 Second, because CDSChecker must be able to manage your program for you, your
143 program should declare its main entry point as `user_main(int, char**)` rather
144 than `main(int, char**)`.
146 Third, test programs must use the standard C11/C++11 library headers (see below
147 for supported APIs) and must compile against the versions provided in
148 CDSChecker's `include/` directory. Notably, we only support C11 thread syntax
149 (`thrd_t`, etc. from `<thread.h>`).
151 Test programs may also use our included happens-before race detector by
152 including <librace.h> and utilizing the appropriate functions
153 (`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for storing/loading data
154 to/from non-atomic shared memory.
156 CDSChecker can also check boolean assertions in your test programs. Just
157 include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
158 CDSChecker will report a bug in any possible execution in which the argument to
159 `MODEL_ASSERT()` evaluates to false (that is, 0).
161 Test programs should be compiled against our shared library (libmodel.so) using
162 the headers in the `include/` directory. Then the shared library must be made
163 available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
164 variable, for instance.
167 ### Supported C11/C++11 APIs ###
169 To model-check multithreaded code properly, CDSChecker needs to instrument any
170 concurrency-related API calls made in your code. Currently, we support parts of
171 the following thread-support libraries. The C versions can be used in either C
174 * `<atomic>`, `<cstdatomic>`, `<stdatomic.h>`
175 * `<condition_variable>`
179 Because we want to extend support to legacy (i.e., non-C++11) compilers, we do
180 not support some new C++11 features that can't be implemented in C++03 (e.g.,
183 Reading an execution trace
184 --------------------------
186 When CDSChecker detects a bug in your program (or when run with the `--verbose`
187 flag), it prints the output of the program run (STDOUT) along with some summary
188 trace information for the execution in question. The trace is given as a
189 sequence of lines, where each line represents an operation in the execution
190 trace. These lines are ordered by the order in which they were run by CDSChecker
191 (i.e., the "execution order"), which does not necessarily align with the "order"
192 of the values observed (i.e., the modification order or the reads-from
195 The following list describes each of the columns in the execution trace output:
197 * \#: The sequence number within the execution. That is, sequence number "9"
198 means the operation was the 9th operation executed by CDSChecker. Note that
199 this represents the execution order, not necessarily any other order (e.g.,
200 modification order or reads-from).
202 * t: The thread number
204 * Action type: The type of operation performed
206 * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
207 `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
209 * Location: The memory location on which this operation is operating. This is
210 well-defined for atomic write/read/RMW, but other operations are subject to
211 CDSChecker implementation details.
213 * Value: For reads/writes/RMW, the value returned by the operation. Note that
214 for RMW, this is the value that is *read*, not the value that was *written*.
215 For other operations, 'value' may have some CDSChecker-internal meaning, or
216 it may simply be a don't-care (such as `0xdeadbeef`).
218 * Rf: For reads, the sequence number of the operation from which it reads.
219 [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
220 as printed during `--verbose` execution, reads may not be resolved and so may
221 have Rf=? or Rf=Px, where x is a promised future value.]
223 * CV: The clock vector, encapsulating the happens-before relation (see our
224 paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
225 similar to [1]. The "clock" is just the sequence number (#). The clock vector
226 can be read as follows:
228 Each entry is indexed as CV[i], where
230 i = 0, 1, 2, ..., <number of threads>
232 So for any thread i, we say CV[i] is the sequence number of the most recent
233 operation in thread i such that operation i happens-before this operation.
234 Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
237 See the following example trace:
239 ------------------------------------------------------------------------------------
240 # t Action type MO Location Value Rf CV
241 ------------------------------------------------------------------------------------
242 1 1 thread start seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 1)
243 2 1 init atomic relaxed 0x601068 0 ( 0, 2)
244 3 1 init atomic relaxed 0x60106c 0 ( 0, 3)
245 4 1 thread create seq_cst 0x7f68fe51c710 0x7f68fe51c6e0 ( 0, 4)
246 5 2 thread start seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 5)
247 6 2 atomic read relaxed 0x60106c 0 3 ( 0, 4, 6)
248 7 1 thread create seq_cst 0x7f68fe51c720 0x7f68fe51c6e0 ( 0, 7)
249 8 3 thread start seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 8)
250 9 2 atomic write relaxed 0x601068 0 ( 0, 4, 9)
251 10 3 atomic read relaxed 0x601068 0 2 ( 0, 7, 0, 10)
252 11 2 thread finish seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 11)
253 12 3 atomic write relaxed 0x60106c 0x2a ( 0, 7, 0, 12)
254 13 1 thread join seq_cst 0x7f68ff11ebc0 0x2 ( 0, 13, 11)
255 14 3 thread finish seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 14)
256 15 1 thread join seq_cst 0x7f68ff11efc0 0x3 ( 0, 15, 11, 14)
257 16 1 thread finish seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 16, 11, 14)
259 ------------------------------------------------------------------------------------
261 Now consider, for example, operation 10:
263 This is the 10th operation in the execution order. It is an atomic read-relaxed
264 operation performed by thread 3 at memory address `0x601068`. It reads the value
265 "0", which was written by the 2nd operation in the execution order. Its clock
266 vector consists of the following values:
268 CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
270 End of Execution Summary
271 ------------------------
273 CDSChecker prints summary statistics at the end of each execution. These
274 summaries are based off of a few different properties of an execution, which we
275 will break down here:
277 * An _infeasible_ execution is an execution which is not consistent with the
278 memory model. Such an execution can be considered overhead for the
279 model-checker, since it should never appear in practice.
281 * A _buggy_ execution is an execution in which CDSChecker has found a real
282 bug: a data race, a deadlock, failure of a user-provided assertion, or an
283 uninitialized load, for instance. CDSChecker will only report bugs in feasible
286 * A _redundant_ execution is a feasible execution that is exploring the same
287 state space explored by a previous feasible execution. Such exploration is
288 another instance of overhead, so CDSChecker terminates these executions as
289 soon as they are detected. CDSChecker is mostly able to avoid such executions
290 but may encounter them if a fairness option is enabled.
292 Now, we can examine the end-of-execution summary of one test program:
294 $ ./run.sh test/rmwprog.o
296 ******* Model-checking complete: *******
297 Number of complete, bug-free executions: 6
298 Number of redundant executions: 0
299 Number of buggy executions: 0
300 Number of infeasible executions: 29
303 * _Number of complete, bug-free executions:_ these are feasible, non-buggy, and
304 non-redundant executions. They each represent different, legal behaviors you
305 can expect to see in practice.
307 * _Number of redundant executions:_ these are feasible but redundant executions
308 that were terminated as soon as CDSChecker noticed the redundancy.
310 * _Number of buggy executions:_ these are feasible, buggy executions. These are
311 the trouble spots where your program is triggering a bug or assertion.
312 Ideally, this number should be 0.
314 * _Number of infeasible executions:_ these are infeasible executions,
315 representing some of the overhead of model-checking.
317 * _Total executions:_ the total number of executions explored by CDSChecker.
318 Should be the sum of the above categories, since they are mutually exclusive.
321 Other Notes and Pitfalls
322 ------------------------
324 * Many programs require some form of fairness in order to terminate in a finite
325 amount of time. CDSChecker supports the `-y num` and `-f num` flags for these
326 cases. The `-y` option (yield-based fairness) is preferable, but it requires
327 careful usage of yields (i.e., `thrd_yield()`) in the test program. For
328 programs without proper `thrd_yield()`, you may consider using `-f` instead.
330 * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
331 following test program.
333 > ./run.sh test/deadlock.o
335 Deadlock detection currently detects when a thread is about to step into a
336 deadlock, without actually including the final step in the trace. But you can
337 examine the program to see the next step.
339 * CDSChecker has to speculatively explore many execution behaviors due to the
340 relaxed memory model, and many of these turn out to be infeasible (that is,
341 they cannot be legally produced by the memory model). CDSChecker discards
342 these executions as soon as it identifies them (see the "Number of infeasible
343 executions" statistic); however, the speculation can occasionally cause
344 CDSChecker to hit unexpected parts of the unit test program (causing a
345 division by 0, for instance). In such programs, you might consider running
346 CDSChecker with the `-u num` option.
348 * Related to the previous point, CDSChecker may report more than one bug for a
349 particular candidate execution. This is because some bugs may not be
350 reportable until CDSChecker has explored more of the program, and in the
351 time between initial discovery and final assessment of the bug, CDSChecker may
352 discover another bug.
354 * Data races may be reported as multiple bugs, one for each byte-address of the
355 data race in question. See, for example, this run:
357 $ ./run.sh test/releaseseq.o
359 Bug report: 4 bugs detected
360 [BUG] Data race detected @ address 0x601078:
361 Access 1: write in thread 2 @ clock 4
362 Access 2: read in thread 3 @ clock 9
363 [BUG] Data race detected @ address 0x601079:
364 Access 1: write in thread 2 @ clock 4
365 Access 2: read in thread 3 @ clock 9
366 [BUG] Data race detected @ address 0x60107a:
367 Access 1: write in thread 2 @ clock 4
368 Access 2: read in thread 3 @ clock 9
369 [BUG] Data race detected @ address 0x60107b:
370 Access 1: write in thread 2 @ clock 4
371 Access 2: read in thread 3 @ clock 9
377 The CDSChecker project page:
379 > <http://demsky.eecs.uci.edu/c11modelchecker.html>
381 The CDSChecker source and accompanying benchmarks on Gitweb:
383 > <http://demsky.eecs.uci.edu/git/?p=model-checker.git>
385 > <http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git>
391 Please feel free to contact us for more information. Bug reports are welcome,
392 and we are happy to hear from our users. We are also very interested to know if
393 CDSChecker catches bugs in your programs.
395 Contact Brian Norris at <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
401 Copyright © 2013 Regents of the University of California. All rights reserved.
403 CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
409 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
410 system. CACM, 21(7):558-565, July 1978.