X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=README;h=3064ce64e3c8cfe1d64c984ce480f5191b0a6e6a;hp=f5ed857bca750a1785bb2b821264279c5d8f2f42;hb=7641eae45f89c0df9ba21d4ca43f1ebafdcb5bd8;hpb=11da849ab540fbcec939797a0c5ef17d651829e7 diff --git a/README b/README index f5ed857..3064ce6 100644 --- a/README +++ b/README @@ -1,27 +1,53 @@ **************************************** -CDSChecker Readme + CDSChecker Readme **************************************** -This is an evaluation-only version of CDSChecker. Please do not distribute. +Copyright (c) 2013 Regents of the University of California. All rights reserved. -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 distributed under the GPL v2. See the LICENSE file for details. -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 ). +This README is divided into sections as follows: -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. + I. Overview + II. Basic build and run + III. Running your own code + IV. Reading an execution trace +Appendix + A. References -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. +---------------------------------------- + I. Overview +---------------------------------------- + +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): + + 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. + +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: @@ -29,26 +55,54 @@ $ make $ export LD_LIBRARY_PATH=. $ ./test/userprog.o # Runs simple test program $ ./test/userprog.o -h # Prints help information -Usage: [MC_OPTIONS] -- [PROGRAM ARGUMENTS] - -Options: --h Display this help message and exit --m Maximum times a thread can read from the same write - while other writes exist. Default: 0 --M Maximum number of future values that can be sent to - the same read. Default: 0 --s Maximum actions that the model checker will wait for - a write from the future past the expected number of - actions. Default: 100 --S Future value expiration sloppiness. Default: 10 --f Specify a fairness window in which actions that are - enabled sufficiently many times should receive - priority for execution. Default: 0 --e Enabled count. Default: 1 --b Upper length bound. Default: 0 --v Print verbose execution information. --y CHESS like yield based fairness. Default: 0 --- Program arguments follow. +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 Note that we also provide a series of benchmarks (distributed separately), @@ -57,5 +111,133 @@ you can build and run the benchmarks as follows: cd benchmarks make - ./run.sh barrier/barrier -f 10 -m 2 # runs barrier test with fairness/memory liveness - ./bench.sh # run all benchmarks twice, with timing results; all logged to + ./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 +non-atomic shared memory. + +CDSChecker can also check boolean assertions in your test programs. Just +include 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) 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. + +---------------------------------------- + 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 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). + +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 + this represents the execution order, not necessarily any other order (e.g., + modification order or reads-from). + + o t: The thread number + + o Action type: The type of operation performed + + o MO: The memory-order for this operation (i.e., memory_order_XXX, where XXX is + relaxed, release, acquire, rel_acq, or seq_cst) + + o 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. + + 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, 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), + 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.] + + o CV: The clock vector, encapsulating the happens-before relation (see our + paper, or the C/C++ memory model itself). We use a Lamport-style clock vector + similar to [1]. The "clock" is just the sequence number (#). The clock vector + can be read as follows: + + Each entry is indexed as CV[i], where + + i = 0, 1, 2, ..., + + 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 + operations. + +See the following example trace: + +------------------------------------------------------------------------------------ +# 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: + +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 +"0", which was written by the 2nd operation in the execution order. Its clock +vector consists of the following values: + + CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10 + + +---------------------------------------- + A. References +---------------------------------------- + +[1] L. Lamport. Time, clocks, and the ordering of events in a distributed + system. CACM, 21(7):558–565, July 1978.