X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=README.md;h=f2a6380a332c8c940659de6e854dda12838afe63;hp=005f5121d7540025daaa11fd16859e29f74a0b4c;hb=251ac4b4bf3a9f2d3cfacc1e6618200ca1c431ac;hpb=a177614511b9244854659a8d5f304d3e912c1658 diff --git a/README.md b/README.md index 005f5121..f2a6380a 100644 --- a/README.md +++ b/README.md @@ -1,16 +1,23 @@ -C11Tester: A Fuzzer for C11 and C++11 Atomics +C11Tester: A Testing tool for C11 and C++11 Atomics ===================================================== -C11Tester is a fuzzer for C11/C++11 which randomly explores the +C11Tester is a testing tool for C11/C++11 which randomly explores the behaviors of code under the C/C++ memory model. 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.). -C11Tester should compile on Linux OSX. Instrumenting programs -requires using our LLVM pass. It likely can be ported to other \*NIX -flavors. +C11Tester compiles on Linux. Instrumenting programs requires using +our LLVM pass. It likely can be ported to other \*NIX flavors. + +Mailing List +------------ + +If you have questions, you can contact us at c11tester@googlegroups.com. + +You can sign up for the C11Tester mailing list at: + Getting Started @@ -18,11 +25,15 @@ Getting Started If you haven't done so already, you may download C11Tester using git: - git clone git://demsky.eecs.uci.edu/c11fuzzer.git + git clone git://plrg.eecs.uci.edu/c11tester.git Get the benchmarks (not required; distributed separately): - git clone git://demsky.eecs.uci.edu/concurrency-benchmarks.git + git clone git://plrg.eecs.uci.edu/c11concurrency-benchmarks.git + +Get the LLVM frontend using git and follow its directions to build: + + git clone git://plrg.eecs.uci.edu/c11llvm.git Compile the fuzzer: @@ -40,83 +51,32 @@ Useful Options > Verbose: show all executions and not just buggy ones. -`-u num` +`-x num` - > Value to provide to atomics loads from uninitialized memory locations. The - > default is 0, but this may cause some programs to throw exceptions - > (segfault) before the model checker prints a trace. + > Specify the number number of executions to run. Benchmarks ------------------- -Many simple tests are located in the `tests/` directory. You may also want to -try the larger benchmarks (distributed separately), which can be placed under -the `benchmarks/` directory. After building C11Tester, you can build and run -the benchmarks as follows: +Many simple tests are located in the `test/` directory. These are +manually instrumented and can just be run. -> make benchmarks -> cd benchmarks -> -> # run barrier test with fairness/memory liveness -> ./run.sh barrier/barrier -y -m 2 -> -> # Linux reader/write lock test with fairness/memory liveness -> ./run.sh linuxrwlocks/linuxrwlocks -y -m 2 -> -> # run all benchmarks and provide timing results -> ./bench.sh +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 simple tests. To do so, you -need to perform a few steps. - -First, because C11Tester 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. - -Second, because C11Tester must be able to manage your program for you, your -program should declare its main entry point as `user_main(int, char**)` rather -than `main(int, char**)`. +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. -Third, test programs must use the standard C11/C++11 library headers (see below -for supported APIs) and must compile against the versions provided in -C11Tester's `include/` directory. Notably, we only support C11 thread syntax -(`thrd_t`, etc. from ``). +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 may also use our included happens-before race detector by -including and utilizing the appropriate functions -(`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for storing/loading data -to/from non-atomic shared memory. - -C11Tester can also check boolean assertions in your test programs. Just -include `` and use the `MODEL_ASSERT()` macro in your test program. -C11Tester 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) 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. - - -### Supported C11/C++11 APIs ### - -To model-check multithreaded code properly, C11Tester needs to instrument any -concurrency-related API calls made in your code. Currently, we support parts of -the following thread-support libraries. The C versions can be used in either C -or C++. - -* ``, ``, `` -* `` -* `` -* `` - -Because we want to extend support to legacy (i.e., non-C++11) compilers, we do -not support some new C++11 features that can't be implemented in C++03 (e.g., -C++ ``). Reading an execution trace -------------------------- @@ -212,83 +172,14 @@ 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: -* An _infeasible_ execution is an execution which is not consistent with the - memory model. Such an execution can be considered overhead for the - model-checker, since it should never appear in practice. - * A _buggy_ execution is an execution in which C11Tester has found a real - bug: a data race, a deadlock, failure of a user-provided assertion, or an - uninitialized load, for instance. C11Tester will only report bugs in feasible - executions. - -* A _redundant_ execution is a feasible execution that is exploring the same - state space explored by a previous feasible execution. Such exploration is - another instance of overhead, so C11Tester terminates these executions as - soon as they are detected. C11Tester is mostly able to avoid such executions - but may encounter them if a fairness option is enabled. - -Now, we can examine the end-of-execution summary of one test program: - - $ ./run.sh test/rmwprog.o - + test/rmwprog.o - ******* Model-checking complete: ******* - Number of complete, bug-free executions: 6 - Number of redundant executions: 0 - Number of buggy executions: 0 - Number of infeasible executions: 29 - Total executions: 35 - -* _Number of complete, bug-free executions:_ these are feasible, non-buggy, and - non-redundant executions. They each represent different, legal behaviors you - can expect to see in practice. - -* _Number of redundant executions:_ these are feasible but redundant executions - that were terminated as soon as C11Tester noticed the redundancy. - -* _Number of buggy executions:_ these are feasible, buggy executions. These are - the trouble spots where your program is triggering a bug or assertion. - Ideally, this number should be 0. - -* _Number of infeasible executions:_ these are infeasible executions, - representing some of the overhead of model-checking. - -* _Total executions:_ the total number of executions explored by C11Tester. - Should be the sum of the above categories, since they are mutually exclusive. + 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 ------------------------ -* Many programs require some form of fairness in order to terminate in a finite - amount of time. C11Tester supports the `-y num` and `-f num` flags for these - cases. The `-y` option (yield-based fairness) is preferable, but it requires - careful usage of yields (i.e., `thrd_yield()`) in the test program. For - programs without proper `thrd_yield()`, you may consider using `-f` instead. - -* Deadlock detection: C11Tester can detect deadlocks. For instance, try the - following test program. - - > ./run.sh test/deadlock.o - - Deadlock detection currently detects when a thread is about to step into a - deadlock, without actually including the final step in the trace. But you can - examine the program to see the next step. - -* C11Tester has to speculatively explore many execution behaviors due to the - relaxed memory model, and many of these turn out to be infeasible (that is, - they cannot be legally produced by the memory model). C11Tester discards - these executions as soon as it identifies them (see the "Number of infeasible - executions" statistic); however, the speculation can occasionally cause - C11Tester to hit unexpected parts of the unit test program (causing a - division by 0, for instance). In such programs, you might consider running - C11Tester with the `-u num` option. - -* Related to the previous point, C11Tester may report more than one bug for a - particular candidate execution. This is because some bugs may not be - reportable until C11Tester has explored more of the program, and in the - time between initial discovery and final assessment of the bug, C11Tester may - discover another bug. - * Data races may be reported as multiple bugs, one for each byte-address of the data race in question. See, for example, this run: @@ -314,13 +205,16 @@ See Also The C11Tester project page: -> +> The C11Tester source and accompanying benchmarks on Gitweb: -> +> +> +> > -> +> + Contact @@ -341,6 +235,18 @@ Copyright © 2013 and 2019 Regents of the University of California. All righ 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 ----------