README.md

   1 C11Tester: A Fuzzer for C11 and C++11 Atomics
   2 =====================================================
   3
   4 C11Tester is a fuzzer 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 should compile on Linux OSX.  Instrumenting programs
  12 requires using our LLVM pass.  It likely can be ported to other \*NIX
  13 flavors.
  14
  15
  16 Getting Started
  17 ---------------
  18
  19 If you haven't done so already, you may download C11Tester using git:
  20
  21       git clone git://demsky.eecs.uci.edu/c11fuzzer.git
  22
  23 Get the benchmarks (not required; distributed separately):
  24
  25       git clone git://demsky.eecs.uci.edu/concurrency-benchmarks.git
  26
  27 Compile the fuzzer:
  28
  29       make
  30
  31 To see the help message on how to run C11Tester, execute:
  32
  33       ./run.sh -h
  34
  35
  36 Useful Options
  37 --------------
  38
  39 `-v`
  40
  41   > Verbose: show all executions and not just buggy ones.
  42
  43 `-u num`
  44
  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.
  48
  49 Benchmarks
  50 -------------------
  51
  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:
  56
  57 >     make benchmarks
  58 >     cd benchmarks
  59 >
  60 >     # run barrier test with fairness/memory liveness
  61 >     ./run.sh barrier/barrier -y -m 2
  62 >
  63 >     # Linux reader/write lock test with fairness/memory liveness
  64 >     ./run.sh linuxrwlocks/linuxrwlocks -y -m 2
  65 >
  66 >     # run all benchmarks and provide timing results
  67 >     ./bench.sh
  68
  69
  70 Running your own code
  71 ---------------------
  72
  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.
  75
  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.
  79
  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**)`.
  83
  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>`).
  88
  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.
  93
  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).
  98
  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.
 103
 104
 105 ### Supported C11/C++11 APIs ###
 106
 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
 110 or C++.
 111
 112 * `<atomic>`, `<cstdatomic>`, `<stdatomic.h>`
 113 * `<condition_variable>`
 114 * `<mutex>`
 115 * `<threads.h>`
 116
 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.,
 119 C++ `<thread>`).
 120
 121 Reading an execution trace
 122 --------------------------
 123
 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
 131 relation).
 132
 133 The following list describes each of the columns in the execution trace output:
 134
 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).
 139
 140  * t: The thread number
 141
 142  * Action type: The type of operation performed
 143
 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`)
 146
 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.
 150
 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`).
 155
 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.]
 160
 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:
 165
 166    Each entry is indexed as CV[i], where
 167
 168             i = 0, 1, 2, ..., <number of threads>
 169
 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
 173    operations.
 174
 175 See the following example trace:
 176
 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)
 196     HASH 4073708854
 197     ------------------------------------------------------------------------------------
 198
 199 Now consider, for example, operation 10:
 200
 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:
 205
 206         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
 207
 208 End of Execution Summary
 209 ------------------------
 210
 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:
 214
 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.
 218
 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
 222   executions.
 223
 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.
 229
 230 Now, we can examine the end-of-execution summary of one test program:
 231
 232     $ ./run.sh test/rmwprog.o
 233     + 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
 239     Total executions: 35
 240
 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.
 244
 245 * _Number of redundant executions:_ these are feasible but redundant executions
 246   that were terminated as soon as C11Tester noticed the redundancy.
 247
 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.
 251
 252 * _Number of infeasible executions:_ these are infeasible executions,
 253   representing some of the overhead of model-checking.
 254
 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.
 257
 258
 259 Other Notes and Pitfalls
 260 ------------------------
 261
 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.
 267
 268 * Deadlock detection: C11Tester can detect deadlocks. For instance, try the
 269   following test program.
 270
 271   >     ./run.sh test/deadlock.o
 272
 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.
 276
 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.
 285
 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.
 291
 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:
 294
 295         $ ./run.sh test/releaseseq.o
 296         ...
 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
 310
 311
 312 See Also
 313 --------
 314
 315 The C11Tester project page:
 316
 317 >   <http://demsky.eecs.uci.edu/c11modelchecker.html>
 318
 319 The C11Tester source and accompanying benchmarks on Gitweb:
 320
 321 >   <http://demsky.eecs.uci.edu/git/?p=model-checker.git>
 322 >
 323 >   <http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git>
 324
 325
 326 Contact
 327 -------
 328
 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.
 332
 333 Contact Weiyu Luo at <weiyul7@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
 334
 335
 336 Copyright
 337 ---------
 338
 339 Copyright &copy; 2013 and 2019 Regents of the University of California. All rights reserved.
 340
 341 C11Tester is distributed under the GPL v2. See the LICENSE file for details.
 342
 343
 344 References
 345 ----------
 346
 347 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
 348     system. CACM, 21(7):558-565, July 1978.