X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=README;h=42061c01a1c70097d1e4579f29a5adf40abdec95;hb=402caea290ab08ddb12cb79cbf73ec7e97066863;hp=3064ce64e3c8cfe1d64c984ce480f5191b0a6e6a;hpb=7641eae45f89c0df9ba21d4ca43f1ebafdcb5bd8;p=model-checker.git diff --git a/README b/README deleted file mode 100644 index 3064ce6..0000000 --- a/README +++ /dev/null @@ -1,243 +0,0 @@ -**************************************** - CDSChecker Readme -**************************************** - -Copyright (c) 2013 Regents of the University of California. All rights reserved. - -CDSChecker is distributed under the GPL v2. See the LICENSE file for details. - -This README is divided into sections as follows: - - I. Overview - II. Basic build and run - III. Running your own code - IV. Reading an execution trace -Appendix - A. References - ----------------------------------------- - 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: - -$ 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 - - -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 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. diff --git a/README b/README new file mode 120000 index 0000000..42061c0 --- /dev/null +++ b/README @@ -0,0 +1 @@ +README.md \ No newline at end of file