ichange
[model-checker.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, bool *enabled)
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(-1)
31 {
32         if (act)
33                 act->set_node(this);
34         enabled_array=(bool *)MYMALLOC(sizeof(bool)*num_threads);
35         if (enabled)
36                 memcpy(enabled_array, enabled, sizeof(bool)*num_threads);
37         else 
38                 for(int i=0;i<num_threads;i++)
39                         enabled_array[i]=false;
40 }
41
42 /** @brief Node desctructor */
43 Node::~Node()
44 {
45         if (action)
46                 delete action;
47         MYFREE(enabled_array);
48 }
49
50 /** Prints debugging info for the ModelAction associated with this Node */
51 void Node::print()
52 {
53         if (action)
54                 action->print();
55         else
56                 printf("******** empty action ********\n");
57 }
58
59 /** @brief Prints info about may_read_from set */
60 void Node::print_may_read_from()
61 {
62         for (unsigned int i = 0; i < may_read_from.size(); i++)
63                 may_read_from[i]->print();
64 }
65
66 /**
67  * Sets a promise to explore meeting with the given node.
68  * @param i is the promise index.
69  */
70 void Node::set_promise(unsigned int i) {
71         if (i >= promises.size())
72                 promises.resize(i + 1, PROMISE_IGNORE);
73         if (promises[i] == PROMISE_IGNORE)
74                 promises[i] = PROMISE_UNFULFILLED;
75 }
76
77 /**
78  * Looks up whether a given promise should be satisfied by this node.
79  * @param i The promise index.
80  * @return true if the promise should be satisfied by the given model action.
81  */
82 bool Node::get_promise(unsigned int i) {
83         return (i < promises.size()) && (promises[i] == PROMISE_FULFILLED);
84 }
85
86 /**
87  * Increments to the next combination of promises.
88  * @return true if we have a valid combination.
89  */
90 bool Node::increment_promise() {
91         for (unsigned int i = 0; i < promises.size(); i++) {
92                 if (promises[i] == PROMISE_UNFULFILLED) {
93                         promises[i] = PROMISE_FULFILLED;
94                         while (i > 0) {
95                                 i--;
96                                 if (promises[i] == PROMISE_FULFILLED)
97                                         promises[i] = PROMISE_UNFULFILLED;
98                         }
99                         return true;
100                 }
101         }
102         return false;
103 }
104
105 /**
106  * Returns whether the promise set is empty.
107  * @return true if we have explored all promise combinations.
108  */
109 bool Node::promise_empty() {
110         for (unsigned int i = 0; i < promises.size();i++)
111                 if (promises[i] == PROMISE_UNFULFILLED)
112                         return false;
113         return true;
114 }
115
116 /**
117  * Adds a value from a weakly ordered future write to backtrack to.
118  * @param value is the value to backtrack to.
119  */
120 bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
121         int suitableindex=-1;
122         for (unsigned int i = 0; i < future_values.size(); i++) {
123                 if (future_values[i].value == value) {
124                         if (future_values[i].expiration>=expiration)
125                                 return false;
126                         if (future_index < i) {
127                                 suitableindex=i;
128                         }
129                 }
130         }
131
132         if (suitableindex!=-1) {
133                 future_values[suitableindex].expiration=expiration;
134                 return true;
135         }
136         struct future_value newfv={value, expiration};
137         future_values.push_back(newfv);
138         return true;
139 }
140
141 /**
142  * Checks whether the future_values set for this node is empty.
143  * @return true if the future_values set is empty.
144  */
145 bool Node::future_value_empty() {
146         return ((future_index + 1) >= future_values.size());
147 }
148
149 /**
150  * Checks if the Thread associated with this thread ID has been explored from
151  * this Node already.
152  * @param tid is the thread ID to check
153  * @return true if this thread choice has been explored already, false
154  * otherwise
155  */
156 bool Node::has_been_explored(thread_id_t tid)
157 {
158         int id = id_to_int(tid);
159         return explored_children[id];
160 }
161
162 /**
163  * Checks if the backtracking set is empty.
164  * @return true if the backtracking set is empty
165  */
166 bool Node::backtrack_empty()
167 {
168         return (numBacktracks == 0);
169 }
170
171 /**
172  * Checks whether the readsfrom set for this node is empty.
173  * @return true if the readsfrom set is empty.
174  */
175 bool Node::read_from_empty() {
176         return ((read_from_index+1) >= may_read_from.size());
177 }
178
179 /**
180  * Mark the appropriate backtracking information for exploring a thread choice.
181  * @param act The ModelAction to explore
182  */
183 void Node::explore_child(ModelAction *act)
184 {
185         explore(act->get_tid());
186 }
187
188 /**
189  * Records a backtracking reference for a thread choice within this Node.
190  * Provides feedback as to whether this thread choice is already set for
191  * backtracking.
192  * @return false if the thread was already set to be backtracked, true
193  * otherwise
194  */
195 bool Node::set_backtrack(thread_id_t id)
196 {
197         int i = id_to_int(id);
198         if (backtrack[i])
199                 return false;
200         backtrack[i] = true;
201         numBacktracks++;
202         return true;
203 }
204
205 thread_id_t Node::get_next_backtrack()
206 {
207         /** @todo Find next backtrack */
208         unsigned int i;
209         for (i = 0; i < backtrack.size(); i++)
210                 if (backtrack[i] == true)
211                         break;
212         /* Backtrack set was empty? */
213         ASSERT(i != backtrack.size());
214
215         backtrack[i] = false;
216         numBacktracks--;
217         return int_to_id(i);
218 }
219
220 bool Node::is_enabled(Thread *t)
221 {
222         int thread_id=id_to_int(t->get_id());
223         return thread_id < num_threads && enabled_array[thread_id];
224 }
225
226 /**
227  * Add an action to the may_read_from set.
228  * @param act is the action to add
229  */
230 void Node::add_read_from(const ModelAction *act)
231 {
232         may_read_from.push_back(act);
233 }
234
235 /**
236  * Gets the next 'future_value' value from this Node. Only valid for a node
237  * where this->action is a 'read'.
238  * @return The first element in future_values
239  */
240 uint64_t Node::get_future_value() {
241         ASSERT(future_index<future_values.size());
242         return future_values[future_index].value;
243 }
244
245 modelclock_t Node::get_future_value_expiration() {
246         ASSERT(future_index<future_values.size());
247         return future_values[future_index].expiration;
248 }
249
250
251 int Node::get_read_from_size() {
252         return may_read_from.size();
253 }
254
255 const ModelAction * Node::get_read_from_at(int i) {
256         return may_read_from[i];
257 }
258
259 /**
260  * Gets the next 'may_read_from' action from this Node. Only valid for a node
261  * where this->action is a 'read'.
262  * @return The first element in may_read_from
263  */
264 const ModelAction * Node::get_read_from() {
265         if (read_from_index < may_read_from.size())
266                 return may_read_from[read_from_index];
267         else
268                 return NULL;
269 }
270
271 /**
272  * Increments the index into the readsfrom set to explore the next item.
273  * @return Returns false if we have explored all items.
274  */
275 bool Node::increment_read_from() {
276         read_from_index++;
277         return (read_from_index < may_read_from.size());
278 }
279
280 /**
281  * Increments the index into the future_values set to explore the next item.
282  * @return Returns false if we have explored all values.
283  */
284 bool Node::increment_future_value() {
285         future_index++;
286         return (future_index < future_values.size());
287 }
288
289 void Node::explore(thread_id_t tid)
290 {
291         int i = id_to_int(tid);
292         if (backtrack[i]) {
293                 backtrack[i] = false;
294                 numBacktracks--;
295         }
296         explored_children[i] = true;
297 }
298
299 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
300                                                node_list_t::iterator end)
301 {
302         node_list_t::iterator it;
303
304         for (it = start; it != end; it++)
305                 delete (*it);
306         list->erase(start, end);
307 }
308
309 NodeStack::NodeStack()
310         : total_nodes(0)
311 {
312         node_list.push_back(new Node());
313         total_nodes++;
314         iter = node_list.begin();
315 }
316
317 NodeStack::~NodeStack()
318 {
319         clear_node_list(&node_list, node_list.begin(), node_list.end());
320 }
321
322 void NodeStack::print()
323 {
324         node_list_t::iterator it;
325         printf("............................................\n");
326         printf("NodeStack printing node_list:\n");
327         for (it = node_list.begin(); it != node_list.end(); it++) {
328                 if (it == this->iter)
329                         printf("vvv following action is the current iterator vvv\n");
330                 (*it)->print();
331         }
332         printf("............................................\n");
333 }
334
335 ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
336 {
337         DBG();
338
339         ASSERT(!node_list.empty());
340         node_list_t::iterator it=iter;
341         it++;
342
343         if (it != node_list.end()) {
344                 iter++;
345                 return (*iter)->get_action();
346         }
347
348         /* Record action */
349         get_head()->explore_child(act);
350         node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
351         total_nodes++;
352         iter++;
353         return NULL;
354 }
355
356 /**
357  * Empties the stack of all trailing nodes after a given position and calls the
358  * destructor for each. This function is provided an offset which determines
359  * how many nodes (relative to the current replay state) to save before popping
360  * the stack.
361  * @param numAhead gives the number of Nodes (including this Node) to skip over
362  * before removing nodes.
363  */
364 void NodeStack::pop_restofstack(int numAhead)
365 {
366         /* Diverging from previous execution; clear out remainder of list */
367         node_list_t::iterator it = iter;
368         while (numAhead--)
369                 it++;
370         clear_node_list(&node_list, it, node_list.end());
371 }
372
373 Node * NodeStack::get_head()
374 {
375         if (node_list.empty())
376                 return NULL;
377         return *iter;
378 }
379
380 Node * NodeStack::get_next()
381 {
382         node_list_t::iterator it = iter;
383         if (node_list.empty()) {
384                 DEBUG("Empty\n");
385                 return NULL;
386         }
387         it++;
388         if (it == node_list.end()) {
389                 DEBUG("At end\n");
390                 return NULL;
391         }
392         return *it;
393 }
394
395 void NodeStack::reset_execution()
396 {
397         iter = node_list.begin();
398 }