README.md

   1 CDSChecker: A Model Checker for C11 and C++11 Atomics
   2 =====================================================
   3
   4 CDSChecker is a model checker for C11/C++11 which exhaustively explores the
   5 behaviors of code under the C/C++ memory model. It uses partial order reduction
   6 as well as a few other novel techniques to eliminate time spent on redundant
   7 execution behaviors and to significantly shrink the state space. The model
   8 checking algorithm is described in more detail in this paper (published in
   9 OOPSLA '13):
  10
  11 >   <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
  12
  13 It is designed to support unit tests on concurrent data structure written using
  14 C/C++ atomics.
  15
  16 CDSChecker is constructed as a dynamically-linked shared library which
  17 implements the C and C++ atomic types and portions of the other thread-support
  18 libraries of C/C++ (e.g., std::atomic, std::mutex, etc.). Notably, we only
  19 support the C version of threads (i.e., `thrd_t` and similar, from `<threads.h>`),
  20 because C++ threads require features which are only available to a C++11
  21 compiler (and we want to support others, at least for now).
  22
  23 CDSChecker should compile on Linux and Mac OSX with no dependencies and has been
  24 tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX
  25 flavors. We have not attempted to port to Windows.
  26
  27
  28 Getting Started
  29 ---------------
  30
  31 If you haven't done so already, you may download CDSChecker using
  32 [git](http://git-scm.com/):
  33
  34       git clone git://demsky.eecs.uci.edu/model-checker.git
  35
  36 Source code can also be downloaded via the snapshot links on Gitweb (found in
  37 the __See Also__ section).
  38
  39 Get the benchmarks (not required; distributed separately), placing them as a
  40 subdirectory under the `model-checker` directory:
  41
  42       cd model-checker
  43       git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks
  44
  45 Compile the model checker:
  46
  47       make
  48
  49 Compile the benchmarks:
  50
  51       make benchmarks
  52
  53 Run a simple example (the `run.sh` script does some very minimal processing for
  54 you):
  55
  56       ./run.sh test/userprog.o
  57
  58 To see the help message on how to run CDSChecker, execute:
  59
  60       ./run.sh -h
  61
  62
  63 Useful Options
  64 --------------
  65
  66 `-m num`
  67
  68   > Controls the liveness of the memory system. Note that multithreaded programs
  69   > often rely on memory liveness for termination, so this parameter is
  70   > necessary for such programs.
  71   >
  72   > Liveness is controlled by `num`: the number of times a load is allowed to
  73   > see the same store when a newer store exists---one that is ordered later in
  74   > the modification order.
  75
  76 `-y`
  77
  78   > Turns on CHESS-like yield-based fairness support (requires `thrd_yield()`
  79   > instrumentation in test program).
  80
  81 `-f num`
  82
  83   > Turns on alternative fairness support (less desirable than `-y`). A
  84   > necessary alternative for some programs that do not support yield-based
  85   > fairness properly.
  86
  87 `-v`
  88
  89   > Verbose: show all executions and not just buggy ones.
  90
  91 `-s num`
  92
  93   > Constrain how long we will run to wait for a future value past when it is
  94   > expected
  95
  96 `-u num`
  97
  98   > Value to provide to atomics loads from uninitialized memory locations. The
  99   > default is 0, but this may cause some programs to throw exceptions
 100   > (segfault) before the model checker prints a trace.
 101
 102 Suggested options:
 103
 104 >     -m 2 -y
 105
 106 or
 107
 108 >     -m 2 -f 10
 109
 110
 111 Benchmarks
 112 -------------------
 113
 114 Many simple tests are located in the `tests/` directory. You may also want to
 115 try the larger benchmarks (distributed separately), which can be placed under
 116 the `benchmarks/` directory. After building CDSChecker, you can build and run
 117 the benchmarks as follows:
 118
 119 >     make benchmarks
 120 >     cd benchmarks
 121 >
 122 >     # run barrier test with fairness/memory liveness
 123 >     ./run.sh barrier/barrier -y -m 2
 124 >
 125 >     # Linux reader/write lock test with fairness/memory liveness
 126 >     ./run.sh linuxrwlocks/linuxrwlocks -y -m 2
 127 >
 128 >     # run all benchmarks and provide timing results
 129 >     ./bench.sh
 130
 131
 132 Running your own code
 133 ---------------------
 134
 135 You likely want to test your own code, not just our simple tests. To do so, you
 136 need to perform a few steps.
 137
 138 First, because CDSChecker executes your program dozens (if not hundreds or
 139 thousands) of times, you will have the most success if your code is written as a
 140 unit test and not as a full-blown program.
 141
 142 Second, because CDSChecker must be able to manage your program for you, your
 143 program should declare its main entry point as `user_main(int, char**)` rather
 144 than `main(int, char**)`.
 145
 146 Third, test programs must use the standard C11/C++11 library headers (see below
 147 for supported APIs) and must compile against the versions provided in
 148 CDSChecker's `include/` directory. Notably, we only support C11 thread syntax
 149 (`thrd_t`, etc. from `<thread.h>`).
 150
 151 Test programs may also use our included happens-before race detector by
 152 including <librace.h> and utilizing the appropriate functions
 153 (`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for storing/loading data
 154 to/from non-atomic shared memory.
 155
 156 CDSChecker can also check boolean assertions in your test programs. Just
 157 include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
 158 CDSChecker will report a bug in any possible execution in which the argument to
 159 `MODEL_ASSERT()` evaluates to false (that is, 0).
 160
 161 Test programs should be compiled against our shared library (libmodel.so) using
 162 the headers in the `include/` directory. Then the shared library must be made
 163 available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
 164 variable, for instance.
 165
 166
 167 ### Supported C11/C++11 APIs ###
 168
 169 To model-check multithreaded code properly, CDSChecker needs to instrument any
 170 concurrency-related API calls made in your code. Currently, we support parts of
 171 the following thread-support libraries. The C versions can be used in either C
 172 or C++.
 173
 174 * `<atomic>`, `<cstdatomic>`, `<stdatomic.h>`
 175 * `<condition_variable>`
 176 * `<mutex>`
 177 * `<threads.h>`
 178
 179 Because we want to extend support to legacy (i.e., non-C++11) compilers, we do
 180 not support some new C++11 features that can't be implemented in C++03 (e.g.,
 181 C++ `<thread>`).
 182
 183 Reading an execution trace
 184 --------------------------
 185
 186 When CDSChecker detects a bug in your program (or when run with the `--verbose`
 187 flag), it prints the output of the program run (STDOUT) along with some summary
 188 trace information for the execution in question. The trace is given as a
 189 sequence of lines, where each line represents an operation in the execution
 190 trace. These lines are ordered by the order in which they were run by CDSChecker
 191 (i.e., the "execution order"), which does not necessarily align with the "order"
 192 of the values observed (i.e., the modification order or the reads-from
 193 relation).
 194
 195 The following list describes each of the columns in the execution trace output:
 196
 197  * \#: The sequence number within the execution. That is, sequence number "9"
 198    means the operation was the 9th operation executed by CDSChecker. Note that
 199    this represents the execution order, not necessarily any other order (e.g.,
 200    modification order or reads-from).
 201
 202  * t: The thread number
 203
 204  * Action type: The type of operation performed
 205
 206  * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
 207    `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
 208
 209  * Location: The memory location on which this operation is operating. This is
 210    well-defined for atomic write/read/RMW, but other operations are subject to
 211    CDSChecker implementation details.
 212
 213  * Value: For reads/writes/RMW, the value returned by the operation. Note that
 214    for RMW, this is the value that is *read*, not the value that was *written*.
 215    For other operations, 'value' may have some CDSChecker-internal meaning, or
 216    it may simply be a don't-care (such as `0xdeadbeef`).
 217
 218  * Rf: For reads, the sequence number of the operation from which it reads.
 219    [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
 220    as printed during `--verbose` execution, reads may not be resolved and so may
 221    have Rf=? or Rf=Px, where x is a promised future value.]
 222
 223  * CV: The clock vector, encapsulating the happens-before relation (see our
 224    paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
 225    similar to [1]. The "clock" is just the sequence number (#). The clock vector
 226    can be read as follows:
 227
 228    Each entry is indexed as CV[i], where
 229
 230             i = 0, 1, 2, ..., <number of threads>
 231
 232    So for any thread i, we say CV[i] is the sequence number of the most recent
 233    operation in thread i such that operation i happens-before this operation.
 234    Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
 235    operations.
 236
 237 See the following example trace:
 238
 239     ------------------------------------------------------------------------------------
 240     #    t    Action type     MO       Location         Value               Rf  CV
 241     ------------------------------------------------------------------------------------
 242     1    1    thread start    seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0,  1)
 243     2    1    init atomic     relaxed        0x601068   0                       ( 0,  2)
 244     3    1    init atomic     relaxed        0x60106c   0                       ( 0,  3)
 245     4    1    thread create   seq_cst  0x7f68fe51c710   0x7f68fe51c6e0          ( 0,  4)
 246     5    2    thread start    seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4,  5)
 247     6    2    atomic read     relaxed        0x60106c   0                   3   ( 0,  4,  6)
 248     7    1    thread create   seq_cst  0x7f68fe51c720   0x7f68fe51c6e0          ( 0,  7)
 249     8    3    thread start    seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0,  8)
 250     9    2    atomic write    relaxed        0x601068   0                       ( 0,  4,  9)
 251     10   3    atomic read     relaxed        0x601068   0                   2   ( 0,  7,  0, 10)
 252     11   2    thread finish   seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4, 11)
 253     12   3    atomic write    relaxed        0x60106c   0x2a                    ( 0,  7,  0, 12)
 254     13   1    thread join     seq_cst  0x7f68ff11ebc0   0x2                     ( 0, 13, 11)
 255     14   3    thread finish   seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0, 14)
 256     15   1    thread join     seq_cst  0x7f68ff11efc0   0x3                     ( 0, 15, 11, 14)
 257     16   1    thread finish   seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0, 16, 11, 14)
 258     HASH 4073708854
 259     ------------------------------------------------------------------------------------
 260
 261 Now consider, for example, operation 10:
 262
 263 This is the 10th operation in the execution order. It is an atomic read-relaxed
 264 operation performed by thread 3 at memory address `0x601068`. It reads the value
 265 "0", which was written by the 2nd operation in the execution order. Its clock
 266 vector consists of the following values:
 267
 268         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
 269
 270 End of Execution Summary
 271 ------------------------
 272
 273 CDSChecker prints summary statistics at the end of each execution. These
 274 summaries are based off of a few different properties of an execution, which we
 275 will break down here:
 276
 277 * An _infeasible_ execution is an execution which is not consistent with the
 278   memory model. Such an execution can be considered overhead for the
 279   model-checker, since it should never appear in practice.
 280
 281 * A _buggy_ execution is an execution in which CDSChecker has found a real
 282   bug: a data race, a deadlock, failure of a user-provided assertion, or an
 283   uninitialized load, for instance. CDSChecker will only report bugs in feasible
 284   executions.
 285
 286 * A _redundant_ execution is a feasible execution that is exploring the same
 287   state space explored by a previous feasible execution. Such exploration is
 288   another instance of overhead, so CDSChecker terminates these executions as
 289   soon as they are detected. CDSChecker is mostly able to avoid such executions
 290   but may encounter them if a fairness option is enabled.
 291
 292 Now, we can examine the end-of-execution summary of one test program:
 293
 294     $ ./run.sh test/rmwprog.o
 295     + test/rmwprog.o
 296     ******* Model-checking complete: *******
 297     Number of complete, bug-free executions: 6
 298     Number of redundant executions: 0
 299     Number of buggy executions: 0
 300     Number of infeasible executions: 29
 301     Total executions: 35
 302
 303 * _Number of complete, bug-free executions:_ these are feasible, non-buggy, and
 304   non-redundant executions. They each represent different, legal behaviors you
 305   can expect to see in practice.
 306
 307 * _Number of redundant executions:_ these are feasible but redundant executions
 308   that were terminated as soon as CDSChecker noticed the redundancy.
 309
 310 * _Number of buggy executions:_ these are feasible, buggy executions. These are
 311   the trouble spots where your program is triggering a bug or assertion.
 312   Ideally, this number should be 0.
 313
 314 * _Number of infeasible executions:_ these are infeasible executions,
 315   representing some of the overhead of model-checking.
 316
 317 * _Total executions:_ the total number of executions explored by CDSChecker.
 318   Should be the sum of the above categories, since they are mutually exclusive.
 319
 320
 321 Other Notes and Pitfalls
 322 ------------------------
 323
 324 * Many programs require some form of fairness in order to terminate in a finite
 325   amount of time. CDSChecker supports the `-y num` and `-f num` flags for these
 326   cases. The `-y` option (yield-based fairness) is preferable, but it requires
 327   careful usage of yields (i.e., `thrd_yield()`) in the test program. For
 328   programs without proper `thrd_yield()`, you may consider using `-f` instead.
 329
 330 * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
 331   following test program.
 332
 333   >     ./run.sh test/deadlock.o
 334
 335   Deadlock detection currently detects when a thread is about to step into a
 336   deadlock, without actually including the final step in the trace. But you can
 337   examine the program to see the next step.
 338
 339 * CDSChecker has to speculatively explore many execution behaviors due to the
 340   relaxed memory model, and many of these turn out to be infeasible (that is,
 341   they cannot be legally produced by the memory model). CDSChecker discards
 342   these executions as soon as it identifies them (see the "Number of infeasible
 343   executions" statistic); however, the speculation can occasionally cause
 344   CDSChecker to hit unexpected parts of the unit test program (causing a
 345   division by 0, for instance). In such programs, you might consider running
 346   CDSChecker with the `-u num` option.
 347
 348 * Related to the previous point, CDSChecker may report more than one bug for a
 349   particular candidate execution. This is because some bugs may not be
 350   reportable until CDSChecker has explored more of the program, and in the
 351   time between initial discovery and final assessment of the bug, CDSChecker may
 352   discover another bug.
 353
 354 * Data races may be reported as multiple bugs, one for each byte-address of the
 355   data race in question. See, for example, this run:
 356
 357         $ ./run.sh test/releaseseq.o
 358         ...
 359         Bug report: 4 bugs detected
 360           [BUG] Data race detected @ address 0x601078:
 361             Access 1: write in thread  2 @ clock   4
 362             Access 2:  read in thread  3 @ clock   9
 363           [BUG] Data race detected @ address 0x601079:
 364             Access 1: write in thread  2 @ clock   4
 365             Access 2:  read in thread  3 @ clock   9
 366           [BUG] Data race detected @ address 0x60107a:
 367             Access 1: write in thread  2 @ clock   4
 368             Access 2:  read in thread  3 @ clock   9
 369           [BUG] Data race detected @ address 0x60107b:
 370             Access 1: write in thread  2 @ clock   4
 371             Access 2:  read in thread  3 @ clock   9
 372
 373
 374 See Also
 375 --------
 376
 377 The CDSChecker project page:
 378
 379 >   <http://demsky.eecs.uci.edu/c11modelchecker.html>
 380
 381 The CDSChecker source and accompanying benchmarks on Gitweb:
 382
 383 >   <http://demsky.eecs.uci.edu/git/?p=model-checker.git>
 384 >
 385 >   <http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git>
 386
 387
 388 Contact
 389 -------
 390
 391 Please feel free to contact us for more information. Bug reports are welcome,
 392 and we are happy to hear from our users. We are also very interested to know if
 393 CDSChecker catches bugs in your programs.
 394
 395 Contact Brian Norris at <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
 396
 397
 398 Copyright
 399 ---------
 400
 401 Copyright &copy; 2013 Regents of the University of California. All rights reserved.
 402
 403 CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
 404
 405
 406 References
 407 ----------
 408
 409 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
 410     system. CACM, 21(7):558-565, July 1978.