README.md

   1 C11Tester: A Testing tool for C11 and C++11 Atomics
   2 =====================================================
   3
   4 C11Tester is a testing tool for C11/C++11 which randomly explores the
   5 behaviors of code under the C/C++ memory model.
   6
   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.).
  10
  11 C11Tester compiles on Linux.  Instrumenting programs requires using
  12 our LLVM pass.  It likely can be ported to other \*NIX flavors.
  13
  14 Mailing List
  15 ------------
  16
  17 If you have questions, you can contact us at c11tester@googlegroups.com.
  18
  19 You can sign up for the C11Tester mailing list at:
  20 <https://groups.google.com/forum/#!forum/c11tester>
  21
  22
  23 Getting Started
  24 ---------------
  25
  26 If you haven't done so already, you may download C11Tester using git:
  27
  28       git clone git://plrg.eecs.uci.edu/c11tester.git
  29
  30 Get the benchmarks (not required; distributed separately):
  31
  32       git clone git://plrg.eecs.uci.edu/c11concurrency-benchmarks.git
  33
  34 Get the LLVM frontend using git and follow its directions to build:
  35
  36       git clone git://plrg.eecs.uci.edu/c11llvm.git
  37
  38 Compile the fuzzer:
  39
  40       make
  41
  42 To see the help message on how to run C11Tester, execute:
  43
  44       ./run.sh -h
  45
  46
  47 Useful Options
  48 --------------
  49
  50 `-v`
  51
  52   > Verbose: show all executions and not just buggy ones.
  53
  54 `-x num`
  55
  56   > Specify the number number of executions to run.
  57
  58 Benchmarks
  59 -------------------
  60
  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.
  63
  64 Running your own code
  65 ---------------------
  66
  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.
  70
  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
  74 instance.
  75
  76
  77 Reading an execution trace
  78 --------------------------
  79
  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
  87 relation).
  88
  89 The following list describes each of the columns in the execution trace output:
  90
  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).
  95
  96  * t: The thread number
  97
  98  * Action type: The type of operation performed
  99
 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`)
 102
 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.
 106
 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`).
 111
 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.]
 116
 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:
 121
 122    Each entry is indexed as CV[i], where
 123
 124             i = 0, 1, 2, ..., <number of threads>
 125
 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
 129    operations.
 130
 131 See the following example trace:
 132
 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)
 152     HASH 4073708854
 153     ------------------------------------------------------------------------------------
 154
 155 Now consider, for example, operation 10:
 156
 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:
 161
 162         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
 163
 164 End of Execution Summary
 165 ------------------------
 166
 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:
 170
 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.
 174
 175
 176 Other Notes and Pitfalls
 177 ------------------------
 178
 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:
 181
 182         $ ./run.sh test/releaseseq.o
 183         ...
 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
 197
 198
 199 See Also
 200 --------
 201
 202 The C11Tester project page:
 203
 204 >   <http://demsky.eecs.uci.edu/c11tester.html>
 205
 206 The C11Tester source and accompanying benchmarks on Gitweb:
 207
 208 >   <http://plrg.eecs.uci.edu/git/?p=c11tester.git>
 209 >
 210 >   <http://plrg.eecs.uci.edu/git/?p=c11llvm.git>
 211 >
 212 >   <http://plrg.eecs.uci.edu/git/?p=c11concurrency-benchmarks.git>
 213
 214
 215
 216 Contact
 217 -------
 218
 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.
 222
 223 Contact Weiyu Luo at <weiyul7@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
 224
 225
 226 Copyright
 227 ---------
 228
 229 Copyright &copy; 2013 and 2019 Regents of the University of California. All rights reserved.
 230
 231 C11Tester is distributed under the GPL v2. See the LICENSE file for details.
 232
 233
 234 Acknowledgments
 235 ---------------
 236
 237 This material is based upon work supported by the National Science
 238 Foundation under Grant Numbers 1740210 and 1319786 and Google Research
 239 awards.
 240
 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.
 244
 245
 246 References
 247 ----------
 248
 249 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
 250     system. CACM, 21(7):558-565, July 1978.