-CDSChecker Readme
-=================
+C11Tester: A Testing tool for C11 and C++11 Atomics
+=====================================================
-Copyright © 2013 Regents of the University of California. All rights reserved.
+C11Tester is a testing tool for C11/C++11 which randomly explores the
+behaviors of code under the C/C++ memory model.
-CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
+C11Tester is constructed as a dynamically-linked shared library which
+implements the C and C++ atomic types and portions of the other thread-support
+libraries of C/C++ (e.g., std::atomic, std::mutex, etc.).
-This README is divided into sections as follows:
+C11Tester compiles on Linux. Instrumenting programs requires using
+our LLVM pass. It likely can be ported to other \*NIX flavors.
- * Overview
- * Basic build and run
- * Running your own code
- * Reading an execution trace
- * References
+Mailing List
+------------
-Overview
---------
+If you have questions, you can contact us at c11tester@googlegroups.com.
-CDSChecker is a model checker for C11/C++11 exhaustively explores the behaviors
-of code under the C11/C++11 memory model. It uses partial order reduction to
-eliminate redundant executions to significantly shrink the state space.
-The model checking algorithm is described in more detail in this paper
-(currently under review):
+You can sign up for the C11Tester mailing list at:
+<https://groups.google.com/forum/#!forum/c11tester>
- <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.
+Getting Started
+---------------
-CDSChecker is constructed as a dynamically-linked shared library which
-implements the C and C++ atomic types and portions of the other thread-support
-libraries of C/C++ (e.g., std::atomic, std::mutex, etc.). Notably, we only
-support the C version of threads (i.e., `thrd_t` and similar, from `<threads.h>`),
-because C++ threads require features which are only available to a C++11
-compiler (and we want to support others, at least for now).
+If you haven't done so already, you may download C11Tester using git:
-CDSChecker should compile on Linux and Mac OSX with no dependencies and has been
-tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX
-flavors. We have not attempted to port to Windows.
+ git clone git://plrg.eecs.uci.edu/c11tester.git
-Other references can be found at the main project page:
+Get the benchmarks (not required; distributed separately):
- <http://demsky.eecs.uci.edu/c11modelchecker.php>
+ git clone git://plrg.eecs.uci.edu/c11concurrency-benchmarks.git
-Basic build and run
--------------------
+Get the LLVM frontend using git and follow its directions to build:
-Sample run instructions:
-
-<pre>
-$ make
-$ export LD_LIBRARY_PATH=.
-$ ./test/userprog.o # Runs simple test program
-$ ./test/userprog.o -h # Prints help information
-Copyright (c) 2013 Regents of the University of California. All rights reserved.
-Distributed under the GPLv2
-Written by Brian Norris and Brian Demsky
-
-Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
-
-MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments
-provided after the `--' (the PROGRAM ARGS) are passed to the user program.
-
-Model-checker options:
--h, --help Display this help message and exit
--m, --liveness=NUM Maximum times a thread can read from the same write
- while other writes exist.
- Default: 0
--M, --maxfv=NUM Maximum number of future values that can be sent to
- the same read.
- Default: 0
--s, --maxfvdelay=NUM Maximum actions that the model checker will wait for
- a write from the future past the expected number
- of actions.
- Default: 6
--S, --fvslop=NUM Future value expiration sloppiness.
- Default: 4
--y, --yield Enable CHESS-like yield-based fairness support.
- Default: disabled
--Y, --yieldblock Prohibit an execution from running a yield.
- Default: disabled
--f, --fairness=WINDOW Specify a fairness window in which actions that are
- enabled sufficiently many times should receive
- priority for execution (not recommended).
- Default: 0
--e, --enabled=COUNT Enabled count.
- Default: 1
--b, --bound=MAX Upper length bound.
- Default: 0
--v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:
- 0 is quiet; 1 is noisy; 2 is noisier.
- Default: 0
--u, --uninitialized=VALUE Return VALUE any load which may read from an
- uninitialized atomic.
- Default: 0
--t, --analysis=NAME Use Analysis Plugin.
--o, --options=NAME Option for previous analysis plugin.
- -o help for a list of options
- -- Program arguments follow.
-
-Analysis plugins:
-SC
-</pre>
-
-
-Note that we also provide a series of benchmarks (distributed separately),
-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 and provide timing results
+ git clone git://plrg.eecs.uci.edu/c11llvm.git
-Running your own code
----------------------
+Compile the fuzzer:
+
+ make
+
+To see the help message on how to run C11Tester, execute:
+
+ ./run.sh -h
+
+
+Useful Options
+--------------
+
+`-v`
-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.
+ > Verbose: show all executions and not just buggy ones.
-First, because CDSChecker executes your program dozens (if not hundreds or
-thousands) of times, you will have the most success if your code is written as a
-unit test and not as a full-blown program.
+`-x num`
-Next, test programs should use the standard C11/C++11 library headers
-(`<atomic>`/`<stdatomic.h>`, `<mutex>`, `<condition_variable>`, `<thread.h>`) and must
-name their main routine as `user_main(int, char**)` rather than `main(int, char**)`.
-We only support C11 thread syntax (`thrd_t`, etc. from `<thread.h>`).
+ > Specify the number number of executions to run.
-Test programs may also use our included happens-before race detector by
-including <librace.h> and utilizing the appropriate functions
-(`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for loading/storing data from/to
-non-atomic shared memory.
+Benchmarks
+-------------------
+
+Many simple tests are located in the `test/` directory. These are
+manually instrumented and can just be run.
+
+You may also want to try the larger benchmarks (distributed
+separately). These require LLVM to instrument.
+
+
+Running your own code
+---------------------
+
+You likely want to test your own code, not just our tests. You will
+likely need to use our LLVM pass to instrument your program. You will
+have to modify your build environment to do this.
-CDSChecker can also check boolean assertions in your test programs. Just
-include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
-CDSChecker will report a bug in any possible execution in which the argument to
-`MODEL_ASSERT()` evaluates to false (that is, 0).
+Test programs should be compiled against our shared library
+(libmodel.so). Then the shared library must be made available to the
+dynamic linker, using the `LD_LIBRARY_PATH` environment variable, for
+instance.
-Test programs should be compiled against our shared library (libmodel.so) using
-the headers in the `include/` directory. Then the shared library must be made
-available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
-variable, for instance.
Reading an execution trace
--------------------------
-When CDSChecker detects a bug in your program (or when run with the `--verbose`
+When C11Tester 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
-trace. These lines are ordered by the order in which they were run by CDSChecker
+trace. These lines are ordered by the order in which they were run by C11Tester
(i.e., the "execution order"), which does not necessarily align with the "order"
of the values observed (i.e., the modification order or the reads-from
relation).
The following list describes each of the columns in the execution trace output:
* \#: The sequence number within the execution. That is, sequence number "9"
- means the operation was the 9th operation executed by CDSChecker. Note that
+ means the operation was the 9th operation executed by C11Tester. Note that
this represents the execution order, not necessarily any other order (e.g.,
modification order or reads-from).
* 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
- CDSChecker implementation details.
+ C11Tester implementation details.
* 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
+ For other operations, 'value' may have some C11Tester-internal meaning, or
it may simply be a don't-care (such as `0xdeadbeef`).
* Rf: For reads, the sequence number of the operation from which it reads.
So for any thread i, we say CV[i] is the sequence number of the most recent
operation in thread i such that operation i happens-before this operation.
- Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
+ Notably, thread 0 is reserved as a dummy thread for certain C11Tester
operations.
See the following example trace:
-<pre>
-------------------------------------------------------------------------------------
-# t Action type MO Location Value Rf CV
-------------------------------------------------------------------------------------
-1 1 thread start seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 1)
-2 1 init atomic relaxed 0x601068 0 ( 0, 2)
-3 1 init atomic relaxed 0x60106c 0 ( 0, 3)
-4 1 thread create seq_cst 0x7f68fe51c710 0x7f68fe51c6e0 ( 0, 4)
-5 2 thread start seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 5)
-6 2 atomic read relaxed 0x60106c 0 3 ( 0, 4, 6)
-7 1 thread create seq_cst 0x7f68fe51c720 0x7f68fe51c6e0 ( 0, 7)
-8 3 thread start seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 8)
-9 2 atomic write relaxed 0x601068 0 ( 0, 4, 9)
-10 3 atomic read relaxed 0x601068 0 2 ( 0, 7, 0, 10)
-11 2 thread finish seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 11)
-12 3 atomic write relaxed 0x60106c 0x2a ( 0, 7, 0, 12)
-13 1 thread join seq_cst 0x7f68ff11ebc0 0x2 ( 0, 13, 11)
-14 3 thread finish seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 14)
-15 1 thread join seq_cst 0x7f68ff11efc0 0x3 ( 0, 15, 11, 14)
-16 1 thread finish seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 16, 11, 14)
-HASH 4073708854
-------------------------------------------------------------------------------------
-</pre>
+ ------------------------------------------------------------------------------------
+ # t Action type MO Location Value Rf CV
+ ------------------------------------------------------------------------------------
+ 1 1 thread start seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 1)
+ 2 1 init atomic relaxed 0x601068 0 ( 0, 2)
+ 3 1 init atomic relaxed 0x60106c 0 ( 0, 3)
+ 4 1 thread create seq_cst 0x7f68fe51c710 0x7f68fe51c6e0 ( 0, 4)
+ 5 2 thread start seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 5)
+ 6 2 atomic read relaxed 0x60106c 0 3 ( 0, 4, 6)
+ 7 1 thread create seq_cst 0x7f68fe51c720 0x7f68fe51c6e0 ( 0, 7)
+ 8 3 thread start seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 8)
+ 9 2 atomic write relaxed 0x601068 0 ( 0, 4, 9)
+ 10 3 atomic read relaxed 0x601068 0 2 ( 0, 7, 0, 10)
+ 11 2 thread finish seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 11)
+ 12 3 atomic write relaxed 0x60106c 0x2a ( 0, 7, 0, 12)
+ 13 1 thread join seq_cst 0x7f68ff11ebc0 0x2 ( 0, 13, 11)
+ 14 3 thread finish seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 14)
+ 15 1 thread join seq_cst 0x7f68ff11efc0 0x3 ( 0, 15, 11, 14)
+ 16 1 thread finish seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 16, 11, 14)
+ HASH 4073708854
+ ------------------------------------------------------------------------------------
Now consider, for example, operation 10:
CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
+End of Execution Summary
+------------------------
+
+C11Tester prints summary statistics at the end of each execution. These
+summaries are based off of a few different properties of an execution, which we
+will break down here:
+
+* A _buggy_ execution is an execution in which C11Tester has found a real
+ bug: a data race, a deadlock, or a failure of a user-provided assertion.
+ C11Tester will only report bugs in feasible executions.
+
+
+Other Notes and Pitfalls
+------------------------
+
+* Data races may be reported as multiple bugs, one for each byte-address of the
+ data race in question. See, for example, this run:
+
+ $ ./run.sh test/releaseseq.o
+ ...
+ Bug report: 4 bugs detected
+ [BUG] Data race detected @ address 0x601078:
+ Access 1: write in thread 2 @ clock 4
+ Access 2: read in thread 3 @ clock 9
+ [BUG] Data race detected @ address 0x601079:
+ Access 1: write in thread 2 @ clock 4
+ Access 2: read in thread 3 @ clock 9
+ [BUG] Data race detected @ address 0x60107a:
+ Access 1: write in thread 2 @ clock 4
+ Access 2: read in thread 3 @ clock 9
+ [BUG] Data race detected @ address 0x60107b:
+ Access 1: write in thread 2 @ clock 4
+ Access 2: read in thread 3 @ clock 9
+
+
+See Also
+--------
+
+The C11Tester project page:
+
+> <http://demsky.eecs.uci.edu/c11tester.html>
+
+The C11Tester source and accompanying benchmarks on Gitweb:
+
+> <http://plrg.eecs.uci.edu/git/?p=c11tester.git>
+>
+> <http://plrg.eecs.uci.edu/git/?p=c11llvm.git>
+>
+> <http://plrg.eecs.uci.edu/git/?p=c11concurrency-benchmarks.git>
+
+
+
+Contact
+-------
+
+Please feel free to contact us for more information. Bug reports are welcome,
+and we are happy to hear from our users. We are also very interested to know if
+C11Tester catches bugs in your programs.
+
+Contact Weiyu Luo at <weiyul7@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
+
+
+Copyright
+---------
+
+Copyright © 2013 and 2019 Regents of the University of California. All rights reserved.
+
+C11Tester is distributed under the GPL v2. See the LICENSE file for details.
+
+
+Acknowledgments
+---------------
+
+This material is based upon work supported by the National Science
+Foundation under Grant Numbers 1740210 and 1319786 and Google Research
+awards.
+
+Any opinions, findings, and conclusions or recommendations expressed in
+this material are those of the author(s) and do not necessarily reflect
+the views of the National Science Foundation.
+
References
----------
projects / c11tester.git / blobdiff