promise: add is_compatible_exclusive()
[model-checker.git] / model.cc
1 #include <stdio.h>
2 #include <algorithm>
3 #include <mutex>
4 #include <new>
5
6 #include "model.h"
7 #include "action.h"
8 #include "nodestack.h"
9 #include "schedule.h"
10 #include "snapshot-interface.h"
11 #include "common.h"
12 #include "clockvector.h"
13 #include "cyclegraph.h"
14 #include "promise.h"
15 #include "datarace.h"
16 #include "threads-model.h"
17 #include "output.h"
18
19 #define INITIAL_THREAD_ID       0
20
21 ModelChecker *model;
22
23 struct bug_message {
24         bug_message(const char *str) {
25                 const char *fmt = "  [BUG] %s\n";
26                 msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
27                 sprintf(msg, fmt, str);
28         }
29         ~bug_message() { if (msg) snapshot_free(msg); }
30
31         char *msg;
32         void print() { model_print("%s", msg); }
33
34         SNAPSHOTALLOC
35 };
36
37 /**
38  * Structure for holding small ModelChecker members that should be snapshotted
39  */
40 struct model_snapshot_members {
41         model_snapshot_members() :
42                 current_action(NULL),
43                 /* First thread created will have id INITIAL_THREAD_ID */
44                 next_thread_id(INITIAL_THREAD_ID),
45                 used_sequence_numbers(0),
46                 next_backtrack(NULL),
47                 bugs(),
48                 stats(),
49                 failed_promise(false),
50                 too_many_reads(false),
51                 bad_synchronization(false),
52                 asserted(false)
53         { }
54
55         ~model_snapshot_members() {
56                 for (unsigned int i = 0; i < bugs.size(); i++)
57                         delete bugs[i];
58                 bugs.clear();
59         }
60
61         ModelAction *current_action;
62         unsigned int next_thread_id;
63         modelclock_t used_sequence_numbers;
64         ModelAction *next_backtrack;
65         std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
66         struct execution_stats stats;
67         bool failed_promise;
68         bool too_many_reads;
69         /** @brief Incorrectly-ordered synchronization was made */
70         bool bad_synchronization;
71         bool asserted;
72
73         SNAPSHOTALLOC
74 };
75
76 /** @brief Constructor */
77 ModelChecker::ModelChecker(struct model_params params) :
78         /* Initialize default scheduler */
79         params(params),
80         scheduler(new Scheduler()),
81         diverge(NULL),
82         earliest_diverge(NULL),
83         action_trace(new action_list_t()),
84         thread_map(new HashTable<int, Thread *, int>()),
85         obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
86         lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
87         condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
88         obj_thrd_map(new HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 >()),
89         promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
90         futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
91         pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
92         thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
93         thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
94         node_stack(new NodeStack()),
95         priv(new struct model_snapshot_members()),
96         mo_graph(new CycleGraph())
97 {
98         /* Initialize a model-checker thread, for special ModelActions */
99         model_thread = new Thread(get_next_id());
100         thread_map->put(id_to_int(model_thread->get_id()), model_thread);
101 }
102
103 /** @brief Destructor */
104 ModelChecker::~ModelChecker()
105 {
106         for (unsigned int i = 0; i < get_num_threads(); i++)
107                 delete thread_map->get(i);
108         delete thread_map;
109
110         delete obj_thrd_map;
111         delete obj_map;
112         delete lock_waiters_map;
113         delete condvar_waiters_map;
114         delete action_trace;
115
116         for (unsigned int i = 0; i < promises->size(); i++)
117                 delete (*promises)[i];
118         delete promises;
119
120         delete pending_rel_seqs;
121
122         delete thrd_last_action;
123         delete thrd_last_fence_release;
124         delete node_stack;
125         delete scheduler;
126         delete mo_graph;
127         delete priv;
128 }
129
130 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
131 {
132         action_list_t *tmp = hash->get(ptr);
133         if (tmp == NULL) {
134                 tmp = new action_list_t();
135                 hash->put(ptr, tmp);
136         }
137         return tmp;
138 }
139
140 static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
141 {
142         std::vector<action_list_t> *tmp = hash->get(ptr);
143         if (tmp == NULL) {
144                 tmp = new std::vector<action_list_t>();
145                 hash->put(ptr, tmp);
146         }
147         return tmp;
148 }
149
150 /**
151  * Restores user program to initial state and resets all model-checker data
152  * structures.
153  */
154 void ModelChecker::reset_to_initial_state()
155 {
156         DEBUG("+++ Resetting to initial state +++\n");
157         node_stack->reset_execution();
158
159         /* Print all model-checker output before rollback */
160         fflush(model_out);
161
162         snapshot_backtrack_before(0);
163 }
164
165 /** @return a thread ID for a new Thread */
166 thread_id_t ModelChecker::get_next_id()
167 {
168         return priv->next_thread_id++;
169 }
170
171 /** @return the number of user threads created during this execution */
172 unsigned int ModelChecker::get_num_threads() const
173 {
174         return priv->next_thread_id;
175 }
176
177 /**
178  * Must be called from user-thread context (e.g., through the global
179  * thread_current() interface)
180  *
181  * @return The currently executing Thread.
182  */
183 Thread * ModelChecker::get_current_thread() const
184 {
185         return scheduler->get_current_thread();
186 }
187
188 /** @return a sequence number for a new ModelAction */
189 modelclock_t ModelChecker::get_next_seq_num()
190 {
191         return ++priv->used_sequence_numbers;
192 }
193
194 Node * ModelChecker::get_curr_node() const
195 {
196         return node_stack->get_head();
197 }
198
199 /**
200  * @brief Choose the next thread to execute.
201  *
202  * This function chooses the next thread that should execute. It can force the
203  * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
204  * followed by a THREAD_START, or it can enforce execution replay/backtracking.
205  * The model-checker may have no preference regarding the next thread (i.e.,
206  * when exploring a new execution ordering), in which case this will return
207  * NULL.
208  * @param curr The current ModelAction. This action might guide the choice of
209  * next thread.
210  * @return The next thread to run. If the model-checker has no preference, NULL.
211  */
212 Thread * ModelChecker::get_next_thread(ModelAction *curr)
213 {
214         thread_id_t tid;
215
216         if (curr != NULL) {
217                 /* Do not split atomic actions. */
218                 if (curr->is_rmwr())
219                         return thread_current();
220                 else if (curr->get_type() == THREAD_CREATE)
221                         return curr->get_thread_operand();
222         }
223
224         /* Have we completed exploring the preselected path? */
225         if (diverge == NULL)
226                 return NULL;
227
228         /* Else, we are trying to replay an execution */
229         ModelAction *next = node_stack->get_next()->get_action();
230
231         if (next == diverge) {
232                 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
233                         earliest_diverge = diverge;
234
235                 Node *nextnode = next->get_node();
236                 Node *prevnode = nextnode->get_parent();
237                 scheduler->update_sleep_set(prevnode);
238
239                 /* Reached divergence point */
240                 if (nextnode->increment_misc()) {
241                         /* The next node will try to satisfy a different misc_index values. */
242                         tid = next->get_tid();
243                         node_stack->pop_restofstack(2);
244                 } else if (nextnode->increment_promise()) {
245                         /* The next node will try to satisfy a different set of promises. */
246                         tid = next->get_tid();
247                         node_stack->pop_restofstack(2);
248                 } else if (nextnode->increment_read_from()) {
249                         /* The next node will read from a different value. */
250                         tid = next->get_tid();
251                         node_stack->pop_restofstack(2);
252                 } else if (nextnode->increment_future_value()) {
253                         /* The next node will try to read from a different future value. */
254                         tid = next->get_tid();
255                         node_stack->pop_restofstack(2);
256                 } else if (nextnode->increment_relseq_break()) {
257                         /* The next node will try to resolve a release sequence differently */
258                         tid = next->get_tid();
259                         node_stack->pop_restofstack(2);
260                 } else {
261                         ASSERT(prevnode);
262                         /* Make a different thread execute for next step */
263                         scheduler->add_sleep(get_thread(next->get_tid()));
264                         tid = prevnode->get_next_backtrack();
265                         /* Make sure the backtracked thread isn't sleeping. */
266                         node_stack->pop_restofstack(1);
267                         if (diverge == earliest_diverge) {
268                                 earliest_diverge = prevnode->get_action();
269                         }
270                 }
271                 /* The correct sleep set is in the parent node. */
272                 execute_sleep_set();
273
274                 DEBUG("*** Divergence point ***\n");
275
276                 diverge = NULL;
277         } else {
278                 tid = next->get_tid();
279         }
280         DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
281         ASSERT(tid != THREAD_ID_T_NONE);
282         return thread_map->get(id_to_int(tid));
283 }
284
285 /**
286  * We need to know what the next actions of all threads in the sleep
287  * set will be.  This method computes them and stores the actions at
288  * the corresponding thread object's pending action.
289  */
290
291 void ModelChecker::execute_sleep_set()
292 {
293         for (unsigned int i = 0; i < get_num_threads(); i++) {
294                 thread_id_t tid = int_to_id(i);
295                 Thread *thr = get_thread(tid);
296                 if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
297                         thr->set_state(THREAD_RUNNING);
298                         scheduler->next_thread(thr);
299                         Thread::swap(&system_context, thr);
300                         priv->current_action->set_sleep_flag();
301                         thr->set_pending(priv->current_action);
302                 }
303         }
304 }
305
306 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
307 {
308         for (unsigned int i = 0; i < get_num_threads(); i++) {
309                 Thread *thr = get_thread(int_to_id(i));
310                 if (scheduler->is_sleep_set(thr)) {
311                         ModelAction *pending_act = thr->get_pending();
312                         if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
313                                 //Remove this thread from sleep set
314                                 scheduler->remove_sleep(thr);
315                 }
316         }
317 }
318
319 /** @brief Alert the model-checker that an incorrectly-ordered
320  * synchronization was made */
321 void ModelChecker::set_bad_synchronization()
322 {
323         priv->bad_synchronization = true;
324 }
325
326 bool ModelChecker::has_asserted() const
327 {
328         return priv->asserted;
329 }
330
331 void ModelChecker::set_assert()
332 {
333         priv->asserted = true;
334 }
335
336 /**
337  * Check if we are in a deadlock. Should only be called at the end of an
338  * execution, although it should not give false positives in the middle of an
339  * execution (there should be some ENABLED thread).
340  *
341  * @return True if program is in a deadlock; false otherwise
342  */
343 bool ModelChecker::is_deadlocked() const
344 {
345         bool blocking_threads = false;
346         for (unsigned int i = 0; i < get_num_threads(); i++) {
347                 thread_id_t tid = int_to_id(i);
348                 if (is_enabled(tid))
349                         return false;
350                 Thread *t = get_thread(tid);
351                 if (!t->is_model_thread() && t->get_pending())
352                         blocking_threads = true;
353         }
354         return blocking_threads;
355 }
356
357 /**
358  * Check if this is a complete execution. That is, have all thread completed
359  * execution (rather than exiting because sleep sets have forced a redundant
360  * execution).
361  *
362  * @return True if the execution is complete.
363  */
364 bool ModelChecker::is_complete_execution() const
365 {
366         for (unsigned int i = 0; i < get_num_threads(); i++)
367                 if (is_enabled(int_to_id(i)))
368                         return false;
369         return true;
370 }
371
372 /**
373  * @brief Assert a bug in the executing program.
374  *
375  * Use this function to assert any sort of bug in the user program. If the
376  * current trace is feasible (actually, a prefix of some feasible execution),
377  * then this execution will be aborted, printing the appropriate message. If
378  * the current trace is not yet feasible, the error message will be stashed and
379  * printed if the execution ever becomes feasible.
380  *
381  * @param msg Descriptive message for the bug (do not include newline char)
382  * @return True if bug is immediately-feasible
383  */
384 bool ModelChecker::assert_bug(const char *msg)
385 {
386         priv->bugs.push_back(new bug_message(msg));
387
388         if (isfeasibleprefix()) {
389                 set_assert();
390                 return true;
391         }
392         return false;
393 }
394
395 /**
396  * @brief Assert a bug in the executing program, asserted by a user thread
397  * @see ModelChecker::assert_bug
398  * @param msg Descriptive message for the bug (do not include newline char)
399  */
400 void ModelChecker::assert_user_bug(const char *msg)
401 {
402         /* If feasible bug, bail out now */
403         if (assert_bug(msg))
404                 switch_to_master(NULL);
405 }
406
407 /** @return True, if any bugs have been reported for this execution */
408 bool ModelChecker::have_bug_reports() const
409 {
410         return priv->bugs.size() != 0;
411 }
412
413 /** @brief Print bug report listing for this execution (if any bugs exist) */
414 void ModelChecker::print_bugs() const
415 {
416         if (have_bug_reports()) {
417                 model_print("Bug report: %zu bug%s detected\n",
418                                 priv->bugs.size(),
419                                 priv->bugs.size() > 1 ? "s" : "");
420                 for (unsigned int i = 0; i < priv->bugs.size(); i++)
421                         priv->bugs[i]->print();
422         }
423 }
424
425 /**
426  * @brief Record end-of-execution stats
427  *
428  * Must be run when exiting an execution. Records various stats.
429  * @see struct execution_stats
430  */
431 void ModelChecker::record_stats()
432 {
433         stats.num_total++;
434         if (!isfeasibleprefix())
435                 stats.num_infeasible++;
436         else if (have_bug_reports())
437                 stats.num_buggy_executions++;
438         else if (is_complete_execution())
439                 stats.num_complete++;
440         else
441                 stats.num_redundant++;
442 }
443
444 /** @brief Print execution stats */
445 void ModelChecker::print_stats() const
446 {
447         model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
448         model_print("Number of redundant executions: %d\n", stats.num_redundant);
449         model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
450         model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
451         model_print("Total executions: %d\n", stats.num_total);
452         model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
453 }
454
455 /**
456  * @brief End-of-exeuction print
457  * @param printbugs Should any existing bugs be printed?
458  */
459 void ModelChecker::print_execution(bool printbugs) const
460 {
461         print_program_output();
462
463         if (DBG_ENABLED() || params.verbose) {
464                 model_print("Earliest divergence point since last feasible execution:\n");
465                 if (earliest_diverge)
466                         earliest_diverge->print();
467                 else
468                         model_print("(Not set)\n");
469
470                 model_print("\n");
471                 print_stats();
472         }
473
474         /* Don't print invalid bugs */
475         if (printbugs)
476                 print_bugs();
477
478         model_print("\n");
479         print_summary();
480 }
481
482 /**
483  * Queries the model-checker for more executions to explore and, if one
484  * exists, resets the model-checker state to execute a new execution.
485  *
486  * @return If there are more executions to explore, return true. Otherwise,
487  * return false.
488  */
489 bool ModelChecker::next_execution()
490 {
491         DBG();
492         /* Is this execution a feasible execution that's worth bug-checking? */
493         bool complete = isfeasibleprefix() && (is_complete_execution() ||
494                         have_bug_reports());
495
496         /* End-of-execution bug checks */
497         if (complete) {
498                 if (is_deadlocked())
499                         assert_bug("Deadlock detected");
500
501                 checkDataRaces();
502         }
503
504         record_stats();
505
506         /* Output */
507         if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
508                 print_execution(complete);
509         else
510                 clear_program_output();
511
512         if (complete)
513                 earliest_diverge = NULL;
514
515         if ((diverge = get_next_backtrack()) == NULL)
516                 return false;
517
518         if (DBG_ENABLED()) {
519                 model_print("Next execution will diverge at:\n");
520                 diverge->print();
521         }
522
523         reset_to_initial_state();
524         return true;
525 }
526
527 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
528 {
529         switch (act->get_type()) {
530         case ATOMIC_FENCE:
531         case ATOMIC_READ:
532         case ATOMIC_WRITE:
533         case ATOMIC_RMW: {
534                 /* Optimization: relaxed operations don't need backtracking */
535                 if (act->is_relaxed())
536                         return NULL;
537                 /* linear search: from most recent to oldest */
538                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
539                 action_list_t::reverse_iterator rit;
540                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
541                         ModelAction *prev = *rit;
542                         if (prev->could_synchronize_with(act))
543                                 return prev;
544                 }
545                 break;
546         }
547         case ATOMIC_LOCK:
548         case ATOMIC_TRYLOCK: {
549                 /* linear search: from most recent to oldest */
550                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
551                 action_list_t::reverse_iterator rit;
552                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
553                         ModelAction *prev = *rit;
554                         if (act->is_conflicting_lock(prev))
555                                 return prev;
556                 }
557                 break;
558         }
559         case ATOMIC_UNLOCK: {
560                 /* linear search: from most recent to oldest */
561                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
562                 action_list_t::reverse_iterator rit;
563                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
564                         ModelAction *prev = *rit;
565                         if (!act->same_thread(prev) && prev->is_failed_trylock())
566                                 return prev;
567                 }
568                 break;
569         }
570         case ATOMIC_WAIT: {
571                 /* linear search: from most recent to oldest */
572                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
573                 action_list_t::reverse_iterator rit;
574                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
575                         ModelAction *prev = *rit;
576                         if (!act->same_thread(prev) && prev->is_failed_trylock())
577                                 return prev;
578                         if (!act->same_thread(prev) && prev->is_notify())
579                                 return prev;
580                 }
581                 break;
582         }
583
584         case ATOMIC_NOTIFY_ALL:
585         case ATOMIC_NOTIFY_ONE: {
586                 /* linear search: from most recent to oldest */
587                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
588                 action_list_t::reverse_iterator rit;
589                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
590                         ModelAction *prev = *rit;
591                         if (!act->same_thread(prev) && prev->is_wait())
592                                 return prev;
593                 }
594                 break;
595         }
596         default:
597                 break;
598         }
599         return NULL;
600 }
601
602 /** This method finds backtracking points where we should try to
603  * reorder the parameter ModelAction against.
604  *
605  * @param the ModelAction to find backtracking points for.
606  */
607 void ModelChecker::set_backtracking(ModelAction *act)
608 {
609         Thread *t = get_thread(act);
610         ModelAction *prev = get_last_conflict(act);
611         if (prev == NULL)
612                 return;
613
614         Node *node = prev->get_node()->get_parent();
615
616         int low_tid, high_tid;
617         if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
618                 low_tid = id_to_int(act->get_tid());
619                 high_tid = low_tid + 1;
620         } else {
621                 low_tid = 0;
622                 high_tid = get_num_threads();
623         }
624
625         for (int i = low_tid; i < high_tid; i++) {
626                 thread_id_t tid = int_to_id(i);
627
628                 /* Make sure this thread can be enabled here. */
629                 if (i >= node->get_num_threads())
630                         break;
631
632                 /* Don't backtrack into a point where the thread is disabled or sleeping. */
633                 if (node->enabled_status(tid) != THREAD_ENABLED)
634                         continue;
635
636                 /* Check if this has been explored already */
637                 if (node->has_been_explored(tid))
638                         continue;
639
640                 /* See if fairness allows */
641                 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
642                         bool unfair = false;
643                         for (int t = 0; t < node->get_num_threads(); t++) {
644                                 thread_id_t tother = int_to_id(t);
645                                 if (node->is_enabled(tother) && node->has_priority(tother)) {
646                                         unfair = true;
647                                         break;
648                                 }
649                         }
650                         if (unfair)
651                                 continue;
652                 }
653                 /* Cache the latest backtracking point */
654                 set_latest_backtrack(prev);
655
656                 /* If this is a new backtracking point, mark the tree */
657                 if (!node->set_backtrack(tid))
658                         continue;
659                 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
660                                         id_to_int(prev->get_tid()),
661                                         id_to_int(t->get_id()));
662                 if (DBG_ENABLED()) {
663                         prev->print();
664                         act->print();
665                 }
666         }
667 }
668
669 /**
670  * @brief Cache the a backtracking point as the "most recent", if eligible
671  *
672  * Note that this does not prepare the NodeStack for this backtracking
673  * operation, it only caches the action on a per-execution basis
674  *
675  * @param act The operation at which we should explore a different next action
676  * (i.e., backtracking point)
677  * @return True, if this action is now the most recent backtracking point;
678  * false otherwise
679  */
680 bool ModelChecker::set_latest_backtrack(ModelAction *act)
681 {
682         if (!priv->next_backtrack || *act > *priv->next_backtrack) {
683                 priv->next_backtrack = act;
684                 return true;
685         }
686         return false;
687 }
688
689 /**
690  * Returns last backtracking point. The model checker will explore a different
691  * path for this point in the next execution.
692  * @return The ModelAction at which the next execution should diverge.
693  */
694 ModelAction * ModelChecker::get_next_backtrack()
695 {
696         ModelAction *next = priv->next_backtrack;
697         priv->next_backtrack = NULL;
698         return next;
699 }
700
701 /**
702  * Processes a read or rmw model action.
703  * @param curr is the read model action to process.
704  * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
705  * @return True if processing this read updates the mo_graph.
706  */
707 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
708 {
709         uint64_t value = VALUE_NONE;
710         bool updated = false;
711         while (true) {
712                 const ModelAction *reads_from = curr->get_node()->get_read_from();
713                 if (reads_from != NULL) {
714                         mo_graph->startChanges();
715
716                         value = reads_from->get_value();
717                         bool r_status = false;
718
719                         if (!second_part_of_rmw) {
720                                 check_recency(curr, reads_from);
721                                 r_status = r_modification_order(curr, reads_from);
722                         }
723
724                         if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
725                                 mo_graph->rollbackChanges();
726                                 priv->too_many_reads = false;
727                                 continue;
728                         }
729
730                         read_from(curr, reads_from);
731                         mo_graph->commitChanges();
732                         mo_check_promises(curr->get_tid(), reads_from, NULL);
733
734                         updated |= r_status;
735                 } else if (!second_part_of_rmw) {
736                         /* Read from future value */
737                         struct future_value fv = curr->get_node()->get_future_value();
738                         Promise *promise = new Promise(curr, fv);
739                         value = fv.value;
740                         curr->set_read_from_promise(promise);
741                         promises->push_back(promise);
742                         mo_graph->startChanges();
743                         updated = r_modification_order(curr, promise);
744                         mo_graph->commitChanges();
745                 }
746                 get_thread(curr)->set_return_value(value);
747                 return updated;
748         }
749 }
750
751 /**
752  * Processes a lock, trylock, or unlock model action.  @param curr is
753  * the read model action to process.
754  *
755  * The try lock operation checks whether the lock is taken.  If not,
756  * it falls to the normal lock operation case.  If so, it returns
757  * fail.
758  *
759  * The lock operation has already been checked that it is enabled, so
760  * it just grabs the lock and synchronizes with the previous unlock.
761  *
762  * The unlock operation has to re-enable all of the threads that are
763  * waiting on the lock.
764  *
765  * @return True if synchronization was updated; false otherwise
766  */
767 bool ModelChecker::process_mutex(ModelAction *curr)
768 {
769         std::mutex *mutex = NULL;
770         struct std::mutex_state *state = NULL;
771
772         if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
773                 mutex = (std::mutex *)curr->get_location();
774                 state = mutex->get_state();
775         } else if (curr->is_wait()) {
776                 mutex = (std::mutex *)curr->get_value();
777                 state = mutex->get_state();
778         }
779
780         switch (curr->get_type()) {
781         case ATOMIC_TRYLOCK: {
782                 bool success = !state->islocked;
783                 curr->set_try_lock(success);
784                 if (!success) {
785                         get_thread(curr)->set_return_value(0);
786                         break;
787                 }
788                 get_thread(curr)->set_return_value(1);
789         }
790                 //otherwise fall into the lock case
791         case ATOMIC_LOCK: {
792                 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
793                         assert_bug("Lock access before initialization");
794                 state->islocked = true;
795                 ModelAction *unlock = get_last_unlock(curr);
796                 //synchronize with the previous unlock statement
797                 if (unlock != NULL) {
798                         curr->synchronize_with(unlock);
799                         return true;
800                 }
801                 break;
802         }
803         case ATOMIC_UNLOCK: {
804                 //unlock the lock
805                 state->islocked = false;
806                 //wake up the other threads
807                 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
808                 //activate all the waiting threads
809                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
810                         scheduler->wake(get_thread(*rit));
811                 }
812                 waiters->clear();
813                 break;
814         }
815         case ATOMIC_WAIT: {
816                 //unlock the lock
817                 state->islocked = false;
818                 //wake up the other threads
819                 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
820                 //activate all the waiting threads
821                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
822                         scheduler->wake(get_thread(*rit));
823                 }
824                 waiters->clear();
825                 //check whether we should go to sleep or not...simulate spurious failures
826                 if (curr->get_node()->get_misc() == 0) {
827                         get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
828                         //disable us
829                         scheduler->sleep(get_thread(curr));
830                 }
831                 break;
832         }
833         case ATOMIC_NOTIFY_ALL: {
834                 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
835                 //activate all the waiting threads
836                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
837                         scheduler->wake(get_thread(*rit));
838                 }
839                 waiters->clear();
840                 break;
841         }
842         case ATOMIC_NOTIFY_ONE: {
843                 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
844                 int wakeupthread = curr->get_node()->get_misc();
845                 action_list_t::iterator it = waiters->begin();
846                 advance(it, wakeupthread);
847                 scheduler->wake(get_thread(*it));
848                 waiters->erase(it);
849                 break;
850         }
851
852         default:
853                 ASSERT(0);
854         }
855         return false;
856 }
857
858 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
859 {
860         /* Do more ambitious checks now that mo is more complete */
861         if (mo_may_allow(writer, reader)) {
862                 Node *node = reader->get_node();
863
864                 /* Find an ancestor thread which exists at the time of the reader */
865                 Thread *write_thread = get_thread(writer);
866                 while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
867                         write_thread = write_thread->get_parent();
868
869                 struct future_value fv = {
870                         writer->get_value(),
871                         writer->get_seq_number() + params.maxfuturedelay,
872                         write_thread->get_id(),
873                 };
874                 if (node->add_future_value(fv))
875                         set_latest_backtrack(reader);
876         }
877 }
878
879 /**
880  * Process a write ModelAction
881  * @param curr The ModelAction to process
882  * @return True if the mo_graph was updated or promises were resolved
883  */
884 bool ModelChecker::process_write(ModelAction *curr)
885 {
886         bool updated_mod_order = w_modification_order(curr);
887         bool updated_promises = resolve_promises(curr);
888
889         if (promises->size() == 0) {
890                 for (unsigned int i = 0; i < futurevalues->size(); i++) {
891                         struct PendingFutureValue pfv = (*futurevalues)[i];
892                         add_future_value(pfv.writer, pfv.act);
893                 }
894                 futurevalues->clear();
895         }
896
897         mo_graph->commitChanges();
898         mo_check_promises(curr->get_tid(), curr, NULL);
899
900         get_thread(curr)->set_return_value(VALUE_NONE);
901         return updated_mod_order || updated_promises;
902 }
903
904 /**
905  * Process a fence ModelAction
906  * @param curr The ModelAction to process
907  * @return True if synchronization was updated
908  */
909 bool ModelChecker::process_fence(ModelAction *curr)
910 {
911         /*
912          * fence-relaxed: no-op
913          * fence-release: only log the occurence (not in this function), for
914          *   use in later synchronization
915          * fence-acquire (this function): search for hypothetical release
916          *   sequences
917          */
918         bool updated = false;
919         if (curr->is_acquire()) {
920                 action_list_t *list = action_trace;
921                 action_list_t::reverse_iterator rit;
922                 /* Find X : is_read(X) && X --sb-> curr */
923                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
924                         ModelAction *act = *rit;
925                         if (act == curr)
926                                 continue;
927                         if (act->get_tid() != curr->get_tid())
928                                 continue;
929                         /* Stop at the beginning of the thread */
930                         if (act->is_thread_start())
931                                 break;
932                         /* Stop once we reach a prior fence-acquire */
933                         if (act->is_fence() && act->is_acquire())
934                                 break;
935                         if (!act->is_read())
936                                 continue;
937                         /* read-acquire will find its own release sequences */
938                         if (act->is_acquire())
939                                 continue;
940
941                         /* Establish hypothetical release sequences */
942                         rel_heads_list_t release_heads;
943                         get_release_seq_heads(curr, act, &release_heads);
944                         for (unsigned int i = 0; i < release_heads.size(); i++)
945                                 if (!curr->synchronize_with(release_heads[i]))
946                                         set_bad_synchronization();
947                         if (release_heads.size() != 0)
948                                 updated = true;
949                 }
950         }
951         return updated;
952 }
953
954 /**
955  * @brief Process the current action for thread-related activity
956  *
957  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
958  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
959  * synchronization, etc.  This function is a no-op for non-THREAD actions
960  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
961  *
962  * @param curr The current action
963  * @return True if synchronization was updated or a thread completed
964  */
965 bool ModelChecker::process_thread_action(ModelAction *curr)
966 {
967         bool updated = false;
968
969         switch (curr->get_type()) {
970         case THREAD_CREATE: {
971                 Thread *th = curr->get_thread_operand();
972                 th->set_creation(curr);
973                 /* Promises can be satisfied by children */
974                 for (unsigned int i = 0; i < promises->size(); i++) {
975                         Promise *promise = (*promises)[i];
976                         if (promise->thread_is_available(curr->get_tid()))
977                                 promise->add_thread(th->get_id());
978                 }
979                 break;
980         }
981         case THREAD_JOIN: {
982                 Thread *blocking = curr->get_thread_operand();
983                 ModelAction *act = get_last_action(blocking->get_id());
984                 curr->synchronize_with(act);
985                 updated = true; /* trigger rel-seq checks */
986                 break;
987         }
988         case THREAD_FINISH: {
989                 Thread *th = get_thread(curr);
990                 while (!th->wait_list_empty()) {
991                         ModelAction *act = th->pop_wait_list();
992                         scheduler->wake(get_thread(act));
993                 }
994                 th->complete();
995                 /* Completed thread can't satisfy promises */
996                 for (unsigned int i = 0; i < promises->size(); i++) {
997                         Promise *promise = (*promises)[i];
998                         if (promise->thread_is_available(th->get_id()))
999                                 if (promise->eliminate_thread(th->get_id()))
1000                                         priv->failed_promise = true;
1001                 }
1002                 updated = true; /* trigger rel-seq checks */
1003                 break;
1004         }
1005         case THREAD_START: {
1006                 check_promises(curr->get_tid(), NULL, curr->get_cv());
1007                 break;
1008         }
1009         default:
1010                 break;
1011         }
1012
1013         return updated;
1014 }
1015
1016 /**
1017  * @brief Process the current action for release sequence fixup activity
1018  *
1019  * Performs model-checker release sequence fixups for the current action,
1020  * forcing a single pending release sequence to break (with a given, potential
1021  * "loose" write) or to complete (i.e., synchronize). If a pending release
1022  * sequence forms a complete release sequence, then we must perform the fixup
1023  * synchronization, mo_graph additions, etc.
1024  *
1025  * @param curr The current action; must be a release sequence fixup action
1026  * @param work_queue The work queue to which to add work items as they are
1027  * generated
1028  */
1029 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
1030 {
1031         const ModelAction *write = curr->get_node()->get_relseq_break();
1032         struct release_seq *sequence = pending_rel_seqs->back();
1033         pending_rel_seqs->pop_back();
1034         ASSERT(sequence);
1035         ModelAction *acquire = sequence->acquire;
1036         const ModelAction *rf = sequence->rf;
1037         const ModelAction *release = sequence->release;
1038         ASSERT(acquire);
1039         ASSERT(release);
1040         ASSERT(rf);
1041         ASSERT(release->same_thread(rf));
1042
1043         if (write == NULL) {
1044                 /**
1045                  * @todo Forcing a synchronization requires that we set
1046                  * modification order constraints. For instance, we can't allow
1047                  * a fixup sequence in which two separate read-acquire
1048                  * operations read from the same sequence, where the first one
1049                  * synchronizes and the other doesn't. Essentially, we can't
1050                  * allow any writes to insert themselves between 'release' and
1051                  * 'rf'
1052                  */
1053
1054                 /* Must synchronize */
1055                 if (!acquire->synchronize_with(release)) {
1056                         set_bad_synchronization();
1057                         return;
1058                 }
1059                 /* Re-check all pending release sequences */
1060                 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1061                 /* Re-check act for mo_graph edges */
1062                 work_queue->push_back(MOEdgeWorkEntry(acquire));
1063
1064                 /* propagate synchronization to later actions */
1065                 action_list_t::reverse_iterator rit = action_trace->rbegin();
1066                 for (; (*rit) != acquire; rit++) {
1067                         ModelAction *propagate = *rit;
1068                         if (acquire->happens_before(propagate)) {
1069                                 propagate->synchronize_with(acquire);
1070                                 /* Re-check 'propagate' for mo_graph edges */
1071                                 work_queue->push_back(MOEdgeWorkEntry(propagate));
1072                         }
1073                 }
1074         } else {
1075                 /* Break release sequence with new edges:
1076                  *   release --mo--> write --mo--> rf */
1077                 mo_graph->addEdge(release, write);
1078                 mo_graph->addEdge(write, rf);
1079         }
1080
1081         /* See if we have realized a data race */
1082         checkDataRaces();
1083 }
1084
1085 /**
1086  * Initialize the current action by performing one or more of the following
1087  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
1088  * in the NodeStack, manipulating backtracking sets, allocating and
1089  * initializing clock vectors, and computing the promises to fulfill.
1090  *
1091  * @param curr The current action, as passed from the user context; may be
1092  * freed/invalidated after the execution of this function, with a different
1093  * action "returned" its place (pass-by-reference)
1094  * @return True if curr is a newly-explored action; false otherwise
1095  */
1096 bool ModelChecker::initialize_curr_action(ModelAction **curr)
1097 {
1098         ModelAction *newcurr;
1099
1100         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
1101                 newcurr = process_rmw(*curr);
1102                 delete *curr;
1103
1104                 if (newcurr->is_rmw())
1105                         compute_promises(newcurr);
1106
1107                 *curr = newcurr;
1108                 return false;
1109         }
1110
1111         (*curr)->set_seq_number(get_next_seq_num());
1112
1113         newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
1114         if (newcurr) {
1115                 /* First restore type and order in case of RMW operation */
1116                 if ((*curr)->is_rmwr())
1117                         newcurr->copy_typeandorder(*curr);
1118
1119                 ASSERT((*curr)->get_location() == newcurr->get_location());
1120                 newcurr->copy_from_new(*curr);
1121
1122                 /* Discard duplicate ModelAction; use action from NodeStack */
1123                 delete *curr;
1124
1125                 /* Always compute new clock vector */
1126                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1127
1128                 *curr = newcurr;
1129                 return false; /* Action was explored previously */
1130         } else {
1131                 newcurr = *curr;
1132
1133                 /* Always compute new clock vector */
1134                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1135
1136                 /* Assign most recent release fence */
1137                 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
1138
1139                 /*
1140                  * Perform one-time actions when pushing new ModelAction onto
1141                  * NodeStack
1142                  */
1143                 if (newcurr->is_write())
1144                         compute_promises(newcurr);
1145                 else if (newcurr->is_relseq_fixup())
1146                         compute_relseq_breakwrites(newcurr);
1147                 else if (newcurr->is_wait())
1148                         newcurr->get_node()->set_misc_max(2);
1149                 else if (newcurr->is_notify_one()) {
1150                         newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
1151                 }
1152                 return true; /* This was a new ModelAction */
1153         }
1154 }
1155
1156 /**
1157  * @brief Establish reads-from relation between two actions
1158  *
1159  * Perform basic operations involved with establishing a concrete rf relation,
1160  * including setting the ModelAction data and checking for release sequences.
1161  *
1162  * @param act The action that is reading (must be a read)
1163  * @param rf The action from which we are reading (must be a write)
1164  *
1165  * @return True if this read established synchronization
1166  */
1167 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
1168 {
1169         act->set_read_from(rf);
1170         if (rf != NULL && act->is_acquire()) {
1171                 rel_heads_list_t release_heads;
1172                 get_release_seq_heads(act, act, &release_heads);
1173                 int num_heads = release_heads.size();
1174                 for (unsigned int i = 0; i < release_heads.size(); i++)
1175                         if (!act->synchronize_with(release_heads[i])) {
1176                                 set_bad_synchronization();
1177                                 num_heads--;
1178                         }
1179                 return num_heads > 0;
1180         }
1181         return false;
1182 }
1183
1184 /**
1185  * @brief Check whether a model action is enabled.
1186  *
1187  * Checks whether a lock or join operation would be successful (i.e., is the
1188  * lock already locked, or is the joined thread already complete). If not, put
1189  * the action in a waiter list.
1190  *
1191  * @param curr is the ModelAction to check whether it is enabled.
1192  * @return a bool that indicates whether the action is enabled.
1193  */
1194 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1195         if (curr->is_lock()) {
1196                 std::mutex *lock = (std::mutex *)curr->get_location();
1197                 struct std::mutex_state *state = lock->get_state();
1198                 if (state->islocked) {
1199                         //Stick the action in the appropriate waiting queue
1200                         get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1201                         return false;
1202                 }
1203         } else if (curr->get_type() == THREAD_JOIN) {
1204                 Thread *blocking = (Thread *)curr->get_location();
1205                 if (!blocking->is_complete()) {
1206                         blocking->push_wait_list(curr);
1207                         return false;
1208                 }
1209         }
1210
1211         return true;
1212 }
1213
1214 /**
1215  * Stores the ModelAction for the current thread action.  Call this
1216  * immediately before switching from user- to system-context to pass
1217  * data between them.
1218  * @param act The ModelAction created by the user-thread action
1219  */
1220 void ModelChecker::set_current_action(ModelAction *act) {
1221         priv->current_action = act;
1222 }
1223
1224 /**
1225  * This is the heart of the model checker routine. It performs model-checking
1226  * actions corresponding to a given "current action." Among other processes, it
1227  * calculates reads-from relationships, updates synchronization clock vectors,
1228  * forms a memory_order constraints graph, and handles replay/backtrack
1229  * execution when running permutations of previously-observed executions.
1230  *
1231  * @param curr The current action to process
1232  * @return The ModelAction that is actually executed; may be different than
1233  * curr; may be NULL, if the current action is not enabled to run
1234  */
1235 ModelAction * ModelChecker::check_current_action(ModelAction *curr)
1236 {
1237         ASSERT(curr);
1238         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1239
1240         if (!check_action_enabled(curr)) {
1241                 /* Make the execution look like we chose to run this action
1242                  * much later, when a lock/join can succeed */
1243                 get_thread(curr)->set_pending(curr);
1244                 scheduler->sleep(get_thread(curr));
1245                 return NULL;
1246         }
1247
1248         bool newly_explored = initialize_curr_action(&curr);
1249
1250         DBG();
1251         if (DBG_ENABLED())
1252                 curr->print();
1253
1254         wake_up_sleeping_actions(curr);
1255
1256         /* Add the action to lists before any other model-checking tasks */
1257         if (!second_part_of_rmw)
1258                 add_action_to_lists(curr);
1259
1260         /* Build may_read_from set for newly-created actions */
1261         if (newly_explored && curr->is_read())
1262                 build_reads_from_past(curr);
1263
1264         /* Initialize work_queue with the "current action" work */
1265         work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1266         while (!work_queue.empty() && !has_asserted()) {
1267                 WorkQueueEntry work = work_queue.front();
1268                 work_queue.pop_front();
1269
1270                 switch (work.type) {
1271                 case WORK_CHECK_CURR_ACTION: {
1272                         ModelAction *act = work.action;
1273                         bool update = false; /* update this location's release seq's */
1274                         bool update_all = false; /* update all release seq's */
1275
1276                         if (process_thread_action(curr))
1277                                 update_all = true;
1278
1279                         if (act->is_read() && process_read(act, second_part_of_rmw))
1280                                 update = true;
1281
1282                         if (act->is_write() && process_write(act))
1283                                 update = true;
1284
1285                         if (act->is_fence() && process_fence(act))
1286                                 update_all = true;
1287
1288                         if (act->is_mutex_op() && process_mutex(act))
1289                                 update_all = true;
1290
1291                         if (act->is_relseq_fixup())
1292                                 process_relseq_fixup(curr, &work_queue);
1293
1294                         if (update_all)
1295                                 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1296                         else if (update)
1297                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1298                         break;
1299                 }
1300                 case WORK_CHECK_RELEASE_SEQ:
1301                         resolve_release_sequences(work.location, &work_queue);
1302                         break;
1303                 case WORK_CHECK_MO_EDGES: {
1304                         /** @todo Complete verification of work_queue */
1305                         ModelAction *act = work.action;
1306                         bool updated = false;
1307
1308                         if (act->is_read()) {
1309                                 const ModelAction *rf = act->get_reads_from();
1310                                 const Promise *promise = act->get_reads_from_promise();
1311                                 if (rf) {
1312                                         if (r_modification_order(act, rf))
1313                                                 updated = true;
1314                                 } else if (promise) {
1315                                         if (r_modification_order(act, promise))
1316                                                 updated = true;
1317                                 }
1318                         }
1319                         if (act->is_write()) {
1320                                 if (w_modification_order(act))
1321                                         updated = true;
1322                         }
1323                         mo_graph->commitChanges();
1324
1325                         if (updated)
1326                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1327                         break;
1328                 }
1329                 default:
1330                         ASSERT(false);
1331                         break;
1332                 }
1333         }
1334
1335         check_curr_backtracking(curr);
1336         set_backtracking(curr);
1337         return curr;
1338 }
1339
1340 void ModelChecker::check_curr_backtracking(ModelAction *curr)
1341 {
1342         Node *currnode = curr->get_node();
1343         Node *parnode = currnode->get_parent();
1344
1345         if ((parnode && !parnode->backtrack_empty()) ||
1346                          !currnode->misc_empty() ||
1347                          !currnode->read_from_empty() ||
1348                          !currnode->future_value_empty() ||
1349                          !currnode->promise_empty() ||
1350                          !currnode->relseq_break_empty()) {
1351                 set_latest_backtrack(curr);
1352         }
1353 }
1354
1355 bool ModelChecker::promises_expired() const
1356 {
1357         for (unsigned int i = 0; i < promises->size(); i++) {
1358                 Promise *promise = (*promises)[i];
1359                 if (promise->get_expiration() < priv->used_sequence_numbers)
1360                         return true;
1361         }
1362         return false;
1363 }
1364
1365 /**
1366  * This is the strongest feasibility check available.
1367  * @return whether the current trace (partial or complete) must be a prefix of
1368  * a feasible trace.
1369  */
1370 bool ModelChecker::isfeasibleprefix() const
1371 {
1372         return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
1373 }
1374
1375 /**
1376  * Print disagnostic information about an infeasible execution
1377  * @param prefix A string to prefix the output with; if NULL, then a default
1378  * message prefix will be provided
1379  */
1380 void ModelChecker::print_infeasibility(const char *prefix) const
1381 {
1382         char buf[100];
1383         char *ptr = buf;
1384         if (mo_graph->checkForCycles())
1385                 ptr += sprintf(ptr, "[mo cycle]");
1386         if (priv->failed_promise)
1387                 ptr += sprintf(ptr, "[failed promise]");
1388         if (priv->too_many_reads)
1389                 ptr += sprintf(ptr, "[too many reads]");
1390         if (priv->bad_synchronization)
1391                 ptr += sprintf(ptr, "[bad sw ordering]");
1392         if (promises_expired())
1393                 ptr += sprintf(ptr, "[promise expired]");
1394         if (promises->size() != 0)
1395                 ptr += sprintf(ptr, "[unresolved promise]");
1396         if (ptr != buf)
1397                 model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
1398 }
1399
1400 /**
1401  * Returns whether the current completed trace is feasible, except for pending
1402  * release sequences.
1403  */
1404 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
1405 {
1406         return !is_infeasible() && promises->size() == 0;
1407 }
1408
1409 /**
1410  * Check if the current partial trace is infeasible. Does not check any
1411  * end-of-execution flags, which might rule out the execution. Thus, this is
1412  * useful only for ruling an execution as infeasible.
1413  * @return whether the current partial trace is infeasible.
1414  */
1415 bool ModelChecker::is_infeasible() const
1416 {
1417         return mo_graph->checkForCycles() ||
1418                 priv->failed_promise ||
1419                 priv->too_many_reads ||
1420                 priv->bad_synchronization ||
1421                 promises_expired();
1422 }
1423
1424 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1425 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1426         ModelAction *lastread = get_last_action(act->get_tid());
1427         lastread->process_rmw(act);
1428         if (act->is_rmw() && lastread->get_reads_from() != NULL) {
1429                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1430                 mo_graph->commitChanges();
1431         }
1432         return lastread;
1433 }
1434
1435 /**
1436  * Checks whether a thread has read from the same write for too many times
1437  * without seeing the effects of a later write.
1438  *
1439  * Basic idea:
1440  * 1) there must a different write that we could read from that would satisfy the modification order,
1441  * 2) we must have read from the same value in excess of maxreads times, and
1442  * 3) that other write must have been in the reads_from set for maxreads times.
1443  *
1444  * If so, we decide that the execution is no longer feasible.
1445  */
1446 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
1447 {
1448         if (params.maxreads != 0) {
1449                 if (curr->get_node()->get_read_from_size() <= 1)
1450                         return;
1451                 //Must make sure that execution is currently feasible...  We could
1452                 //accidentally clear by rolling back
1453                 if (is_infeasible())
1454                         return;
1455                 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1456                 int tid = id_to_int(curr->get_tid());
1457
1458                 /* Skip checks */
1459                 if ((int)thrd_lists->size() <= tid)
1460                         return;
1461                 action_list_t *list = &(*thrd_lists)[tid];
1462
1463                 action_list_t::reverse_iterator rit = list->rbegin();
1464                 /* Skip past curr */
1465                 for (; (*rit) != curr; rit++)
1466                         ;
1467                 /* go past curr now */
1468                 rit++;
1469
1470                 action_list_t::reverse_iterator ritcopy = rit;
1471                 //See if we have enough reads from the same value
1472                 int count = 0;
1473                 for (; count < params.maxreads; rit++, count++) {
1474                         if (rit == list->rend())
1475                                 return;
1476                         ModelAction *act = *rit;
1477                         if (!act->is_read())
1478                                 return;
1479
1480                         if (act->get_reads_from() != rf)
1481                                 return;
1482                         if (act->get_node()->get_read_from_size() <= 1)
1483                                 return;
1484                 }
1485                 for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
1486                         /* Get write */
1487                         const ModelAction *write = curr->get_node()->get_read_from_at(i);
1488
1489                         /* Need a different write */
1490                         if (write == rf)
1491                                 continue;
1492
1493                         /* Test to see whether this is a feasible write to read from */
1494                         mo_graph->startChanges();
1495                         r_modification_order(curr, write);
1496                         bool feasiblereadfrom = !is_infeasible();
1497                         mo_graph->rollbackChanges();
1498
1499                         if (!feasiblereadfrom)
1500                                 continue;
1501                         rit = ritcopy;
1502
1503                         bool feasiblewrite = true;
1504                         //new we need to see if this write works for everyone
1505
1506                         for (int loop = count; loop > 0; loop--, rit++) {
1507                                 ModelAction *act = *rit;
1508                                 bool foundvalue = false;
1509                                 for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
1510                                         if (act->get_node()->get_read_from_at(j) == write) {
1511                                                 foundvalue = true;
1512                                                 break;
1513                                         }
1514                                 }
1515                                 if (!foundvalue) {
1516                                         feasiblewrite = false;
1517                                         break;
1518                                 }
1519                         }
1520                         if (feasiblewrite) {
1521                                 priv->too_many_reads = true;
1522                                 return;
1523                         }
1524                 }
1525         }
1526 }
1527
1528 /**
1529  * Updates the mo_graph with the constraints imposed from the current
1530  * read.
1531  *
1532  * Basic idea is the following: Go through each other thread and find
1533  * the last action that happened before our read.  Two cases:
1534  *
1535  * (1) The action is a write => that write must either occur before
1536  * the write we read from or be the write we read from.
1537  *
1538  * (2) The action is a read => the write that that action read from
1539  * must occur before the write we read from or be the same write.
1540  *
1541  * @param curr The current action. Must be a read.
1542  * @param rf The ModelAction or Promise that curr reads from. Must be a write.
1543  * @return True if modification order edges were added; false otherwise
1544  */
1545 template <typename rf_type>
1546 bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
1547 {
1548         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1549         unsigned int i;
1550         bool added = false;
1551         ASSERT(curr->is_read());
1552
1553         /* Last SC fence in the current thread */
1554         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1555
1556         /* Iterate over all threads */
1557         for (i = 0; i < thrd_lists->size(); i++) {
1558                 /* Last SC fence in thread i */
1559                 ModelAction *last_sc_fence_thread_local = NULL;
1560                 if (int_to_id((int)i) != curr->get_tid())
1561                         last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
1562
1563                 /* Last SC fence in thread i, before last SC fence in current thread */
1564                 ModelAction *last_sc_fence_thread_before = NULL;
1565                 if (last_sc_fence_local)
1566                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1567
1568                 /* Iterate over actions in thread, starting from most recent */
1569                 action_list_t *list = &(*thrd_lists)[i];
1570                 action_list_t::reverse_iterator rit;
1571                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1572                         ModelAction *act = *rit;
1573
1574                         if (act->is_write() && !act->equals(rf) && act != curr) {
1575                                 /* C++, Section 29.3 statement 5 */
1576                                 if (curr->is_seqcst() && last_sc_fence_thread_local &&
1577                                                 *act < *last_sc_fence_thread_local) {
1578                                         added = mo_graph->addEdge(act, rf) || added;
1579                                         break;
1580                                 }
1581                                 /* C++, Section 29.3 statement 4 */
1582                                 else if (act->is_seqcst() && last_sc_fence_local &&
1583                                                 *act < *last_sc_fence_local) {
1584                                         added = mo_graph->addEdge(act, rf) || added;
1585                                         break;
1586                                 }
1587                                 /* C++, Section 29.3 statement 6 */
1588                                 else if (last_sc_fence_thread_before &&
1589                                                 *act < *last_sc_fence_thread_before) {
1590                                         added = mo_graph->addEdge(act, rf) || added;
1591                                         break;
1592                                 }
1593                         }
1594
1595                         /*
1596                          * Include at most one act per-thread that "happens
1597                          * before" curr. Don't consider reflexively.
1598                          */
1599                         if (act->happens_before(curr) && act != curr) {
1600                                 if (act->is_write()) {
1601                                         if (!act->equals(rf)) {
1602                                                 added = mo_graph->addEdge(act, rf) || added;
1603                                         }
1604                                 } else {
1605                                         const ModelAction *prevreadfrom = act->get_reads_from();
1606                                         //if the previous read is unresolved, keep going...
1607                                         if (prevreadfrom == NULL)
1608                                                 continue;
1609
1610                                         if (!prevreadfrom->equals(rf)) {
1611                                                 added = mo_graph->addEdge(prevreadfrom, rf) || added;
1612                                         }
1613                                 }
1614                                 break;
1615                         }
1616                 }
1617         }
1618
1619         return added;
1620 }
1621
1622 /** This method fixes up the modification order when we resolve a
1623  *  promises.  The basic problem is that actions that occur after the
1624  *  read curr could not property add items to the modification order
1625  *  for our read.
1626  *
1627  *  So for each thread, we find the earliest item that happens after
1628  *  the read curr.  This is the item we have to fix up with additional
1629  *  constraints.  If that action is write, we add a MO edge between
1630  *  the Action rf and that action.  If the action is a read, we add a
1631  *  MO edge between the Action rf, and whatever the read accessed.
1632  *
1633  * @param curr is the read ModelAction that we are fixing up MO edges for.
1634  * @param rf is the write ModelAction that curr reads from.
1635  *
1636  */
1637 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1638 {
1639         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1640         unsigned int i;
1641         ASSERT(curr->is_read());
1642
1643         /* Iterate over all threads */
1644         for (i = 0; i < thrd_lists->size(); i++) {
1645                 /* Iterate over actions in thread, starting from most recent */
1646                 action_list_t *list = &(*thrd_lists)[i];
1647                 action_list_t::reverse_iterator rit;
1648                 ModelAction *lastact = NULL;
1649
1650                 /* Find last action that happens after curr that is either not curr or a rmw */
1651                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1652                         ModelAction *act = *rit;
1653                         if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1654                                 lastact = act;
1655                         } else
1656                                 break;
1657                 }
1658
1659                         /* Include at most one act per-thread that "happens before" curr */
1660                 if (lastact != NULL) {
1661                         if (lastact == curr) {
1662                                 //Case 1: The resolved read is a RMW, and we need to make sure
1663                                 //that the write portion of the RMW mod order after rf
1664
1665                                 mo_graph->addEdge(rf, lastact);
1666                         } else if (lastact->is_read()) {
1667                                 //Case 2: The resolved read is a normal read and the next
1668                                 //operation is a read, and we need to make sure the value read
1669                                 //is mod ordered after rf
1670
1671                                 const ModelAction *postreadfrom = lastact->get_reads_from();
1672                                 if (postreadfrom != NULL && rf != postreadfrom)
1673                                         mo_graph->addEdge(rf, postreadfrom);
1674                         } else {
1675                                 //Case 3: The resolved read is a normal read and the next
1676                                 //operation is a write, and we need to make sure that the
1677                                 //write is mod ordered after rf
1678                                 if (lastact != rf)
1679                                         mo_graph->addEdge(rf, lastact);
1680                         }
1681                         break;
1682                 }
1683         }
1684 }
1685
1686 /**
1687  * Updates the mo_graph with the constraints imposed from the current write.
1688  *
1689  * Basic idea is the following: Go through each other thread and find
1690  * the lastest action that happened before our write.  Two cases:
1691  *
1692  * (1) The action is a write => that write must occur before
1693  * the current write
1694  *
1695  * (2) The action is a read => the write that that action read from
1696  * must occur before the current write.
1697  *
1698  * This method also handles two other issues:
1699  *
1700  * (I) Sequential Consistency: Making sure that if the current write is
1701  * seq_cst, that it occurs after the previous seq_cst write.
1702  *
1703  * (II) Sending the write back to non-synchronizing reads.
1704  *
1705  * @param curr The current action. Must be a write.
1706  * @return True if modification order edges were added; false otherwise
1707  */
1708 bool ModelChecker::w_modification_order(ModelAction *curr)
1709 {
1710         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1711         unsigned int i;
1712         bool added = false;
1713         ASSERT(curr->is_write());
1714
1715         if (curr->is_seqcst()) {
1716                 /* We have to at least see the last sequentially consistent write,
1717                          so we are initialized. */
1718                 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
1719                 if (last_seq_cst != NULL) {
1720                         added = mo_graph->addEdge(last_seq_cst, curr) || added;
1721                 }
1722         }
1723
1724         /* Last SC fence in the current thread */
1725         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1726
1727         /* Iterate over all threads */
1728         for (i = 0; i < thrd_lists->size(); i++) {
1729                 /* Last SC fence in thread i, before last SC fence in current thread */
1730                 ModelAction *last_sc_fence_thread_before = NULL;
1731                 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
1732                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1733
1734                 /* Iterate over actions in thread, starting from most recent */
1735                 action_list_t *list = &(*thrd_lists)[i];
1736                 action_list_t::reverse_iterator rit;
1737                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1738                         ModelAction *act = *rit;
1739                         if (act == curr) {
1740                                 /*
1741                                  * 1) If RMW and it actually read from something, then we
1742                                  * already have all relevant edges, so just skip to next
1743                                  * thread.
1744                                  *
1745                                  * 2) If RMW and it didn't read from anything, we should
1746                                  * whatever edge we can get to speed up convergence.
1747                                  *
1748                                  * 3) If normal write, we need to look at earlier actions, so
1749                                  * continue processing list.
1750                                  */
1751                                 if (curr->is_rmw()) {
1752                                         if (curr->get_reads_from() != NULL)
1753                                                 break;
1754                                         else
1755                                                 continue;
1756                                 } else
1757                                         continue;
1758                         }
1759
1760                         /* C++, Section 29.3 statement 7 */
1761                         if (last_sc_fence_thread_before && act->is_write() &&
1762                                         *act < *last_sc_fence_thread_before) {
1763                                 added = mo_graph->addEdge(act, curr) || added;
1764                                 break;
1765                         }
1766
1767                         /*
1768                          * Include at most one act per-thread that "happens
1769                          * before" curr
1770                          */
1771                         if (act->happens_before(curr)) {
1772                                 /*
1773                                  * Note: if act is RMW, just add edge:
1774                                  *   act --mo--> curr
1775                                  * The following edge should be handled elsewhere:
1776                                  *   readfrom(act) --mo--> act
1777                                  */
1778                                 if (act->is_write())
1779                                         added = mo_graph->addEdge(act, curr) || added;
1780                                 else if (act->is_read()) {
1781                                         //if previous read accessed a null, just keep going
1782                                         if (act->get_reads_from() == NULL)
1783                                                 continue;
1784                                         added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
1785                                 }
1786                                 break;
1787                         } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1788                                                      !act->same_thread(curr)) {
1789                                 /* We have an action that:
1790                                    (1) did not happen before us
1791                                    (2) is a read and we are a write
1792                                    (3) cannot synchronize with us
1793                                    (4) is in a different thread
1794                                    =>
1795                                    that read could potentially read from our write.  Note that
1796                                    these checks are overly conservative at this point, we'll
1797                                    do more checks before actually removing the
1798                                    pendingfuturevalue.
1799
1800                                  */
1801                                 if (thin_air_constraint_may_allow(curr, act)) {
1802                                         if (!is_infeasible())
1803                                                 futurevalues->push_back(PendingFutureValue(curr, act));
1804                                         else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
1805                                                 add_future_value(curr, act);
1806                                 }
1807                         }
1808                 }
1809         }
1810
1811         return added;
1812 }
1813
1814 /** Arbitrary reads from the future are not allowed.  Section 29.3
1815  * part 9 places some constraints.  This method checks one result of constraint
1816  * constraint.  Others require compiler support. */
1817 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
1818 {
1819         if (!writer->is_rmw())
1820                 return true;
1821
1822         if (!reader->is_rmw())
1823                 return true;
1824
1825         for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1826                 if (search == reader)
1827                         return false;
1828                 if (search->get_tid() == reader->get_tid() &&
1829                                 search->happens_before(reader))
1830                         break;
1831         }
1832
1833         return true;
1834 }
1835
1836 /**
1837  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1838  * some constraints. This method checks one the following constraint (others
1839  * require compiler support):
1840  *
1841  *   If X --hb-> Y --mo-> Z, then X should not read from Z.
1842  */
1843 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1844 {
1845         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1846         unsigned int i;
1847         /* Iterate over all threads */
1848         for (i = 0; i < thrd_lists->size(); i++) {
1849                 const ModelAction *write_after_read = NULL;
1850
1851                 /* Iterate over actions in thread, starting from most recent */
1852                 action_list_t *list = &(*thrd_lists)[i];
1853                 action_list_t::reverse_iterator rit;
1854                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1855                         ModelAction *act = *rit;
1856
1857                         /* Don't disallow due to act == reader */
1858                         if (!reader->happens_before(act) || reader == act)
1859                                 break;
1860                         else if (act->is_write())
1861                                 write_after_read = act;
1862                         else if (act->is_read() && act->get_reads_from() != NULL)
1863                                 write_after_read = act->get_reads_from();
1864                 }
1865
1866                 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1867                         return false;
1868         }
1869         return true;
1870 }
1871
1872 /**
1873  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1874  * The ModelAction under consideration is expected to be taking part in
1875  * release/acquire synchronization as an object of the "reads from" relation.
1876  * Note that this can only provide release sequence support for RMW chains
1877  * which do not read from the future, as those actions cannot be traced until
1878  * their "promise" is fulfilled. Similarly, we may not even establish the
1879  * presence of a release sequence with certainty, as some modification order
1880  * constraints may be decided further in the future. Thus, this function
1881  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1882  * and a boolean representing certainty.
1883  *
1884  * @param rf The action that might be part of a release sequence. Must be a
1885  * write.
1886  * @param release_heads A pass-by-reference style return parameter. After
1887  * execution of this function, release_heads will contain the heads of all the
1888  * relevant release sequences, if any exists with certainty
1889  * @param pending A pass-by-reference style return parameter which is only used
1890  * when returning false (i.e., uncertain). Returns most information regarding
1891  * an uncertain release sequence, including any write operations that might
1892  * break the sequence.
1893  * @return true, if the ModelChecker is certain that release_heads is complete;
1894  * false otherwise
1895  */
1896 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1897                 rel_heads_list_t *release_heads,
1898                 struct release_seq *pending) const
1899 {
1900         /* Only check for release sequences if there are no cycles */
1901         if (mo_graph->checkForCycles())
1902                 return false;
1903
1904         while (rf) {
1905                 ASSERT(rf->is_write());
1906
1907                 if (rf->is_release())
1908                         release_heads->push_back(rf);
1909                 else if (rf->get_last_fence_release())
1910                         release_heads->push_back(rf->get_last_fence_release());
1911                 if (!rf->is_rmw())
1912                         break; /* End of RMW chain */
1913
1914                 /** @todo Need to be smarter here...  In the linux lock
1915                  * example, this will run to the beginning of the program for
1916                  * every acquire. */
1917                 /** @todo The way to be smarter here is to keep going until 1
1918                  * thread has a release preceded by an acquire and you've seen
1919                  *       both. */
1920
1921                 /* acq_rel RMW is a sufficient stopping condition */
1922                 if (rf->is_acquire() && rf->is_release())
1923                         return true; /* complete */
1924
1925                 rf = rf->get_reads_from();
1926         };
1927         if (!rf) {
1928                 /* read from future: need to settle this later */
1929                 pending->rf = NULL;
1930                 return false; /* incomplete */
1931         }
1932
1933         if (rf->is_release())
1934                 return true; /* complete */
1935
1936         /* else relaxed write
1937          * - check for fence-release in the same thread (29.8, stmt. 3)
1938          * - check modification order for contiguous subsequence
1939          *   -> rf must be same thread as release */
1940
1941         const ModelAction *fence_release = rf->get_last_fence_release();
1942         /* Synchronize with a fence-release unconditionally; we don't need to
1943          * find any more "contiguous subsequence..." for it */
1944         if (fence_release)
1945                 release_heads->push_back(fence_release);
1946
1947         int tid = id_to_int(rf->get_tid());
1948         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
1949         action_list_t *list = &(*thrd_lists)[tid];
1950         action_list_t::const_reverse_iterator rit;
1951
1952         /* Find rf in the thread list */
1953         rit = std::find(list->rbegin(), list->rend(), rf);
1954         ASSERT(rit != list->rend());
1955
1956         /* Find the last {write,fence}-release */
1957         for (; rit != list->rend(); rit++) {
1958                 if (fence_release && *(*rit) < *fence_release)
1959                         break;
1960                 if ((*rit)->is_release())
1961                         break;
1962         }
1963         if (rit == list->rend()) {
1964                 /* No write-release in this thread */
1965                 return true; /* complete */
1966         } else if (fence_release && *(*rit) < *fence_release) {
1967                 /* The fence-release is more recent (and so, "stronger") than
1968                  * the most recent write-release */
1969                 return true; /* complete */
1970         } /* else, need to establish contiguous release sequence */
1971         ModelAction *release = *rit;
1972
1973         ASSERT(rf->same_thread(release));
1974
1975         pending->writes.clear();
1976
1977         bool certain = true;
1978         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1979                 if (id_to_int(rf->get_tid()) == (int)i)
1980                         continue;
1981                 list = &(*thrd_lists)[i];
1982
1983                 /* Can we ensure no future writes from this thread may break
1984                  * the release seq? */
1985                 bool future_ordered = false;
1986
1987                 ModelAction *last = get_last_action(int_to_id(i));
1988                 Thread *th = get_thread(int_to_id(i));
1989                 if ((last && rf->happens_before(last)) ||
1990                                 !is_enabled(th) ||
1991                                 th->is_complete())
1992                         future_ordered = true;
1993
1994                 ASSERT(!th->is_model_thread() || future_ordered);
1995
1996                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1997                         const ModelAction *act = *rit;
1998                         /* Reach synchronization -> this thread is complete */
1999                         if (act->happens_before(release))
2000                                 break;
2001                         if (rf->happens_before(act)) {
2002                                 future_ordered = true;
2003                                 continue;
2004                         }
2005
2006                         /* Only non-RMW writes can break release sequences */
2007                         if (!act->is_write() || act->is_rmw())
2008                                 continue;
2009
2010                         /* Check modification order */
2011                         if (mo_graph->checkReachable(rf, act)) {
2012                                 /* rf --mo--> act */
2013                                 future_ordered = true;
2014                                 continue;
2015                         }
2016                         if (mo_graph->checkReachable(act, release))
2017                                 /* act --mo--> release */
2018                                 break;
2019                         if (mo_graph->checkReachable(release, act) &&
2020                                       mo_graph->checkReachable(act, rf)) {
2021                                 /* release --mo-> act --mo--> rf */
2022                                 return true; /* complete */
2023                         }
2024                         /* act may break release sequence */
2025                         pending->writes.push_back(act);
2026                         certain = false;
2027                 }
2028                 if (!future_ordered)
2029                         certain = false; /* This thread is uncertain */
2030         }
2031
2032         if (certain) {
2033                 release_heads->push_back(release);
2034                 pending->writes.clear();
2035         } else {
2036                 pending->release = release;
2037                 pending->rf = rf;
2038         }
2039         return certain;
2040 }
2041
2042 /**
2043  * An interface for getting the release sequence head(s) with which a
2044  * given ModelAction must synchronize. This function only returns a non-empty
2045  * result when it can locate a release sequence head with certainty. Otherwise,
2046  * it may mark the internal state of the ModelChecker so that it will handle
2047  * the release sequence at a later time, causing @a acquire to update its
2048  * synchronization at some later point in execution.
2049  *
2050  * @param acquire The 'acquire' action that may synchronize with a release
2051  * sequence
2052  * @param read The read action that may read from a release sequence; this may
2053  * be the same as acquire, or else an earlier action in the same thread (i.e.,
2054  * when 'acquire' is a fence-acquire)
2055  * @param release_heads A pass-by-reference return parameter. Will be filled
2056  * with the head(s) of the release sequence(s), if they exists with certainty.
2057  * @see ModelChecker::release_seq_heads
2058  */
2059 void ModelChecker::get_release_seq_heads(ModelAction *acquire,
2060                 ModelAction *read, rel_heads_list_t *release_heads)
2061 {
2062         const ModelAction *rf = read->get_reads_from();
2063         struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
2064         sequence->acquire = acquire;
2065         sequence->read = read;
2066
2067         if (!release_seq_heads(rf, release_heads, sequence)) {
2068                 /* add act to 'lazy checking' list */
2069                 pending_rel_seqs->push_back(sequence);
2070         } else {
2071                 snapshot_free(sequence);
2072         }
2073 }
2074
2075 /**
2076  * Attempt to resolve all stashed operations that might synchronize with a
2077  * release sequence for a given location. This implements the "lazy" portion of
2078  * determining whether or not a release sequence was contiguous, since not all
2079  * modification order information is present at the time an action occurs.
2080  *
2081  * @param location The location/object that should be checked for release
2082  * sequence resolutions. A NULL value means to check all locations.
2083  * @param work_queue The work queue to which to add work items as they are
2084  * generated
2085  * @return True if any updates occurred (new synchronization, new mo_graph
2086  * edges)
2087  */
2088 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
2089 {
2090         bool updated = false;
2091         std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
2092         while (it != pending_rel_seqs->end()) {
2093                 struct release_seq *pending = *it;
2094                 ModelAction *acquire = pending->acquire;
2095                 const ModelAction *read = pending->read;
2096
2097                 /* Only resolve sequences on the given location, if provided */
2098                 if (location && read->get_location() != location) {
2099                         it++;
2100                         continue;
2101                 }
2102
2103                 const ModelAction *rf = read->get_reads_from();
2104                 rel_heads_list_t release_heads;
2105                 bool complete;
2106                 complete = release_seq_heads(rf, &release_heads, pending);
2107                 for (unsigned int i = 0; i < release_heads.size(); i++) {
2108                         if (!acquire->has_synchronized_with(release_heads[i])) {
2109                                 if (acquire->synchronize_with(release_heads[i]))
2110                                         updated = true;
2111                                 else
2112                                         set_bad_synchronization();
2113                         }
2114                 }
2115
2116                 if (updated) {
2117                         /* Re-check all pending release sequences */
2118                         work_queue->push_back(CheckRelSeqWorkEntry(NULL));
2119                         /* Re-check read-acquire for mo_graph edges */
2120                         if (acquire->is_read())
2121                                 work_queue->push_back(MOEdgeWorkEntry(acquire));
2122
2123                         /* propagate synchronization to later actions */
2124                         action_list_t::reverse_iterator rit = action_trace->rbegin();
2125                         for (; (*rit) != acquire; rit++) {
2126                                 ModelAction *propagate = *rit;
2127                                 if (acquire->happens_before(propagate)) {
2128                                         propagate->synchronize_with(acquire);
2129                                         /* Re-check 'propagate' for mo_graph edges */
2130                                         work_queue->push_back(MOEdgeWorkEntry(propagate));
2131                                 }
2132                         }
2133                 }
2134                 if (complete) {
2135                         it = pending_rel_seqs->erase(it);
2136                         snapshot_free(pending);
2137                 } else {
2138                         it++;
2139                 }
2140         }
2141
2142         // If we resolved promises or data races, see if we have realized a data race.
2143         checkDataRaces();
2144
2145         return updated;
2146 }
2147
2148 /**
2149  * Performs various bookkeeping operations for the current ModelAction. For
2150  * instance, adds action to the per-object, per-thread action vector and to the
2151  * action trace list of all thread actions.
2152  *
2153  * @param act is the ModelAction to add.
2154  */
2155 void ModelChecker::add_action_to_lists(ModelAction *act)
2156 {
2157         int tid = id_to_int(act->get_tid());
2158         ModelAction *uninit = NULL;
2159         int uninit_id = -1;
2160         action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
2161         if (list->empty() && act->is_atomic_var()) {
2162                 uninit = new_uninitialized_action(act->get_location());
2163                 uninit_id = id_to_int(uninit->get_tid());
2164                 list->push_back(uninit);
2165         }
2166         list->push_back(act);
2167
2168         action_trace->push_back(act);
2169         if (uninit)
2170                 action_trace->push_front(uninit);
2171
2172         std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
2173         if (tid >= (int)vec->size())
2174                 vec->resize(priv->next_thread_id);
2175         (*vec)[tid].push_back(act);
2176         if (uninit)
2177                 (*vec)[uninit_id].push_front(uninit);
2178
2179         if ((int)thrd_last_action->size() <= tid)
2180                 thrd_last_action->resize(get_num_threads());
2181         (*thrd_last_action)[tid] = act;
2182         if (uninit)
2183                 (*thrd_last_action)[uninit_id] = uninit;
2184
2185         if (act->is_fence() && act->is_release()) {
2186                 if ((int)thrd_last_fence_release->size() <= tid)
2187                         thrd_last_fence_release->resize(get_num_threads());
2188                 (*thrd_last_fence_release)[tid] = act;
2189         }
2190
2191         if (act->is_wait()) {
2192                 void *mutex_loc = (void *) act->get_value();
2193                 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
2194
2195                 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
2196                 if (tid >= (int)vec->size())
2197                         vec->resize(priv->next_thread_id);
2198                 (*vec)[tid].push_back(act);
2199         }
2200 }
2201
2202 /**
2203  * @brief Get the last action performed by a particular Thread
2204  * @param tid The thread ID of the Thread in question
2205  * @return The last action in the thread
2206  */
2207 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
2208 {
2209         int threadid = id_to_int(tid);
2210         if (threadid < (int)thrd_last_action->size())
2211                 return (*thrd_last_action)[id_to_int(tid)];
2212         else
2213                 return NULL;
2214 }
2215
2216 /**
2217  * @brief Get the last fence release performed by a particular Thread
2218  * @param tid The thread ID of the Thread in question
2219  * @return The last fence release in the thread, if one exists; NULL otherwise
2220  */
2221 ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
2222 {
2223         int threadid = id_to_int(tid);
2224         if (threadid < (int)thrd_last_fence_release->size())
2225                 return (*thrd_last_fence_release)[id_to_int(tid)];
2226         else
2227                 return NULL;
2228 }
2229
2230 /**
2231  * Gets the last memory_order_seq_cst write (in the total global sequence)
2232  * performed on a particular object (i.e., memory location), not including the
2233  * current action.
2234  * @param curr The current ModelAction; also denotes the object location to
2235  * check
2236  * @return The last seq_cst write
2237  */
2238 ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
2239 {
2240         void *location = curr->get_location();
2241         action_list_t *list = get_safe_ptr_action(obj_map, location);
2242         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
2243         action_list_t::reverse_iterator rit;
2244         for (rit = list->rbegin(); rit != list->rend(); rit++)
2245                 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
2246                         return *rit;
2247         return NULL;
2248 }
2249
2250 /**
2251  * Gets the last memory_order_seq_cst fence (in the total global sequence)
2252  * performed in a particular thread, prior to a particular fence.
2253  * @param tid The ID of the thread to check
2254  * @param before_fence The fence from which to begin the search; if NULL, then
2255  * search for the most recent fence in the thread.
2256  * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
2257  */
2258 ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
2259 {
2260         /* All fences should have NULL location */
2261         action_list_t *list = get_safe_ptr_action(obj_map, NULL);
2262         action_list_t::reverse_iterator rit = list->rbegin();
2263
2264         if (before_fence) {
2265                 for (; rit != list->rend(); rit++)
2266                         if (*rit == before_fence)
2267                                 break;
2268
2269                 ASSERT(*rit == before_fence);
2270                 rit++;
2271         }
2272
2273         for (; rit != list->rend(); rit++)
2274                 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
2275                         return *rit;
2276         return NULL;
2277 }
2278
2279 /**
2280  * Gets the last unlock operation performed on a particular mutex (i.e., memory
2281  * location). This function identifies the mutex according to the current
2282  * action, which is presumed to perform on the same mutex.
2283  * @param curr The current ModelAction; also denotes the object location to
2284  * check
2285  * @return The last unlock operation
2286  */
2287 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
2288 {
2289         void *location = curr->get_location();
2290         action_list_t *list = get_safe_ptr_action(obj_map, location);
2291         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
2292         action_list_t::reverse_iterator rit;
2293         for (rit = list->rbegin(); rit != list->rend(); rit++)
2294                 if ((*rit)->is_unlock() || (*rit)->is_wait())
2295                         return *rit;
2296         return NULL;
2297 }
2298
2299 ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
2300 {
2301         ModelAction *parent = get_last_action(tid);
2302         if (!parent)
2303                 parent = get_thread(tid)->get_creation();
2304         return parent;
2305 }
2306
2307 /**
2308  * Returns the clock vector for a given thread.
2309  * @param tid The thread whose clock vector we want
2310  * @return Desired clock vector
2311  */
2312 ClockVector * ModelChecker::get_cv(thread_id_t tid) const
2313 {
2314         return get_parent_action(tid)->get_cv();
2315 }
2316
2317 /**
2318  * Resolve a set of Promises with a current write. The set is provided in the
2319  * Node corresponding to @a write.
2320  * @param write The ModelAction that is fulfilling Promises
2321  * @return True if promises were resolved; false otherwise
2322  */
2323 bool ModelChecker::resolve_promises(ModelAction *write)
2324 {
2325         bool resolved = false;
2326         std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
2327
2328         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
2329                 Promise *promise = (*promises)[promise_index];
2330                 if (write->get_node()->get_promise(i)) {
2331                         ModelAction *read = promise->get_action();
2332                         if (read->is_rmw()) {
2333                                 mo_graph->addRMWEdge(write, read);
2334                         }
2335                         read_from(read, write);
2336                         //First fix up the modification order for actions that happened
2337                         //before the read
2338                         r_modification_order(read, write);
2339                         //Next fix up the modification order for actions that happened
2340                         //after the read.
2341                         post_r_modification_order(read, write);
2342                         //Make sure the promise's value matches the write's value
2343                         ASSERT(promise->get_value() == write->get_value());
2344                         delete promise;
2345
2346                         promises->erase(promises->begin() + promise_index);
2347                         actions_to_check.push_back(read);
2348
2349                         resolved = true;
2350                 } else
2351                         promise_index++;
2352         }
2353
2354         //Check whether reading these writes has made threads unable to
2355         //resolve promises
2356
2357         for (unsigned int i = 0; i < actions_to_check.size(); i++) {
2358                 ModelAction *read=actions_to_check[i];
2359                 mo_check_promises(read->get_tid(), write, read);
2360         }
2361
2362         return resolved;
2363 }
2364
2365 /**
2366  * Compute the set of promises that could potentially be satisfied by this
2367  * action. Note that the set computation actually appears in the Node, not in
2368  * ModelChecker.
2369  * @param curr The ModelAction that may satisfy promises
2370  */
2371 void ModelChecker::compute_promises(ModelAction *curr)
2372 {
2373         for (unsigned int i = 0; i < promises->size(); i++) {
2374                 Promise *promise = (*promises)[i];
2375                 const ModelAction *act = promise->get_action();
2376                 if (!act->happens_before(curr) &&
2377                                 act->is_read() &&
2378                                 !act->could_synchronize_with(curr) &&
2379                                 !act->same_thread(curr) &&
2380                                 act->get_location() == curr->get_location() &&
2381                                 promise->get_value() == curr->get_value()) {
2382                         curr->get_node()->set_promise(i, act->is_rmw());
2383                 }
2384         }
2385 }
2386
2387 /** Checks promises in response to change in ClockVector Threads. */
2388 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2389 {
2390         for (unsigned int i = 0; i < promises->size(); i++) {
2391                 Promise *promise = (*promises)[i];
2392                 const ModelAction *act = promise->get_action();
2393                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2394                                 merge_cv->synchronized_since(act)) {
2395                         if (promise->eliminate_thread(tid)) {
2396                                 //Promise has failed
2397                                 priv->failed_promise = true;
2398                                 return;
2399                         }
2400                 }
2401         }
2402 }
2403
2404 void ModelChecker::check_promises_thread_disabled()
2405 {
2406         for (unsigned int i = 0; i < promises->size(); i++) {
2407                 Promise *promise = (*promises)[i];
2408                 if (promise->has_failed()) {
2409                         priv->failed_promise = true;
2410                         return;
2411                 }
2412         }
2413 }
2414
2415 /**
2416  * @brief Checks promises in response to addition to modification order for
2417  * threads.
2418  *
2419  * Definitions:
2420  *
2421  * pthread is the thread that performed the read that created the promise
2422  *
2423  * pread is the read that created the promise
2424  *
2425  * pwrite is either the first write to same location as pread by
2426  * pthread that is sequenced after pread or the write read by the
2427  * first read to the same location as pread by pthread that is
2428  * sequenced after pread.
2429  *
2430  * 1. If tid=pthread, then we check what other threads are reachable
2431  * through the mod order starting with pwrite.  Those threads cannot
2432  * perform a write that will resolve the promise due to modification
2433  * order constraints.
2434  *
2435  * 2. If the tid is not pthread, we check whether pwrite can reach the
2436  * action write through the modification order.  If so, that thread
2437  * cannot perform a future write that will resolve the promise due to
2438  * modificatin order constraints.
2439  *
2440  * @param tid The thread that either read from the model action write, or
2441  * actually did the model action write.
2442  *
2443  * @param write The ModelAction representing the relevant write.
2444  * @param read  The ModelAction that reads a promised write, or NULL otherwise.
2445  */
2446 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
2447 {
2448         void *location = write->get_location();
2449         for (unsigned int i = 0; i < promises->size(); i++) {
2450                 Promise *promise = (*promises)[i];
2451                 const ModelAction *act = promise->get_action();
2452
2453                 // Is this promise on the same location?
2454                 if (act->get_location() != location)
2455                         continue;
2456
2457                 // same thread as the promise
2458                 if (act->get_tid() == tid) {
2459                         // make sure that the reader of this write happens after the promise
2460                         if ((read == NULL) || (promise->get_action()->happens_before(read))) {
2461                                 // do we have a pwrite for the promise, if not, set it
2462                                 if (promise->get_write() == NULL) {
2463                                         promise->set_write(write);
2464                                         // The pwrite cannot happen before the promise
2465                                         if (write->happens_before(act) && (write != act)) {
2466                                                 priv->failed_promise = true;
2467                                                 return;
2468                                         }
2469                                 }
2470
2471                                 if (mo_graph->checkPromise(write, promise)) {
2472                                         priv->failed_promise = true;
2473                                         return;
2474                                 }
2475                         }
2476                 }
2477
2478                 // Don't do any lookups twice for the same thread
2479                 if (!promise->thread_is_available(tid))
2480                         continue;
2481
2482                 if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
2483                         if (promise->eliminate_thread(tid)) {
2484                                 priv->failed_promise = true;
2485                                 return;
2486                         }
2487                 }
2488         }
2489 }
2490
2491 /**
2492  * Compute the set of writes that may break the current pending release
2493  * sequence. This information is extracted from previou release sequence
2494  * calculations.
2495  *
2496  * @param curr The current ModelAction. Must be a release sequence fixup
2497  * action.
2498  */
2499 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2500 {
2501         if (pending_rel_seqs->empty())
2502                 return;
2503
2504         struct release_seq *pending = pending_rel_seqs->back();
2505         for (unsigned int i = 0; i < pending->writes.size(); i++) {
2506                 const ModelAction *write = pending->writes[i];
2507                 curr->get_node()->add_relseq_break(write);
2508         }
2509
2510         /* NULL means don't break the sequence; just synchronize */
2511         curr->get_node()->add_relseq_break(NULL);
2512 }
2513
2514 /**
2515  * Build up an initial set of all past writes that this 'read' action may read
2516  * from. This set is determined by the clock vector's "happens before"
2517  * relationship.
2518  * @param curr is the current ModelAction that we are exploring; it must be a
2519  * 'read' operation.
2520  */
2521 void ModelChecker::build_reads_from_past(ModelAction *curr)
2522 {
2523         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2524         unsigned int i;
2525         ASSERT(curr->is_read());
2526
2527         ModelAction *last_sc_write = NULL;
2528
2529         if (curr->is_seqcst())
2530                 last_sc_write = get_last_seq_cst_write(curr);
2531
2532         /* Iterate over all threads */
2533         for (i = 0; i < thrd_lists->size(); i++) {
2534                 /* Iterate over actions in thread, starting from most recent */
2535                 action_list_t *list = &(*thrd_lists)[i];
2536                 action_list_t::reverse_iterator rit;
2537                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2538                         ModelAction *act = *rit;
2539
2540                         /* Only consider 'write' actions */
2541                         if (!act->is_write() || act == curr)
2542                                 continue;
2543
2544                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2545                         bool allow_read = true;
2546
2547                         if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
2548                                 allow_read = false;
2549                         else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
2550                                 allow_read = false;
2551
2552                         if (allow_read)
2553                                 curr->get_node()->add_read_from(act);
2554
2555                         /* Include at most one act per-thread that "happens before" curr */
2556                         if (act->happens_before(curr))
2557                                 break;
2558                 }
2559         }
2560
2561         if (DBG_ENABLED()) {
2562                 model_print("Reached read action:\n");
2563                 curr->print();
2564                 model_print("Printing may_read_from\n");
2565                 curr->get_node()->print_may_read_from();
2566                 model_print("End printing may_read_from\n");
2567         }
2568 }
2569
2570 bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
2571 {
2572         while (true) {
2573                 /* UNINIT actions don't have a Node, and they never sleep */
2574                 if (write->is_uninitialized())
2575                         return true;
2576                 Node *prevnode = write->get_node()->get_parent();
2577
2578                 bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
2579                 if (write->is_release() && thread_sleep)
2580                         return true;
2581                 if (!write->is_rmw()) {
2582                         return false;
2583                 }
2584                 if (write->get_reads_from() == NULL)
2585                         return true;
2586                 write = write->get_reads_from();
2587         }
2588 }
2589
2590 /**
2591  * @brief Create a new action representing an uninitialized atomic
2592  * @param location The memory location of the atomic object
2593  * @return A pointer to a new ModelAction
2594  */
2595 ModelAction * ModelChecker::new_uninitialized_action(void *location) const
2596 {
2597         ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
2598         act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
2599         act->create_cv(NULL);
2600         return act;
2601 }
2602
2603 static void print_list(action_list_t *list)
2604 {
2605         action_list_t::iterator it;
2606
2607         model_print("---------------------------------------------------------------------\n");
2608
2609         unsigned int hash = 0;
2610
2611         for (it = list->begin(); it != list->end(); it++) {
2612                 (*it)->print();
2613                 hash = hash^(hash<<3)^((*it)->hash());
2614         }
2615         model_print("HASH %u\n", hash);
2616         model_print("---------------------------------------------------------------------\n");
2617 }
2618
2619 #if SUPPORT_MOD_ORDER_DUMP
2620 void ModelChecker::dumpGraph(char *filename) const
2621 {
2622         char buffer[200];
2623         sprintf(buffer, "%s.dot", filename);
2624         FILE *file = fopen(buffer, "w");
2625         fprintf(file, "digraph %s {\n", filename);
2626         mo_graph->dumpNodes(file);
2627         ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
2628
2629         for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2630                 ModelAction *action = *it;
2631                 if (action->is_read()) {
2632                         fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
2633                         if (action->get_reads_from() != NULL)
2634                                 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2635                 }
2636                 if (thread_array[action->get_tid()] != NULL) {
2637                         fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2638                 }
2639
2640                 thread_array[action->get_tid()] = action;
2641         }
2642         fprintf(file, "}\n");
2643         model_free(thread_array);
2644         fclose(file);
2645 }
2646 #endif
2647
2648 /** @brief Prints an execution trace summary. */
2649 void ModelChecker::print_summary() const
2650 {
2651 #if SUPPORT_MOD_ORDER_DUMP
2652         char buffername[100];
2653         sprintf(buffername, "exec%04u", stats.num_total);
2654         mo_graph->dumpGraphToFile(buffername);
2655         sprintf(buffername, "graph%04u", stats.num_total);
2656         dumpGraph(buffername);
2657 #endif
2658
2659         model_print("Execution %d:", stats.num_total);
2660         if (isfeasibleprefix())
2661                 model_print("\n");
2662         else
2663                 print_infeasibility(" INFEASIBLE");
2664         print_list(action_trace);
2665         model_print("\n");
2666 }
2667
2668 /**
2669  * Add a Thread to the system for the first time. Should only be called once
2670  * per thread.
2671  * @param t The Thread to add
2672  */
2673 void ModelChecker::add_thread(Thread *t)
2674 {
2675         thread_map->put(id_to_int(t->get_id()), t);
2676         scheduler->add_thread(t);
2677 }
2678
2679 /**
2680  * Removes a thread from the scheduler.
2681  * @param the thread to remove.
2682  */
2683 void ModelChecker::remove_thread(Thread *t)
2684 {
2685         scheduler->remove_thread(t);
2686 }
2687
2688 /**
2689  * @brief Get a Thread reference by its ID
2690  * @param tid The Thread's ID
2691  * @return A Thread reference
2692  */
2693 Thread * ModelChecker::get_thread(thread_id_t tid) const
2694 {
2695         return thread_map->get(id_to_int(tid));
2696 }
2697
2698 /**
2699  * @brief Get a reference to the Thread in which a ModelAction was executed
2700  * @param act The ModelAction
2701  * @return A Thread reference
2702  */
2703 Thread * ModelChecker::get_thread(const ModelAction *act) const
2704 {
2705         return get_thread(act->get_tid());
2706 }
2707
2708 /**
2709  * @brief Check if a Thread is currently enabled
2710  * @param t The Thread to check
2711  * @return True if the Thread is currently enabled
2712  */
2713 bool ModelChecker::is_enabled(Thread *t) const
2714 {
2715         return scheduler->is_enabled(t);
2716 }
2717
2718 /**
2719  * @brief Check if a Thread is currently enabled
2720  * @param tid The ID of the Thread to check
2721  * @return True if the Thread is currently enabled
2722  */
2723 bool ModelChecker::is_enabled(thread_id_t tid) const
2724 {
2725         return scheduler->is_enabled(tid);
2726 }
2727
2728 /**
2729  * Switch from a user-context to the "master thread" context (a.k.a. system
2730  * context). This switch is made with the intention of exploring a particular
2731  * model-checking action (described by a ModelAction object). Must be called
2732  * from a user-thread context.
2733  *
2734  * @param act The current action that will be explored. May be NULL only if
2735  * trace is exiting via an assertion (see ModelChecker::set_assert and
2736  * ModelChecker::has_asserted).
2737  * @return Return the value returned by the current action
2738  */
2739 uint64_t ModelChecker::switch_to_master(ModelAction *act)
2740 {
2741         DBG();
2742         Thread *old = thread_current();
2743         set_current_action(act);
2744         old->set_state(THREAD_READY);
2745         if (Thread::swap(old, &system_context) < 0) {
2746                 perror("swap threads");
2747                 exit(EXIT_FAILURE);
2748         }
2749         return old->get_return_value();
2750 }
2751
2752 /**
2753  * Takes the next step in the execution, if possible.
2754  * @param curr The current step to take
2755  * @return Returns true (success) if a step was taken and false otherwise.
2756  */
2757 bool ModelChecker::take_step(ModelAction *curr)
2758 {
2759         if (has_asserted())
2760                 return false;
2761
2762         Thread *curr_thrd = get_thread(curr);
2763         ASSERT(curr_thrd->get_state() == THREAD_READY);
2764
2765         curr = check_current_action(curr);
2766
2767         /* Infeasible -> don't take any more steps */
2768         if (is_infeasible())
2769                 return false;
2770         else if (isfeasibleprefix() && have_bug_reports()) {
2771                 set_assert();
2772                 return false;
2773         }
2774
2775         if (params.bound != 0)
2776                 if (priv->used_sequence_numbers > params.bound)
2777                         return false;
2778
2779         if (curr_thrd->is_blocked() || curr_thrd->is_complete())
2780                 scheduler->remove_thread(curr_thrd);
2781
2782         Thread *next_thrd = get_next_thread(curr);
2783         next_thrd = scheduler->next_thread(next_thrd);
2784
2785         DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
2786                         next_thrd ? id_to_int(next_thrd->get_id()) : -1);
2787
2788         /*
2789          * Launch end-of-execution release sequence fixups only when there are:
2790          *
2791          * (1) no more user threads to run (or when execution replay chooses
2792          *     the 'model_thread')
2793          * (2) pending release sequences
2794          * (3) pending assertions (i.e., data races)
2795          * (4) no pending promises
2796          */
2797         if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
2798                         is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
2799                 model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2800                                 pending_rel_seqs->size());
2801                 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2802                                 std::memory_order_seq_cst, NULL, VALUE_NONE,
2803                                 model_thread);
2804                 set_current_action(fixup);
2805                 return true;
2806         }
2807
2808         /* next_thrd == NULL -> don't take any more steps */
2809         if (!next_thrd)
2810                 return false;
2811
2812         next_thrd->set_state(THREAD_RUNNING);
2813
2814         if (next_thrd->get_pending() != NULL) {
2815                 /* restart a pending action */
2816                 set_current_action(next_thrd->get_pending());
2817                 next_thrd->set_pending(NULL);
2818                 next_thrd->set_state(THREAD_READY);
2819                 return true;
2820         }
2821
2822         /* Return false only if swap fails with an error */
2823         return (Thread::swap(&system_context, next_thrd) == 0);
2824 }
2825
2826 /** Wrapper to run the user's main function, with appropriate arguments */
2827 void user_main_wrapper(void *)
2828 {
2829         user_main(model->params.argc, model->params.argv);
2830 }
2831
2832 /** @brief Run ModelChecker for the user program */
2833 void ModelChecker::run()
2834 {
2835         do {
2836                 thrd_t user_thread;
2837                 Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
2838
2839                 add_thread(t);
2840
2841                 /* Run user thread up to its first action */
2842                 scheduler->next_thread(t);
2843                 Thread::swap(&system_context, t);
2844
2845                 /* Wait for all threads to complete */
2846                 while (take_step(priv->current_action));
2847         } while (next_execution());
2848
2849         print_stats();
2850 }