From 16b2fd3b0f423ce6ed9fa878ed35eb2d68ff5934 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 31 May 2013 15:32:39 -0700 Subject: [PATCH] README: improve sections, provide better intro --- README | 90 ++++++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 66 insertions(+), 24 deletions(-) diff --git a/README b/README index 93d9723..89f9e24 100644 --- a/README +++ b/README @@ -9,31 +9,45 @@ CDSChecker is distributed under the GPL v2. This README is divided into sections as follows: I. Overview - II. Reading an execution trace + II. Basic build and run + III. Running your own code + IV. Reading an execution trace +Appendix A. References ---------------------------------------- I. Overview ---------------------------------------- -CDSChecker compiles as a dynamically-linked shared library by simply running -'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM -(clang/clang++) and GCC. +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): -Test programs should use the standard C11/C++11 library headers -(/, , , ) 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 ). + http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf -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 loading/storing data from/to -from non-atomic shared memory. +It is designed to support unit tests on concurrent data structure written using +C11/C++11 atomics. -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. +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 ), +because C++ threads require features which are only available to a C++11 +compiler (and we want to support others, at least for now). + +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. + +Other references can be found at the main project page: + + http://demsky.eecs.uci.edu/c11modelchecker.php + +---------------------------------------- + II. Basic build and run +---------------------------------------- Sample run instructions: @@ -95,20 +109,47 @@ you can build and run the benchmarks as follows: ./run.sh barrier/barrier -y -m 2 # runs barrier test with fairness/memory liveness ./bench.sh # run all benchmarks twice, with timing results +---------------------------------------- + III. Running your own code +---------------------------------------- + +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. + +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. + +Next, test programs should use the standard C11/C++11 library headers +(/, , , ) 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 ). + +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 loading/storing data from/to +from non-atomic shared memory. + +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. ---------------------------------------- - II. Reading an execution trace + IV. Reading an execution trace ---------------------------------------- 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. 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 (i.e., the "execution order"), which -does not necessarily align with the "order" of the values observed (i.e., the -modification order and the reads-from relation). +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 +(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). -Columns: +The following list describes each of the columns in the execution trace output: o #: The sequence number within the execution. That is, sequence number "9" means the operation was the 9th operation executed by CDSChecker. Note that @@ -128,7 +169,8 @@ Columns: o 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. + For other operations, 'value' may have some CDSChecker-internal meaning, or + it may simply be a don't-care (such as 0xdeadbeef). o Rf: For reads, the sequence number of the operation from which it reads. [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE), -- 2.34.1