Defining the interfaces to add various regions to snapshot

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index aba3e8bc0c1783f87cad0c9b5b60b5ba9e3ae4c3..51715d22614afaa3e61afa05df063cddba64c4a6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -4,6 +4,8 @@
 #include "action.h"
 #include "tree.h"
 #include "schedule.h"
+#include "snapshot-interface.h"
+#undef DEBUG
 #include "common.h"
 
 #define INITIAL_THREAD_ID      0
@@ -30,6 +32,14 @@ private:
 
 ModelChecker *model;
 
+void free_action_list(action_list_t *list)
+{
+       action_list_t::iterator it;
+       for (it = list->begin(); it != list->end(); it++)
+               delete (*it);
+       delete list;
+}
+
 ModelChecker::ModelChecker()
 {
        /* First thread created will have id INITIAL_THREAD_ID */
@@ -43,14 +53,20 @@ ModelChecker::ModelChecker()
        this->exploring = NULL;
        this->nextThread = THREAD_ID_T_NONE;
 
-       rootNode = new TreeNode(NULL);
+       rootNode = new TreeNode();
        currentNode = rootNode;
        action_trace = new action_list_t();
 }
 
 ModelChecker::~ModelChecker()
 {
-       delete action_trace;
+       std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
+       for (it = thread_map.begin(); it != thread_map.end(); it++)
+               delete (*it).second;
+       thread_map.clear();
+
+       free_action_list(action_trace);
+
        delete this->scheduler;
        delete rootNode;
 }
@@ -58,7 +74,7 @@ ModelChecker::~ModelChecker()
 void ModelChecker::reset_to_initial_state()
 {
        DEBUG("+++ Resetting to initial state +++\n");
-       std::map<int, class Thread *>::iterator it;
+       std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
        for (it = thread_map.begin(); it != thread_map.end(); it++)
                delete (*it).second;
        thread_map.clear();
@@ -86,8 +102,9 @@ Thread * ModelChecker::schedule_next_thread()
        if (nextThread == THREAD_ID_T_NONE)
                return NULL;
        t = thread_map[id_to_int(nextThread)];
-       if (t == NULL)
-               DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
+
+       ASSERT(t != NULL);
+
        return t;
 }
 
@@ -182,6 +199,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 {
        ModelAction *prev;
        TreeNode *node;
+       Thread *t = get_thread(act->get_tid());
 
        prev = get_last_conflict(act);
        if (prev == NULL)
@@ -189,15 +207,18 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
        node = prev->get_node();
 
+       while (t && !node->is_enabled(t))
+               t = t->get_parent();
+
        /* Check if this has been explored already */
-       if (node->hasBeenExplored(act->get_tid()))
+       if (node->hasBeenExplored(t->get_id()))
                return;
        /* If this is a new backtracking point, mark the tree */
-       if (node->setBacktrack(act->get_tid()) != 0)
+       if (node->setBacktrack(t->get_id()) != 0)
                return;
 
        DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-                       prev->get_tid(), act->get_tid());
+                       prev->get_tid(), t->get_id());
        if (DBG_ENABLED()) {
                prev->print();
                act->print();
@@ -229,7 +250,7 @@ void ModelChecker::check_current_action(void)
        nextThread = advance_backtracking_state();
        next->set_node(currentNode);
        set_backtracking(next);
-       currentNode = currentNode->exploreChild(next->get_tid());
+       currentNode = currentNode->explore_child(next);
        this->action_trace->push_back(next);
 }
 
@@ -281,99 +302,3 @@ int ModelChecker::switch_to_master(ModelAction *act)
        old->set_state(THREAD_READY);
        return Thread::swap(old, get_system_context());
 }
-
-ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
-{
-       Thread *t = thread_current();
-       ModelAction *act = this;
-
-       act->type = type;
-       act->order = order;
-       act->location = loc;
-       act->tid = t->get_id();
-       act->value = value;
-       act->seq_number = model->get_next_seq_num();
-}
-
-bool ModelAction::is_read()
-{
-       return type == ATOMIC_READ;
-}
-
-bool ModelAction::is_write()
-{
-       return type == ATOMIC_WRITE;
-}
-
-bool ModelAction::is_acquire()
-{
-       switch (order) {
-       case memory_order_acquire:
-       case memory_order_acq_rel:
-       case memory_order_seq_cst:
-               return true;
-       default:
-               return false;
-       }
-}
-
-bool ModelAction::is_release()
-{
-       switch (order) {
-       case memory_order_release:
-       case memory_order_acq_rel:
-       case memory_order_seq_cst:
-               return true;
-       default:
-               return false;
-       }
-}
-
-bool ModelAction::same_var(ModelAction *act)
-{
-       return location == act->location;
-}
-
-bool ModelAction::same_thread(ModelAction *act)
-{
-       return tid == act->tid;
-}
-
-bool ModelAction::is_dependent(ModelAction *act)
-{
-       if (!is_read() && !is_write())
-               return false;
-       if (!act->is_read() && !act->is_write())
-               return false;
-       if (same_var(act) && !same_thread(act) &&
-                       (is_write() || act->is_write()))
-               return true;
-       return false;
-}
-
-void ModelAction::print(void)
-{
-       const char *type_str;
-       switch (this->type) {
-       case THREAD_CREATE:
-               type_str = "thread create";
-               break;
-       case THREAD_YIELD:
-               type_str = "thread yield";
-               break;
-       case THREAD_JOIN:
-               type_str = "thread join";
-               break;
-       case ATOMIC_READ:
-               type_str = "atomic read";
-               break;
-       case ATOMIC_WRITE:
-               type_str = "atomic write";
-               break;
-       default:
-               type_str = "unknown type";
-       }
-
-       printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n",
-                       seq_number, id_to_int(tid), type_str, order, location, value);
-}