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 This README is divided into sections as follows:
   9
  10  *  Overview
  11  *  Basic build and run
  12  *  Running your own code
  13  *  Reading an execution trace
  14  *  References
  15
  16 Overview
  17 --------
  18
  19 CDSChecker is a model checker for C11/C++11 exhaustively explores the behaviors
  20 of code under the C11/C++11 memory model. It uses partial order reduction to
  21 eliminate redundant executions to significantly shrink the state space.
  22 The model checking algorithm is described in more detail in this paper
  23 (currently under review):
  24
  25   <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
  26
  27 It is designed to support unit tests on concurrent data structure written using
  28 C11/C++11 atomics.
  29
  30 CDSChecker is constructed as a dynamically-linked shared library which
  31 implements the C and C++ atomic types and portions of the other thread-support
  32 libraries of C/C++ (e.g., std::atomic, std::mutex, etc.). Notably, we only
  33 support the C version of threads (i.e., `thrd_t` and similar, from `<threads.h>`),
  34 because C++ threads require features which are only available to a C++11
  35 compiler (and we want to support others, at least for now).
  36
  37 CDSChecker should compile on Linux and Mac OSX with no dependencies and has been
  38 tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX
  39 flavors. We have not attempted to port to Windows.
  40
  41 Other references can be found at the main project page:
  42
  43   <http://demsky.eecs.uci.edu/c11modelchecker.php>
  44
  45 Basic build and run
  46 -------------------
  47
  48 Sample run instructions:
  49
  50 <pre>
  51 $ make
  52 $ export LD_LIBRARY_PATH=.
  53 $ ./test/userprog.o                   # Runs simple test program
  54 $ ./test/userprog.o -h                # Prints help information
  55 Copyright (c) 2013 Regents of the University of California. All rights reserved.
  56 Distributed under the GPLv2
  57 Written by Brian Norris and Brian Demsky
  58
  59 Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
  60
  61 MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments
  62 provided after the `--' (the PROGRAM ARGS) are passed to the user program.
  63
  64 Model-checker options:
  65 -h, --help                  Display this help message and exit
  66 -m, --liveness=NUM          Maximum times a thread can read from the same write
  67                               while other writes exist.
  68                               Default: 0
  69 -M, --maxfv=NUM             Maximum number of future values that can be sent to
  70                               the same read.
  71                               Default: 0
  72 -s, --maxfvdelay=NUM        Maximum actions that the model checker will wait for
  73                               a write from the future past the expected number
  74                               of actions.
  75                               Default: 6
  76 -S, --fvslop=NUM            Future value expiration sloppiness.
  77                               Default: 4
  78 -y, --yield                 Enable CHESS-like yield-based fairness support.
  79                               Default: disabled
  80 -Y, --yieldblock            Prohibit an execution from running a yield.
  81                               Default: disabled
  82 -f, --fairness=WINDOW       Specify a fairness window in which actions that are
  83                               enabled sufficiently many times should receive
  84                               priority for execution (not recommended).
  85                               Default: 0
  86 -e, --enabled=COUNT         Enabled count.
  87                               Default: 1
  88 -b, --bound=MAX             Upper length bound.
  89                               Default: 0
  90 -v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:
  91                               0 is quiet; 1 is noisy; 2 is noisier.
  92                               Default: 0
  93 -u, --uninitialized=VALUE   Return VALUE any load which may read from an
  94                               uninitialized atomic.
  95                               Default: 0
  96 -t, --analysis=NAME         Use Analysis Plugin.
  97 -o, --options=NAME          Option for previous analysis plugin.
  98                             -o help for a list of options
  99  --                         Program arguments follow.
 100
 101 Analysis plugins:
 102 SC
 103 </pre>
 104
 105
 106 Note that we also provide a series of benchmarks (distributed separately),
 107 which can be placed under the `benchmarks/` directory. After building CDSChecker,
 108 you can build and run the benchmarks as follows:
 109
 110         cd benchmarks
 111         make
 112         ./run.sh barrier/barrier -y -m 2     # runs barrier test with fairness/memory liveness
 113         ./bench.sh                           # run all benchmarks and provide timing results
 114
 115 Running your own code
 116 ---------------------
 117
 118 We provide several test and sample programs under the `test/` directory, which
 119 should compile and run with no trouble. Of course, you likely want to test your
 120 own code. To do so, you need to perform a few steps.
 121
 122 First, because CDSChecker executes your program dozens (if not hundreds or
 123 thousands) of times, you will have the most success if your code is written as a
 124 unit test and not as a full-blown program.
 125
 126 Next, test programs should use the standard C11/C++11 library headers
 127 (`<atomic>`/`<stdatomic.h>`, `<mutex>`, `<condition_variable>`, `<thread.h>`) and must
 128 name their main routine as `user_main(int, char**)` rather than `main(int, char**)`.
 129 We only support C11 thread syntax (`thrd_t`, etc. from `<thread.h>`).
 130
 131 Test programs may also use our included happens-before race detector by
 132 including <librace.h> and utilizing the appropriate functions
 133 (`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for loading/storing data from/to
 134 non-atomic shared memory.
 135
 136 CDSChecker can also check boolean assertions in your test programs. Just
 137 include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
 138 CDSChecker will report a bug in any possible execution in which the argument to
 139 `MODEL_ASSERT()` evaluates to false (that is, 0).
 140
 141 Test programs should be compiled against our shared library (libmodel.so) using
 142 the headers in the `include/` directory. Then the shared library must be made
 143 available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
 144 variable, for instance.
 145
 146 Reading an execution trace
 147 --------------------------
 148
 149 When CDSChecker detects a bug in your program (or when run with the `--verbose`
 150 flag), it prints the output of the program run (STDOUT) along with some summary
 151 trace information for the execution in question. The trace is given as a
 152 sequence of lines, where each line represents an operation in the execution
 153 trace. These lines are ordered by the order in which they were run by CDSChecker
 154 (i.e., the "execution order"), which does not necessarily align with the "order"
 155 of the values observed (i.e., the modification order or the reads-from
 156 relation).
 157
 158 The following list describes each of the columns in the execution trace output:
 159
 160  * \#: The sequence number within the execution. That is, sequence number "9"
 161    means the operation was the 9th operation executed by CDSChecker. Note that
 162    this represents the execution order, not necessarily any other order (e.g.,
 163    modification order or reads-from).
 164
 165  * t: The thread number
 166
 167  * Action type: The type of operation performed
 168
 169  * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
 170    `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
 171
 172  * Location: The memory location on which this operation is operating. This is
 173    well-defined for atomic write/read/RMW, but other operations are subject to
 174    CDSChecker implementation details.
 175
 176  * Value: For reads/writes/RMW, the value returned by the operation. Note that
 177    for RMW, this is the value that is *read*, not the value that was *written*.
 178    For other operations, 'value' may have some CDSChecker-internal meaning, or
 179    it may simply be a don't-care (such as `0xdeadbeef`).
 180
 181  * Rf: For reads, the sequence number of the operation from which it reads.
 182    [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
 183    as printed during `--verbose` execution, reads may not be resolved and so may
 184    have Rf=? or Rf=Px, where x is a promised future value.]
 185
 186  * CV: The clock vector, encapsulating the happens-before relation (see our
 187    paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
 188    similar to [1]. The "clock" is just the sequence number (#). The clock vector
 189    can be read as follows:
 190
 191    Each entry is indexed as CV[i], where
 192
 193             i = 0, 1, 2, ..., <number of threads>
 194
 195    So for any thread i, we say CV[i] is the sequence number of the most recent
 196    operation in thread i such that operation i happens-before this operation.
 197    Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
 198    operations.
 199
 200 See the following example trace:
 201
 202 <pre>
 203 ------------------------------------------------------------------------------------
 204 #    t    Action type     MO       Location         Value               Rf  CV
 205 ------------------------------------------------------------------------------------
 206 1    1    thread start    seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0,  1)
 207 2    1    init atomic     relaxed        0x601068   0                       ( 0,  2)
 208 3    1    init atomic     relaxed        0x60106c   0                       ( 0,  3)
 209 4    1    thread create   seq_cst  0x7f68fe51c710   0x7f68fe51c6e0          ( 0,  4)
 210 5    2    thread start    seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4,  5)
 211 6    2    atomic read     relaxed        0x60106c   0                   3   ( 0,  4,  6)
 212 7    1    thread create   seq_cst  0x7f68fe51c720   0x7f68fe51c6e0          ( 0,  7)
 213 8    3    thread start    seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0,  8)
 214 9    2    atomic write    relaxed        0x601068   0                       ( 0,  4,  9)
 215 10   3    atomic read     relaxed        0x601068   0                   2   ( 0,  7,  0, 10)
 216 11   2    thread finish   seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4, 11)
 217 12   3    atomic write    relaxed        0x60106c   0x2a                    ( 0,  7,  0, 12)
 218 13   1    thread join     seq_cst  0x7f68ff11ebc0   0x2                     ( 0, 13, 11)
 219 14   3    thread finish   seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0, 14)
 220 15   1    thread join     seq_cst  0x7f68ff11efc0   0x3                     ( 0, 15, 11, 14)
 221 16   1    thread finish   seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0, 16, 11, 14)
 222 HASH 4073708854
 223 ------------------------------------------------------------------------------------
 224 </pre>
 225
 226 Now consider, for example, operation 10:
 227
 228 This is the 10th operation in the execution order. It is an atomic read-relaxed
 229 operation performed by thread 3 at memory address `0x601068`. It reads the value
 230 "0", which was written by the 2nd operation in the execution order. Its clock
 231 vector consists of the following values:
 232
 233         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
 234
 235
 236 References
 237 ----------
 238
 239 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
 240     system. CACM, 21(7):558-565, July 1978.