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