From 6b87c110fbda87ccec4f58b1e292d5f9434c8691 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 13 Nov 2012 20:05:45 -0800 Subject: [PATCH] README: more edits, for -h info --- README | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/README b/README index 10af03d..e403c48 100644 --- a/README +++ b/README @@ -25,9 +25,29 @@ variable, for instance. Sample run instructions: - make - export LD_LIBRARY_PATH=. - # run test program +$ 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 -- 2.34.1