1 C11Tester: A Testing tool for C11 and C++11 Atomics
2 =====================================================
4 C11Tester is a testing tool 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 compiles on Linux. Instrumenting programs requires using
12 our LLVM pass. It likely can be ported to other \*NIX flavors.
17 If you have questions, you can contact us at c11tester@googlegroups.com.
19 You can sign up for the C11Tester mailing list at:
20 <https://groups.google.com/forum/#!forum/c11tester>
26 If you haven't done so already, you may download C11Tester using git:
28 git clone git://plrg.eecs.uci.edu/c11tester.git
30 Get the benchmarks (not required; distributed separately):
32 git clone git://plrg.eecs.uci.edu/c11concurrency-benchmarks.git
34 Get the LLVM frontend using git and follow its directions to build:
36 git clone git://plrg.eecs.uci.edu/c11llvm.git
42 To see the help message on how to run C11Tester, execute:
52 > Verbose: show all executions and not just buggy ones.
56 > Specify the number number of executions to run.
61 The benchmarks are distributed separately. These require LLVM to instrument.
62 You may also follow the steps in the Artifact Appendix of our paper (https://dl.acm.org/doi/abs/10.1145/3445814.3446711) to run the benchmarks.
67 You likely want to test your own code, not just our tests. You will
68 likely need to use our LLVM pass to instrument your program. You will
69 have to modify your build environment to do this.
71 Test programs should be compiled against our shared library
72 (libmodel.so). Then the shared library must be made available to the
73 dynamic linker, using the `LD_LIBRARY_PATH` environment variable, for
77 Reading an execution trace
78 --------------------------
80 When C11Tester detects a bug in your program (or when run with the `--verbose`
81 flag), it prints the output of the program run (STDOUT) along with some summary
82 trace information for the execution in question. The trace is given as a
83 sequence of lines, where each line represents an operation in the execution
84 trace. These lines are ordered by the order in which they were run by C11Tester
85 (i.e., the "execution order"), which does not necessarily align with the "order"
86 of the values observed (i.e., the modification order or the reads-from
89 The following list describes each of the columns in the execution trace output:
91 * \#: The sequence number within the execution. That is, sequence number "9"
92 means the operation was the 9th operation executed by C11Tester. Note that
93 this represents the execution order, not necessarily any other order (e.g.,
94 modification order or reads-from).
96 * t: The thread number
98 * Action type: The type of operation performed
100 * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
101 `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
103 * Location: The memory location on which this operation is operating. This is
104 well-defined for atomic write/read/RMW, but other operations are subject to
105 C11Tester implementation details.
107 * Value: For reads/writes/RMW, the value returned by the operation. Note that
108 for RMW, this is the value that is *read*, not the value that was *written*.
109 For other operations, 'value' may have some C11Tester-internal meaning, or
110 it may simply be a don't-care (such as `0xdeadbeef`).
112 * Rf: For reads, the sequence number of the operation from which it reads.
113 [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
114 as printed during `--verbose` execution, reads may not be resolved and so may
115 have Rf=? or Rf=Px, where x is a promised future value.]
117 * CV: The clock vector, encapsulating the happens-before relation (see our
118 paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
119 similar to [1]. The "clock" is just the sequence number (#). The clock vector
120 can be read as follows:
122 Each entry is indexed as CV[i], where
124 i = 0, 1, 2, ..., <number of threads>
126 So for any thread i, we say CV[i] is the sequence number of the most recent
127 operation in thread i such that operation i happens-before this operation.
128 Notably, thread 0 is reserved as a dummy thread for certain C11Tester
131 See the following example trace:
133 ------------------------------------------------------------------------------------
134 # t Action type MO Location Value Rf CV
135 ------------------------------------------------------------------------------------
136 1 1 thread start seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 1)
137 2 1 init atomic relaxed 0x601068 0 ( 0, 2)
138 3 1 init atomic relaxed 0x60106c 0 ( 0, 3)
139 4 1 thread create seq_cst 0x7f68fe51c710 0x7f68fe51c6e0 ( 0, 4)
140 5 2 thread start seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 5)
141 6 2 atomic read relaxed 0x60106c 0 3 ( 0, 4, 6)
142 7 1 thread create seq_cst 0x7f68fe51c720 0x7f68fe51c6e0 ( 0, 7)
143 8 3 thread start seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 8)
144 9 2 atomic write relaxed 0x601068 0 ( 0, 4, 9)
145 10 3 atomic read relaxed 0x601068 0 2 ( 0, 7, 0, 10)
146 11 2 thread finish seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 11)
147 12 3 atomic write relaxed 0x60106c 0x2a ( 0, 7, 0, 12)
148 13 1 thread join seq_cst 0x7f68ff11ebc0 0x2 ( 0, 13, 11)
149 14 3 thread finish seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 14)
150 15 1 thread join seq_cst 0x7f68ff11efc0 0x3 ( 0, 15, 11, 14)
151 16 1 thread finish seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 16, 11, 14)
153 ------------------------------------------------------------------------------------
155 Now consider, for example, operation 10:
157 This is the 10th operation in the execution order. It is an atomic read-relaxed
158 operation performed by thread 3 at memory address `0x601068`. It reads the value
159 "0", which was written by the 2nd operation in the execution order. Its clock
160 vector consists of the following values:
162 CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
164 End of Execution Summary
165 ------------------------
167 C11Tester prints summary statistics at the end of each execution. These
168 summaries are based off of a few different properties of an execution, which we
169 will break down here:
171 * A _buggy_ execution is an execution in which C11Tester has found a real
172 bug: a data race, a deadlock, or a failure of a user-provided assertion.
173 C11Tester will only report bugs in feasible executions.
176 Other Notes and Pitfalls
177 ------------------------
179 * Data races may be reported as multiple bugs, one for each byte-address of the
180 data race in question. See, for example, this run:
182 $ ./run.sh test/releaseseq.o
184 Bug report: 4 bugs detected
185 [BUG] Data race detected @ address 0x601078:
186 Access 1: write in thread 2 @ clock 4
187 Access 2: read in thread 3 @ clock 9
188 [BUG] Data race detected @ address 0x601079:
189 Access 1: write in thread 2 @ clock 4
190 Access 2: read in thread 3 @ clock 9
191 [BUG] Data race detected @ address 0x60107a:
192 Access 1: write in thread 2 @ clock 4
193 Access 2: read in thread 3 @ clock 9
194 [BUG] Data race detected @ address 0x60107b:
195 Access 1: write in thread 2 @ clock 4
196 Access 2: read in thread 3 @ clock 9
202 The C11Tester project page:
204 > <http://demsky.eecs.uci.edu/c11tester.html>
206 The C11Tester source and accompanying benchmarks on Gitweb:
208 > <http://plrg.eecs.uci.edu/git/?p=c11tester.git>
210 > <http://plrg.eecs.uci.edu/git/?p=c11llvm.git>
212 > <http://plrg.eecs.uci.edu/git/?p=c11concurrency-benchmarks.git>
219 Please feel free to contact us for more information. Bug reports are welcome,
220 and we are happy to hear from our users. We are also very interested to know if
221 C11Tester catches bugs in your programs.
223 Contact Weiyu Luo at <weiyul7@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
229 Copyright © 2013 and 2019 Regents of the University of California. All rights reserved.
231 C11Tester is distributed under the GPL v2. See the LICENSE file for details.
237 This material is based upon work supported by the National Science
238 Foundation under Grant Numbers 1740210 and 1319786 and Google Research
241 Any opinions, findings, and conclusions or recommendations expressed in
242 this material are those of the author(s) and do not necessarily reflect
243 the views of the National Science Foundation.
249 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
250 system. CACM, 21(7):558-565, July 1978.