1 C11Tester: A Fuzzer for C11 and C++11 Atomics
2 =====================================================
4 C11Tester is a fuzzer for C11/C++11 which randomly explores the
5 behaviors of code under the C/C++ memory model.
7 C11Tester is constructed as a dynamically-linked shared library which
8 implements the C and C++ atomic types and portions of the other thread-support
9 libraries of C/C++ (e.g., std::atomic, std::mutex, etc.).
11 C11Tester should compile on Linux OSX. Instrumenting programs
12 requires using our LLVM pass. It likely can be ported to other \*NIX
19 If you haven't done so already, you may download C11Tester using git:
21 git clone git://demsky.eecs.uci.edu/c11fuzzer.git
23 Get the benchmarks (not required; distributed separately):
25 git clone git://demsky.eecs.uci.edu/concurrency-benchmarks.git
31 To see the help message on how to run C11Tester, execute:
41 > Verbose: show all executions and not just buggy ones.
45 > Value to provide to atomics loads from uninitialized memory locations. The
46 > default is 0, but this may cause some programs to throw exceptions
47 > (segfault) before the model checker prints a trace.
52 Many simple tests are located in the `tests/` directory. You may also want to
53 try the larger benchmarks (distributed separately), which can be placed under
54 the `benchmarks/` directory. After building C11Tester, you can build and run
55 the benchmarks as follows:
60 > # run barrier test with fairness/memory liveness
61 > ./run.sh barrier/barrier -y -m 2
63 > # Linux reader/write lock test with fairness/memory liveness
64 > ./run.sh linuxrwlocks/linuxrwlocks -y -m 2
66 > # run all benchmarks and provide timing results
73 You likely want to test your own code, not just our simple tests. To do so, you
74 need to perform a few steps.
76 First, because C11Tester executes your program dozens (if not hundreds or
77 thousands) of times, you will have the most success if your code is written as a
78 unit test and not as a full-blown program.
80 Second, because C11Tester must be able to manage your program for you, your
81 program should declare its main entry point as `user_main(int, char**)` rather
82 than `main(int, char**)`.
84 Third, test programs must use the standard C11/C++11 library headers (see below
85 for supported APIs) and must compile against the versions provided in
86 C11Tester's `include/` directory. Notably, we only support C11 thread syntax
87 (`thrd_t`, etc. from `<thread.h>`).
89 Test programs may also use our included happens-before race detector by
90 including <librace.h> and utilizing the appropriate functions
91 (`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for storing/loading data
92 to/from non-atomic shared memory.
94 C11Tester can also check boolean assertions in your test programs. Just
95 include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
96 C11Tester will report a bug in any possible execution in which the argument to
97 `MODEL_ASSERT()` evaluates to false (that is, 0).
99 Test programs should be compiled against our shared library (libmodel.so) using
100 the headers in the `include/` directory. Then the shared library must be made
101 available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
102 variable, for instance.
105 ### Supported C11/C++11 APIs ###
107 To model-check multithreaded code properly, C11Tester needs to instrument any
108 concurrency-related API calls made in your code. Currently, we support parts of
109 the following thread-support libraries. The C versions can be used in either C
112 * `<atomic>`, `<cstdatomic>`, `<stdatomic.h>`
113 * `<condition_variable>`
117 Because we want to extend support to legacy (i.e., non-C++11) compilers, we do
118 not support some new C++11 features that can't be implemented in C++03 (e.g.,
121 Reading an execution trace
122 --------------------------
124 When C11Tester detects a bug in your program (or when run with the `--verbose`
125 flag), it prints the output of the program run (STDOUT) along with some summary
126 trace information for the execution in question. The trace is given as a
127 sequence of lines, where each line represents an operation in the execution
128 trace. These lines are ordered by the order in which they were run by C11Tester
129 (i.e., the "execution order"), which does not necessarily align with the "order"
130 of the values observed (i.e., the modification order or the reads-from
133 The following list describes each of the columns in the execution trace output:
135 * \#: The sequence number within the execution. That is, sequence number "9"
136 means the operation was the 9th operation executed by C11Tester. Note that
137 this represents the execution order, not necessarily any other order (e.g.,
138 modification order or reads-from).
140 * t: The thread number
142 * Action type: The type of operation performed
144 * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
145 `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
147 * Location: The memory location on which this operation is operating. This is
148 well-defined for atomic write/read/RMW, but other operations are subject to
149 C11Tester implementation details.
151 * Value: For reads/writes/RMW, the value returned by the operation. Note that
152 for RMW, this is the value that is *read*, not the value that was *written*.
153 For other operations, 'value' may have some C11Tester-internal meaning, or
154 it may simply be a don't-care (such as `0xdeadbeef`).
156 * Rf: For reads, the sequence number of the operation from which it reads.
157 [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
158 as printed during `--verbose` execution, reads may not be resolved and so may
159 have Rf=? or Rf=Px, where x is a promised future value.]
161 * CV: The clock vector, encapsulating the happens-before relation (see our
162 paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
163 similar to [1]. The "clock" is just the sequence number (#). The clock vector
164 can be read as follows:
166 Each entry is indexed as CV[i], where
168 i = 0, 1, 2, ..., <number of threads>
170 So for any thread i, we say CV[i] is the sequence number of the most recent
171 operation in thread i such that operation i happens-before this operation.
172 Notably, thread 0 is reserved as a dummy thread for certain C11Tester
175 See the following example trace:
177 ------------------------------------------------------------------------------------
178 # t Action type MO Location Value Rf CV
179 ------------------------------------------------------------------------------------
180 1 1 thread start seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 1)
181 2 1 init atomic relaxed 0x601068 0 ( 0, 2)
182 3 1 init atomic relaxed 0x60106c 0 ( 0, 3)
183 4 1 thread create seq_cst 0x7f68fe51c710 0x7f68fe51c6e0 ( 0, 4)
184 5 2 thread start seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 5)
185 6 2 atomic read relaxed 0x60106c 0 3 ( 0, 4, 6)
186 7 1 thread create seq_cst 0x7f68fe51c720 0x7f68fe51c6e0 ( 0, 7)
187 8 3 thread start seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 8)
188 9 2 atomic write relaxed 0x601068 0 ( 0, 4, 9)
189 10 3 atomic read relaxed 0x601068 0 2 ( 0, 7, 0, 10)
190 11 2 thread finish seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 11)
191 12 3 atomic write relaxed 0x60106c 0x2a ( 0, 7, 0, 12)
192 13 1 thread join seq_cst 0x7f68ff11ebc0 0x2 ( 0, 13, 11)
193 14 3 thread finish seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 14)
194 15 1 thread join seq_cst 0x7f68ff11efc0 0x3 ( 0, 15, 11, 14)
195 16 1 thread finish seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 16, 11, 14)
197 ------------------------------------------------------------------------------------
199 Now consider, for example, operation 10:
201 This is the 10th operation in the execution order. It is an atomic read-relaxed
202 operation performed by thread 3 at memory address `0x601068`. It reads the value
203 "0", which was written by the 2nd operation in the execution order. Its clock
204 vector consists of the following values:
206 CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
208 End of Execution Summary
209 ------------------------
211 C11Tester prints summary statistics at the end of each execution. These
212 summaries are based off of a few different properties of an execution, which we
213 will break down here:
215 * An _infeasible_ execution is an execution which is not consistent with the
216 memory model. Such an execution can be considered overhead for the
217 model-checker, since it should never appear in practice.
219 * A _buggy_ execution is an execution in which C11Tester has found a real
220 bug: a data race, a deadlock, failure of a user-provided assertion, or an
221 uninitialized load, for instance. C11Tester will only report bugs in feasible
224 * A _redundant_ execution is a feasible execution that is exploring the same
225 state space explored by a previous feasible execution. Such exploration is
226 another instance of overhead, so C11Tester terminates these executions as
227 soon as they are detected. C11Tester is mostly able to avoid such executions
228 but may encounter them if a fairness option is enabled.
230 Now, we can examine the end-of-execution summary of one test program:
232 $ ./run.sh test/rmwprog.o
234 ******* Model-checking complete: *******
235 Number of complete, bug-free executions: 6
236 Number of redundant executions: 0
237 Number of buggy executions: 0
238 Number of infeasible executions: 29
241 * _Number of complete, bug-free executions:_ these are feasible, non-buggy, and
242 non-redundant executions. They each represent different, legal behaviors you
243 can expect to see in practice.
245 * _Number of redundant executions:_ these are feasible but redundant executions
246 that were terminated as soon as C11Tester noticed the redundancy.
248 * _Number of buggy executions:_ these are feasible, buggy executions. These are
249 the trouble spots where your program is triggering a bug or assertion.
250 Ideally, this number should be 0.
252 * _Number of infeasible executions:_ these are infeasible executions,
253 representing some of the overhead of model-checking.
255 * _Total executions:_ the total number of executions explored by C11Tester.
256 Should be the sum of the above categories, since they are mutually exclusive.
259 Other Notes and Pitfalls
260 ------------------------
262 * Many programs require some form of fairness in order to terminate in a finite
263 amount of time. C11Tester supports the `-y num` and `-f num` flags for these
264 cases. The `-y` option (yield-based fairness) is preferable, but it requires
265 careful usage of yields (i.e., `thrd_yield()`) in the test program. For
266 programs without proper `thrd_yield()`, you may consider using `-f` instead.
268 * Deadlock detection: C11Tester can detect deadlocks. For instance, try the
269 following test program.
271 > ./run.sh test/deadlock.o
273 Deadlock detection currently detects when a thread is about to step into a
274 deadlock, without actually including the final step in the trace. But you can
275 examine the program to see the next step.
277 * C11Tester has to speculatively explore many execution behaviors due to the
278 relaxed memory model, and many of these turn out to be infeasible (that is,
279 they cannot be legally produced by the memory model). C11Tester discards
280 these executions as soon as it identifies them (see the "Number of infeasible
281 executions" statistic); however, the speculation can occasionally cause
282 C11Tester to hit unexpected parts of the unit test program (causing a
283 division by 0, for instance). In such programs, you might consider running
284 C11Tester with the `-u num` option.
286 * Related to the previous point, C11Tester may report more than one bug for a
287 particular candidate execution. This is because some bugs may not be
288 reportable until C11Tester has explored more of the program, and in the
289 time between initial discovery and final assessment of the bug, C11Tester may
290 discover another bug.
292 * Data races may be reported as multiple bugs, one for each byte-address of the
293 data race in question. See, for example, this run:
295 $ ./run.sh test/releaseseq.o
297 Bug report: 4 bugs detected
298 [BUG] Data race detected @ address 0x601078:
299 Access 1: write in thread 2 @ clock 4
300 Access 2: read in thread 3 @ clock 9
301 [BUG] Data race detected @ address 0x601079:
302 Access 1: write in thread 2 @ clock 4
303 Access 2: read in thread 3 @ clock 9
304 [BUG] Data race detected @ address 0x60107a:
305 Access 1: write in thread 2 @ clock 4
306 Access 2: read in thread 3 @ clock 9
307 [BUG] Data race detected @ address 0x60107b:
308 Access 1: write in thread 2 @ clock 4
309 Access 2: read in thread 3 @ clock 9
315 The C11Tester project page:
317 > <http://demsky.eecs.uci.edu/c11modelchecker.html>
319 The C11Tester source and accompanying benchmarks on Gitweb:
321 > <http://demsky.eecs.uci.edu/git/?p=model-checker.git>
323 > <http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git>
329 Please feel free to contact us for more information. Bug reports are welcome,
330 and we are happy to hear from our users. We are also very interested to know if
331 C11Tester catches bugs in your programs.
333 Contact Weiyu Luo at <weiyul7@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
339 Copyright © 2013 and 2019 Regents of the University of California. All rights reserved.
341 C11Tester is distributed under the GPL v2. See the LICENSE file for details.
347 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
348 system. CACM, 21(7):558-565, July 1978.