some changes towards reading from future writes

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 59f148ef0f6c4a7b316a970bb1024d9e6aa0ed9a..bfa3e02997ee42ed860fcf872d297906a6ac38b5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -8,6 +8,7 @@
 #include "common.h"
 #include "clockvector.h"
 #include "cyclegraph.h"
+#include "promise.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -27,9 +28,10 @@ ModelChecker::ModelChecker()
        diverge(NULL),
        nextThread(THREAD_ID_T_NONE),
        action_trace(new action_list_t()),
-       thread_map(new std::map<int, Thread *>),
-       obj_map(new std::map<const void *, action_list_t>()),
-       obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
+       thread_map(new HashTable<int, Thread *, int>()),
+       obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
+       obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
+       promises(new std::vector<Promise *>(1)),
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
        next_backtrack(NULL),
@@ -40,9 +42,9 @@ ModelChecker::ModelChecker()
 /** @brief Destructor */
 ModelChecker::~ModelChecker()
 {
-       std::map<int, Thread *>::iterator it;
+       /*      std::map<int, Thread *>::iterator it;
        for (it = thread_map->begin(); it != thread_map->end(); it++)
-               delete (*it).second;
+       delete (*it).second;*/
        delete thread_map;
 
        delete obj_thrd_map;
@@ -102,7 +104,7 @@ Thread * ModelChecker::schedule_next_thread()
        Thread *t;
        if (nextThread == THREAD_ID_T_NONE)
                return NULL;
-       t = (*thread_map)[id_to_int(nextThread)];
+       t = thread_map->get(id_to_int(nextThread));
 
        ASSERT(t != NULL);
 
@@ -118,7 +120,6 @@ Thread * ModelChecker::schedule_next_thread()
  */
 thread_id_t ModelChecker::get_next_replay_thread()
 {
-       ModelAction *next;
        thread_id_t tid;
 
        /* Have we completed exploring the preselected path? */
@@ -126,7 +127,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
                return THREAD_ID_T_NONE;
 
        /* Else, we are trying to replay an execution */
-       next = node_stack->get_next()->get_action();
+       ModelAction * next = node_stack->get_next()->get_action();
 
        if (next == diverge) {
                Node *nextnode = next->get_node();
@@ -191,7 +192,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
                        return NULL;
        }
        /* linear search: from most recent to oldest */
-       action_list_t *list = &(*obj_map)[act->get_location()];
+       action_list_t *list = obj_map->ensureptr(act->get_location());
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++) {
                ModelAction *prev = *rit;
@@ -308,17 +309,16 @@ void ModelChecker::check_current_action(void)
        if (!already_added)
                add_action_to_lists(curr);
 
-       /* Do not split atomic actions. */
-       if (curr->is_rmwr()) {
-               nextThread = thread_current()->get_id();
-               return;
-       }
-
        /* Is there a better interface for setting the next thread rather
                 than this field/convoluted approach?  Perhaps like just returning
                 it or something? */
 
-       nextThread = get_next_replay_thread();
+       /* Do not split atomic actions. */
+       if (curr->is_rmwr()) {
+               nextThread = thread_current()->get_id();
+       } else {
+               nextThread = get_next_replay_thread();
+       }
 
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
@@ -351,7 +351,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction * act) {
  * @param rf The action that curr reads from. Must be a write.
  */
 void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
-       std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 
@@ -383,7 +383,7 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r
  * @param curr The current action. Must be a write.
  */
 void ModelChecker::w_modification_order(ModelAction * curr) {
-       std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_write());
 
@@ -427,9 +427,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        action_trace->push_back(act);
 
-       (*obj_map)[act->get_location()].push_back(act);
+       obj_map->ensureptr(act->get_location())->push_back(act);
 
-       std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
+       std::vector<action_list_t> *vec = obj_thrd_map->ensureptr(act->get_location());
        if (tid >= (int)vec->size())
                vec->resize(next_thread_id);
        (*vec)[tid].push_back(act);
@@ -455,7 +455,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid)
  */
 ModelAction * ModelChecker::get_last_seq_cst(const void *location)
 {
-       action_list_t *list = &(*obj_map)[location];
+       action_list_t *list = obj_map->ensureptr(location);
        /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++)
@@ -490,7 +490,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
  */
 void ModelChecker::build_reads_from_past(ModelAction *curr)
 {
-       std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 
@@ -538,7 +538,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        }
 
        if (!initialized) {
-               /* TODO: need a more informative way of reporting errors */
+               /** @todo Need a more informative way of reporting errors. */
                printf("ERROR: may read from uninitialized atomic\n");
        }
 
@@ -582,7 +582,7 @@ void ModelChecker::print_summary(void)
 
 int ModelChecker::add_thread(Thread *t)
 {
-       (*thread_map)[id_to_int(t->get_id())] = t;
+       thread_map->put(id_to_int(t->get_id()), t);
        scheduler->add_thread(t);
        return 0;
 }