From: Brian Norris Date: Sun, 2 Jun 2013 00:06:33 +0000 (-0700) Subject: README: convert to Markdown format X-Git-Tag: oopsla2013-final~15^2~2 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=402caea290ab08ddb12cb79cbf73ec7e97066863 README: convert to Markdown format Now we can easily generate an HTML version, while retaining readability as a simple text file. --- diff --git a/.gitignore b/.gitignore index 4acd010..47ba0d5 100644 --- a/.gitignore +++ b/.gitignore @@ -12,3 +12,4 @@ /tags /doc/docs /benchmarks +/README.html diff --git a/Makefile b/Makefile index 0ad9fa6..b7fd60b 100644 --- a/Makefile +++ b/Makefile @@ -18,15 +18,20 @@ endif TESTS_DIR := test -all: $(LIB_SO) tests +MARKDOWN := doc/Markdown/Markdown.pl + +all: $(LIB_SO) tests README.html debug: CPPFLAGS += -DCONFIG_DEBUG debug: all PHONY += docs -docs: *.c *.cc *.h +docs: *.c *.cc *.h README.html doxygen +README.html: README.md + $(MARKDOWN) $< > $@ + $(LIB_SO): $(OBJECTS) $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS) 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 diff --git a/README.md b/README.md new file mode 100644 index 0000000..37eb962 --- /dev/null +++ b/README.md @@ -0,0 +1,240 @@ +CDSChecker Readme +================= + +Copyright © 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: + + * Overview + * Basic build and run + * Running your own code + * Reading an execution trace + * References + +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](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](http://demsky.eecs.uci.edu/c11modelchecker.php) + +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 + +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. + +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: + + * \#: 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). + + * t: The thread number + + * Action type: The type of operation performed + + * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where XXX is + relaxed, release, acquire, rel_acq, or seq_cst) + + * 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. + + * 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). + + * 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.] + + * 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 + + +References +---------- + +[1] L. Lamport. Time, clocks, and the ordering of events in a distributed + system. CACM, 21(7):558-565, July 1978.