README.md

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