+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 <threads.h>),
+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