4 Copyright © 2013 Regents of the University of California. All rights reserved.
6 CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
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
18 <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
20 It is designed to support unit tests on concurrent data structure written using
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).
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.
34 You may also refer to the CDSChecker project page:
36 <http://demsky.eecs.uci.edu/c11modelchecker.php>
41 If you haven't done so already, you may download CDSChecker using
42 [git](http://git-scm.com/):
44 git clone git://demsky.eecs.uci.edu/model-checker.git
46 Get the benchmarks (not required; distributed separately):
49 git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks
51 Compile the model checker:
55 Compile the benchmarks:
59 Run a simple example (the `run.sh` script does some very minimal processing for
62 ./run.sh test/userprog.o
64 To see the help message on how to run CDSChecker, execute:
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.
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.
83 > Turns on CHESS-like yield-based fairness support (requires `thrd_yield()`
84 > instrumentation in test program).
88 > Turns on alternative fairness support (less desirable than `-y`).
92 > Verbose: show all executions and not just buggy ones.
96 > Constrain how long we will run to wait for a future value past when it is
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.
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:
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
126 Running your own code
127 ---------------------
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.
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.
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**)`.
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
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.
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).
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.
160 Reading an execution trace
161 --------------------------
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
172 The following list describes each of the columns in the execution trace output:
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).
179 * t: The thread number
181 * Action type: The type of operation performed
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`)
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.
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`).
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.]
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:
205 Each entry is indexed as CV[i], where
207 i = 0, 1, 2, ..., <number of threads>
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
214 See the following example trace:
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)
237 ------------------------------------------------------------------------------------
240 Now consider, for example, operation 10:
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:
247 CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
253 * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
254 following test program.
256 > ./run.sh test/deadlock.o
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.
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.
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.
279 Contact Brian Norris at <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
285 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
286 system. CACM, 21(7):558-565, July 1978.