Defining the interfaces to add various regions to snapshot

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 2c7404703bd614341f832df5a6fb6f40d31128fe..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
@@ -58,7 +60,7 @@ ModelChecker::ModelChecker()
 
 ModelChecker::~ModelChecker()
 {
-       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();
@@ -72,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();
@@ -300,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);
-}