X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=README;h=e403c487616d30438edb5c71dfe9bbf56892e572;hp=de6bbc9f75593abddc29cec6d762a36aeb35a51d;hb=6b87c110fbda87ccec4f58b1e292d5f9434c8691;hpb=dd56df466206a5f34f1d9b1777d1f076f7c33e0f diff --git a/README b/README index de6bbc9..e403c48 100644 --- a/README +++ b/README @@ -25,6 +25,35 @@ variable, for instance. Sample run instructions: +$ 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 +-- 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 # run all benchmarks twice, with timing results; all logged to