README

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