3cde3456bb9363bc08f2549035166b6f7fe3bd15
[model-checker.git] / nodestack.cc
1 #define __STDC_FORMAT_MACROS
2 #include <inttypes.h>
3
4 #include <string.h>
5
6 #include "nodestack.h"
7 #include "action.h"
8 #include "common.h"
9 #include "model.h"
10 #include "threads-model.h"
11 #include "modeltypes.h"
12
13 /**
14  * @brief Node constructor
15  *
16  * Constructs a single Node for use in a NodeStack. Each Node is associated
17  * with exactly one ModelAction (exception: the first Node should be created
18  * as an empty stub, to represent the first thread "choice") and up to one
19  * parent.
20  *
21  * @param act The ModelAction to associate with this Node. May be NULL.
22  * @param par The parent Node in the NodeStack. May be NULL if there is no
23  * parent.
24  * @param nthreads The number of threads which exist at this point in the
25  * execution trace.
26  */
27 Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
28         read_from_status(READ_FROM_PAST),
29         action(act),
30         parent(par),
31         num_threads(nthreads),
32         explored_children(num_threads),
33         backtrack(num_threads),
34         fairness(num_threads),
35         numBacktracks(0),
36         enabled_array(NULL),
37         read_from_past(),
38         read_from_past_idx(0),
39         read_from_promises(),
40         read_from_promise_idx(-1),
41         future_values(),
42         future_index(-1),
43         relseq_break_writes(),
44         relseq_break_index(0),
45         misc_index(0),
46         misc_max(0)
47 {
48         ASSERT(act);
49         act->set_node(this);
50         int currtid = id_to_int(act->get_tid());
51         int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0;
52
53         if (model->params.fairwindow != 0) {
54                 for (int i = 0; i < num_threads; i++) {
55                         ASSERT(i < ((int)fairness.size()));
56                         struct fairness_info *fi = &fairness[i];
57                         struct fairness_info *prevfi = (parent && i < parent->get_num_threads()) ? &parent->fairness[i] : NULL;
58                         if (prevfi) {
59                                 *fi = *prevfi;
60                         }
61                         if (parent && parent->is_enabled(int_to_id(i))) {
62                                 fi->enabled_count++;
63                         }
64                         if (i == currtid) {
65                                 fi->turns++;
66                                 fi->priority = false;
67                         }
68                         /* Do window processing */
69                         if (prevfairness != NULL) {
70                                 if (prevfairness->parent->is_enabled(int_to_id(i)))
71                                         fi->enabled_count--;
72                                 if (i == prevtid) {
73                                         fi->turns--;
74                                 }
75                                 /* Need full window to start evaluating
76                                  * conditions
77                                  * If we meet the enabled count and have no
78                                  * turns, give us priority */
79                                 if ((fi->enabled_count >= model->params.enabledcount) &&
80                                                 (fi->turns == 0))
81                                         fi->priority = true;
82                         }
83                 }
84         }
85 }
86
87 /** @brief Node desctructor */
88 Node::~Node()
89 {
90         delete action;
91         if (enabled_array)
92                 model_free(enabled_array);
93 }
94
95 /** Prints debugging info for the ModelAction associated with this Node */
96 void Node::print() const
97 {
98         action->print();
99         model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
100         for (int i = 0; i < (int)backtrack.size(); i++)
101                 if (backtrack[i] == true)
102                         model_print("[%d]", i);
103         model_print("\n");
104
105         model_print("          read from past: %s", read_from_past_empty() ? "empty" : "non-empty ");
106         for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++)
107                 model_print("[%d]", read_from_past[i]->get_seq_number());
108         model_print("\n");
109
110         model_print("          read-from promises: %s", read_from_promise_empty() ? "empty" : "non-empty ");
111         for (int i = read_from_promise_idx + 1; i < (int)read_from_promises.size(); i++)
112                 model_print("[%d]", read_from_promises[i]->get_seq_number());
113         model_print("\n");
114
115         model_print("          future values: %s", future_value_empty() ? "empty" : "non-empty ");
116         for (int i = future_index + 1; i < (int)future_values.size(); i++)
117                 model_print("[%#" PRIx64 "]", future_values[i].value);
118         model_print("\n");
119
120         model_print("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
121         model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
122         model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
123 }
124
125 /**
126  * Sets a promise to explore meeting with the given node.
127  * @param i is the promise index.
128  */
129 void Node::set_promise(unsigned int i, bool is_rmw)
130 {
131         if (i >= promises.size())
132                 promises.resize(i + 1, PROMISE_IGNORE);
133         if (promises[i] == PROMISE_IGNORE) {
134                 promises[i] = PROMISE_UNFULFILLED;
135                 if (is_rmw)
136                         promises[i] |= PROMISE_RMW;
137         }
138 }
139
140 /**
141  * Looks up whether a given promise should be satisfied by this node.
142  * @param i The promise index.
143  * @return true if the promise should be satisfied by the given model action.
144  */
145 bool Node::get_promise(unsigned int i) const
146 {
147         return (i < promises.size()) && ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED);
148 }
149
150 /**
151  * Increments to the next combination of promises.
152  * @return true if we have a valid combination.
153  */
154 bool Node::increment_promise()
155 {
156         DBG();
157         unsigned int rmw_count = 0;
158         for (unsigned int i = 0; i < promises.size(); i++) {
159                 if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED))
160                         rmw_count++;
161         }
162
163         for (unsigned int i = 0; i < promises.size(); i++) {
164                 if ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED) {
165                         if ((rmw_count > 0) && (promises[i] & PROMISE_RMW)) {
166                                 //sending our value to two rmws... not going to work..try next combination
167                                 continue;
168                         }
169                         promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_FULFILLED;
170                         while (i > 0) {
171                                 i--;
172                                 if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED)
173                                         promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_UNFULFILLED;
174                         }
175                         return true;
176                 } else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
177                         rmw_count--;
178                 }
179         }
180         return false;
181 }
182
183 /**
184  * Returns whether the promise set is empty.
185  * @return true if we have explored all promise combinations.
186  */
187 bool Node::promise_empty() const
188 {
189         bool fulfilledrmw = false;
190         for (int i = promises.size() - 1; i >= 0; i--) {
191                 if (promises[i] == PROMISE_UNFULFILLED)
192                         return false;
193                 if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED))
194                         return false;
195                 if (promises[i] == (PROMISE_FULFILLED | PROMISE_RMW))
196                         fulfilledrmw = true;
197         }
198         return true;
199 }
200
201 void Node::set_misc_max(int i)
202 {
203         misc_max = i;
204 }
205
206 int Node::get_misc() const
207 {
208         return misc_index;
209 }
210
211 bool Node::increment_misc()
212 {
213         return (misc_index < misc_max) && ((++misc_index) < misc_max);
214 }
215
216 bool Node::misc_empty() const
217 {
218         return (misc_index + 1) >= misc_max;
219 }
220
221 /**
222  * Checks if the Thread associated with this thread ID has been explored from
223  * this Node already.
224  * @param tid is the thread ID to check
225  * @return true if this thread choice has been explored already, false
226  * otherwise
227  */
228 bool Node::has_been_explored(thread_id_t tid) const
229 {
230         int id = id_to_int(tid);
231         return explored_children[id];
232 }
233
234 /**
235  * Checks if the backtracking set is empty.
236  * @return true if the backtracking set is empty
237  */
238 bool Node::backtrack_empty() const
239 {
240         return (numBacktracks == 0);
241 }
242
243 /**
244  * Mark the appropriate backtracking information for exploring a thread choice.
245  * @param act The ModelAction to explore
246  */
247 void Node::explore_child(ModelAction *act, enabled_type_t *is_enabled)
248 {
249         if (!enabled_array)
250                 enabled_array = (enabled_type_t *)model_malloc(sizeof(enabled_type_t) * num_threads);
251         if (is_enabled != NULL)
252                 memcpy(enabled_array, is_enabled, sizeof(enabled_type_t) * num_threads);
253         else {
254                 for (int i = 0; i < num_threads; i++)
255                         enabled_array[i] = THREAD_DISABLED;
256         }
257
258         explore(act->get_tid());
259 }
260
261 /**
262  * Records a backtracking reference for a thread choice within this Node.
263  * Provides feedback as to whether this thread choice is already set for
264  * backtracking.
265  * @return false if the thread was already set to be backtracked, true
266  * otherwise
267  */
268 bool Node::set_backtrack(thread_id_t id)
269 {
270         int i = id_to_int(id);
271         ASSERT(i < ((int)backtrack.size()));
272         if (backtrack[i])
273                 return false;
274         backtrack[i] = true;
275         numBacktracks++;
276         return true;
277 }
278
279 thread_id_t Node::get_next_backtrack()
280 {
281         /** @todo Find next backtrack */
282         unsigned int i;
283         for (i = 0; i < backtrack.size(); i++)
284                 if (backtrack[i] == true)
285                         break;
286         /* Backtrack set was empty? */
287         ASSERT(i != backtrack.size());
288
289         backtrack[i] = false;
290         numBacktracks--;
291         return int_to_id(i);
292 }
293
294 void Node::clear_backtracking()
295 {
296         for (unsigned int i = 0; i < backtrack.size(); i++)
297                 backtrack[i] = false;
298         for (unsigned int i = 0; i < explored_children.size(); i++)
299                 explored_children[i] = false;
300 }
301
302 bool Node::is_enabled(Thread *t) const
303 {
304         int thread_id = id_to_int(t->get_id());
305         return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
306 }
307
308 enabled_type_t Node::enabled_status(thread_id_t tid) const
309 {
310         int thread_id = id_to_int(tid);
311         if (thread_id < num_threads)
312                 return enabled_array[thread_id];
313         else
314                 return THREAD_DISABLED;
315 }
316
317 bool Node::is_enabled(thread_id_t tid) const
318 {
319         int thread_id = id_to_int(tid);
320         return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
321 }
322
323 bool Node::has_priority(thread_id_t tid) const
324 {
325         return fairness[id_to_int(tid)].priority;
326 }
327
328 /*********************************** read from ********************************/
329
330 /**
331  * Get the current state of the may-read-from set iteration
332  * @return The read-from type we should currently be checking (past or future)
333  */
334 read_from_type_t Node::get_read_from_status()
335 {
336         if (read_from_status == READ_FROM_PAST && read_from_past.empty())
337                 increment_read_from();
338         return read_from_status;
339 }
340
341 /**
342  * Iterate one step in the may-read-from iteration. This includes a step in
343  * reading from the either the past or the future.
344  * @return True if there is a new read-from to explore; false otherwise
345  */
346 bool Node::increment_read_from()
347 {
348         promises.clear();
349         if (increment_read_from_past()) {
350                read_from_status = READ_FROM_PAST;
351                return true;
352         } else if (increment_read_from_promise()) {
353                 read_from_status = READ_FROM_PROMISE;
354                 return true;
355         } else if (increment_future_value()) {
356                 read_from_status = READ_FROM_FUTURE;
357                 return true;
358         }
359         read_from_status = READ_FROM_NONE;
360         return false;
361 }
362
363 /**
364  * @return True if there are any new read-froms to explore
365  */
366 bool Node::read_from_empty() const
367 {
368         return read_from_past_empty() && future_value_empty();
369 }
370
371 /**
372  * Get the total size of the may-read-from set, including both past and future
373  * values
374  * @return The size of may-read-from
375  */
376 unsigned int Node::read_from_size() const
377 {
378         return read_from_past.size() + future_values.size();
379 }
380
381 /******************************* end read from ********************************/
382
383 /****************************** read from past ********************************/
384
385 /** @brief Prints info about read_from_past set */
386 void Node::print_read_from_past()
387 {
388         for (unsigned int i = 0; i < read_from_past.size(); i++)
389                 read_from_past[i]->print();
390 }
391
392 /**
393  * Add an action to the read_from_past set.
394  * @param act is the action to add
395  */
396 void Node::add_read_from_past(const ModelAction *act)
397 {
398         read_from_past.push_back(act);
399 }
400
401 /**
402  * Gets the next 'read_from_past' action from this Node. Only valid for a node
403  * where this->action is a 'read'.
404  * @return The first element in read_from_past
405  */
406 const ModelAction * Node::get_read_from_past() const
407 {
408         if (read_from_past_idx < read_from_past.size())
409                 return read_from_past[read_from_past_idx];
410         else
411                 return NULL;
412 }
413
414 const ModelAction * Node::get_read_from_past(int i) const
415 {
416         return read_from_past[i];
417 }
418
419 int Node::get_read_from_past_size() const
420 {
421         return read_from_past.size();
422 }
423
424 /**
425  * Checks whether the readsfrom set for this node is empty.
426  * @return true if the readsfrom set is empty.
427  */
428 bool Node::read_from_past_empty() const
429 {
430         return ((read_from_past_idx + 1) >= read_from_past.size());
431 }
432
433 /**
434  * Increments the index into the readsfrom set to explore the next item.
435  * @return Returns false if we have explored all items.
436  */
437 bool Node::increment_read_from_past()
438 {
439         DBG();
440         if (read_from_past_idx < read_from_past.size()) {
441                 read_from_past_idx++;
442                 return read_from_past_idx < read_from_past.size();
443         }
444         return false;
445 }
446
447 /************************** end read from past ********************************/
448
449 /***************************** read_from_promises *****************************/
450
451 /**
452  * Add an action to the read_from_promises set.
453  * @param reader The read which generated the Promise; we use the ModelAction
454  * instead of the Promise because the Promise does not last across executions
455  */
456 void Node::add_read_from_promise(const ModelAction *reader)
457 {
458         read_from_promises.push_back(reader);
459 }
460
461 /**
462  * Gets the next 'read-from-promise' from this Node. Only valid for a node
463  * where this->action is a 'read'.
464  * @return The current element in read_from_promises
465  */
466 const Promise * Node::get_read_from_promise() const
467 {
468         if (read_from_promise_idx < 0 || read_from_promise_idx >= ((int)read_from_promises.size()))
469                 return NULL;
470         return read_from_promises[read_from_promise_idx]->get_reads_from_promise();
471 }
472
473 /**
474  * Checks whether the read_from_promises set for this node is empty.
475  * @return true if the read_from_promises set is empty.
476  */
477 bool Node::read_from_promise_empty() const
478 {
479         return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size()));
480 }
481
482 /**
483  * Increments the index into the read_from_promises set to explore the next item.
484  * @return Returns false if we have explored all promises.
485  */
486 bool Node::increment_read_from_promise()
487 {
488         DBG();
489         if (read_from_promise_idx < ((int)read_from_promises.size())) {
490                 read_from_promise_idx++;
491                 return (read_from_promise_idx < ((int)read_from_promises.size()));
492         }
493         return false;
494 }
495
496 /************************* end read_from_promises *****************************/
497
498 /****************************** future values *********************************/
499
500 /**
501  * Adds a value from a weakly ordered future write to backtrack to. This
502  * operation may "fail" if the future value has already been run (within some
503  * sloppiness window of this expiration), or if the futurevalues set has
504  * reached its maximum.
505  * @see model_params.maxfuturevalues
506  *
507  * @param value is the value to backtrack to.
508  * @return True if the future value was successully added; false otherwise
509  */
510 bool Node::add_future_value(struct future_value fv)
511 {
512         uint64_t value = fv.value;
513         modelclock_t expiration = fv.expiration;
514         thread_id_t tid = fv.tid;
515         int idx = -1; /* Highest index where value is found */
516         for (unsigned int i = 0; i < future_values.size(); i++) {
517                 if (future_values[i].value == value && future_values[i].tid == tid) {
518                         if (expiration <= future_values[i].expiration)
519                                 return false;
520                         idx = i;
521                 }
522         }
523         if (idx > future_index) {
524                 /* Future value hasn't been explored; update expiration */
525                 future_values[idx].expiration = expiration;
526                 return true;
527         } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
528                 /* Future value has been explored and is within the "sloppy" window */
529                 return false;
530         }
531
532         /* Limit the size of the future-values set */
533         if (model->params.maxfuturevalues > 0 &&
534                         (int)future_values.size() >= model->params.maxfuturevalues)
535                 return false;
536
537         future_values.push_back(fv);
538         return true;
539 }
540
541 /**
542  * Gets the next 'future_value' from this Node. Only valid for a node where
543  * this->action is a 'read'.
544  * @return The first element in future_values
545  */
546 struct future_value Node::get_future_value() const
547 {
548         ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
549         return future_values[future_index];
550 }
551
552 /**
553  * Checks whether the future_values set for this node is empty.
554  * @return true if the future_values set is empty.
555  */
556 bool Node::future_value_empty() const
557 {
558         return ((future_index + 1) >= ((int)future_values.size()));
559 }
560
561 /**
562  * Increments the index into the future_values set to explore the next item.
563  * @return Returns false if we have explored all values.
564  */
565 bool Node::increment_future_value()
566 {
567         DBG();
568         if (future_index < ((int)future_values.size())) {
569                 future_index++;
570                 return (future_index < ((int)future_values.size()));
571         }
572         return false;
573 }
574
575 /************************** end future values *********************************/
576
577 /**
578  * Add a write ModelAction to the set of writes that may break the release
579  * sequence. This is used during replay exploration of pending release
580  * sequences. This Node must correspond to a release sequence fixup action.
581  *
582  * @param write The write that may break the release sequence. NULL means we
583  * allow the release sequence to synchronize.
584  */
585 void Node::add_relseq_break(const ModelAction *write)
586 {
587         relseq_break_writes.push_back(write);
588 }
589
590 /**
591  * Get the write that may break the current pending release sequence,
592  * according to the replay / divergence pattern.
593  *
594  * @return A write that may break the release sequence. If NULL, that means
595  * the release sequence should not be broken.
596  */
597 const ModelAction * Node::get_relseq_break() const
598 {
599         if (relseq_break_index < (int)relseq_break_writes.size())
600                 return relseq_break_writes[relseq_break_index];
601         else
602                 return NULL;
603 }
604
605 /**
606  * Increments the index into the relseq_break_writes set to explore the next
607  * item.
608  * @return Returns false if we have explored all values.
609  */
610 bool Node::increment_relseq_break()
611 {
612         DBG();
613         promises.clear();
614         if (relseq_break_index < ((int)relseq_break_writes.size())) {
615                 relseq_break_index++;
616                 return (relseq_break_index < ((int)relseq_break_writes.size()));
617         }
618         return false;
619 }
620
621 /**
622  * @return True if all writes that may break the release sequence have been
623  * explored
624  */
625 bool Node::relseq_break_empty() const
626 {
627         return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
628 }
629
630 void Node::explore(thread_id_t tid)
631 {
632         int i = id_to_int(tid);
633         ASSERT(i < ((int)backtrack.size()));
634         if (backtrack[i]) {
635                 backtrack[i] = false;
636                 numBacktracks--;
637         }
638         explored_children[i] = true;
639 }
640
641 NodeStack::NodeStack() :
642         node_list(),
643         head_idx(-1),
644         total_nodes(0)
645 {
646         total_nodes++;
647 }
648
649 NodeStack::~NodeStack()
650 {
651         for (unsigned int i = 0; i < node_list.size(); i++)
652                 delete node_list[i];
653 }
654
655 void NodeStack::print() const
656 {
657         model_print("............................................\n");
658         model_print("NodeStack printing node_list:\n");
659         for (unsigned int it = 0; it < node_list.size(); it++) {
660                 if ((int)it == this->head_idx)
661                         model_print("vvv following action is the current iterator vvv\n");
662                 node_list[it]->print();
663         }
664         model_print("............................................\n");
665 }
666
667 /** Note: The is_enabled set contains what actions were enabled when
668  *  act was chosen. */
669 ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_enabled)
670 {
671         DBG();
672
673         if ((head_idx + 1) < (int)node_list.size()) {
674                 head_idx++;
675                 return node_list[head_idx]->get_action();
676         }
677
678         /* Record action */
679         Node *head = get_head();
680         Node *prevfairness = NULL;
681         if (head) {
682                 head->explore_child(act, is_enabled);
683                 if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow)
684                         prevfairness = node_list[head_idx - model->params.fairwindow];
685         }
686
687         int next_threads = model->get_num_threads();
688         if (act->get_type() == THREAD_CREATE)
689                 next_threads++;
690         node_list.push_back(new Node(act, head, next_threads, prevfairness));
691         total_nodes++;
692         head_idx++;
693         return NULL;
694 }
695
696 /**
697  * Empties the stack of all trailing nodes after a given position and calls the
698  * destructor for each. This function is provided an offset which determines
699  * how many nodes (relative to the current replay state) to save before popping
700  * the stack.
701  * @param numAhead gives the number of Nodes (including this Node) to skip over
702  * before removing nodes.
703  */
704 void NodeStack::pop_restofstack(int numAhead)
705 {
706         /* Diverging from previous execution; clear out remainder of list */
707         unsigned int it = head_idx + numAhead;
708         for (unsigned int i = it; i < node_list.size(); i++)
709                 delete node_list[i];
710         node_list.resize(it);
711         node_list.back()->clear_backtracking();
712 }
713
714 Node * NodeStack::get_head() const
715 {
716         if (node_list.empty() || head_idx < 0)
717                 return NULL;
718         return node_list[head_idx];
719 }
720
721 Node * NodeStack::get_next() const
722 {
723         if (node_list.empty()) {
724                 DEBUG("Empty\n");
725                 return NULL;
726         }
727         unsigned int it = head_idx + 1;
728         if (it == node_list.size()) {
729                 DEBUG("At end\n");
730                 return NULL;
731         }
732         return node_list[it];
733 }
734
735 void NodeStack::reset_execution()
736 {
737         head_idx = -1;
738 }