nodestack.cc

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