Merge branch 'norris'

diff --combined model.cc
index 7c6684f567ab48958f5701045c862313ba80d56c,44c7e353d79b5f8cd87de1f50763c1b705b6224e..25f85d0ee4403ebb1b6ef00531cf872bbdd29892
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -200,7 -200,7 +200,7 @@@ ModelAction * ModelChecker::get_last_co
                        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;
@@@ -384,7 -384,7 +384,7 @@@ ModelAction * ModelChecker::process_rmw
   * @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());
  
@@@ -414,7 -414,7 +414,7 @@@
  /** Updates the cyclegraph 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());
  
@@@ -453,7 -453,7 +453,7 @@@
   * @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());
  
@@@ -510,9 -510,9 +510,9 @@@ void ModelChecker::add_action_to_lists(
        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);
@@@ -538,7 -538,7 +538,7 @@@ ModelAction * ModelChecker::get_last_ac
   */
  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++)
@@@ -626,7 -626,7 +626,7 @@@ void ModelChecker::check_promises(Clock
   */
  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());
  
@@@ -716,11 -716,15 +716,15 @@@ void ModelChecker::print_summary(
        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)
@@@ -745,5 -749,48 +749,48 @@@ int ModelChecker::switch_to_master(Mode
        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());
  }