1 ****************************************
3 ****************************************
5 Copyright (c) 2013 Regents of the University of California. All rights reserved.
7 CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
9 This README is divided into sections as follows:
12 II. Basic build and run
13 III. Running your own code
14 IV. Reading an execution trace
18 ----------------------------------------
20 ----------------------------------------
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):
28 http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf
30 It is designed to support unit tests on concurrent data structure written using
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).
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.
44 Other references can be found at the main project page:
46 http://demsky.eecs.uci.edu/c11modelchecker.php
48 ----------------------------------------
49 II. Basic build and run
50 ----------------------------------------
52 Sample run instructions:
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
62 Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
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.
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.
72 -M, --maxfv=NUM Maximum number of future values that can be sent to
75 -s, --maxfvdelay=NUM Maximum actions that the model checker will wait for
76 a write from the future past the expected number
79 -S, --fvslop=NUM Future value expiration sloppiness.
81 -y, --yield Enable CHESS-like yield-based fairness support.
83 -Y, --yieldblock Prohibit an execution from running a yield.
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).
89 -e, --enabled=COUNT Enabled count.
91 -b, --bound=MAX Upper length bound.
93 -v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:
94 0 is quiet; 1 is noisy; 2 is noisier.
96 -u, --uninitialized=VALUE Return VALUE any load which may read from an
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.
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:
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
117 ----------------------------------------
118 III. Running your own code
119 ----------------------------------------
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.
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.
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>).
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 from non-atomic shared memory.
139 Test programs should be compiled against our shared library (libmodel.so) using
140 the headers in the include/ directory. Then the shared library must be made
141 available to the dynamic linker, using the LD_LIBRARY_PATH environment
142 variable, for instance.
144 ----------------------------------------
145 IV. Reading an execution trace
146 ----------------------------------------
148 When CDSChecker detects a bug in your program (or when run with the --verbose
149 flag), it prints the output of the program run (STDOUT) along with some summary
150 trace information for the execution in question. The trace is given as a
151 sequence of lines, where each line represents an operation in the execution
152 trace. These lines are ordered by the order in which they were run by CDSChecker
153 (i.e., the "execution order"), which does not necessarily align with the "order"
154 of the values observed (i.e., the modification order or the reads-from
157 The following list describes each of the columns in the execution trace output:
159 o #: The sequence number within the execution. That is, sequence number "9"
160 means the operation was the 9th operation executed by CDSChecker. Note that
161 this represents the execution order, not necessarily any other order (e.g.,
162 modification order or reads-from).
164 o t: The thread number
166 o Action type: The type of operation performed
168 o MO: The memory-order for this operation (i.e., memory_order_XXX, where XXX is
169 relaxed, release, acquire, rel_acq, or seq_cst)
171 o Location: The memory location on which this operation is operating. This is
172 well-defined for atomic write/read/RMW, but other operations are subject to
173 CDSChecker implementation details.
175 o Value: For reads/writes/RMW, the value returned by the operation. Note that
176 for RMW, this is the value that is *read*, not the value that was *written*.
177 For other operations, 'value' may have some CDSChecker-internal meaning, or
178 it may simply be a don't-care (such as 0xdeadbeef).
180 o Rf: For reads, the sequence number of the operation from which it reads.
181 [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
182 as printed during --verbose execution, reads may not be resolved and so may
183 have Rf=? or Rf=Px, where x is a promised future value.]
185 o CV: The clock vector, encapsulating the happens-before relation (see our
186 paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
187 similar to [1]. The "clock" is just the sequence number (#). The clock vector
188 can be read as follows:
190 Each entry is indexed as CV[i], where
192 i = 0, 1, 2, ..., <number of threads>
194 So for any thread i, we say CV[i] is the sequence number of the most recent
195 operation in thread i such that operation i happens-before this operation.
196 Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
199 See the following example trace:
201 ------------------------------------------------------------------------------------
202 # t Action type MO Location Value Rf CV
203 ------------------------------------------------------------------------------------
204 1 1 thread start seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 1)
205 2 1 init atomic relaxed 0x601068 0 ( 0, 2)
206 3 1 init atomic relaxed 0x60106c 0 ( 0, 3)
207 4 1 thread create seq_cst 0x7f68fe51c710 0x7f68fe51c6e0 ( 0, 4)
208 5 2 thread start seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 5)
209 6 2 atomic read relaxed 0x60106c 0 3 ( 0, 4, 6)
210 7 1 thread create seq_cst 0x7f68fe51c720 0x7f68fe51c6e0 ( 0, 7)
211 8 3 thread start seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 8)
212 9 2 atomic write relaxed 0x601068 0 ( 0, 4, 9)
213 10 3 atomic read relaxed 0x601068 0 2 ( 0, 7, 0, 10)
214 11 2 thread finish seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 11)
215 12 3 atomic write relaxed 0x60106c 0x2a ( 0, 7, 0, 12)
216 13 1 thread join seq_cst 0x7f68ff11ebc0 0x2 ( 0, 13, 11)
217 14 3 thread finish seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 14)
218 15 1 thread join seq_cst 0x7f68ff11efc0 0x3 ( 0, 15, 11, 14)
219 16 1 thread finish seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 16, 11, 14)
221 ------------------------------------------------------------------------------------
223 Now consider, for example, operation 10:
225 This is the 10th operation in the execution order. It is an atomic read-relaxed
226 operation performed by thread 3 at memory address 0x601068. It reads the value
227 "0", which was written by the 2nd operation in the execution order. Its clock
228 vector consists of the following values:
230 CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
233 ----------------------------------------
235 ----------------------------------------
237 [1] L. Lamport. Time, clocks, and the ordering of events in a distributed
238 system. CACM, 21(7):558–565, July 1978.