1 ****************************************
3 ****************************************
5 Copyright (c) 2013 Regents of the University of California. All rights reserved.
7 CDSChecker is distributed under the GPL v2.
9 This README is divided into sections as follows:
12 II. Reading an execution trace
15 ----------------------------------------
17 ----------------------------------------
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.
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>).
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.
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.
38 Sample run instructions:
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
48 Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
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.
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.
58 -M, --maxfv=NUM Maximum number of future values that can be sent to
61 -s, --maxfvdelay=NUM Maximum actions that the model checker will wait for
62 a write from the future past the expected number
65 -S, --fvslop=NUM Future value expiration sloppiness.
67 -y, --yield Enable CHESS-like yield-based fairness support.
69 -Y, --yieldblock Prohibit an execution from running a yield.
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).
75 -e, --enabled=COUNT Enabled count.
77 -b, --bound=MAX Upper length bound.
79 -v, --verbose Print verbose execution information.
80 -u, --uninitialized=VALUE Return VALUE any load which may read from an
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.
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:
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
99 ----------------------------------------
100 II. Reading an execution trace
101 ----------------------------------------
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).
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).
118 o t: The thread number
120 o Action type: The type of operation performed
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)
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.
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.
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.]
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:
143 Each entry is indexed as CV[i], where
145 i = 0, 1, 2, ..., <number of threads>
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
152 See the following example trace:
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)
174 ------------------------------------------------------------------------------------
176 Now consider, for example, operation 10:
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:
183 CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
186 ----------------------------------------
188 ----------------------------------------
190 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
191 system. CACM, 21(7):558–565, July 1978.