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