Merge branch 'norris'

Primary change: push 'add_action_to_lists()' before main work in
'check_current_action()'

diff --git a/common.cc b/common.cc
index 8cb649bbb10db23b0cb2b4cd2e374e294e73390c..ac5cb59601ba7a6025ac1d8d5f24f62fef0666b7 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -3,6 +3,7 @@
 #include <stdlib.h>
 
 #include "common.h"
+#include "model.h"
 
 #define MAX_TRACE_LEN 100
 
@@ -23,3 +24,8 @@ void print_trace(void)
 
        free(strings);
 }
+
+void model_print_summary(void)
+{
+       model->print_summary();
+}

diff --git a/common.h b/common.h
index 80bc9ad6e8c6977fb3622b8754c1982cf64c25f5..2dc8b7d9e8e59457fd4bfee6b850af028414d9c9 100644 (file)
--- a/common.h
+++ b/common.h
@@ -22,6 +22,8 @@
 do { \
        if (!(expr)) { \
                fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
+               print_trace(); \
+               model_print_summary(); \
                exit(EXIT_FAILURE); \
        } \
 } while (0);
@@ -29,5 +31,6 @@ do { \
 #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__)
 
 void print_trace(void);
+void model_print_summary(void);
 
 #endif /* __COMMON_H__ */

diff --git a/cyclegraph.cc b/cyclegraph.cc
index ecf8a781c2770ebd09766cff47030e3e094bd2d7..2bfe76ac424c274bf8152638543ad7dd6bc1d31f 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -41,6 +41,7 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) {
 void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
        ASSERT(from);
        ASSERT(to);
+       ASSERT(from != to);
 
        CycleNode *fromnode=getNode(from);
        CycleNode *tonode=getNode(to);
@@ -82,6 +83,7 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
 void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
        ASSERT(from);
        ASSERT(rmw);
+       ASSERT(from != rmw);
 
        CycleNode *fromnode=getNode(from);
        CycleNode *rmwnode=getNode(rmw);

diff --git a/model.cc b/model.cc
index 483e83232ffb2ec7272e1eae1c7283af3b4eac84..9faf4e2a28eb26b7c7891114f86592aee80480b9 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() {
+       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() {
+       if (DBG_ENABLED() && promises->size() != 0)
+               DEBUG("Infeasible: unrevolved promises\n");
+
        return isfeasible() && promises->size() == 0;
 }