The model checking algorithm is described in more detail in this paper
(currently under review):
- [http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf](http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf)
+ <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
It is designed to support unit tests on concurrent data structure written using
C11/C++11 atomics.
Other references can be found at the main project page:
- [http://demsky.eecs.uci.edu/c11modelchecker.php](http://demsky.eecs.uci.edu/c11modelchecker.php)
+ <http://demsky.eecs.uci.edu/c11modelchecker.php>
Basic build and run
-------------------
Note that we also provide a series of benchmarks (distributed separately),
-which can be placed under the benchmarks/ directory. After building CDSChecker,
+which can be placed under the `benchmarks/` directory. After building CDSChecker,
you can build and run the benchmarks as follows:
cd benchmarks
make
./run.sh barrier/barrier -y -m 2 # runs barrier test with fairness/memory liveness
- ./bench.sh # run all benchmarks twice, with timing results
+ ./bench.sh # run all benchmarks and provide timing results
Running your own code
---------------------
-We provide several test and sample programs under the test/ directory, which
+We provide several test and sample programs under the `test/` directory, which
should compile and run with no trouble. Of course, you likely want to test your
own code. To do so, you need to perform a few steps.
Reading an execution trace
--------------------------
-When CDSChecker detects a bug in your program (or when run with the --verbose
+When CDSChecker detects a bug in your program (or when run with the `--verbose`
flag), it prints the output of the program run (STDOUT) along with some summary
trace information for the execution in question. The trace is given as a
sequence of lines, where each line represents an operation in the execution
* Action type: The type of operation performed
- * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where XXX is
- relaxed, release, acquire, rel_acq, or seq_cst)
+ * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
+ `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
* Location: The memory location on which this operation is operating. This is
well-defined for atomic write/read/RMW, but other operations are subject to
* Value: For reads/writes/RMW, the value returned by the operation. Note that
for RMW, this is the value that is *read*, not the value that was *written*.
For other operations, 'value' may have some CDSChecker-internal meaning, or
- it may simply be a don't-care (such as 0xdeadbeef).
+ it may simply be a don't-care (such as `0xdeadbeef`).
* Rf: For reads, the sequence number of the operation from which it reads.
[Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
- as printed during --verbose execution, reads may not be resolved and so may
+ as printed during `--verbose` execution, reads may not be resolved and so may
have Rf=? or Rf=Px, where x is a promised future value.]
* CV: The clock vector, encapsulating the happens-before relation (see our
Now consider, for example, operation 10:
This is the 10th operation in the execution order. It is an atomic read-relaxed
-operation performed by thread 3 at memory address 0x601068. It reads the value
+operation performed by thread 3 at memory address `0x601068`. It reads the value
"0", which was written by the 2nd operation in the execution order. Its clock
vector consists of the following values:
projects / cdsspec-compiler.git / blobdiff