model: add support for modification orders

This update adds support for modification orders and kills the bogus executions
seen before...

[Updated, split by Brian Norris]

diff --git a/main.cc b/main.cc
index 339b85efd45d427096546cbf8641d3afbb71067f..cbf93b67fce125aef65f9e90801c295633d8c46a 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -31,6 +31,8 @@ static int thread_system_next(void) {
                        ASSERT(false);
        }
        next = model->scheduler->next_thread();
+       if (!model->isfeasible())
+               return 1;
        if (next)
                next->set_state(THREAD_RUNNING);
        DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);

diff --git a/model.cc b/model.cc
index e9d1f1df069cb5f0f1b79c9683143b59c4b39ffe..31809918361c185cedc7d1ac791044f01bd23bad 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -7,6 +7,7 @@
 #include "snapshot-interface.h"
 #include "common.h"
 #include "clockvector.h"
+#include "cyclegraph.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -31,7 +32,8 @@ ModelChecker::ModelChecker()
        obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
-       next_backtrack(NULL)
+       next_backtrack(NULL),
+       cyclegraph(new CycleGraph())
 {
 }
 
@@ -49,6 +51,7 @@ ModelChecker::~ModelChecker()
        delete thrd_last_action;
        delete node_stack;
        delete scheduler;
+       delete cyclegraph;
 }
 
 /**
@@ -279,8 +282,6 @@ void ModelChecker::check_current_action(void)
 
        set_backtracking(curr);
 
-       add_action_to_lists(curr);
-
        /* Assign reads_from values */
        /* TODO: perform release/acquire synchronization here; include
         * reads_from as ModelAction member? */
@@ -291,8 +292,80 @@ void ModelChecker::check_current_action(void)
                value = reads_from->get_value();
                /* Assign reads_from, perform release/acquire synchronization */
                curr->read_from(reads_from);
+               r_modification_order(curr,reads_from);
+       } else if (curr->is_write()) {
+               w_modification_order(curr);
        }
+
        th->set_return_value(value);
+
+       /* Add action to list last.  */
+       add_action_to_lists(curr);
+}
+
+bool ModelChecker::isfeasible() {
+       return !cyclegraph->checkForCycles();
+}
+
+void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
+       std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+       unsigned int i;
+       ASSERT(curr->is_read());
+
+       /* Iterate over all threads */
+       for (i = 0; i < thrd_lists->size(); i++) {
+               /* Iterate over actions in thread, starting from most recent */
+               action_list_t *list = &(*thrd_lists)[i];
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *act = *rit;
+
+                       /* Include at most one act per-thread that "happens before" curr */
+                       if (act->happens_before(curr)) {
+                               if (act->is_read()) {
+                                       const ModelAction * prevreadfrom=act->get_reads_from();
+                                       if (rf!=prevreadfrom)
+                                               cyclegraph->addEdge(rf, prevreadfrom);
+                               } else if (rf!=act) {
+                                       cyclegraph->addEdge(rf, act);
+                               }
+                               break;
+                       }
+               }
+       }
+}
+
+void ModelChecker::w_modification_order(ModelAction * curr) {
+       std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+       unsigned int i;
+       ASSERT(curr->is_write());
+
+       if (curr->is_seqcst()) {
+               /* We have to at least see the last sequentially consistent write,
+                        so we are initialized. */
+               ModelAction * last_seq_cst=get_last_seq_cst(curr->get_location());
+               if (last_seq_cst!=NULL)
+                       cyclegraph->addEdge(curr, last_seq_cst);
+       }
+
+       /* Iterate over all threads */
+       for (i = 0; i < thrd_lists->size(); i++) {
+               /* Iterate over actions in thread, starting from most recent */
+               action_list_t *list = &(*thrd_lists)[i];
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *act = *rit;
+
+                       /* Include at most one act per-thread that "happens before" curr */
+                       if (act->happens_before(curr)) {
+                               if (act->is_read()) {
+                                       cyclegraph->addEdge(curr, act->get_reads_from());
+                               } else
+                                       cyclegraph->addEdge(curr, act);
+                               break;
+                       }
+               }
+       }
 }
 
 /**
@@ -446,6 +519,8 @@ void ModelChecker::print_summary(void)
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
        printf("Total nodes created: %d\n", node_stack->get_total_nodes());
+       if (!isfeasible())
+               printf("INFEASIBLE EXECUTION!\n");
 
        scheduler->print();
 

diff --git a/model.h b/model.h
index 2093bf4b19cb31579d2b5e1040bcdb3ce55eb63c..4c0af0af1f3e33ba3aaa0e3bc5a74f67f6cd9c10 100644 (file)
--- a/model.h
+++ b/model.h
@@ -21,6 +21,7 @@
 
 /* Forward declaration */
 class NodeStack;
+class CycleGraph;
 
 /** @brief The central structure for model-checking */
 class ModelChecker {
@@ -55,6 +56,7 @@ public:
        int switch_to_master(ModelAction *act);
        ClockVector * get_cv(thread_id_t tid);
        bool next_execution();
+       bool isfeasible();
 
        MEMALLOC
 private:
@@ -81,6 +83,9 @@ private:
        ModelAction * get_parent_action(thread_id_t tid);
        ModelAction * get_last_seq_cst(const void *location);
        void build_reads_from_past(ModelAction *curr);
+       void r_modification_order(ModelAction * curr, const ModelAction *rf);
+       void w_modification_order(ModelAction * curr);
+
 
        ModelAction *current_action;
        ModelAction *diverge;
@@ -98,6 +103,7 @@ private:
        std::vector<ModelAction *> *thrd_last_action;
        NodeStack *node_stack;
        ModelAction *next_backtrack;
+       CycleGraph * cyclegraph;
 };
 
 extern ModelChecker *model;