model: rename 'cyclegraph' to 'mo_graph'
[model-checker.git] / model.cc
index 71cf14a3ce136202276e941372ae412787848bac..b3ced383b59c1b1cbca02fc135df87cd006d4523 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -34,7 +34,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
        next_backtrack(NULL),
-       cyclegraph(new CycleGraph()),
+       mo_graph(new CycleGraph()),
        failed_promise(false)
 {
 }
@@ -49,10 +49,15 @@ ModelChecker::~ModelChecker()
        delete obj_thrd_map;
        delete obj_map;
        delete action_trace;
+
+       for (unsigned int i = 0; i < promises->size(); i++)
+               delete (*promises)[i];
+       delete promises;
+
        delete thrd_last_action;
        delete node_stack;
        delete scheduler;
-       delete cyclegraph;
+       delete mo_graph;
 }
 
 /**
@@ -172,9 +177,8 @@ bool ModelChecker::next_execution()
 
        num_executions++;
 
-       bool feasible = isfinalfeasible();
-       if (feasible || DBG_ENABLED())
-               print_summary(feasible);
+       if (isfinalfeasible() || DBG_ENABLED())
+               print_summary();
 
        if ((diverge = model->get_next_backtrack()) == NULL)
                return false;
@@ -201,7 +205,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
                        return NULL;
        }
        /* linear search: from most recent to oldest */
-       action_list_t *list = obj_map->ensureptr(act->get_location());
+       action_list_t *list = obj_map->get_safe_ptr(act->get_location());
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++) {
                ModelAction *prev = *rit;
@@ -361,7 +365,7 @@ void ModelChecker::check_current_action(void)
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
-       return !cyclegraph->checkForCycles() && !failed_promise;
+       return !mo_graph->checkForCycles() && !failed_promise;
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -375,17 +379,17 @@ ModelAction * ModelChecker::process_rmw(ModelAction * act) {
        ModelAction *lastread = get_last_action(tid);
        lastread->process_rmw(act);
        if (act->is_rmw())
-               cyclegraph->addRMWEdge(lastread, lastread->get_reads_from());
+               mo_graph->addRMWEdge(lastread, lastread->get_reads_from());
        return lastread;
 }
 
 /**
- * Updates the cyclegraph with the constraints imposed from the current read.
+ * Updates the mo_graph with the constraints imposed from the current read.
  * @param curr The current action. Must be a read.
  * @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->ensureptr(curr->get_location());
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 
@@ -402,9 +406,9 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r
                                if (act->is_read()) {
                                        const ModelAction * prevreadfrom = act->get_reads_from();
                                        if (prevreadfrom != NULL && rf != prevreadfrom)
-                                               cyclegraph->addEdge(rf, prevreadfrom);
+                                               mo_graph->addEdge(rf, prevreadfrom);
                                } else if (rf != act) {
-                                       cyclegraph->addEdge(rf, act);
+                                       mo_graph->addEdge(rf, act);
                                }
                                break;
                        }
@@ -412,10 +416,9 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r
        }
 }
 
-/** Updates the cyclegraph with the constraints imposed from the
- *  current read. */
+/** Updates the mo_graph with the constraints imposed from the current read. */
 void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelAction *rf) {
-       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 
@@ -440,9 +443,9 @@ void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelActi
                        if (lastact->is_read()) {
                                const ModelAction * postreadfrom = lastact->get_reads_from();
                                if (postreadfrom != NULL&&rf != postreadfrom)
-                                       cyclegraph->addEdge(postreadfrom, rf);
+                                       mo_graph->addEdge(postreadfrom, rf);
                        } else if (rf != lastact) {
-                               cyclegraph->addEdge(lastact, rf);
+                               mo_graph->addEdge(lastact, rf);
                        }
                        break;
                }
@@ -450,11 +453,11 @@ void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelActi
 }
 
 /**
- * Updates the cyclegraph with the constraints imposed from the current write.
+ * Updates the mo_graph with the constraints imposed from the current write.
  * @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->ensureptr(curr->get_location());
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_write());
 
@@ -463,7 +466,7 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
                         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);
+                       mo_graph->addEdge(curr, last_seq_cst);
        }
 
        /* Iterate over all threads */
@@ -476,25 +479,24 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
 
                        /* 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);
+                               if (act->is_read())
+                                       mo_graph->addEdge(curr, act->get_reads_from());
+                               else
+                                       mo_graph->addEdge(curr, act);
                                break;
-                       } else {
-                               if (act->is_read()&&!act->is_synchronizing(curr)&&!act->same_thread(curr)) {
-                                       /* We have an action that:
-                                                (1) did not happen before us
-                                                (2) is a read and we are a write
-                                                (3) cannot synchronize with us
-                                                (4) is in a different thread
-                                                =>
-                                                that read could potentially read from our write.
-                                       */
-                                       if (act->get_node()->add_future_value(curr->get_value())&&
-                                                       (!next_backtrack || *act > * next_backtrack))
-                                               next_backtrack = act;
-                               }
+                       } else if (act->is_read() && !act->is_synchronizing(curr) &&
+                                                    !act->same_thread(curr)) {
+                               /* We have an action that:
+                                  (1) did not happen before us
+                                  (2) is a read and we are a write
+                                  (3) cannot synchronize with us
+                                  (4) is in a different thread
+                                  =>
+                                  that read could potentially read from our write.
+                                */
+                               if (act->get_node()->add_future_value(curr->get_value()) &&
+                                               (!next_backtrack || *act > *next_backtrack))
+                                       next_backtrack = act;
                        }
                }
        }
@@ -512,9 +514,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        action_trace->push_back(act);
 
-       obj_map->ensureptr(act->get_location())->push_back(act);
+       obj_map->get_safe_ptr(act->get_location())->push_back(act);
 
-       std::vector<action_list_t> *vec = obj_thrd_map->ensureptr(act->get_location());
+       std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
        if (tid >= (int)vec->size())
                vec->resize(next_thread_id);
        (*vec)[tid].push_back(act);
@@ -540,7 +542,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->ensureptr(location);
+       action_list_t *list = obj_map->get_safe_ptr(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++)
@@ -628,7 +630,7 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) {
  */
 void ModelChecker::build_reads_from_past(ModelAction *curr)
 {
-       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 
@@ -704,7 +706,7 @@ static void print_list(action_list_t *list)
        printf("---------------------------------------------------------------------\n");
 }
 
-void ModelChecker::print_summary(bool feasible)
+void ModelChecker::print_summary()
 {
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
@@ -712,17 +714,21 @@ void ModelChecker::print_summary(bool feasible)
 
        scheduler->print();
 
-       if (!feasible)
+       if (!isfinalfeasible())
                printf("INFEASIBLE EXECUTION!\n");
        print_list(action_trace);
        printf("\n");
 }
 
-int ModelChecker::add_thread(Thread *t)
+/**
+ * Add a Thread to the system for the first time. Should only be called once
+ * per thread.
+ * @param t The Thread to add
+ */
+void ModelChecker::add_thread(Thread *t)
 {
        thread_map->put(id_to_int(t->get_id()), t);
        scheduler->add_thread(t);
-       return 0;
 }
 
 void ModelChecker::remove_thread(Thread *t)
@@ -747,5 +753,48 @@ int ModelChecker::switch_to_master(ModelAction *act)
        Thread * old = thread_current();
        set_current_action(act);
        old->set_state(THREAD_READY);
-       return Thread::swap(old, get_system_context());
+       return Thread::swap(old, &system_context);
+}
+
+/**
+ * Takes the next step in the execution, if possible.
+ * @return Returns true (success) if a step was taken and false otherwise.
+ */
+bool ModelChecker::take_step() {
+       Thread *curr, *next;
+
+       curr = thread_current();
+       if (curr) {
+               if (curr->get_state() == THREAD_READY) {
+                       check_current_action();
+                       scheduler->add_thread(curr);
+               } else if (curr->get_state() == THREAD_RUNNING) {
+                       /* Stopped while running; i.e., completed */
+                       curr->complete();
+               } else {
+                       ASSERT(false);
+               }
+       }
+       next = scheduler->next_thread();
+
+       /* Infeasible -> don't take any more steps */
+       if (!isfeasible())
+               return false;
+
+       if (next)
+               next->set_state(THREAD_RUNNING);
+       DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+
+       /* next == NULL -> don't take any more steps */
+       if (!next)
+               return false;
+       /* Return false only if swap fails with an error */
+       return (Thread::swap(&system_context, next) == 0);
+}
+
+/** Runs the current execution until threre are no more steps to take. */
+void ModelChecker::finish_execution() {
+       DBG();
+
+       while (take_step());
 }