X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=README.md;h=d5838cd98be0a1f84058fc092bdeec4ab8c9ebf1;hb=c7a6544c3f19d8c4d71b82871c832a866f8dbb79;hp=c85a727db920d6fd8758188c0c285960eb436536;hpb=278ff43e5570a6cd8a42aa03070c5b59d079a999;p=model-checker.git diff --git a/README.md b/README.md index c85a727..d5838cd 100644 --- a/README.md +++ b/README.md @@ -37,12 +37,15 @@ Getting Started --------------- If you haven't done so already, you may download CDSChecker using -[git](http://git-scm.com/) (for those without git, snapshots can be found at the -Gitweb URLs below): +[git](http://git-scm.com/): git clone git://demsky.eecs.uci.edu/model-checker.git -Get the benchmarks (not required; distributed separately): +Source code can also be downloaded via the snapshot links on Gitweb (found in +the __See Also__ section). + +Get the benchmarks (not required; distributed separately), placing them as a +subdirectory under the `model-checker` directory: cd model-checker git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks @@ -85,7 +88,9 @@ Useful Options `-f num` - > Turns on alternative fairness support (less desirable than `-y`). + > Turns on alternative fairness support (less desirable than `-y`). A + > necessary alternative for some programs that do not support yield-based + > fairness properly. `-v` @@ -324,6 +329,12 @@ Now, we can examine the end-of-execution summary of one test program: Other Notes and Pitfalls ------------------------ +* Many programs require some form of fairness in order to terminate in a finite + amount of time. CDSChecker supports the `-y num` and `-f num` flags for these + cases. The `-y` option (yield-based fairness) is preferable, but it requires + careful usage of yields (i.e., `thrd_yield()`) in the test program. For + programs without proper `thrd_yield()`, you may consider using `-f` instead. + * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the following test program.