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.
   8
   9 This README is divided into sections as follows:
  10
  11  I.    Overview
  12  II.   Reading an execution trace
  13  A.    References
  14
  15 ----------------------------------------
  16  I. Overview
  17 ----------------------------------------
  18
  19 CDSChecker compiles as a dynamically-linked shared library by simply running
  20 'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM
  21 (clang/clang++) and GCC.
  22
  23 Test programs should use the standard C11/C++11 library headers
  24 (<atomic>/<stdatomic.h>, <mutex>, <condition_variable>, <thread.h>) and must
  25 name their main routine as user_main(int, char**) rather than main(int, char**).
  26 We only support C11 thread syntax (thrd_t, etc. from <thread.h>).
  27
  28 Test programs may also use our included happens-before race detector by
  29 including <librace.h> and utilizing the appropriate functions
  30 (store_{8,16,32,64}() and load_{8,16,32,64}()) for loading/storing data from/to
  31 from non-atomic shared memory.
  32
  33 Test programs should be compiled against our shared library (libmodel.so) using
  34 the headers in the include/ directory. Then the shared library must be made
  35 available to the dynamic linker, using the LD_LIBRARY_PATH environment
  36 variable, for instance.
  37
  38 Sample run instructions:
  39
  40 $ make
  41 $ export LD_LIBRARY_PATH=.
  42 $ ./test/userprog.o                   # Runs simple test program
  43 $ ./test/userprog.o -h                # Prints help information
  44 Copyright (c) 2013 Regents of the University of California. All rights reserved.
  45 Distributed under the GPLv2
  46 Written by Brian Norris and Brian Demsky
  47
  48 Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
  49
  50 MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments
  51 provided after the `--' (the PROGRAM ARGS) are passed to the user program.
  52
  53 Model-checker options:
  54 -h, --help                  Display this help message and exit
  55 -m, --liveness=NUM          Maximum times a thread can read from the same write
  56                               while other writes exist.
  57                               Default: 0
  58 -M, --maxfv=NUM             Maximum number of future values that can be sent to
  59                               the same read.
  60                               Default: 0
  61 -s, --maxfvdelay=NUM        Maximum actions that the model checker will wait for
  62                               a write from the future past the expected number
  63                               of actions.
  64                               Default: 6
  65 -S, --fvslop=NUM            Future value expiration sloppiness.
  66                               Default: 4
  67 -y, --yield                 Enable CHESS-like yield-based fairness support.
  68                               Default: disabled
  69 -Y, --yieldblock            Prohibit an execution from running a yield.
  70                               Default: disabled
  71 -f, --fairness=WINDOW       Specify a fairness window in which actions that are
  72                               enabled sufficiently many times should receive
  73                               priority for execution (not recommended).
  74                               Default: 0
  75 -e, --enabled=COUNT         Enabled count.
  76                               Default: 1
  77 -b, --bound=MAX             Upper length bound.
  78                               Default: 0
  79 -v, --verbose               Print verbose execution information.
  80 -u, --uninitialized=VALUE   Return VALUE any load which may read from an
  81                               uninitialized atomic.
  82                               Default: 0
  83 -t, --analysis=NAME         Use Analysis Plugin.
  84 -o, --options=NAME          Option for previous analysis plugin.
  85                             -o help for a list of options
  86  --                         Program arguments follow.
  87
  88
  89 Note that we also provide a series of benchmarks (distributed separately),
  90 which can be placed under the benchmarks/ directory. After building CDSChecker,
  91 you can build and run the benchmarks as follows:
  92
  93   cd benchmarks
  94   make
  95   ./run.sh barrier/barrier -y -m 2     # runs barrier test with fairness/memory liveness
  96   ./bench.sh                           # run all benchmarks twice, with timing results
  97
  98
  99 ----------------------------------------
 100  II. Reading an execution trace
 101 ----------------------------------------
 102
 103 When CDSChecker detects a bug in your program (or when run with the --verbose
 104 flag), it prints the output of the program run (STDOUT) along with some summary
 105 trace information. The trace is given as a sequence of lines, where each line
 106 represents an operation in the execution trace. These lines are ordered by the
 107 order in which they were run by CDSChecker (i.e., the "execution order"), which
 108 does not necessarily align with the "order" of the values observed (i.e., the
 109 modification order and the reads-from relation).
 110
 111 Columns:
 112
 113  o #: The sequence number within the execution. That is, sequence number "9"
 114    means the operation was the 9th operation executed by CDSChecker. Note that
 115    this represents the execution order, not necessarily any other order (e.g.,
 116    modification order or reads-from).
 117
 118  o t: The thread number
 119
 120  o Action type: The type of operation performed
 121
 122  o MO: The memory-order for this operation (i.e., memory_order_XXX, where XXX is
 123    relaxed, release, acquire, rel_acq, or seq_cst)
 124
 125  o Location: The memory location on which this operation is operating. This is
 126    well-defined for atomic write/read/RMW, but other operations are subject to
 127    CDSChecker implementation details.
 128
 129  o Value: For reads/writes/RMW, the value returned by the operation. Note that
 130    for RMW, this is the value that is *read*, not the value that was *written*.
 131    For other operations, 'value' may have some CDSChecker-internal meaning.
 132
 133  o Rf: For reads, the sequence number of the operation from which it reads.
 134    [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
 135    as printed during --verbose execution, reads may not be resolved and so may
 136    have Rf=? or Rf=Px, where x is a promised future value.]
 137
 138  o CV: The clock vector, encapsulating the happens-before relation (see our
 139    paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
 140    similar to [1]. The "clock" is just the sequence number (#). The clock vector
 141    can be read as follows:
 142
 143    Each entry is indexed as CV[i], where
 144
 145      i = 0, 1, 2, ..., <number of threads>
 146
 147    So for any thread i, we say CV[i] is the sequence number of the most recent
 148    operation in thread i such that operation i happens-before this operation.
 149    Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
 150    operations.
 151
 152 See the following example trace:
 153
 154 ------------------------------------------------------------------------------------
 155 #    t    Action type     MO       Location         Value               Rf  CV
 156 ------------------------------------------------------------------------------------
 157 1    1    thread start    seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0,  1)
 158 2    1    init atomic     relaxed        0x601068   0                       ( 0,  2)
 159 3    1    init atomic     relaxed        0x60106c   0                       ( 0,  3)
 160 4    1    thread create   seq_cst  0x7f68fe51c710   0x7f68fe51c6e0          ( 0,  4)
 161 5    2    thread start    seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4,  5)
 162 6    2    atomic read     relaxed        0x60106c   0                   3   ( 0,  4,  6)
 163 7    1    thread create   seq_cst  0x7f68fe51c720   0x7f68fe51c6e0          ( 0,  7)
 164 8    3    thread start    seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0,  8)
 165 9    2    atomic write    relaxed        0x601068   0                       ( 0,  4,  9)
 166 10   3    atomic read     relaxed        0x601068   0                   2   ( 0,  7,  0, 10)
 167 11   2    thread finish   seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4, 11)
 168 12   3    atomic write    relaxed        0x60106c   0x2a                    ( 0,  7,  0, 12)
 169 13   1    thread join     seq_cst  0x7f68ff11ebc0   0x2                     ( 0, 13, 11)
 170 14   3    thread finish   seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0, 14)
 171 15   1    thread join     seq_cst  0x7f68ff11efc0   0x3                     ( 0, 15, 11, 14)
 172 16   1    thread finish   seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0, 16, 11, 14)
 173 HASH 4073708854
 174 ------------------------------------------------------------------------------------
 175
 176 Now consider, for example, operation 10:
 177
 178 This is the 10th operation in the execution order. It is an atomic read-relaxed
 179 operation performed by thread 3 at memory address 0x601068. It reads the value
 180 "0", which was written by the 2nd operation in the execution order. Its clock
 181 vector consists of the following values:
 182
 183   CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
 184
 185
 186 ----------------------------------------
 187  A. References
 188 ----------------------------------------
 189
 190 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
 191     system. CACM, 21(7):558–565, July 1978.