changes
[c11tester.git] / nodestack.cc
1 #include "nodestack.h"
2 #include "action.h"
3 #include "common.h"
4 #include "model.h"
5
6 /**
7  * @brief Node constructor
8  *
9  * Constructs a single Node for use in a NodeStack. Each Node is associated
10  * with exactly one ModelAction (exception: the first Node should be created
11  * as an empty stub, to represent the first thread "choice") and up to one
12  * parent.
13  *
14  * @param act The ModelAction to associate with this Node. May be NULL.
15  * @param par The parent Node in the NodeStack. May be NULL if there is no
16  * parent.
17  * @param nthreads The number of threads which exist at this point in the
18  * execution trace.
19  */
20 Node::Node(ModelAction *act, Node *par, int nthreads)
21         : action(act),
22         parent(par),
23         num_threads(nthreads),
24         explored_children(num_threads),
25         backtrack(num_threads),
26         numBacktracks(0),
27         may_read_from(),
28         read_from_index(0),
29         future_values(),
30         future_index(0)
31 {
32         if (act)
33                 act->set_node(this);
34 }
35
36 /** @brief Node desctructor */
37 Node::~Node()
38 {
39         if (action)
40                 delete action;
41 }
42
43 /** Prints debugging info for the ModelAction associated with this Node */
44 void Node::print()
45 {
46         if (action)
47                 action->print();
48         else
49                 printf("******** empty action ********\n");
50 }
51
52 /** @brief Prints info about may_read_from set */
53 void Node::print_may_read_from()
54 {
55         readfrom_set_t::iterator it;
56         for (it = may_read_from.begin(); it != may_read_from.end(); it++)
57                 (*it)->print();
58 }
59
60 /**
61  * Adds a value from a weakly ordered future write to backtrack to.
62  * @param value is the value to backtrack to.
63  */
64
65 bool Node::add_future_value(uint64_t value) {
66         for(int i=0;i<future_values.size();i++)
67                 if (future_values[i]==value)
68                         return false;
69         future_values.push_back(value);
70         return true;
71 }
72
73
74 /**
75  * Checks if the Thread associated with this thread ID has been explored from
76  * this Node already.
77  * @param tid is the thread ID to check
78  * @return true if this thread choice has been explored already, false
79  * otherwise
80  */
81 bool Node::has_been_explored(thread_id_t tid)
82 {
83         int id = id_to_int(tid);
84         return explored_children[id];
85 }
86
87 /**
88  * Checks if the backtracking set is empty.
89  * @return true if the backtracking set is empty
90  */
91 bool Node::backtrack_empty()
92 {
93         return (numBacktracks == 0);
94 }
95
96
97 /**
98  * Checks whether the readsfrom set for this node is empty.
99  * @return true if the readsfrom set is empty.
100  */
101 bool Node::readsfrom_empty() {
102         return ((read_from_index+1)>=may_read_from.size());
103 }
104
105 /** 
106  * Checks whether the future_values set for this node is empty.
107  * @return true if the future_values set is empty.
108  */
109
110 bool Node::futurevalues_empty() {
111         return ((future_index+1)>=future_values.size());
112 }
113
114 /**
115  * Mark the appropriate backtracking information for exploring a thread choice.
116  * @param act The ModelAction to explore
117  */
118 void Node::explore_child(ModelAction *act)
119 {
120         explore(act->get_tid());
121 }
122
123 /**
124  * Records a backtracking reference for a thread choice within this Node.
125  * Provides feedback as to whether this thread choice is already set for
126  * backtracking.
127  * @return false if the thread was already set to be backtracked, true
128  * otherwise
129  */
130 bool Node::set_backtrack(thread_id_t id)
131 {
132         int i = id_to_int(id);
133         if (backtrack[i])
134                 return false;
135         backtrack[i] = true;
136         numBacktracks++;
137         return true;
138 }
139
140 thread_id_t Node::get_next_backtrack()
141 {
142         /** @todo Find next backtrack */
143         unsigned int i;
144         for (i = 0; i < backtrack.size(); i++)
145                 if (backtrack[i] == true)
146                         break;
147         /* Backtrack set was empty? */
148         ASSERT(i != backtrack.size());
149
150         backtrack[i] = false;
151         numBacktracks--;
152         return int_to_id(i);
153 }
154
155 bool Node::is_enabled(Thread *t)
156 {
157         return id_to_int(t->get_id()) < num_threads;
158 }
159
160 /**
161  * Add an action to the may_read_from set.
162  * @param act is the action to add
163  */
164 void Node::add_read_from(const ModelAction *act)
165 {
166         may_read_from.push_back(act);
167 }
168
169 /**
170  * Gets the next 'future_value' value from this Node. Only valid for a node
171  * where this->action is a 'read'.
172  * @return The first element in future_values
173  */
174
175 uint64_t Node::get_future_value() {
176         ASSERT(future_index<future_values.size());
177         return future_values[future_index];
178 }
179
180 /**
181  * Gets the next 'may_read_from' action from this Node. Only valid for a node
182  * where this->action is a 'read'.
183  * @todo Perform reads_from backtracking/replay properly, so that this function
184  * may remove elements from may_read_from
185  * @return The first element in may_read_from
186  */
187 const ModelAction * Node::get_read_from() {
188         if (read_from_index<may_read_from.size())
189                 return may_read_from[read_from_index];
190         else
191                 return NULL;
192 }
193
194 /**
195  * Increments the index into the readsfrom set to explore the next item.
196  * @return Returns false if we have explored all items.
197  */
198 bool Node::increment_read_from() {
199         read_from_index++;
200         return (read_from_index<may_read_from.size());
201 }
202
203 /**
204  * Increments the index into the future_values set to explore the next item.
205  * @return Returns false if we have explored all values.
206  */
207
208 bool Node::increment_future_values() {
209         future_index++;
210         return (future_index<future_values.size());
211 }
212
213 void Node::explore(thread_id_t tid)
214 {
215         int i = id_to_int(tid);
216         if (backtrack[i]) {
217                 backtrack[i] = false;
218                 numBacktracks--;
219         }
220         explored_children[i] = true;
221 }
222
223 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
224                                                node_list_t::iterator end)
225 {
226         node_list_t::iterator it;
227
228         for (it = start; it != end; it++)
229                 delete (*it);
230         list->erase(start, end);
231 }
232
233 NodeStack::NodeStack()
234         : total_nodes(0)
235 {
236         node_list.push_back(new Node());
237         total_nodes++;
238         iter = node_list.begin();
239 }
240
241 NodeStack::~NodeStack()
242 {
243         clear_node_list(&node_list, node_list.begin(), node_list.end());
244 }
245
246 void NodeStack::print()
247 {
248         node_list_t::iterator it;
249         printf("............................................\n");
250         printf("NodeStack printing node_list:\n");
251         for (it = node_list.begin(); it != node_list.end(); it++) {
252                 if (it == this->iter)
253                         printf("vvv following action is the current iterator vvv\n");
254                 (*it)->print();
255         }
256         printf("............................................\n");
257 }
258
259 ModelAction * NodeStack::explore_action(ModelAction *act)
260 {
261         DBG();
262
263         ASSERT(!node_list.empty());
264         node_list_t::iterator it=iter;
265         it++;
266
267         if (it != node_list.end()) {
268                 iter++;
269                 return (*iter)->get_action();
270         }
271
272         /* Record action */
273         get_head()->explore_child(act);
274         node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
275         total_nodes++;
276         iter++;
277         return NULL;
278 }
279
280 /**
281  * Empties the stack of all trailing nodes after a given position and calls the
282  * destructor for each. This function is provided an offset which determines
283  * how many nodes (relative to the current replay state) to save before popping
284  * the stack.
285  * @param numAhead gives the number of Nodes (including this Node) to skip over
286  * before removing nodes.
287  */
288 void NodeStack::pop_restofstack(int numAhead)
289 {
290         /* Diverging from previous execution; clear out remainder of list */
291         node_list_t::iterator it = iter;
292         while (numAhead--)
293                 it++;
294         clear_node_list(&node_list, it, node_list.end());
295 }
296
297 Node * NodeStack::get_head()
298 {
299         if (node_list.empty())
300                 return NULL;
301         return *iter;
302 }
303
304 Node * NodeStack::get_next()
305 {
306         node_list_t::iterator it = iter;
307         if (node_list.empty()) {
308                 DEBUG("Empty\n");
309                 return NULL;
310         }
311         it++;
312         if (it == node_list.end()) {
313                 DEBUG("At end\n");
314                 return NULL;
315         }
316         return *it;
317 }
318
319 void NodeStack::reset_execution()
320 {
321         iter = node_list.begin();
322 }