projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
e678e5e
)
README.md: add more fairness notes
author
Brian Norris
<banorris@uci.edu>
Wed, 14 Aug 2013 06:29:20 +0000
(23:29 -0700)
committer
Brian Norris
<banorris@uci.edu>
Wed, 14 Aug 2013 06:29:20 +0000
(23:29 -0700)
README.md
patch
|
blob
|
history
diff --git
a/README.md
b/README.md
index c85a727db920d6fd8758188c0c285960eb436536..023a73767d1b3c4a29a1735db887946c846135d3 100644
(file)
--- a/
README.md
+++ b/
README.md
@@
-85,7
+85,9
@@
Useful Options
`-f num`
`-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`
`-v`
@@
-324,6
+326,12
@@
Now, we can examine the end-of-execution summary of one test program:
Other Notes and Pitfalls
------------------------
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.
* Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
following test program.