nodestack.cc

   1 #include "nodestack.h"
   2 #include "action.h"
   3 #include "common.h"
   4 #include "model.h"
   5
   6 int Node::total_nodes = 0;
   7
   8 Node::Node(ModelAction *act, int nthreads)
   9         : action(act),
  10         num_threads(nthreads),
  11         explored_children(num_threads),
  12         backtrack(num_threads)
  13 {
  14         total_nodes++;
  15 }
  16
  17 Node::~Node()
  18 {
  19         if (action)
  20                 delete action;
  21 }
  22
  23 void Node::print()
  24 {
  25         if (action)
  26                 action->print();
  27         else
  28                 printf("******** empty action ********\n");
  29 }
  30
  31 bool Node::has_been_explored(thread_id_t tid)
  32 {
  33         int id = id_to_int(tid);
  34         return explored_children[id];
  35 }
  36
  37 bool Node::backtrack_empty()
  38 {
  39         unsigned int i;
  40         for (i = 0; i < backtrack.size(); i++)
  41                 if (backtrack[i] == true)
  42                         return false;
  43         return true;
  44 }
  45
  46 void Node::explore_child(ModelAction *act)
  47 {
  48         act->set_node(this);
  49         explore(act->get_tid());
  50 }
  51
  52 bool Node::set_backtrack(thread_id_t id)
  53 {
  54         int i = id_to_int(id);
  55         if (backtrack[i])
  56                 return false;
  57         backtrack[i] = true;
  58         return true;
  59 }
  60
  61 thread_id_t Node::get_next_backtrack()
  62 {
  63         /* TODO: find next backtrack */
  64         unsigned int i;
  65         for (i = 0; i < backtrack.size(); i++)
  66                 if (backtrack[i] == true)
  67                         break;
  68         if (i >= backtrack.size())
  69                 return THREAD_ID_T_NONE;
  70         backtrack[i] = false;
  71         return int_to_id(i);
  72 }
  73
  74 bool Node::is_enabled(Thread *t)
  75 {
  76         return id_to_int(t->get_id()) < num_threads;
  77 }
  78
  79 void Node::explore(thread_id_t tid)
  80 {
  81         int i = id_to_int(tid);
  82         backtrack[i] = false;
  83         explored_children[i] = true;
  84 }
  85
  86 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
  87                                                node_list_t::iterator end)
  88 {
  89         node_list_t::iterator it;
  90
  91         for (it = start; it != end; it++)
  92                 delete (*it);
  93         list->erase(start, end);
  94 }
  95
  96 NodeStack::NodeStack()
  97 {
  98         node_list.push_back(new Node());
  99         iter = node_list.begin();
 100 }
 101
 102 NodeStack::~NodeStack()
 103 {
 104         clear_node_list(&node_list, node_list.begin(), node_list.end());
 105 }
 106
 107 void NodeStack::print()
 108 {
 109         node_list_t::iterator it;
 110         printf("............................................\n");
 111         printf("NodeStack printing node_list:\n");
 112         for (it = node_list.begin(); it != node_list.end(); it++) {
 113                 if (it == this->iter)
 114                         printf("vvv following action is the current iterator vvv\n");
 115                 (*it)->print();
 116         }
 117         printf("............................................\n");
 118 }
 119
 120 ModelAction * NodeStack::explore_action(ModelAction *act, ModelAction *parent)
 121 {
 122         DBG();
 123
 124         ASSERT(!node_list.empty());
 125
 126         if (get_head()->has_been_explored(act->get_tid())) {
 127                 /* Discard duplicate ModelAction */
 128                 delete act;
 129                 iter++;
 130         } else { /* Diverging from previous execution */
 131                 /* Clear out remainder of list */
 132                 node_list_t::iterator it = iter;
 133                 it++;
 134                 clear_node_list(&node_list, it, node_list.end());
 135
 136                 /* Record action */
 137                 get_head()->explore_child(act);
 138                 act->create_cv(parent);
 139                 node_list.push_back(new Node(act, model->get_num_threads()));
 140                 iter++;
 141         }
 142         return (*iter)->get_action();
 143 }
 144
 145 Node * NodeStack::get_head()
 146 {
 147         if (node_list.empty())
 148                 return NULL;
 149         return *iter;
 150 }
 151
 152 Node * NodeStack::get_next()
 153 {
 154         node_list_t::iterator it = iter;
 155         if (node_list.empty()) {
 156                 DEBUG("Empty\n");
 157                 return NULL;
 158         }
 159         it++;
 160         if (it == node_list.end()) {
 161                 DEBUG("At end\n");
 162                 return NULL;
 163         }
 164         return *it;
 165 }
 166
 167 void NodeStack::reset_execution()
 168 {
 169         iter = node_list.begin();
 170 }