projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
4203bde
)
model: add infeasibility debugging
author
Brian Norris
<banorris@uci.edu>
Tue, 18 Sep 2012 19:00:30 +0000
(12:00 -0700)
committer
Brian Norris
<banorris@uci.edu>
Tue, 18 Sep 2012 19:00:30 +0000
(12:00 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 954c07dd6dacdfc9473a4aa3f5e0a2f8db38bcbf..38c5d4a9396f82bde9b8341fac00f8b2d8dc63a6 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-500,11
+500,24
@@
bool ModelChecker::isfeasible() {
/** @returns whether the current partial trace is feasible other than
* multiple RMW reading from the same store. */
bool ModelChecker::isfeasibleotherthanRMW() {
/** @returns whether the current partial trace is feasible other than
* multiple RMW reading from the same store. */
bool ModelChecker::isfeasibleotherthanRMW() {
+ if (DBG_ENABLED()) {
+ if (mo_graph->checkForCycles())
+ DEBUG("Infeasible: modification order cycles\n");
+ if (failed_promise)
+ DEBUG("Infeasible: failed promise\n");
+ if (too_many_reads)
+ DEBUG("Infeasible: too many reads\n");
+ if (promises_expired())
+ DEBUG("Infeasible: promises expired\n");
+ }
return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
}
/** Returns whether the current completed trace is feasible. */
bool ModelChecker::isfinalfeasible() {
return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
}
/** Returns whether the current completed trace is feasible. */
bool ModelChecker::isfinalfeasible() {
+ if (DBG_ENABLED() && promises->size() != 0)
+ DEBUG("Infeasible: unrevolved promises\n");
+
return isfeasible() && promises->size() == 0;
}
return isfeasible() && promises->size() == 0;
}