README.md

   1 CDSChecker: A Model Checker for C11 and C++11 Atomics
   2 =====================================================
   3
   4 Copyright &copy; 2013 Regents of the University of California. All rights reserved.
   5
   6 CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
   7
   8
   9 Overview
  10 --------
  11
  12 CDSChecker is a model checker for C11/C++11 which exhaustively explores the
  13 behaviors of code under the C/C++ memory model. It uses partial order reduction
  14 as well as a few other novel techniques to eliminate time spent on redundant
  15 execution behaviors and to significantly shrink the state space. The model
  16 checking algorithm is described in more detail in this paper (published in
  17 OOPSLA '13):
  18
  19 >   <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
  20
  21 It is designed to support unit tests on concurrent data structure written using
  22 C/C++ atomics.
  23
  24 CDSChecker is constructed as a dynamically-linked shared library which
  25 implements the C and C++ atomic types and portions of the other thread-support
  26 libraries of C/C++ (e.g., std::atomic, std::mutex, etc.). Notably, we only
  27 support the C version of threads (i.e., `thrd_t` and similar, from `<threads.h>`),
  28 because C++ threads require features which are only available to a C++11
  29 compiler (and we want to support others, at least for now).
  30
  31 CDSChecker should compile on Linux and Mac OSX with no dependencies and has been
  32 tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX
  33 flavors. We have not attempted to port to Windows.
  34
  35
  36 Getting Started
  37 ---------------
  38
  39 If you haven't done so already, you may download CDSChecker using
  40 [git](http://git-scm.com/) (for those without git, snapshots can be found at the
  41 Gitweb URLs below):
  42
  43       git clone git://demsky.eecs.uci.edu/model-checker.git
  44
  45 Get the benchmarks (not required; distributed separately):
  46
  47       cd model-checker
  48       git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks
  49
  50 Compile the model checker:
  51
  52       make
  53
  54 Compile the benchmarks:
  55
  56       make benchmarks
  57
  58 Run a simple example (the `run.sh` script does some very minimal processing for
  59 you):
  60
  61       ./run.sh test/userprog.o
  62
  63 To see the help message on how to run CDSChecker, execute:
  64
  65       ./run.sh -h
  66
  67
  68 Useful Options
  69 --------------
  70
  71 `-m num`
  72
  73   > Controls the liveness of the memory system. Note that multithreaded programs
  74   > often rely on memory liveness for termination, so this parameter is
  75   > necessary for such programs.
  76   >
  77   > Liveness is controlled by `num`: the number of times a load is allowed to
  78   > see the same store when a newer store exists---one that is ordered later in
  79   > the modification order.
  80
  81 `-y`
  82
  83   > Turns on CHESS-like yield-based fairness support (requires `thrd_yield()`
  84   > instrumentation in test program).
  85
  86 `-f num`
  87
  88   > Turns on alternative fairness support (less desirable than `-y`).
  89
  90 `-v`
  91
  92   > Verbose: show all executions and not just buggy ones.
  93
  94 `-s num`
  95
  96   > Constrain how long we will run to wait for a future value past when it is
  97   > expected
  98
  99 `-u num`
 100
 101   > Value to provide to atomics loads from uninitialized memory locations. The
 102   > default is 0, but this may cause some programs to throw exceptions
 103   > (segfault) before the model checker prints a trace.
 104
 105 Suggested options:
 106
 107 >     -m 2 -y
 108
 109 or
 110
 111 >     -m 2 -f 10
 112
 113
 114 Benchmarks
 115 -------------------
 116
 117 Many simple tests are located in the `tests/` directory. You may also want to
 118 try the larger benchmarks (distributed separately), which can be placed under
 119 the `benchmarks/` directory. After building CDSChecker, you can build and run
 120 the benchmarks as follows:
 121
 122 >     make benchmarks
 123 >     cd benchmarks
 124 >     ./run.sh barrier/barrier -y -m 2           # runs barrier test with fairness/memory liveness
 125 >     ./run.sh linuxrwlocks/linuxrwlocks -y -m 2 # Linux RW locks test with fairness/liveness
 126 >     ./bench.sh                                 # run all benchmarks and provide timing results
 127
 128
 129 Running your own code
 130 ---------------------
 131
 132 You likely want to test your own code, not just our simple tests. To do so, you
 133 need to perform a few steps.
 134
 135 First, because CDSChecker executes your program dozens (if not hundreds or
 136 thousands) of times, you will have the most success if your code is written as a
 137 unit test and not as a full-blown program.
 138
 139 Second, because CDSChecker must be able to manage your program for you, your
 140 program should declare its main entry point as `user_main(int, char**)` rather
 141 than `main(int, char**)`.
 142
 143 Third, test programs should use the standard C11/C++11 library headers
 144 (`<atomic>`/`<stdatomic.h>`, `<mutex>`, `<condition_variable>`, `<thread.h>`).
 145 As of now, we only support C11 thread syntax (`thrd_t`, etc. from
 146 `<thread.h>`).
 147
 148 Test programs may also use our included happens-before race detector by
 149 including <librace.h> and utilizing the appropriate functions
 150 (`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for loading/storing data from/to
 151 non-atomic shared memory.
 152
 153 CDSChecker can also check boolean assertions in your test programs. Just
 154 include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
 155 CDSChecker will report a bug in any possible execution in which the argument to
 156 `MODEL_ASSERT()` evaluates to false (that is, 0).
 157
 158 Test programs should be compiled against our shared library (libmodel.so) using
 159 the headers in the `include/` directory. Then the shared library must be made
 160 available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
 161 variable, for instance.
 162
 163
 164 Reading an execution trace
 165 --------------------------
 166
 167 When CDSChecker detects a bug in your program (or when run with the `--verbose`
 168 flag), it prints the output of the program run (STDOUT) along with some summary
 169 trace information for the execution in question. The trace is given as a
 170 sequence of lines, where each line represents an operation in the execution
 171 trace. These lines are ordered by the order in which they were run by CDSChecker
 172 (i.e., the "execution order"), which does not necessarily align with the "order"
 173 of the values observed (i.e., the modification order or the reads-from
 174 relation).
 175
 176 The following list describes each of the columns in the execution trace output:
 177
 178  * \#: The sequence number within the execution. That is, sequence number "9"
 179    means the operation was the 9th operation executed by CDSChecker. Note that
 180    this represents the execution order, not necessarily any other order (e.g.,
 181    modification order or reads-from).
 182
 183  * t: The thread number
 184
 185  * Action type: The type of operation performed
 186
 187  * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
 188    `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
 189
 190  * Location: The memory location on which this operation is operating. This is
 191    well-defined for atomic write/read/RMW, but other operations are subject to
 192    CDSChecker implementation details.
 193
 194  * Value: For reads/writes/RMW, the value returned by the operation. Note that
 195    for RMW, this is the value that is *read*, not the value that was *written*.
 196    For other operations, 'value' may have some CDSChecker-internal meaning, or
 197    it may simply be a don't-care (such as `0xdeadbeef`).
 198
 199  * Rf: For reads, the sequence number of the operation from which it reads.
 200    [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
 201    as printed during `--verbose` execution, reads may not be resolved and so may
 202    have Rf=? or Rf=Px, where x is a promised future value.]
 203
 204  * CV: The clock vector, encapsulating the happens-before relation (see our
 205    paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
 206    similar to [1]. The "clock" is just the sequence number (#). The clock vector
 207    can be read as follows:
 208
 209    Each entry is indexed as CV[i], where
 210
 211             i = 0, 1, 2, ..., <number of threads>
 212
 213    So for any thread i, we say CV[i] is the sequence number of the most recent
 214    operation in thread i such that operation i happens-before this operation.
 215    Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
 216    operations.
 217
 218 See the following example trace:
 219
 220 <pre>
 221 ------------------------------------------------------------------------------------
 222 #    t    Action type     MO       Location         Value               Rf  CV
 223 ------------------------------------------------------------------------------------
 224 1    1    thread start    seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0,  1)
 225 2    1    init atomic     relaxed        0x601068   0                       ( 0,  2)
 226 3    1    init atomic     relaxed        0x60106c   0                       ( 0,  3)
 227 4    1    thread create   seq_cst  0x7f68fe51c710   0x7f68fe51c6e0          ( 0,  4)
 228 5    2    thread start    seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4,  5)
 229 6    2    atomic read     relaxed        0x60106c   0                   3   ( 0,  4,  6)
 230 7    1    thread create   seq_cst  0x7f68fe51c720   0x7f68fe51c6e0          ( 0,  7)
 231 8    3    thread start    seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0,  8)
 232 9    2    atomic write    relaxed        0x601068   0                       ( 0,  4,  9)
 233 10   3    atomic read     relaxed        0x601068   0                   2   ( 0,  7,  0, 10)
 234 11   2    thread finish   seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4, 11)
 235 12   3    atomic write    relaxed        0x60106c   0x2a                    ( 0,  7,  0, 12)
 236 13   1    thread join     seq_cst  0x7f68ff11ebc0   0x2                     ( 0, 13, 11)
 237 14   3    thread finish   seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0, 14)
 238 15   1    thread join     seq_cst  0x7f68ff11efc0   0x3                     ( 0, 15, 11, 14)
 239 16   1    thread finish   seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0, 16, 11, 14)
 240 HASH 4073708854
 241 ------------------------------------------------------------------------------------
 242 </pre>
 243
 244 Now consider, for example, operation 10:
 245
 246 This is the 10th operation in the execution order. It is an atomic read-relaxed
 247 operation performed by thread 3 at memory address `0x601068`. It reads the value
 248 "0", which was written by the 2nd operation in the execution order. Its clock
 249 vector consists of the following values:
 250
 251         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
 252
 253
 254 Other Notes
 255 -----------
 256
 257 * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
 258   following test program.
 259
 260   >     ./run.sh test/deadlock.o
 261
 262   Deadlock detection currently detects when a thread is about to step into a
 263   deadlock, without actually including the final step in the trace. But you can
 264   examine the program to see the next step.
 265
 266 * CDSChecker has to speculatively explore many execution behaviors due to the
 267   relaxed memory model, and many of these turn out to be infeasible (that is,
 268   they cannot be legally produced by the memory model). CDSChecker discards
 269   these executions as soon as it identifies them (see the "Number of infeasible
 270   executions" statistic); however, the speculation can occasionally cause
 271   CDSChecker to hit unexpected parts of the unit test program (causing a
 272   division by 0, for instance). In such programs, you might consider running
 273   CDSChecker with the `-u num` option.
 274
 275
 276 See Also
 277 --------
 278
 279 The CDSChecker project page:
 280
 281 >   <http://demsky.eecs.uci.edu/c11modelchecker.php>
 282
 283 The CDSChecker source and accompanying benchmarks on Gitweb:
 284
 285 >   <http://demsky.eecs.uci.edu/git/?p=model-checker.git>
 286 >
 287 >   <http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git>
 288
 289
 290 Contact
 291 -------
 292
 293 Please feel free to contact us for more information. Bug reports are welcome,
 294 and we are happy to hear from our users. We are also very interested to know if
 295 CDSChecker catches bugs in your programs.
 296
 297 Contact Brian Norris at <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
 298
 299
 300 References
 301 ----------
 302
 303 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
 304     system. CACM, 21(7):558-565, July 1978.