promise: associate Promises with a set of threads
[c11tester.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
725                         if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
726                                 mo_graph->rollbackChanges();
727                                 priv->too_many_reads = false;
728                                 continue;
729                         }
730
731                         read_from(curr, reads_from);
732                         mo_graph->commitChanges();
733                         mo_check_promises(curr->get_tid(), reads_from, NULL);
734
735                         updated |= r_status;
736                 } else if (!second_part_of_rmw) {
737                         /* Read from future value */
738                         struct future_value fv = curr->get_node()->get_future_value();
739                         value = fv.value;
740                         curr->set_value(fv.value);
741                         curr->set_read_from(NULL);
742                         promises->push_back(new Promise(curr, fv));
743                 }
744                 get_thread(curr)->set_return_value(value);
745                 return updated;
746         }
747 }
748
749 /**
750  * Processes a lock, trylock, or unlock model action.  @param curr is
751  * the read model action to process.
752  *
753  * The try lock operation checks whether the lock is taken.  If not,
754  * it falls to the normal lock operation case.  If so, it returns
755  * fail.
756  *
757  * The lock operation has already been checked that it is enabled, so
758  * it just grabs the lock and synchronizes with the previous unlock.
759  *
760  * The unlock operation has to re-enable all of the threads that are
761  * waiting on the lock.
762  *
763  * @return True if synchronization was updated; false otherwise
764  */
765 bool ModelChecker::process_mutex(ModelAction *curr)
766 {
767         std::mutex *mutex = NULL;
768         struct std::mutex_state *state = NULL;
769
770         if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
771                 mutex = (std::mutex *)curr->get_location();
772                 state = mutex->get_state();
773         } else if (curr->is_wait()) {
774                 mutex = (std::mutex *)curr->get_value();
775                 state = mutex->get_state();
776         }
777
778         switch (curr->get_type()) {
779         case ATOMIC_TRYLOCK: {
780                 bool success = !state->islocked;
781                 curr->set_try_lock(success);
782                 if (!success) {
783                         get_thread(curr)->set_return_value(0);
784                         break;
785                 }
786                 get_thread(curr)->set_return_value(1);
787         }
788                 //otherwise fall into the lock case
789         case ATOMIC_LOCK: {
790                 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
791                         assert_bug("Lock access before initialization");
792                 state->islocked = true;
793                 ModelAction *unlock = get_last_unlock(curr);
794                 //synchronize with the previous unlock statement
795                 if (unlock != NULL) {
796                         curr->synchronize_with(unlock);
797                         return true;
798                 }
799                 break;
800         }
801         case ATOMIC_UNLOCK: {
802                 //unlock the lock
803                 state->islocked = false;
804                 //wake up the other threads
805                 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
806                 //activate all the waiting threads
807                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
808                         scheduler->wake(get_thread(*rit));
809                 }
810                 waiters->clear();
811                 break;
812         }
813         case ATOMIC_WAIT: {
814                 //unlock the lock
815                 state->islocked = false;
816                 //wake up the other threads
817                 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
818                 //activate all the waiting threads
819                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
820                         scheduler->wake(get_thread(*rit));
821                 }
822                 waiters->clear();
823                 //check whether we should go to sleep or not...simulate spurious failures
824                 if (curr->get_node()->get_misc() == 0) {
825                         get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
826                         //disable us
827                         scheduler->sleep(get_thread(curr));
828                 }
829                 break;
830         }
831         case ATOMIC_NOTIFY_ALL: {
832                 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
833                 //activate all the waiting threads
834                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
835                         scheduler->wake(get_thread(*rit));
836                 }
837                 waiters->clear();
838                 break;
839         }
840         case ATOMIC_NOTIFY_ONE: {
841                 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
842                 int wakeupthread = curr->get_node()->get_misc();
843                 action_list_t::iterator it = waiters->begin();
844                 advance(it, wakeupthread);
845                 scheduler->wake(get_thread(*it));
846                 waiters->erase(it);
847                 break;
848         }
849
850         default:
851                 ASSERT(0);
852         }
853         return false;
854 }
855
856 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
857 {
858         /* Do more ambitious checks now that mo is more complete */
859         if (mo_may_allow(writer, reader)) {
860                 Node *node = reader->get_node();
861
862                 /* Find an ancestor thread which exists at the time of the reader */
863                 Thread *write_thread = get_thread(writer);
864                 while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
865                         write_thread = write_thread->get_parent();
866
867                 struct future_value fv = {
868                         writer->get_value(),
869                         writer->get_seq_number() + params.maxfuturedelay,
870                         write_thread->get_id(),
871                 };
872                 if (node->add_future_value(fv))
873                         set_latest_backtrack(reader);
874         }
875 }
876
877 /**
878  * Process a write ModelAction
879  * @param curr The ModelAction to process
880  * @return True if the mo_graph was updated or promises were resolved
881  */
882 bool ModelChecker::process_write(ModelAction *curr)
883 {
884         bool updated_mod_order = w_modification_order(curr);
885         bool updated_promises = resolve_promises(curr);
886
887         if (promises->size() == 0) {
888                 for (unsigned int i = 0; i < futurevalues->size(); i++) {
889                         struct PendingFutureValue pfv = (*futurevalues)[i];
890                         add_future_value(pfv.writer, pfv.act);
891                 }
892                 futurevalues->clear();
893         }
894
895         mo_graph->commitChanges();
896         mo_check_promises(curr->get_tid(), curr, NULL);
897
898         get_thread(curr)->set_return_value(VALUE_NONE);
899         return updated_mod_order || updated_promises;
900 }
901
902 /**
903  * Process a fence ModelAction
904  * @param curr The ModelAction to process
905  * @return True if synchronization was updated
906  */
907 bool ModelChecker::process_fence(ModelAction *curr)
908 {
909         /*
910          * fence-relaxed: no-op
911          * fence-release: only log the occurence (not in this function), for
912          *   use in later synchronization
913          * fence-acquire (this function): search for hypothetical release
914          *   sequences
915          */
916         bool updated = false;
917         if (curr->is_acquire()) {
918                 action_list_t *list = action_trace;
919                 action_list_t::reverse_iterator rit;
920                 /* Find X : is_read(X) && X --sb-> curr */
921                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
922                         ModelAction *act = *rit;
923                         if (act == curr)
924                                 continue;
925                         if (act->get_tid() != curr->get_tid())
926                                 continue;
927                         /* Stop at the beginning of the thread */
928                         if (act->is_thread_start())
929                                 break;
930                         /* Stop once we reach a prior fence-acquire */
931                         if (act->is_fence() && act->is_acquire())
932                                 break;
933                         if (!act->is_read())
934                                 continue;
935                         /* read-acquire will find its own release sequences */
936                         if (act->is_acquire())
937                                 continue;
938
939                         /* Establish hypothetical release sequences */
940                         rel_heads_list_t release_heads;
941                         get_release_seq_heads(curr, act, &release_heads);
942                         for (unsigned int i = 0; i < release_heads.size(); i++)
943                                 if (!curr->synchronize_with(release_heads[i]))
944                                         set_bad_synchronization();
945                         if (release_heads.size() != 0)
946                                 updated = true;
947                 }
948         }
949         return updated;
950 }
951
952 /**
953  * @brief Process the current action for thread-related activity
954  *
955  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
956  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
957  * synchronization, etc.  This function is a no-op for non-THREAD actions
958  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
959  *
960  * @param curr The current action
961  * @return True if synchronization was updated or a thread completed
962  */
963 bool ModelChecker::process_thread_action(ModelAction *curr)
964 {
965         bool updated = false;
966
967         switch (curr->get_type()) {
968         case THREAD_CREATE: {
969                 Thread *th = curr->get_thread_operand();
970                 th->set_creation(curr);
971                 break;
972         }
973         case THREAD_JOIN: {
974                 Thread *blocking = curr->get_thread_operand();
975                 ModelAction *act = get_last_action(blocking->get_id());
976                 curr->synchronize_with(act);
977                 updated = true; /* trigger rel-seq checks */
978                 break;
979         }
980         case THREAD_FINISH: {
981                 Thread *th = get_thread(curr);
982                 while (!th->wait_list_empty()) {
983                         ModelAction *act = th->pop_wait_list();
984                         scheduler->wake(get_thread(act));
985                 }
986                 th->complete();
987                 updated = true; /* trigger rel-seq checks */
988                 break;
989         }
990         case THREAD_START: {
991                 check_promises(curr->get_tid(), NULL, curr->get_cv());
992                 break;
993         }
994         default:
995                 break;
996         }
997
998         return updated;
999 }
1000
1001 /**
1002  * @brief Process the current action for release sequence fixup activity
1003  *
1004  * Performs model-checker release sequence fixups for the current action,
1005  * forcing a single pending release sequence to break (with a given, potential
1006  * "loose" write) or to complete (i.e., synchronize). If a pending release
1007  * sequence forms a complete release sequence, then we must perform the fixup
1008  * synchronization, mo_graph additions, etc.
1009  *
1010  * @param curr The current action; must be a release sequence fixup action
1011  * @param work_queue The work queue to which to add work items as they are
1012  * generated
1013  */
1014 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
1015 {
1016         const ModelAction *write = curr->get_node()->get_relseq_break();
1017         struct release_seq *sequence = pending_rel_seqs->back();
1018         pending_rel_seqs->pop_back();
1019         ASSERT(sequence);
1020         ModelAction *acquire = sequence->acquire;
1021         const ModelAction *rf = sequence->rf;
1022         const ModelAction *release = sequence->release;
1023         ASSERT(acquire);
1024         ASSERT(release);
1025         ASSERT(rf);
1026         ASSERT(release->same_thread(rf));
1027
1028         if (write == NULL) {
1029                 /**
1030                  * @todo Forcing a synchronization requires that we set
1031                  * modification order constraints. For instance, we can't allow
1032                  * a fixup sequence in which two separate read-acquire
1033                  * operations read from the same sequence, where the first one
1034                  * synchronizes and the other doesn't. Essentially, we can't
1035                  * allow any writes to insert themselves between 'release' and
1036                  * 'rf'
1037                  */
1038
1039                 /* Must synchronize */
1040                 if (!acquire->synchronize_with(release)) {
1041                         set_bad_synchronization();
1042                         return;
1043                 }
1044                 /* Re-check all pending release sequences */
1045                 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1046                 /* Re-check act for mo_graph edges */
1047                 work_queue->push_back(MOEdgeWorkEntry(acquire));
1048
1049                 /* propagate synchronization to later actions */
1050                 action_list_t::reverse_iterator rit = action_trace->rbegin();
1051                 for (; (*rit) != acquire; rit++) {
1052                         ModelAction *propagate = *rit;
1053                         if (acquire->happens_before(propagate)) {
1054                                 propagate->synchronize_with(acquire);
1055                                 /* Re-check 'propagate' for mo_graph edges */
1056                                 work_queue->push_back(MOEdgeWorkEntry(propagate));
1057                         }
1058                 }
1059         } else {
1060                 /* Break release sequence with new edges:
1061                  *   release --mo--> write --mo--> rf */
1062                 mo_graph->addEdge(release, write);
1063                 mo_graph->addEdge(write, rf);
1064         }
1065
1066         /* See if we have realized a data race */
1067         checkDataRaces();
1068 }
1069
1070 /**
1071  * Initialize the current action by performing one or more of the following
1072  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
1073  * in the NodeStack, manipulating backtracking sets, allocating and
1074  * initializing clock vectors, and computing the promises to fulfill.
1075  *
1076  * @param curr The current action, as passed from the user context; may be
1077  * freed/invalidated after the execution of this function, with a different
1078  * action "returned" its place (pass-by-reference)
1079  * @return True if curr is a newly-explored action; false otherwise
1080  */
1081 bool ModelChecker::initialize_curr_action(ModelAction **curr)
1082 {
1083         ModelAction *newcurr;
1084
1085         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
1086                 newcurr = process_rmw(*curr);
1087                 delete *curr;
1088
1089                 if (newcurr->is_rmw())
1090                         compute_promises(newcurr);
1091
1092                 *curr = newcurr;
1093                 return false;
1094         }
1095
1096         (*curr)->set_seq_number(get_next_seq_num());
1097
1098         newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
1099         if (newcurr) {
1100                 /* First restore type and order in case of RMW operation */
1101                 if ((*curr)->is_rmwr())
1102                         newcurr->copy_typeandorder(*curr);
1103
1104                 ASSERT((*curr)->get_location() == newcurr->get_location());
1105                 newcurr->copy_from_new(*curr);
1106
1107                 /* Discard duplicate ModelAction; use action from NodeStack */
1108                 delete *curr;
1109
1110                 /* Always compute new clock vector */
1111                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1112
1113                 *curr = newcurr;
1114                 return false; /* Action was explored previously */
1115         } else {
1116                 newcurr = *curr;
1117
1118                 /* Always compute new clock vector */
1119                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1120
1121                 /* Assign most recent release fence */
1122                 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
1123
1124                 /*
1125                  * Perform one-time actions when pushing new ModelAction onto
1126                  * NodeStack
1127                  */
1128                 if (newcurr->is_write())
1129                         compute_promises(newcurr);
1130                 else if (newcurr->is_relseq_fixup())
1131                         compute_relseq_breakwrites(newcurr);
1132                 else if (newcurr->is_wait())
1133                         newcurr->get_node()->set_misc_max(2);
1134                 else if (newcurr->is_notify_one()) {
1135                         newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
1136                 }
1137                 return true; /* This was a new ModelAction */
1138         }
1139 }
1140
1141 /**
1142  * @brief Establish reads-from relation between two actions
1143  *
1144  * Perform basic operations involved with establishing a concrete rf relation,
1145  * including setting the ModelAction data and checking for release sequences.
1146  *
1147  * @param act The action that is reading (must be a read)
1148  * @param rf The action from which we are reading (must be a write)
1149  *
1150  * @return True if this read established synchronization
1151  */
1152 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
1153 {
1154         act->set_read_from(rf);
1155         if (rf != NULL && act->is_acquire()) {
1156                 rel_heads_list_t release_heads;
1157                 get_release_seq_heads(act, act, &release_heads);
1158                 int num_heads = release_heads.size();
1159                 for (unsigned int i = 0; i < release_heads.size(); i++)
1160                         if (!act->synchronize_with(release_heads[i])) {
1161                                 set_bad_synchronization();
1162                                 num_heads--;
1163                         }
1164                 return num_heads > 0;
1165         }
1166         return false;
1167 }
1168
1169 /**
1170  * @brief Check whether a model action is enabled.
1171  *
1172  * Checks whether a lock or join operation would be successful (i.e., is the
1173  * lock already locked, or is the joined thread already complete). If not, put
1174  * the action in a waiter list.
1175  *
1176  * @param curr is the ModelAction to check whether it is enabled.
1177  * @return a bool that indicates whether the action is enabled.
1178  */
1179 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1180         if (curr->is_lock()) {
1181                 std::mutex *lock = (std::mutex *)curr->get_location();
1182                 struct std::mutex_state *state = lock->get_state();
1183                 if (state->islocked) {
1184                         //Stick the action in the appropriate waiting queue
1185                         get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1186                         return false;
1187                 }
1188         } else if (curr->get_type() == THREAD_JOIN) {
1189                 Thread *blocking = (Thread *)curr->get_location();
1190                 if (!blocking->is_complete()) {
1191                         blocking->push_wait_list(curr);
1192                         return false;
1193                 }
1194         }
1195
1196         return true;
1197 }
1198
1199 /**
1200  * Stores the ModelAction for the current thread action.  Call this
1201  * immediately before switching from user- to system-context to pass
1202  * data between them.
1203  * @param act The ModelAction created by the user-thread action
1204  */
1205 void ModelChecker::set_current_action(ModelAction *act) {
1206         priv->current_action = act;
1207 }
1208
1209 /**
1210  * This is the heart of the model checker routine. It performs model-checking
1211  * actions corresponding to a given "current action." Among other processes, it
1212  * calculates reads-from relationships, updates synchronization clock vectors,
1213  * forms a memory_order constraints graph, and handles replay/backtrack
1214  * execution when running permutations of previously-observed executions.
1215  *
1216  * @param curr The current action to process
1217  * @return The ModelAction that is actually executed; may be different than
1218  * curr; may be NULL, if the current action is not enabled to run
1219  */
1220 ModelAction * ModelChecker::check_current_action(ModelAction *curr)
1221 {
1222         ASSERT(curr);
1223         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1224
1225         if (!check_action_enabled(curr)) {
1226                 /* Make the execution look like we chose to run this action
1227                  * much later, when a lock/join can succeed */
1228                 get_thread(curr)->set_pending(curr);
1229                 scheduler->sleep(get_thread(curr));
1230                 return NULL;
1231         }
1232
1233         bool newly_explored = initialize_curr_action(&curr);
1234
1235         DBG();
1236         if (DBG_ENABLED())
1237                 curr->print();
1238
1239         wake_up_sleeping_actions(curr);
1240
1241         /* Add the action to lists before any other model-checking tasks */
1242         if (!second_part_of_rmw)
1243                 add_action_to_lists(curr);
1244
1245         /* Build may_read_from set for newly-created actions */
1246         if (newly_explored && curr->is_read())
1247                 build_reads_from_past(curr);
1248
1249         /* Initialize work_queue with the "current action" work */
1250         work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1251         while (!work_queue.empty() && !has_asserted()) {
1252                 WorkQueueEntry work = work_queue.front();
1253                 work_queue.pop_front();
1254
1255                 switch (work.type) {
1256                 case WORK_CHECK_CURR_ACTION: {
1257                         ModelAction *act = work.action;
1258                         bool update = false; /* update this location's release seq's */
1259                         bool update_all = false; /* update all release seq's */
1260
1261                         if (process_thread_action(curr))
1262                                 update_all = true;
1263
1264                         if (act->is_read() && process_read(act, second_part_of_rmw))
1265                                 update = true;
1266
1267                         if (act->is_write() && process_write(act))
1268                                 update = true;
1269
1270                         if (act->is_fence() && process_fence(act))
1271                                 update_all = true;
1272
1273                         if (act->is_mutex_op() && process_mutex(act))
1274                                 update_all = true;
1275
1276                         if (act->is_relseq_fixup())
1277                                 process_relseq_fixup(curr, &work_queue);
1278
1279                         if (update_all)
1280                                 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1281                         else if (update)
1282                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1283                         break;
1284                 }
1285                 case WORK_CHECK_RELEASE_SEQ:
1286                         resolve_release_sequences(work.location, &work_queue);
1287                         break;
1288                 case WORK_CHECK_MO_EDGES: {
1289                         /** @todo Complete verification of work_queue */
1290                         ModelAction *act = work.action;
1291                         bool updated = false;
1292
1293                         if (act->is_read()) {
1294                                 const ModelAction *rf = act->get_reads_from();
1295                                 if (rf != NULL && r_modification_order(act, rf))
1296                                         updated = true;
1297                         }
1298                         if (act->is_write()) {
1299                                 if (w_modification_order(act))
1300                                         updated = true;
1301                         }
1302                         mo_graph->commitChanges();
1303
1304                         if (updated)
1305                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1306                         break;
1307                 }
1308                 default:
1309                         ASSERT(false);
1310                         break;
1311                 }
1312         }
1313
1314         check_curr_backtracking(curr);
1315         set_backtracking(curr);
1316         return curr;
1317 }
1318
1319 void ModelChecker::check_curr_backtracking(ModelAction *curr)
1320 {
1321         Node *currnode = curr->get_node();
1322         Node *parnode = currnode->get_parent();
1323
1324         if ((parnode && !parnode->backtrack_empty()) ||
1325                          !currnode->misc_empty() ||
1326                          !currnode->read_from_empty() ||
1327                          !currnode->future_value_empty() ||
1328                          !currnode->promise_empty() ||
1329                          !currnode->relseq_break_empty()) {
1330                 set_latest_backtrack(curr);
1331         }
1332 }
1333
1334 bool ModelChecker::promises_expired() const
1335 {
1336         for (unsigned int i = 0; i < promises->size(); i++) {
1337                 Promise *promise = (*promises)[i];
1338                 if (promise->get_expiration() < priv->used_sequence_numbers)
1339                         return true;
1340         }
1341         return false;
1342 }
1343
1344 /**
1345  * This is the strongest feasibility check available.
1346  * @return whether the current trace (partial or complete) must be a prefix of
1347  * a feasible trace.
1348  */
1349 bool ModelChecker::isfeasibleprefix() const
1350 {
1351         return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
1352 }
1353
1354 /**
1355  * Print disagnostic information about an infeasible execution
1356  * @param prefix A string to prefix the output with; if NULL, then a default
1357  * message prefix will be provided
1358  */
1359 void ModelChecker::print_infeasibility(const char *prefix) const
1360 {
1361         char buf[100];
1362         char *ptr = buf;
1363         if (mo_graph->checkForRMWViolation())
1364                 ptr += sprintf(ptr, "[RMW atomicity]");
1365         if (mo_graph->checkForCycles())
1366                 ptr += sprintf(ptr, "[mo cycle]");
1367         if (priv->failed_promise)
1368                 ptr += sprintf(ptr, "[failed promise]");
1369         if (priv->too_many_reads)
1370                 ptr += sprintf(ptr, "[too many reads]");
1371         if (priv->bad_synchronization)
1372                 ptr += sprintf(ptr, "[bad sw ordering]");
1373         if (promises_expired())
1374                 ptr += sprintf(ptr, "[promise expired]");
1375         if (promises->size() != 0)
1376                 ptr += sprintf(ptr, "[unresolved promise]");
1377         if (ptr != buf)
1378                 model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
1379 }
1380
1381 /**
1382  * Returns whether the current completed trace is feasible, except for pending
1383  * release sequences.
1384  */
1385 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
1386 {
1387         return !is_infeasible() && promises->size() == 0;
1388 }
1389
1390 /**
1391  * Check if the current partial trace is infeasible. Does not check any
1392  * end-of-execution flags, which might rule out the execution. Thus, this is
1393  * useful only for ruling an execution as infeasible.
1394  * @return whether the current partial trace is infeasible.
1395  */
1396 bool ModelChecker::is_infeasible() const
1397 {
1398         return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
1399 }
1400
1401 /**
1402  * Check If the current partial trace is infeasible, while ignoring
1403  * infeasibility related to 2 RMW's reading from the same store. It does not
1404  * check end-of-execution feasibility.
1405  * @see ModelChecker::is_infeasible
1406  * @return whether the current partial trace is infeasible, ignoring multiple
1407  * RMWs reading from the same store.
1408  * */
1409 bool ModelChecker::is_infeasible_ignoreRMW() const
1410 {
1411         return mo_graph->checkForCycles() || priv->failed_promise ||
1412                 priv->too_many_reads || priv->bad_synchronization ||
1413                 promises_expired();
1414 }
1415
1416 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1417 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1418         ModelAction *lastread = get_last_action(act->get_tid());
1419         lastread->process_rmw(act);
1420         if (act->is_rmw() && lastread->get_reads_from() != NULL) {
1421                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1422                 mo_graph->commitChanges();
1423         }
1424         return lastread;
1425 }
1426
1427 /**
1428  * Checks whether a thread has read from the same write for too many times
1429  * without seeing the effects of a later write.
1430  *
1431  * Basic idea:
1432  * 1) there must a different write that we could read from that would satisfy the modification order,
1433  * 2) we must have read from the same value in excess of maxreads times, and
1434  * 3) that other write must have been in the reads_from set for maxreads times.
1435  *
1436  * If so, we decide that the execution is no longer feasible.
1437  */
1438 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
1439 {
1440         if (params.maxreads != 0) {
1441                 if (curr->get_node()->get_read_from_size() <= 1)
1442                         return;
1443                 //Must make sure that execution is currently feasible...  We could
1444                 //accidentally clear by rolling back
1445                 if (is_infeasible())
1446                         return;
1447                 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1448                 int tid = id_to_int(curr->get_tid());
1449
1450                 /* Skip checks */
1451                 if ((int)thrd_lists->size() <= tid)
1452                         return;
1453                 action_list_t *list = &(*thrd_lists)[tid];
1454
1455                 action_list_t::reverse_iterator rit = list->rbegin();
1456                 /* Skip past curr */
1457                 for (; (*rit) != curr; rit++)
1458                         ;
1459                 /* go past curr now */
1460                 rit++;
1461
1462                 action_list_t::reverse_iterator ritcopy = rit;
1463                 //See if we have enough reads from the same value
1464                 int count = 0;
1465                 for (; count < params.maxreads; rit++, count++) {
1466                         if (rit == list->rend())
1467                                 return;
1468                         ModelAction *act = *rit;
1469                         if (!act->is_read())
1470                                 return;
1471
1472                         if (act->get_reads_from() != rf)
1473                                 return;
1474                         if (act->get_node()->get_read_from_size() <= 1)
1475                                 return;
1476                 }
1477                 for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
1478                         /* Get write */
1479                         const ModelAction *write = curr->get_node()->get_read_from_at(i);
1480
1481                         /* Need a different write */
1482                         if (write == rf)
1483                                 continue;
1484
1485                         /* Test to see whether this is a feasible write to read from */
1486                         mo_graph->startChanges();
1487                         r_modification_order(curr, write);
1488                         bool feasiblereadfrom = !is_infeasible();
1489                         mo_graph->rollbackChanges();
1490
1491                         if (!feasiblereadfrom)
1492                                 continue;
1493                         rit = ritcopy;
1494
1495                         bool feasiblewrite = true;
1496                         //new we need to see if this write works for everyone
1497
1498                         for (int loop = count; loop > 0; loop--, rit++) {
1499                                 ModelAction *act = *rit;
1500                                 bool foundvalue = false;
1501                                 for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
1502                                         if (act->get_node()->get_read_from_at(j) == write) {
1503                                                 foundvalue = true;
1504                                                 break;
1505                                         }
1506                                 }
1507                                 if (!foundvalue) {
1508                                         feasiblewrite = false;
1509                                         break;
1510                                 }
1511                         }
1512                         if (feasiblewrite) {
1513                                 priv->too_many_reads = true;
1514                                 return;
1515                         }
1516                 }
1517         }
1518 }
1519
1520 /**
1521  * Updates the mo_graph with the constraints imposed from the current
1522  * read.
1523  *
1524  * Basic idea is the following: Go through each other thread and find
1525  * the lastest action that happened before our read.  Two cases:
1526  *
1527  * (1) The action is a write => that write must either occur before
1528  * the write we read from or be the write we read from.
1529  *
1530  * (2) The action is a read => the write that that action read from
1531  * must occur before the write we read from or be the same write.
1532  *
1533  * @param curr The current action. Must be a read.
1534  * @param rf The action that curr reads from. Must be a write.
1535  * @return True if modification order edges were added; false otherwise
1536  */
1537 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
1538 {
1539         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1540         unsigned int i;
1541         bool added = false;
1542         ASSERT(curr->is_read());
1543
1544         /* Last SC fence in the current thread */
1545         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1546
1547         /* Iterate over all threads */
1548         for (i = 0; i < thrd_lists->size(); i++) {
1549                 /* Last SC fence in thread i */
1550                 ModelAction *last_sc_fence_thread_local = NULL;
1551                 if (int_to_id((int)i) != curr->get_tid())
1552                         last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
1553
1554                 /* Last SC fence in thread i, before last SC fence in current thread */
1555                 ModelAction *last_sc_fence_thread_before = NULL;
1556                 if (last_sc_fence_local)
1557                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1558
1559                 /* Iterate over actions in thread, starting from most recent */
1560                 action_list_t *list = &(*thrd_lists)[i];
1561                 action_list_t::reverse_iterator rit;
1562                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1563                         ModelAction *act = *rit;
1564
1565                         if (act->is_write() && act != rf && act != curr) {
1566                                 /* C++, Section 29.3 statement 5 */
1567                                 if (curr->is_seqcst() && last_sc_fence_thread_local &&
1568                                                 *act < *last_sc_fence_thread_local) {
1569                                         mo_graph->addEdge(act, rf);
1570                                         added = true;
1571                                         break;
1572                                 }
1573                                 /* C++, Section 29.3 statement 4 */
1574                                 else if (act->is_seqcst() && last_sc_fence_local &&
1575                                                 *act < *last_sc_fence_local) {
1576                                         mo_graph->addEdge(act, rf);
1577                                         added = true;
1578                                         break;
1579                                 }
1580                                 /* C++, Section 29.3 statement 6 */
1581                                 else if (last_sc_fence_thread_before &&
1582                                                 *act < *last_sc_fence_thread_before) {
1583                                         mo_graph->addEdge(act, rf);
1584                                         added = true;
1585                                         break;
1586                                 }
1587                         }
1588
1589                         /*
1590                          * Include at most one act per-thread that "happens
1591                          * before" curr. Don't consider reflexively.
1592                          */
1593                         if (act->happens_before(curr) && act != curr) {
1594                                 if (act->is_write()) {
1595                                         if (rf != act) {
1596                                                 mo_graph->addEdge(act, rf);
1597                                                 added = true;
1598                                         }
1599                                 } else {
1600                                         const ModelAction *prevreadfrom = act->get_reads_from();
1601                                         //if the previous read is unresolved, keep going...
1602                                         if (prevreadfrom == NULL)
1603                                                 continue;
1604
1605                                         if (rf != prevreadfrom) {
1606                                                 mo_graph->addEdge(prevreadfrom, rf);
1607                                                 added = true;
1608                                         }
1609                                 }
1610                                 break;
1611                         }
1612                 }
1613         }
1614
1615         return added;
1616 }
1617
1618 /** This method fixes up the modification order when we resolve a
1619  *  promises.  The basic problem is that actions that occur after the
1620  *  read curr could not property add items to the modification order
1621  *  for our read.
1622  *
1623  *  So for each thread, we find the earliest item that happens after
1624  *  the read curr.  This is the item we have to fix up with additional
1625  *  constraints.  If that action is write, we add a MO edge between
1626  *  the Action rf and that action.  If the action is a read, we add a
1627  *  MO edge between the Action rf, and whatever the read accessed.
1628  *
1629  * @param curr is the read ModelAction that we are fixing up MO edges for.
1630  * @param rf is the write ModelAction that curr reads from.
1631  *
1632  */
1633 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1634 {
1635         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1636         unsigned int i;
1637         ASSERT(curr->is_read());
1638
1639         /* Iterate over all threads */
1640         for (i = 0; i < thrd_lists->size(); i++) {
1641                 /* Iterate over actions in thread, starting from most recent */
1642                 action_list_t *list = &(*thrd_lists)[i];
1643                 action_list_t::reverse_iterator rit;
1644                 ModelAction *lastact = NULL;
1645
1646                 /* Find last action that happens after curr that is either not curr or a rmw */
1647                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1648                         ModelAction *act = *rit;
1649                         if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1650                                 lastact = act;
1651                         } else
1652                                 break;
1653                 }
1654
1655                         /* Include at most one act per-thread that "happens before" curr */
1656                 if (lastact != NULL) {
1657                         if (lastact == curr) {
1658                                 //Case 1: The resolved read is a RMW, and we need to make sure
1659                                 //that the write portion of the RMW mod order after rf
1660
1661                                 mo_graph->addEdge(rf, lastact);
1662                         } else if (lastact->is_read()) {
1663                                 //Case 2: The resolved read is a normal read and the next
1664                                 //operation is a read, and we need to make sure the value read
1665                                 //is mod ordered after rf
1666
1667                                 const ModelAction *postreadfrom = lastact->get_reads_from();
1668                                 if (postreadfrom != NULL && rf != postreadfrom)
1669                                         mo_graph->addEdge(rf, postreadfrom);
1670                         } else {
1671                                 //Case 3: The resolved read is a normal read and the next
1672                                 //operation is a write, and we need to make sure that the
1673                                 //write is mod ordered after rf
1674                                 if (lastact != rf)
1675                                         mo_graph->addEdge(rf, lastact);
1676                         }
1677                         break;
1678                 }
1679         }
1680 }
1681
1682 /**
1683  * Updates the mo_graph with the constraints imposed from the current write.
1684  *
1685  * Basic idea is the following: Go through each other thread and find
1686  * the lastest action that happened before our write.  Two cases:
1687  *
1688  * (1) The action is a write => that write must occur before
1689  * the current write
1690  *
1691  * (2) The action is a read => the write that that action read from
1692  * must occur before the current write.
1693  *
1694  * This method also handles two other issues:
1695  *
1696  * (I) Sequential Consistency: Making sure that if the current write is
1697  * seq_cst, that it occurs after the previous seq_cst write.
1698  *
1699  * (II) Sending the write back to non-synchronizing reads.
1700  *
1701  * @param curr The current action. Must be a write.
1702  * @return True if modification order edges were added; false otherwise
1703  */
1704 bool ModelChecker::w_modification_order(ModelAction *curr)
1705 {
1706         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1707         unsigned int i;
1708         bool added = false;
1709         ASSERT(curr->is_write());
1710
1711         if (curr->is_seqcst()) {
1712                 /* We have to at least see the last sequentially consistent write,
1713                          so we are initialized. */
1714                 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
1715                 if (last_seq_cst != NULL) {
1716                         mo_graph->addEdge(last_seq_cst, curr);
1717                         added = true;
1718                 }
1719         }
1720
1721         /* Last SC fence in the current thread */
1722         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1723
1724         /* Iterate over all threads */
1725         for (i = 0; i < thrd_lists->size(); i++) {
1726                 /* Last SC fence in thread i, before last SC fence in current thread */
1727                 ModelAction *last_sc_fence_thread_before = NULL;
1728                 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
1729                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1730
1731                 /* Iterate over actions in thread, starting from most recent */
1732                 action_list_t *list = &(*thrd_lists)[i];
1733                 action_list_t::reverse_iterator rit;
1734                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1735                         ModelAction *act = *rit;
1736                         if (act == curr) {
1737                                 /*
1738                                  * 1) If RMW and it actually read from something, then we
1739                                  * already have all relevant edges, so just skip to next
1740                                  * thread.
1741                                  *
1742                                  * 2) If RMW and it didn't read from anything, we should
1743                                  * whatever edge we can get to speed up convergence.
1744                                  *
1745                                  * 3) If normal write, we need to look at earlier actions, so
1746                                  * continue processing list.
1747                                  */
1748                                 if (curr->is_rmw()) {
1749                                         if (curr->get_reads_from() != NULL)
1750                                                 break;
1751                                         else
1752                                                 continue;
1753                                 } else
1754                                         continue;
1755                         }
1756
1757                         /* C++, Section 29.3 statement 7 */
1758                         if (last_sc_fence_thread_before && act->is_write() &&
1759                                         *act < *last_sc_fence_thread_before) {
1760                                 mo_graph->addEdge(act, curr);
1761                                 added = true;
1762                                 break;
1763                         }
1764
1765                         /*
1766                          * Include at most one act per-thread that "happens
1767                          * before" curr
1768                          */
1769                         if (act->happens_before(curr)) {
1770                                 /*
1771                                  * Note: if act is RMW, just add edge:
1772                                  *   act --mo--> curr
1773                                  * The following edge should be handled elsewhere:
1774                                  *   readfrom(act) --mo--> act
1775                                  */
1776                                 if (act->is_write())
1777                                         mo_graph->addEdge(act, curr);
1778                                 else if (act->is_read()) {
1779                                         //if previous read accessed a null, just keep going
1780                                         if (act->get_reads_from() == NULL)
1781                                                 continue;
1782                                         mo_graph->addEdge(act->get_reads_from(), curr);
1783                                 }
1784                                 added = true;
1785                                 break;
1786                         } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1787                                                      !act->same_thread(curr)) {
1788                                 /* We have an action that:
1789                                    (1) did not happen before us
1790                                    (2) is a read and we are a write
1791                                    (3) cannot synchronize with us
1792                                    (4) is in a different thread
1793                                    =>
1794                                    that read could potentially read from our write.  Note that
1795                                    these checks are overly conservative at this point, we'll
1796                                    do more checks before actually removing the
1797                                    pendingfuturevalue.
1798
1799                                  */
1800                                 if (thin_air_constraint_may_allow(curr, act)) {
1801                                         if (!is_infeasible() ||
1802                                                         (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
1803                                                 futurevalues->push_back(PendingFutureValue(curr, act));
1804                                         }
1805                                 }
1806                         }
1807                 }
1808         }
1809
1810         return added;
1811 }
1812
1813 /** Arbitrary reads from the future are not allowed.  Section 29.3
1814  * part 9 places some constraints.  This method checks one result of constraint
1815  * constraint.  Others require compiler support. */
1816 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
1817 {
1818         if (!writer->is_rmw())
1819                 return true;
1820
1821         if (!reader->is_rmw())
1822                 return true;
1823
1824         for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1825                 if (search == reader)
1826                         return false;
1827                 if (search->get_tid() == reader->get_tid() &&
1828                                 search->happens_before(reader))
1829                         break;
1830         }
1831
1832         return true;
1833 }
1834
1835 /**
1836  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1837  * some constraints. This method checks one the following constraint (others
1838  * require compiler support):
1839  *
1840  *   If X --hb-> Y --mo-> Z, then X should not read from Z.
1841  */
1842 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1843 {
1844         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1845         unsigned int i;
1846         /* Iterate over all threads */
1847         for (i = 0; i < thrd_lists->size(); i++) {
1848                 const ModelAction *write_after_read = NULL;
1849
1850                 /* Iterate over actions in thread, starting from most recent */
1851                 action_list_t *list = &(*thrd_lists)[i];
1852                 action_list_t::reverse_iterator rit;
1853                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1854                         ModelAction *act = *rit;
1855
1856                         /* Don't disallow due to act == reader */
1857                         if (!reader->happens_before(act) || reader == act)
1858                                 break;
1859                         else if (act->is_write())
1860                                 write_after_read = act;
1861                         else if (act->is_read() && act->get_reads_from() != NULL)
1862                                 write_after_read = act->get_reads_from();
1863                 }
1864
1865                 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1866                         return false;
1867         }
1868         return true;
1869 }
1870
1871 /**
1872  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1873  * The ModelAction under consideration is expected to be taking part in
1874  * release/acquire synchronization as an object of the "reads from" relation.
1875  * Note that this can only provide release sequence support for RMW chains
1876  * which do not read from the future, as those actions cannot be traced until
1877  * their "promise" is fulfilled. Similarly, we may not even establish the
1878  * presence of a release sequence with certainty, as some modification order
1879  * constraints may be decided further in the future. Thus, this function
1880  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1881  * and a boolean representing certainty.
1882  *
1883  * @param rf The action that might be part of a release sequence. Must be a
1884  * write.
1885  * @param release_heads A pass-by-reference style return parameter. After
1886  * execution of this function, release_heads will contain the heads of all the
1887  * relevant release sequences, if any exists with certainty
1888  * @param pending A pass-by-reference style return parameter which is only used
1889  * when returning false (i.e., uncertain). Returns most information regarding
1890  * an uncertain release sequence, including any write operations that might
1891  * break the sequence.
1892  * @return true, if the ModelChecker is certain that release_heads is complete;
1893  * false otherwise
1894  */
1895 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1896                 rel_heads_list_t *release_heads,
1897                 struct release_seq *pending) const
1898 {
1899         /* Only check for release sequences if there are no cycles */
1900         if (mo_graph->checkForCycles())
1901                 return false;
1902
1903         while (rf) {
1904                 ASSERT(rf->is_write());
1905
1906                 if (rf->is_release())
1907                         release_heads->push_back(rf);
1908                 else if (rf->get_last_fence_release())
1909                         release_heads->push_back(rf->get_last_fence_release());
1910                 if (!rf->is_rmw())
1911                         break; /* End of RMW chain */
1912
1913                 /** @todo Need to be smarter here...  In the linux lock
1914                  * example, this will run to the beginning of the program for
1915                  * every acquire. */
1916                 /** @todo The way to be smarter here is to keep going until 1
1917                  * thread has a release preceded by an acquire and you've seen
1918                  *       both. */
1919
1920                 /* acq_rel RMW is a sufficient stopping condition */
1921                 if (rf->is_acquire() && rf->is_release())
1922                         return true; /* complete */
1923
1924                 rf = rf->get_reads_from();
1925         };
1926         if (!rf) {
1927                 /* read from future: need to settle this later */
1928                 pending->rf = NULL;
1929                 return false; /* incomplete */
1930         }
1931
1932         if (rf->is_release())
1933                 return true; /* complete */
1934
1935         /* else relaxed write
1936          * - check for fence-release in the same thread (29.8, stmt. 3)
1937          * - check modification order for contiguous subsequence
1938          *   -> rf must be same thread as release */
1939
1940         const ModelAction *fence_release = rf->get_last_fence_release();
1941         /* Synchronize with a fence-release unconditionally; we don't need to
1942          * find any more "contiguous subsequence..." for it */
1943         if (fence_release)
1944                 release_heads->push_back(fence_release);
1945
1946         int tid = id_to_int(rf->get_tid());
1947         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
1948         action_list_t *list = &(*thrd_lists)[tid];
1949         action_list_t::const_reverse_iterator rit;
1950
1951         /* Find rf in the thread list */
1952         rit = std::find(list->rbegin(), list->rend(), rf);
1953         ASSERT(rit != list->rend());
1954
1955         /* Find the last {write,fence}-release */
1956         for (; rit != list->rend(); rit++) {
1957                 if (fence_release && *(*rit) < *fence_release)
1958                         break;
1959                 if ((*rit)->is_release())
1960                         break;
1961         }
1962         if (rit == list->rend()) {
1963                 /* No write-release in this thread */
1964                 return true; /* complete */
1965         } else if (fence_release && *(*rit) < *fence_release) {
1966                 /* The fence-release is more recent (and so, "stronger") than
1967                  * the most recent write-release */
1968                 return true; /* complete */
1969         } /* else, need to establish contiguous release sequence */
1970         ModelAction *release = *rit;
1971
1972         ASSERT(rf->same_thread(release));
1973
1974         pending->writes.clear();
1975
1976         bool certain = true;
1977         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1978                 if (id_to_int(rf->get_tid()) == (int)i)
1979                         continue;
1980                 list = &(*thrd_lists)[i];
1981
1982                 /* Can we ensure no future writes from this thread may break
1983                  * the release seq? */
1984                 bool future_ordered = false;
1985
1986                 ModelAction *last = get_last_action(int_to_id(i));
1987                 Thread *th = get_thread(int_to_id(i));
1988                 if ((last && rf->happens_before(last)) ||
1989                                 !is_enabled(th) ||
1990                                 th->is_complete())
1991                         future_ordered = true;
1992
1993                 ASSERT(!th->is_model_thread() || future_ordered);
1994
1995                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1996                         const ModelAction *act = *rit;
1997                         /* Reach synchronization -> this thread is complete */
1998                         if (act->happens_before(release))
1999                                 break;
2000                         if (rf->happens_before(act)) {
2001                                 future_ordered = true;
2002                                 continue;
2003                         }
2004
2005                         /* Only non-RMW writes can break release sequences */
2006                         if (!act->is_write() || act->is_rmw())
2007                                 continue;
2008
2009                         /* Check modification order */
2010                         if (mo_graph->checkReachable(rf, act)) {
2011                                 /* rf --mo--> act */
2012                                 future_ordered = true;
2013                                 continue;
2014                         }
2015                         if (mo_graph->checkReachable(act, release))
2016                                 /* act --mo--> release */
2017                                 break;
2018                         if (mo_graph->checkReachable(release, act) &&
2019                                       mo_graph->checkReachable(act, rf)) {
2020                                 /* release --mo-> act --mo--> rf */
2021                                 return true; /* complete */
2022                         }
2023                         /* act may break release sequence */
2024                         pending->writes.push_back(act);
2025                         certain = false;
2026                 }
2027                 if (!future_ordered)
2028                         certain = false; /* This thread is uncertain */
2029         }
2030
2031         if (certain) {
2032                 release_heads->push_back(release);
2033                 pending->writes.clear();
2034         } else {
2035                 pending->release = release;
2036                 pending->rf = rf;
2037         }
2038         return certain;
2039 }
2040
2041 /**
2042  * An interface for getting the release sequence head(s) with which a
2043  * given ModelAction must synchronize. This function only returns a non-empty
2044  * result when it can locate a release sequence head with certainty. Otherwise,
2045  * it may mark the internal state of the ModelChecker so that it will handle
2046  * the release sequence at a later time, causing @a acquire to update its
2047  * synchronization at some later point in execution.
2048  *
2049  * @param acquire The 'acquire' action that may synchronize with a release
2050  * sequence
2051  * @param read The read action that may read from a release sequence; this may
2052  * be the same as acquire, or else an earlier action in the same thread (i.e.,
2053  * when 'acquire' is a fence-acquire)
2054  * @param release_heads A pass-by-reference return parameter. Will be filled
2055  * with the head(s) of the release sequence(s), if they exists with certainty.
2056  * @see ModelChecker::release_seq_heads
2057  */
2058 void ModelChecker::get_release_seq_heads(ModelAction *acquire,
2059                 ModelAction *read, rel_heads_list_t *release_heads)
2060 {
2061         const ModelAction *rf = read->get_reads_from();
2062         struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
2063         sequence->acquire = acquire;
2064         sequence->read = read;
2065
2066         if (!release_seq_heads(rf, release_heads, sequence)) {
2067                 /* add act to 'lazy checking' list */
2068                 pending_rel_seqs->push_back(sequence);
2069         } else {
2070                 snapshot_free(sequence);
2071         }
2072 }
2073
2074 /**
2075  * Attempt to resolve all stashed operations that might synchronize with a
2076  * release sequence for a given location. This implements the "lazy" portion of
2077  * determining whether or not a release sequence was contiguous, since not all
2078  * modification order information is present at the time an action occurs.
2079  *
2080  * @param location The location/object that should be checked for release
2081  * sequence resolutions. A NULL value means to check all locations.
2082  * @param work_queue The work queue to which to add work items as they are
2083  * generated
2084  * @return True if any updates occurred (new synchronization, new mo_graph
2085  * edges)
2086  */
2087 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
2088 {
2089         bool updated = false;
2090         std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
2091         while (it != pending_rel_seqs->end()) {
2092                 struct release_seq *pending = *it;
2093                 ModelAction *acquire = pending->acquire;
2094                 const ModelAction *read = pending->read;
2095
2096                 /* Only resolve sequences on the given location, if provided */
2097                 if (location && read->get_location() != location) {
2098                         it++;
2099                         continue;
2100                 }
2101
2102                 const ModelAction *rf = read->get_reads_from();
2103                 rel_heads_list_t release_heads;
2104                 bool complete;
2105                 complete = release_seq_heads(rf, &release_heads, pending);
2106                 for (unsigned int i = 0; i < release_heads.size(); i++) {
2107                         if (!acquire->has_synchronized_with(release_heads[i])) {
2108                                 if (acquire->synchronize_with(release_heads[i]))
2109                                         updated = true;
2110                                 else
2111                                         set_bad_synchronization();
2112                         }
2113                 }
2114
2115                 if (updated) {
2116                         /* Re-check all pending release sequences */
2117                         work_queue->push_back(CheckRelSeqWorkEntry(NULL));
2118                         /* Re-check read-acquire for mo_graph edges */
2119                         if (acquire->is_read())
2120                                 work_queue->push_back(MOEdgeWorkEntry(acquire));
2121
2122                         /* propagate synchronization to later actions */
2123                         action_list_t::reverse_iterator rit = action_trace->rbegin();
2124                         for (; (*rit) != acquire; rit++) {
2125                                 ModelAction *propagate = *rit;
2126                                 if (acquire->happens_before(propagate)) {
2127                                         propagate->synchronize_with(acquire);
2128                                         /* Re-check 'propagate' for mo_graph edges */
2129                                         work_queue->push_back(MOEdgeWorkEntry(propagate));
2130                                 }
2131                         }
2132                 }
2133                 if (complete) {
2134                         it = pending_rel_seqs->erase(it);
2135                         snapshot_free(pending);
2136                 } else {
2137                         it++;
2138                 }
2139         }
2140
2141         // If we resolved promises or data races, see if we have realized a data race.
2142         checkDataRaces();
2143
2144         return updated;
2145 }
2146
2147 /**
2148  * Performs various bookkeeping operations for the current ModelAction. For
2149  * instance, adds action to the per-object, per-thread action vector and to the
2150  * action trace list of all thread actions.
2151  *
2152  * @param act is the ModelAction to add.
2153  */
2154 void ModelChecker::add_action_to_lists(ModelAction *act)
2155 {
2156         int tid = id_to_int(act->get_tid());
2157         ModelAction *uninit = NULL;
2158         int uninit_id = -1;
2159         action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
2160         if (list->empty() && act->is_atomic_var()) {
2161                 uninit = new_uninitialized_action(act->get_location());
2162                 uninit_id = id_to_int(uninit->get_tid());
2163                 list->push_back(uninit);
2164         }
2165         list->push_back(act);
2166
2167         action_trace->push_back(act);
2168         if (uninit)
2169                 action_trace->push_front(uninit);
2170
2171         std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
2172         if (tid >= (int)vec->size())
2173                 vec->resize(priv->next_thread_id);
2174         (*vec)[tid].push_back(act);
2175         if (uninit)
2176                 (*vec)[uninit_id].push_front(uninit);
2177
2178         if ((int)thrd_last_action->size() <= tid)
2179                 thrd_last_action->resize(get_num_threads());
2180         (*thrd_last_action)[tid] = act;
2181         if (uninit)
2182                 (*thrd_last_action)[uninit_id] = uninit;
2183
2184         if (act->is_fence() && act->is_release()) {
2185                 if ((int)thrd_last_fence_release->size() <= tid)
2186                         thrd_last_fence_release->resize(get_num_threads());
2187                 (*thrd_last_fence_release)[tid] = act;
2188         }
2189
2190         if (act->is_wait()) {
2191                 void *mutex_loc = (void *) act->get_value();
2192                 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
2193
2194                 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
2195                 if (tid >= (int)vec->size())
2196                         vec->resize(priv->next_thread_id);
2197                 (*vec)[tid].push_back(act);
2198         }
2199 }
2200
2201 /**
2202  * @brief Get the last action performed by a particular Thread
2203  * @param tid The thread ID of the Thread in question
2204  * @return The last action in the thread
2205  */
2206 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
2207 {
2208         int threadid = id_to_int(tid);
2209         if (threadid < (int)thrd_last_action->size())
2210                 return (*thrd_last_action)[id_to_int(tid)];
2211         else
2212                 return NULL;
2213 }
2214
2215 /**
2216  * @brief Get the last fence release performed by a particular Thread
2217  * @param tid The thread ID of the Thread in question
2218  * @return The last fence release in the thread, if one exists; NULL otherwise
2219  */
2220 ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
2221 {
2222         int threadid = id_to_int(tid);
2223         if (threadid < (int)thrd_last_fence_release->size())
2224                 return (*thrd_last_fence_release)[id_to_int(tid)];
2225         else
2226                 return NULL;
2227 }
2228
2229 /**
2230  * Gets the last memory_order_seq_cst write (in the total global sequence)
2231  * performed on a particular object (i.e., memory location), not including the
2232  * current action.
2233  * @param curr The current ModelAction; also denotes the object location to
2234  * check
2235  * @return The last seq_cst write
2236  */
2237 ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
2238 {
2239         void *location = curr->get_location();
2240         action_list_t *list = get_safe_ptr_action(obj_map, location);
2241         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
2242         action_list_t::reverse_iterator rit;
2243         for (rit = list->rbegin(); rit != list->rend(); rit++)
2244                 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
2245                         return *rit;
2246         return NULL;
2247 }
2248
2249 /**
2250  * Gets the last memory_order_seq_cst fence (in the total global sequence)
2251  * performed in a particular thread, prior to a particular fence.
2252  * @param tid The ID of the thread to check
2253  * @param before_fence The fence from which to begin the search; if NULL, then
2254  * search for the most recent fence in the thread.
2255  * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
2256  */
2257 ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
2258 {
2259         /* All fences should have NULL location */
2260         action_list_t *list = get_safe_ptr_action(obj_map, NULL);
2261         action_list_t::reverse_iterator rit = list->rbegin();
2262
2263         if (before_fence) {
2264                 for (; rit != list->rend(); rit++)
2265                         if (*rit == before_fence)
2266                                 break;
2267
2268                 ASSERT(*rit == before_fence);
2269                 rit++;
2270         }
2271
2272         for (; rit != list->rend(); rit++)
2273                 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
2274                         return *rit;
2275         return NULL;
2276 }
2277
2278 /**
2279  * Gets the last unlock operation performed on a particular mutex (i.e., memory
2280  * location). This function identifies the mutex according to the current
2281  * action, which is presumed to perform on the same mutex.
2282  * @param curr The current ModelAction; also denotes the object location to
2283  * check
2284  * @return The last unlock operation
2285  */
2286 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
2287 {
2288         void *location = curr->get_location();
2289         action_list_t *list = get_safe_ptr_action(obj_map, location);
2290         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
2291         action_list_t::reverse_iterator rit;
2292         for (rit = list->rbegin(); rit != list->rend(); rit++)
2293                 if ((*rit)->is_unlock() || (*rit)->is_wait())
2294                         return *rit;
2295         return NULL;
2296 }
2297
2298 ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
2299 {
2300         ModelAction *parent = get_last_action(tid);
2301         if (!parent)
2302                 parent = get_thread(tid)->get_creation();
2303         return parent;
2304 }
2305
2306 /**
2307  * Returns the clock vector for a given thread.
2308  * @param tid The thread whose clock vector we want
2309  * @return Desired clock vector
2310  */
2311 ClockVector * ModelChecker::get_cv(thread_id_t tid) const
2312 {
2313         return get_parent_action(tid)->get_cv();
2314 }
2315
2316 /**
2317  * Resolve a set of Promises with a current write. The set is provided in the
2318  * Node corresponding to @a write.
2319  * @param write The ModelAction that is fulfilling Promises
2320  * @return True if promises were resolved; false otherwise
2321  */
2322 bool ModelChecker::resolve_promises(ModelAction *write)
2323 {
2324         bool resolved = false;
2325         std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
2326
2327         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
2328                 Promise *promise = (*promises)[promise_index];
2329                 if (write->get_node()->get_promise(i)) {
2330                         ModelAction *read = promise->get_action();
2331                         if (read->is_rmw()) {
2332                                 mo_graph->addRMWEdge(write, read);
2333                         }
2334                         read_from(read, write);
2335                         //First fix up the modification order for actions that happened
2336                         //before the read
2337                         r_modification_order(read, write);
2338                         //Next fix up the modification order for actions that happened
2339                         //after the read.
2340                         post_r_modification_order(read, write);
2341                         //Make sure the promise's value matches the write's value
2342                         ASSERT(promise->get_value() == write->get_value());
2343                         delete(promise);
2344
2345                         promises->erase(promises->begin() + promise_index);
2346                         actions_to_check.push_back(read);
2347
2348                         resolved = true;
2349                 } else
2350                         promise_index++;
2351         }
2352
2353         //Check whether reading these writes has made threads unable to
2354         //resolve promises
2355
2356         for (unsigned int i = 0; i < actions_to_check.size(); i++) {
2357                 ModelAction *read=actions_to_check[i];
2358                 mo_check_promises(read->get_tid(), write, read);
2359         }
2360
2361         return resolved;
2362 }
2363
2364 /**
2365  * Compute the set of promises that could potentially be satisfied by this
2366  * action. Note that the set computation actually appears in the Node, not in
2367  * ModelChecker.
2368  * @param curr The ModelAction that may satisfy promises
2369  */
2370 void ModelChecker::compute_promises(ModelAction *curr)
2371 {
2372         for (unsigned int i = 0; i < promises->size(); i++) {
2373                 Promise *promise = (*promises)[i];
2374                 const ModelAction *act = promise->get_action();
2375                 if (!act->happens_before(curr) &&
2376                                 act->is_read() &&
2377                                 !act->could_synchronize_with(curr) &&
2378                                 !act->same_thread(curr) &&
2379                                 act->get_location() == curr->get_location() &&
2380                                 promise->get_value() == curr->get_value()) {
2381                         curr->get_node()->set_promise(i, act->is_rmw());
2382                 }
2383         }
2384 }
2385
2386 /** Checks promises in response to change in ClockVector Threads. */
2387 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2388 {
2389         for (unsigned int i = 0; i < promises->size(); i++) {
2390                 Promise *promise = (*promises)[i];
2391                 const ModelAction *act = promise->get_action();
2392                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2393                                 merge_cv->synchronized_since(act)) {
2394                         if (promise->eliminate_thread(tid)) {
2395                                 //Promise has failed
2396                                 priv->failed_promise = true;
2397                                 return;
2398                         }
2399                 }
2400         }
2401 }
2402
2403 void ModelChecker::check_promises_thread_disabled()
2404 {
2405         for (unsigned int i = 0; i < promises->size(); i++) {
2406                 Promise *promise = (*promises)[i];
2407                 if (promise->has_failed()) {
2408                         priv->failed_promise = true;
2409                         return;
2410                 }
2411         }
2412 }
2413
2414 /**
2415  * @brief Checks promises in response to addition to modification order for
2416  * threads.
2417  *
2418  * Definitions:
2419  *
2420  * pthread is the thread that performed the read that created the promise
2421  *
2422  * pread is the read that created the promise
2423  *
2424  * pwrite is either the first write to same location as pread by
2425  * pthread that is sequenced after pread or the write read by the
2426  * first read to the same location as pread by pthread that is
2427  * sequenced after pread.
2428  *
2429  * 1. If tid=pthread, then we check what other threads are reachable
2430  * through the mod order starting with pwrite.  Those threads cannot
2431  * perform a write that will resolve the promise due to modification
2432  * order constraints.
2433  *
2434  * 2. If the tid is not pthread, we check whether pwrite can reach the
2435  * action write through the modification order.  If so, that thread
2436  * cannot perform a future write that will resolve the promise due to
2437  * modificatin order constraints.
2438  *
2439  * @param tid The thread that either read from the model action write, or
2440  * actually did the model action write.
2441  *
2442  * @param write The ModelAction representing the relevant write.
2443  * @param read  The ModelAction that reads a promised write, or NULL otherwise.
2444  */
2445 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
2446 {
2447         void *location = write->get_location();
2448         for (unsigned int i = 0; i < promises->size(); i++) {
2449                 Promise *promise = (*promises)[i];
2450                 const ModelAction *act = promise->get_action();
2451
2452                 // Is this promise on the same location?
2453                 if (act->get_location() != location)
2454                         continue;
2455
2456                 // same thread as the promise
2457                 if (act->get_tid() == tid) {
2458                         // make sure that the reader of this write happens after the promise
2459                         if ((read == NULL) || (promise->get_action()->happens_before(read))) {
2460                                 // do we have a pwrite for the promise, if not, set it
2461                                 if (promise->get_write() == NULL) {
2462                                         promise->set_write(write);
2463                                         // The pwrite cannot happen before the promise
2464                                         if (write->happens_before(act) && (write != act)) {
2465                                                 priv->failed_promise = true;
2466                                                 return;
2467                                         }
2468                                 }
2469
2470                                 if (mo_graph->checkPromise(write, promise)) {
2471                                         priv->failed_promise = true;
2472                                         return;
2473                                 }
2474                         }
2475                 }
2476
2477                 // Don't do any lookups twice for the same thread
2478                 if (!promise->thread_is_available(tid))
2479                         continue;
2480
2481                 if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
2482                         if (promise->eliminate_thread(tid)) {
2483                                 priv->failed_promise = true;
2484                                 return;
2485                         }
2486                 }
2487         }
2488 }
2489
2490 /**
2491  * Compute the set of writes that may break the current pending release
2492  * sequence. This information is extracted from previou release sequence
2493  * calculations.
2494  *
2495  * @param curr The current ModelAction. Must be a release sequence fixup
2496  * action.
2497  */
2498 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2499 {
2500         if (pending_rel_seqs->empty())
2501                 return;
2502
2503         struct release_seq *pending = pending_rel_seqs->back();
2504         for (unsigned int i = 0; i < pending->writes.size(); i++) {
2505                 const ModelAction *write = pending->writes[i];
2506                 curr->get_node()->add_relseq_break(write);
2507         }
2508
2509         /* NULL means don't break the sequence; just synchronize */
2510         curr->get_node()->add_relseq_break(NULL);
2511 }
2512
2513 /**
2514  * Build up an initial set of all past writes that this 'read' action may read
2515  * from. This set is determined by the clock vector's "happens before"
2516  * relationship.
2517  * @param curr is the current ModelAction that we are exploring; it must be a
2518  * 'read' operation.
2519  */
2520 void ModelChecker::build_reads_from_past(ModelAction *curr)
2521 {
2522         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2523         unsigned int i;
2524         ASSERT(curr->is_read());
2525
2526         ModelAction *last_sc_write = NULL;
2527
2528         if (curr->is_seqcst())
2529                 last_sc_write = get_last_seq_cst_write(curr);
2530
2531         /* Iterate over all threads */
2532         for (i = 0; i < thrd_lists->size(); i++) {
2533                 /* Iterate over actions in thread, starting from most recent */
2534                 action_list_t *list = &(*thrd_lists)[i];
2535                 action_list_t::reverse_iterator rit;
2536                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2537                         ModelAction *act = *rit;
2538
2539                         /* Only consider 'write' actions */
2540                         if (!act->is_write() || act == curr)
2541                                 continue;
2542
2543                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2544                         bool allow_read = true;
2545
2546                         if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
2547                                 allow_read = false;
2548                         else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
2549                                 allow_read = false;
2550
2551                         if (allow_read)
2552                                 curr->get_node()->add_read_from(act);
2553
2554                         /* Include at most one act per-thread that "happens before" curr */
2555                         if (act->happens_before(curr))
2556                                 break;
2557                 }
2558         }
2559
2560         if (DBG_ENABLED()) {
2561                 model_print("Reached read action:\n");
2562                 curr->print();
2563                 model_print("Printing may_read_from\n");
2564                 curr->get_node()->print_may_read_from();
2565                 model_print("End printing may_read_from\n");
2566         }
2567 }
2568
2569 bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
2570 {
2571         while (true) {
2572                 /* UNINIT actions don't have a Node, and they never sleep */
2573                 if (write->is_uninitialized())
2574                         return true;
2575                 Node *prevnode = write->get_node()->get_parent();
2576
2577                 bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
2578                 if (write->is_release() && thread_sleep)
2579                         return true;
2580                 if (!write->is_rmw()) {
2581                         return false;
2582                 }
2583                 if (write->get_reads_from() == NULL)
2584                         return true;
2585                 write = write->get_reads_from();
2586         }
2587 }
2588
2589 /**
2590  * @brief Create a new action representing an uninitialized atomic
2591  * @param location The memory location of the atomic object
2592  * @return A pointer to a new ModelAction
2593  */
2594 ModelAction * ModelChecker::new_uninitialized_action(void *location) const
2595 {
2596         ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
2597         act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
2598         act->create_cv(NULL);
2599         return act;
2600 }
2601
2602 static void print_list(action_list_t *list)
2603 {
2604         action_list_t::iterator it;
2605
2606         model_print("---------------------------------------------------------------------\n");
2607
2608         unsigned int hash = 0;
2609
2610         for (it = list->begin(); it != list->end(); it++) {
2611                 (*it)->print();
2612                 hash = hash^(hash<<3)^((*it)->hash());
2613         }
2614         model_print("HASH %u\n", hash);
2615         model_print("---------------------------------------------------------------------\n");
2616 }
2617
2618 #if SUPPORT_MOD_ORDER_DUMP
2619 void ModelChecker::dumpGraph(char *filename) const
2620 {
2621         char buffer[200];
2622         sprintf(buffer, "%s.dot", filename);
2623         FILE *file = fopen(buffer, "w");
2624         fprintf(file, "digraph %s {\n", filename);
2625         mo_graph->dumpNodes(file);
2626         ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
2627
2628         for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2629                 ModelAction *action = *it;
2630                 if (action->is_read()) {
2631                         fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
2632                         if (action->get_reads_from() != NULL)
2633                                 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2634                 }
2635                 if (thread_array[action->get_tid()] != NULL) {
2636                         fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2637                 }
2638
2639                 thread_array[action->get_tid()] = action;
2640         }
2641         fprintf(file, "}\n");
2642         model_free(thread_array);
2643         fclose(file);
2644 }
2645 #endif
2646
2647 /** @brief Prints an execution trace summary. */
2648 void ModelChecker::print_summary() const
2649 {
2650 #if SUPPORT_MOD_ORDER_DUMP
2651         scheduler->print();
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 }