From: Brian Norris <banorris@uci.edu>
Date: Wed, 9 Jan 2013 23:54:04 +0000 (-0800)
Subject: model: fixup "infeasible" messages
X-Git-Tag: oopsla2013~363
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=7372f39c67d6e4ea2dc142fca9c1b61c590af94c;hp=b69a6cb48fdd66361adae1d3bbe0c0a743830966

model: fixup "infeasible" messages

These messages should be much more compact and targeted. Currently, we
either get no infeasibility messages (when verbose=0) or we get messages
every time is_infeasible() is executed. Neither is helpful for debugging,
since the infeasibility may be temporary, as we choose a new path for
execution on the fly. So instead, just print the infeasibility message
at the end of infeasible executions.

Also, rather than spread the messages across multiple lines, just put
them together into a single string.
---

diff --git a/model.cc b/model.cc
index 88d5e71..f2d40fe 100644
--- a/model.cc
+++ b/model.cc
@@ -1339,15 +1339,39 @@ bool ModelChecker::isfeasibleprefix() const
 	return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
 }
 
+/**
+ * Print disagnostic information about an infeasible execution
+ * @param prefix A string to prefix the output with; if NULL, then a default
+ * message prefix will be provided
+ */
+void ModelChecker::print_infeasibility(const char *prefix) const
+{
+	char buf[100];
+	char *ptr = buf;
+	if (mo_graph->checkForRMWViolation())
+		ptr += sprintf(ptr, "[RMW atomicity]");
+	if (mo_graph->checkForCycles())
+		ptr += sprintf(ptr, "[mo cycle]");
+	if (priv->failed_promise)
+		ptr += sprintf(ptr, "[failed promise]");
+	if (priv->too_many_reads)
+		ptr += sprintf(ptr, "[too many reads]");
+	if (priv->bad_synchronization)
+		ptr += sprintf(ptr, "[bad sw ordering]");
+	if (promises_expired())
+		ptr += sprintf(ptr, "[promise expired]");
+	if (promises->size() != 0)
+		ptr += sprintf(ptr, "[unrevolved promise]");
+	if (ptr != buf)
+		model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
+}
+
 /**
  * Returns whether the current completed trace is feasible, except for pending
  * release sequences.
  */
 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
 {
-	if (DBG_ENABLED() && promises->size() != 0)
-		DEBUG("Infeasible: unrevolved promises\n");
-
 	return !is_infeasible() && promises->size() == 0;
 }
 
@@ -1359,9 +1383,6 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-	if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
-		DEBUG("Infeasible: RMW violation\n");
-
 	return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
 }
 
@@ -1375,18 +1396,6 @@ bool ModelChecker::is_infeasible() const
  * */
 bool ModelChecker::is_infeasible_ignoreRMW() const
 {
-	if (DBG_ENABLED()) {
-		if (mo_graph->checkForCycles())
-			DEBUG("Infeasible: modification order cycles\n");
-		if (priv->failed_promise)
-			DEBUG("Infeasible: failed promise\n");
-		if (priv->too_many_reads)
-			DEBUG("Infeasible: too many reads\n");
-		if (priv->bad_synchronization)
-			DEBUG("Infeasible: bad synchronization ordering\n");
-		if (promises_expired())
-			DEBUG("Infeasible: promises expired\n");
-	}
 	return mo_graph->checkForCycles() || priv->failed_promise ||
 		priv->too_many_reads || priv->bad_synchronization ||
 		promises_expired();
@@ -2627,7 +2636,7 @@ void ModelChecker::print_summary() const
 #endif
 
 	if (!isfeasibleprefix())
-		model_print("INFEASIBLE EXECUTION!\n");
+		print_infeasibility("INFEASIBLE EXECUTION");
 	print_list(action_trace, stats.num_total);
 	model_print("\n");
 }
diff --git a/model.h b/model.h
index 4fd2667..97a8989 100644
--- a/model.h
+++ b/model.h
@@ -255,6 +255,7 @@ private:
 	struct execution_stats stats;
 	void record_stats();
 
+	void print_infeasibility(const char *prefix) const;
 	bool is_feasible_prefix_ignore_relseq() const;
 	bool is_infeasible_ignoreRMW() const;
 	bool is_infeasible() const;