nodestack.cc

   1 #include "nodestack.h"
   2 #include "action.h"
   3 #include "common.h"
   4 #include "model.h"
   5
   6 /** @brief Node constructor */
   7 Node::Node(ModelAction *act, Node *par, int nthreads)
   8         : action(act),
   9         parent(par),
  10         num_threads(nthreads),
  11         explored_children(num_threads),
  12         backtrack(num_threads),
  13         numBacktracks(0),
  14         may_read_from()
  15 {
  16 }
  17
  18 /** @brief Node desctructor */
  19 Node::~Node()
  20 {
  21         if (action)
  22                 delete action;
  23 }
  24
  25 /** Prints debugging info for the ModelAction associated with this Node */
  26 void Node::print()
  27 {
  28         if (action)
  29                 action->print();
  30         else
  31                 printf("******** empty action ********\n");
  32 }
  33
  34 /**
  35  * Checks if the Thread associated with this thread ID has been explored from
  36  * this Node already.
  37  * @param tid is the thread ID to check
  38  * @return true if this thread choice has been explored already, false
  39  * otherwise
  40  */
  41 bool Node::has_been_explored(thread_id_t tid)
  42 {
  43         int id = id_to_int(tid);
  44         return explored_children[id];
  45 }
  46
  47 /**
  48  * Checks if the backtracking set is empty.
  49  * @return true if the backtracking set is empty
  50  */
  51 bool Node::backtrack_empty()
  52 {
  53         return numBacktracks == 0;
  54 }
  55
  56 /**
  57  * Explore a child Node using a given ModelAction. This updates both the
  58  * Node-internal and the ModelAction data to associate the ModelAction with
  59  * this Node.
  60  * @param act is the ModelAction to explore
  61  */
  62 void Node::explore_child(ModelAction *act)
  63 {
  64         act->set_node(this);
  65         explore(act->get_tid());
  66 }
  67
  68 /**
  69  * Records a backtracking reference for a thread choice within this Node.
  70  * Provides feedback as to whether this thread choice is already set for
  71  * backtracking.
  72  * @return false if the thread was already set to be backtracked, true
  73  * otherwise
  74  */
  75 bool Node::set_backtrack(thread_id_t id)
  76 {
  77         int i = id_to_int(id);
  78         if (backtrack[i])
  79                 return false;
  80         backtrack[i] = true;
  81         numBacktracks++;
  82         return true;
  83 }
  84
  85 thread_id_t Node::get_next_backtrack()
  86 {
  87         /* TODO: find next backtrack */
  88         unsigned int i;
  89         for (i = 0; i < backtrack.size(); i++)
  90                 if (backtrack[i] == true)
  91                         break;
  92         if (i >= backtrack.size())
  93                 return THREAD_ID_T_NONE;
  94         backtrack[i] = false;
  95         numBacktracks--;
  96         return int_to_id(i);
  97 }
  98
  99 bool Node::is_enabled(Thread *t)
 100 {
 101         return id_to_int(t->get_id()) < num_threads;
 102 }
 103
 104 /**
 105  * Add an action to the may_read_from set.
 106  * @param act is the action to add
 107  */
 108 void Node::add_read_from(ModelAction *act)
 109 {
 110         may_read_from.insert(act);
 111 }
 112
 113 void Node::explore(thread_id_t tid)
 114 {
 115         int i = id_to_int(tid);
 116         if (backtrack[i]) {
 117                 backtrack[i] = false;
 118                 numBacktracks--;
 119         }
 120         explored_children[i] = true;
 121 }
 122
 123 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
 124                                                node_list_t::iterator end)
 125 {
 126         node_list_t::iterator it;
 127
 128         for (it = start; it != end; it++)
 129                 delete (*it);
 130         list->erase(start, end);
 131 }
 132
 133 NodeStack::NodeStack()
 134         : total_nodes(0)
 135 {
 136         node_list.push_back(new Node());
 137         total_nodes++;
 138         iter = node_list.begin();
 139 }
 140
 141 NodeStack::~NodeStack()
 142 {
 143         clear_node_list(&node_list, node_list.begin(), node_list.end());
 144 }
 145
 146 void NodeStack::print()
 147 {
 148         node_list_t::iterator it;
 149         printf("............................................\n");
 150         printf("NodeStack printing node_list:\n");
 151         for (it = node_list.begin(); it != node_list.end(); it++) {
 152                 if (it == this->iter)
 153                         printf("vvv following action is the current iterator vvv\n");
 154                 (*it)->print();
 155         }
 156         printf("............................................\n");
 157 }
 158
 159 ModelAction * NodeStack::explore_action(ModelAction *act)
 160 {
 161         DBG();
 162
 163         ASSERT(!node_list.empty());
 164
 165         if (get_head()->has_been_explored(act->get_tid())) {
 166                 iter++;
 167                 return (*iter)->get_action();
 168         }
 169
 170         /* Diverging from previous execution; clear out remainder of list */
 171         node_list_t::iterator it = iter;
 172         it++;
 173         clear_node_list(&node_list, it, node_list.end());
 174
 175         /* Record action */
 176         get_head()->explore_child(act);
 177         node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
 178         total_nodes++;
 179         iter++;
 180         return NULL;
 181 }
 182
 183 Node * NodeStack::get_head()
 184 {
 185         if (node_list.empty())
 186                 return NULL;
 187         return *iter;
 188 }
 189
 190 Node * NodeStack::get_next()
 191 {
 192         node_list_t::iterator it = iter;
 193         if (node_list.empty()) {
 194                 DEBUG("Empty\n");
 195                 return NULL;
 196         }
 197         it++;
 198         if (it == node_list.end()) {
 199                 DEBUG("At end\n");
 200                 return NULL;
 201         }
 202         return *it;
 203 }
 204
 205 void NodeStack::reset_execution()
 206 {
 207         iter = node_list.begin();
 208 }