Sample run instructions:
+$ make
+$ export LD_LIBRARY_PATH=.
+$ ./test/userprog.o # Runs simple test program
+$ ./test/userprog.o -h # Prints help information
+Usage: <program name> [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
+-- Program arguments follow.
+
+
+Note that we also provide a series of benchmarks, placed under the benchmarks/
+directory. After building CDSChecker, you can build and run the benchmarks as
+follows:
+
+ cd benchmarks
make
- export LD_LIBRARY_PATH=.
- # run test program
+ ./run.sh barrier/barrier -f 10 -m 2 # runs barrier test with fairness/memory liveness
+ ./bench.sh <dir> # run all benchmarks twice, with timing results; all logged to <dir>