fix some of the bugs related to barrier example...
[model-checker.git] / model.cc
1 #include <stdio.h>
2 #include <algorithm>
3
4 #include "model.h"
5 #include "action.h"
6 #include "nodestack.h"
7 #include "schedule.h"
8 #include "snapshot-interface.h"
9 #include "common.h"
10 #include "clockvector.h"
11 #include "cyclegraph.h"
12 #include "promise.h"
13 #include "datarace.h"
14 #include "mutex.h"
15 #include "threads-model.h"
16
17 #define INITIAL_THREAD_ID       0
18
19 ModelChecker *model;
20
21 /** @brief Constructor */
22 ModelChecker::ModelChecker(struct model_params params) :
23         /* Initialize default scheduler */
24         params(params),
25         scheduler(new Scheduler()),
26         num_executions(0),
27         num_feasible_executions(0),
28         diverge(NULL),
29         earliest_diverge(NULL),
30         action_trace(new action_list_t()),
31         thread_map(new HashTable<int, Thread *, int>()),
32         obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
33         lock_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
34         obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
35         promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
36         futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
37         pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
38         thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
39         node_stack(new NodeStack()),
40         mo_graph(new CycleGraph()),
41         failed_promise(false),
42         too_many_reads(false),
43         asserted(false),
44         bad_synchronization(false)
45 {
46         /* Allocate this "size" on the snapshotting heap */
47         priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
48         /* First thread created will have id INITIAL_THREAD_ID */
49         priv->next_thread_id = INITIAL_THREAD_ID;
50
51         /* Initialize a model-checker thread, for special ModelActions */
52         model_thread = new Thread(get_next_id());
53         thread_map->put(id_to_int(model_thread->get_id()), model_thread);
54 }
55
56 /** @brief Destructor */
57 ModelChecker::~ModelChecker()
58 {
59         for (unsigned int i = 0; i < get_num_threads(); i++)
60                 delete thread_map->get(i);
61         delete thread_map;
62
63         delete obj_thrd_map;
64         delete obj_map;
65         delete lock_waiters_map;
66         delete action_trace;
67
68         for (unsigned int i = 0; i < promises->size(); i++)
69                 delete (*promises)[i];
70         delete promises;
71
72         delete pending_rel_seqs;
73
74         delete thrd_last_action;
75         delete node_stack;
76         delete scheduler;
77         delete mo_graph;
78 }
79
80 /**
81  * Restores user program to initial state and resets all model-checker data
82  * structures.
83  */
84 void ModelChecker::reset_to_initial_state()
85 {
86         DEBUG("+++ Resetting to initial state +++\n");
87         node_stack->reset_execution();
88         failed_promise = false;
89         too_many_reads = false;
90         bad_synchronization = false;
91         reset_asserted();
92         snapshotObject->backTrackBeforeStep(0);
93 }
94
95 /** @return a thread ID for a new Thread */
96 thread_id_t ModelChecker::get_next_id()
97 {
98         return priv->next_thread_id++;
99 }
100
101 /** @return the number of user threads created during this execution */
102 unsigned int ModelChecker::get_num_threads()
103 {
104         return priv->next_thread_id;
105 }
106
107 /** @return The currently executing Thread. */
108 Thread * ModelChecker::get_current_thread()
109 {
110         return scheduler->get_current_thread();
111 }
112
113 /** @return a sequence number for a new ModelAction */
114 modelclock_t ModelChecker::get_next_seq_num()
115 {
116         return ++priv->used_sequence_numbers;
117 }
118
119 /**
120  * @brief Choose the next thread to execute.
121  *
122  * This function chooses the next thread that should execute. It can force the
123  * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
124  * followed by a THREAD_START, or it can enforce execution replay/backtracking.
125  * The model-checker may have no preference regarding the next thread (i.e.,
126  * when exploring a new execution ordering), in which case this will return
127  * NULL.
128  * @param curr The current ModelAction. This action might guide the choice of
129  * next thread.
130  * @return The next thread to run. If the model-checker has no preference, NULL.
131  */
132 Thread * ModelChecker::get_next_thread(ModelAction *curr)
133 {
134         thread_id_t tid;
135
136         if (curr!=NULL) {
137                 /* Do not split atomic actions. */
138                 if (curr->is_rmwr())
139                         return thread_current();
140                 /* The THREAD_CREATE action points to the created Thread */
141                 else if (curr->get_type() == THREAD_CREATE)
142                         return (Thread *)curr->get_location();
143         }
144
145         /* Have we completed exploring the preselected path? */
146         if (diverge == NULL)
147                 return NULL;
148
149         /* Else, we are trying to replay an execution */
150         ModelAction *next = node_stack->get_next()->get_action();
151
152         if (next == diverge) {
153                 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
154                         earliest_diverge=diverge;
155
156                 Node *nextnode = next->get_node();
157                 Node *prevnode = nextnode->get_parent();
158                 scheduler->update_sleep_set(prevnode);
159
160                 /* Reached divergence point */
161                 if (nextnode->increment_promise()) {
162                         /* The next node will try to satisfy a different set of promises. */
163                         tid = next->get_tid();
164                         node_stack->pop_restofstack(2);
165                 } else if (nextnode->increment_read_from()) {
166                         /* The next node will read from a different value. */
167                         tid = next->get_tid();
168                         node_stack->pop_restofstack(2);
169                 } else if (nextnode->increment_future_value()) {
170                         /* The next node will try to read from a different future value. */
171                         tid = next->get_tid();
172                         node_stack->pop_restofstack(2);
173                 } else if (nextnode->increment_relseq_break()) {
174                         /* The next node will try to resolve a release sequence differently */
175                         tid = next->get_tid();
176                         node_stack->pop_restofstack(2);
177                 } else {
178                         /* Make a different thread execute for next step */
179                         scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
180                         tid = prevnode->get_next_backtrack();
181                         /* Make sure the backtracked thread isn't sleeping. */
182                         node_stack->pop_restofstack(1);
183                         if (diverge==earliest_diverge) {
184                                 earliest_diverge=prevnode->get_action();
185                         }
186                 }
187                 /* The correct sleep set is in the parent node. */
188                 execute_sleep_set();
189
190                 DEBUG("*** Divergence point ***\n");
191
192                 diverge = NULL;
193         } else {
194                 tid = next->get_tid();
195         }
196         DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
197         ASSERT(tid != THREAD_ID_T_NONE);
198         return thread_map->get(id_to_int(tid));
199 }
200
201 /** 
202  * We need to know what the next actions of all threads in the sleep
203  * set will be.  This method computes them and stores the actions at
204  * the corresponding thread object's pending action.
205  */
206
207 void ModelChecker::execute_sleep_set() {
208         for(unsigned int i=0;i<get_num_threads();i++) {
209                 thread_id_t tid=int_to_id(i);
210                 Thread *thr=get_thread(tid);
211                 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
212                         thr->set_state(THREAD_RUNNING);
213                         scheduler->next_thread(thr);
214                         Thread::swap(&system_context, thr);
215                         priv->current_action->set_sleep_flag();
216                         thr->set_pending(priv->current_action);
217                 }
218         }
219         priv->current_action = NULL;
220 }
221
222 void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
223         for(unsigned int i=0;i<get_num_threads();i++) {
224                 thread_id_t tid=int_to_id(i);
225                 Thread *thr=get_thread(tid);
226                 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
227                         ModelAction *pending_act=thr->get_pending();
228                         if (pending_act->could_synchronize_with(curr)) {
229                                 //Remove this thread from sleep set
230                                 scheduler->remove_sleep(thr);
231                         }
232                 }
233         }       
234 }
235
236 /**
237  * Queries the model-checker for more executions to explore and, if one
238  * exists, resets the model-checker state to execute a new execution.
239  *
240  * @return If there are more executions to explore, return true. Otherwise,
241  * return false.
242  */
243 bool ModelChecker::next_execution()
244 {
245         DBG();
246
247         num_executions++;
248
249         if (isfinalfeasible()) {
250                 printf("Earliest divergence point since last feasible execution:\n");
251                 if (earliest_diverge)
252                         earliest_diverge->print();
253                 else
254                         printf("(Not set)\n");
255
256                 earliest_diverge = NULL;
257                 num_feasible_executions++;
258         }
259
260         DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
261                         pending_rel_seqs->size());
262
263
264         if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
265                 print_summary();
266
267         if ((diverge = get_next_backtrack()) == NULL)
268                 return false;
269
270         if (DBG_ENABLED()) {
271                 printf("Next execution will diverge at:\n");
272                 diverge->print();
273         }
274
275         reset_to_initial_state();
276         return true;
277 }
278
279 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
280 {
281         switch (act->get_type()) {
282         case ATOMIC_READ:
283         case ATOMIC_WRITE:
284         case ATOMIC_RMW: {
285                 /* linear search: from most recent to oldest */
286                 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
287                 action_list_t::reverse_iterator rit;
288                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
289                         ModelAction *prev = *rit;
290                         if (prev->could_synchronize_with(act))
291                                 return prev;
292                 }
293                 break;
294         }
295         case ATOMIC_LOCK:
296         case ATOMIC_TRYLOCK: {
297                 /* linear search: from most recent to oldest */
298                 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
299                 action_list_t::reverse_iterator rit;
300                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
301                         ModelAction *prev = *rit;
302                         if (act->is_conflicting_lock(prev))
303                                 return prev;
304                 }
305                 break;
306         }
307         case ATOMIC_UNLOCK: {
308                 /* linear search: from most recent to oldest */
309                 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
310                 action_list_t::reverse_iterator rit;
311                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
312                         ModelAction *prev = *rit;
313                         if (!act->same_thread(prev)&&prev->is_failed_trylock())
314                                 return prev;
315                 }
316                 break;
317         }
318         default:
319                 break;
320         }
321         return NULL;
322 }
323
324 /** This method finds backtracking points where we should try to
325  * reorder the parameter ModelAction against.
326  *
327  * @param the ModelAction to find backtracking points for.
328  */
329 void ModelChecker::set_backtracking(ModelAction *act)
330 {
331         Thread *t = get_thread(act);
332         ModelAction * prev = get_last_conflict(act);
333         if (prev == NULL)
334                 return;
335
336         Node * node = prev->get_node()->get_parent();
337
338         int low_tid, high_tid;
339         if (node->is_enabled(t)) {
340                 low_tid = id_to_int(act->get_tid());
341                 high_tid = low_tid+1;
342         } else {
343                 low_tid = 0;
344                 high_tid = get_num_threads();
345         }
346
347         for(int i = low_tid; i < high_tid; i++) {
348                 thread_id_t tid = int_to_id(i);
349
350                 /* Don't backtrack into a point where the thread is disabled or sleeping. */
351                 if (node->get_enabled_array()[i]!=THREAD_ENABLED)
352                         continue;
353         
354                 /* Check if this has been explored already */
355                 if (node->has_been_explored(tid))
356                         continue;
357
358                 /* See if fairness allows */
359                 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
360                         bool unfair=false;
361                         for(int t=0;t<node->get_num_threads();t++) {
362                                 thread_id_t tother=int_to_id(t);
363                                 if (node->is_enabled(tother) && node->has_priority(tother)) {
364                                         unfair=true;
365                                         break;
366                                 }
367                         }
368                         if (unfair)
369                                 continue;
370                 }
371                 /* Cache the latest backtracking point */
372                 if (!priv->next_backtrack || *prev > *priv->next_backtrack)
373                         priv->next_backtrack = prev;
374
375                 /* If this is a new backtracking point, mark the tree */
376                 if (!node->set_backtrack(tid))
377                         continue;
378                 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
379                                         id_to_int(prev->get_tid()),
380                                         id_to_int(t->get_id()));
381                 if (DBG_ENABLED()) {
382                         prev->print();
383                         act->print();
384                 }
385         }
386 }
387
388 /**
389  * Returns last backtracking point. The model checker will explore a different
390  * path for this point in the next execution.
391  * @return The ModelAction at which the next execution should diverge.
392  */
393 ModelAction * ModelChecker::get_next_backtrack()
394 {
395         ModelAction *next = priv->next_backtrack;
396         priv->next_backtrack = NULL;
397         return next;
398 }
399
400 /**
401  * Processes a read or rmw model action.
402  * @param curr is the read model action to process.
403  * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
404  * @return True if processing this read updates the mo_graph.
405  */
406 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
407 {
408         uint64_t value;
409         bool updated = false;
410         while (true) {
411                 const ModelAction *reads_from = curr->get_node()->get_read_from();
412                 if (reads_from != NULL) {
413                         mo_graph->startChanges();
414
415                         value = reads_from->get_value();
416                         bool r_status = false;
417
418                         if (!second_part_of_rmw) {
419                                 check_recency(curr, reads_from);
420                                 r_status = r_modification_order(curr, reads_from);
421                         }
422
423
424                         if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
425                                 mo_graph->rollbackChanges();
426                                 too_many_reads = false;
427                                 continue;
428                         }
429
430                         curr->read_from(reads_from);
431                         mo_graph->commitChanges();
432                         mo_check_promises(curr->get_tid(), reads_from);
433
434                         updated |= r_status;
435                 } else if (!second_part_of_rmw) {
436                         /* Read from future value */
437                         value = curr->get_node()->get_future_value();
438                         modelclock_t expiration = curr->get_node()->get_future_value_expiration();
439                         curr->read_from(NULL);
440                         Promise *valuepromise = new Promise(curr, value, expiration);
441                         promises->push_back(valuepromise);
442                 }
443                 get_thread(curr)->set_return_value(value);
444                 return updated;
445         }
446 }
447
448 /**
449  * Processes a lock, trylock, or unlock model action.  @param curr is
450  * the read model action to process.
451  *
452  * The try lock operation checks whether the lock is taken.  If not,
453  * it falls to the normal lock operation case.  If so, it returns
454  * fail.
455  *
456  * The lock operation has already been checked that it is enabled, so
457  * it just grabs the lock and synchronizes with the previous unlock.
458  *
459  * The unlock operation has to re-enable all of the threads that are
460  * waiting on the lock.
461  *
462  * @return True if synchronization was updated; false otherwise
463  */
464 bool ModelChecker::process_mutex(ModelAction *curr) {
465         std::mutex *mutex = (std::mutex *)curr->get_location();
466         struct std::mutex_state *state = mutex->get_state();
467         switch (curr->get_type()) {
468         case ATOMIC_TRYLOCK: {
469                 bool success = !state->islocked;
470                 curr->set_try_lock(success);
471                 if (!success) {
472                         get_thread(curr)->set_return_value(0);
473                         break;
474                 }
475                 get_thread(curr)->set_return_value(1);
476         }
477                 //otherwise fall into the lock case
478         case ATOMIC_LOCK: {
479                 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
480                         printf("Lock access before initialization\n");
481                         set_assert();
482                 }
483                 state->islocked = true;
484                 ModelAction *unlock = get_last_unlock(curr);
485                 //synchronize with the previous unlock statement
486                 if (unlock != NULL) {
487                         curr->synchronize_with(unlock);
488                         return true;
489                 }
490                 break;
491         }
492         case ATOMIC_UNLOCK: {
493                 //unlock the lock
494                 state->islocked = false;
495                 //wake up the other threads
496                 action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
497                 //activate all the waiting threads
498                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
499                         scheduler->wake(get_thread(*rit));
500                 }
501                 waiters->clear();
502                 break;
503         }
504         default:
505                 ASSERT(0);
506         }
507         return false;
508 }
509
510 /**
511  * Process a write ModelAction
512  * @param curr The ModelAction to process
513  * @return True if the mo_graph was updated or promises were resolved
514  */
515 bool ModelChecker::process_write(ModelAction *curr)
516 {
517         bool updated_mod_order = w_modification_order(curr);
518         bool updated_promises = resolve_promises(curr);
519
520         if (promises->size() == 0) {
521                 for (unsigned int i = 0; i < futurevalues->size(); i++) {
522                         struct PendingFutureValue pfv = (*futurevalues)[i];
523                         //Do more ambitious checks now that mo is more complete
524                         if (mo_may_allow(pfv.writer, pfv.act)&&
525                                         pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
526                                         (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
527                                 priv->next_backtrack = pfv.act;
528                 }
529                 futurevalues->resize(0);
530         }
531
532         mo_graph->commitChanges();
533         mo_check_promises(curr->get_tid(), curr);
534
535         get_thread(curr)->set_return_value(VALUE_NONE);
536         return updated_mod_order || updated_promises;
537 }
538
539 /**
540  * @brief Process the current action for thread-related activity
541  *
542  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
543  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
544  * synchronization, etc.  This function is a no-op for non-THREAD actions
545  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
546  *
547  * @param curr The current action
548  * @return True if synchronization was updated or a thread completed
549  */
550 bool ModelChecker::process_thread_action(ModelAction *curr)
551 {
552         bool updated = false;
553
554         switch (curr->get_type()) {
555         case THREAD_CREATE: {
556                 Thread *th = (Thread *)curr->get_location();
557                 th->set_creation(curr);
558                 break;
559         }
560         case THREAD_JOIN: {
561                 Thread *blocking = (Thread *)curr->get_location();
562                 ModelAction *act = get_last_action(blocking->get_id());
563                 curr->synchronize_with(act);
564                 updated = true; /* trigger rel-seq checks */
565                 break;
566         }
567         case THREAD_FINISH: {
568                 Thread *th = get_thread(curr);
569                 while (!th->wait_list_empty()) {
570                         ModelAction *act = th->pop_wait_list();
571                         scheduler->wake(get_thread(act));
572                 }
573                 th->complete();
574                 updated = true; /* trigger rel-seq checks */
575                 break;
576         }
577         case THREAD_START: {
578                 check_promises(curr->get_tid(), NULL, curr->get_cv());
579                 break;
580         }
581         default:
582                 break;
583         }
584
585         return updated;
586 }
587
588 /**
589  * @brief Process the current action for release sequence fixup activity
590  *
591  * Performs model-checker release sequence fixups for the current action,
592  * forcing a single pending release sequence to break (with a given, potential
593  * "loose" write) or to complete (i.e., synchronize). If a pending release
594  * sequence forms a complete release sequence, then we must perform the fixup
595  * synchronization, mo_graph additions, etc.
596  *
597  * @param curr The current action; must be a release sequence fixup action
598  * @param work_queue The work queue to which to add work items as they are
599  * generated
600  */
601 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
602 {
603         const ModelAction *write = curr->get_node()->get_relseq_break();
604         struct release_seq *sequence = pending_rel_seqs->back();
605         pending_rel_seqs->pop_back();
606         ASSERT(sequence);
607         ModelAction *acquire = sequence->acquire;
608         const ModelAction *rf = sequence->rf;
609         const ModelAction *release = sequence->release;
610         ASSERT(acquire);
611         ASSERT(release);
612         ASSERT(rf);
613         ASSERT(release->same_thread(rf));
614
615         if (write == NULL) {
616                 /**
617                  * @todo Forcing a synchronization requires that we set
618                  * modification order constraints. For instance, we can't allow
619                  * a fixup sequence in which two separate read-acquire
620                  * operations read from the same sequence, where the first one
621                  * synchronizes and the other doesn't. Essentially, we can't
622                  * allow any writes to insert themselves between 'release' and
623                  * 'rf'
624                  */
625
626                 /* Must synchronize */
627                 if (!acquire->synchronize_with(release)) {
628                         set_bad_synchronization();
629                         return;
630                 }
631                 /* Re-check all pending release sequences */
632                 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
633                 /* Re-check act for mo_graph edges */
634                 work_queue->push_back(MOEdgeWorkEntry(acquire));
635
636                 /* propagate synchronization to later actions */
637                 action_list_t::reverse_iterator rit = action_trace->rbegin();
638                 for (; (*rit) != acquire; rit++) {
639                         ModelAction *propagate = *rit;
640                         if (acquire->happens_before(propagate)) {
641                                 propagate->synchronize_with(acquire);
642                                 /* Re-check 'propagate' for mo_graph edges */
643                                 work_queue->push_back(MOEdgeWorkEntry(propagate));
644                         }
645                 }
646         } else {
647                 /* Break release sequence with new edges:
648                  *   release --mo--> write --mo--> rf */
649                 mo_graph->addEdge(release, write);
650                 mo_graph->addEdge(write, rf);
651         }
652
653         /* See if we have realized a data race */
654         if (checkDataRaces())
655                 set_assert();
656 }
657
658 /**
659  * Initialize the current action by performing one or more of the following
660  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
661  * in the NodeStack, manipulating backtracking sets, allocating and
662  * initializing clock vectors, and computing the promises to fulfill.
663  *
664  * @param curr The current action, as passed from the user context; may be
665  * freed/invalidated after the execution of this function
666  * @return The current action, as processed by the ModelChecker. Is only the
667  * same as the parameter @a curr if this is a newly-explored action.
668  */
669 ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
670 {
671         ModelAction *newcurr;
672
673         if (curr->is_rmwc() || curr->is_rmw()) {
674                 newcurr = process_rmw(curr);
675                 delete curr;
676
677                 if (newcurr->is_rmw())
678                         compute_promises(newcurr);
679                 return newcurr;
680         }
681
682         curr->set_seq_number(get_next_seq_num());
683
684         newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
685         if (newcurr) {
686                 /* First restore type and order in case of RMW operation */
687                 if (curr->is_rmwr())
688                         newcurr->copy_typeandorder(curr);
689
690                 ASSERT(curr->get_location() == newcurr->get_location());
691                 newcurr->copy_from_new(curr);
692
693                 /* Discard duplicate ModelAction; use action from NodeStack */
694                 delete curr;
695
696                 /* Always compute new clock vector */
697                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
698         } else {
699                 newcurr = curr;
700
701                 /* Always compute new clock vector */
702                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
703                 /*
704                  * Perform one-time actions when pushing new ModelAction onto
705                  * NodeStack
706                  */
707                 if (newcurr->is_write())
708                         compute_promises(newcurr);
709                 else if (newcurr->is_relseq_fixup())
710                         compute_relseq_breakwrites(newcurr);
711         }
712         return newcurr;
713 }
714
715 /**
716  * @brief Check whether a model action is enabled.
717  *
718  * Checks whether a lock or join operation would be successful (i.e., is the
719  * lock already locked, or is the joined thread already complete). If not, put
720  * the action in a waiter list.
721  *
722  * @param curr is the ModelAction to check whether it is enabled.
723  * @return a bool that indicates whether the action is enabled.
724  */
725 bool ModelChecker::check_action_enabled(ModelAction *curr) {
726         if (curr->is_lock()) {
727                 std::mutex * lock = (std::mutex *)curr->get_location();
728                 struct std::mutex_state * state = lock->get_state();
729                 if (state->islocked) {
730                         //Stick the action in the appropriate waiting queue
731                         lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
732                         return false;
733                 }
734         } else if (curr->get_type() == THREAD_JOIN) {
735                 Thread *blocking = (Thread *)curr->get_location();
736                 if (!blocking->is_complete()) {
737                         blocking->push_wait_list(curr);
738                         return false;
739                 }
740         }
741
742         return true;
743 }
744
745 /**
746  * This is the heart of the model checker routine. It performs model-checking
747  * actions corresponding to a given "current action." Among other processes, it
748  * calculates reads-from relationships, updates synchronization clock vectors,
749  * forms a memory_order constraints graph, and handles replay/backtrack
750  * execution when running permutations of previously-observed executions.
751  *
752  * @param curr The current action to process
753  * @return The next Thread that must be executed. May be NULL if ModelChecker
754  * makes no choice (e.g., according to replay execution, combining RMW actions,
755  * etc.)
756  */
757 Thread * ModelChecker::check_current_action(ModelAction *curr)
758 {
759         ASSERT(curr);
760         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
761
762         if (!check_action_enabled(curr)) {
763                 /* Make the execution look like we chose to run this action
764                  * much later, when a lock/join can succeed */
765                 get_current_thread()->set_pending(curr);
766                 scheduler->sleep(get_current_thread());
767                 return get_next_thread(NULL);
768         }
769
770         wake_up_sleeping_actions(curr);
771
772         ModelAction *newcurr = initialize_curr_action(curr);
773
774
775         /* Add the action to lists before any other model-checking tasks */
776         if (!second_part_of_rmw)
777                 add_action_to_lists(newcurr);
778
779         /* Build may_read_from set for newly-created actions */
780         if (curr == newcurr && curr->is_read())
781                 build_reads_from_past(curr);
782         curr = newcurr;
783
784         /* Initialize work_queue with the "current action" work */
785         work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
786         while (!work_queue.empty()) {
787                 WorkQueueEntry work = work_queue.front();
788                 work_queue.pop_front();
789
790                 switch (work.type) {
791                 case WORK_CHECK_CURR_ACTION: {
792                         ModelAction *act = work.action;
793                         bool update = false; /* update this location's release seq's */
794                         bool update_all = false; /* update all release seq's */
795
796                         if (process_thread_action(curr))
797                                 update_all = true;
798
799                         if (act->is_read() && process_read(act, second_part_of_rmw))
800                                 update = true;
801
802                         if (act->is_write() && process_write(act))
803                                 update = true;
804
805                         if (act->is_mutex_op() && process_mutex(act))
806                                 update_all = true;
807
808                         if (act->is_relseq_fixup())
809                                 process_relseq_fixup(curr, &work_queue);
810
811                         if (update_all)
812                                 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
813                         else if (update)
814                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
815                         break;
816                 }
817                 case WORK_CHECK_RELEASE_SEQ:
818                         resolve_release_sequences(work.location, &work_queue);
819                         break;
820                 case WORK_CHECK_MO_EDGES: {
821                         /** @todo Complete verification of work_queue */
822                         ModelAction *act = work.action;
823                         bool updated = false;
824
825                         if (act->is_read()) {
826                                 const ModelAction *rf = act->get_reads_from();
827                                 if (rf != NULL && r_modification_order(act, rf))
828                                         updated = true;
829                         }
830                         if (act->is_write()) {
831                                 if (w_modification_order(act))
832                                         updated = true;
833                         }
834                         mo_graph->commitChanges();
835
836                         if (updated)
837                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
838                         break;
839                 }
840                 default:
841                         ASSERT(false);
842                         break;
843                 }
844         }
845
846         check_curr_backtracking(curr);
847         set_backtracking(curr);
848         return get_next_thread(curr);
849 }
850
851 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
852         Node *currnode = curr->get_node();
853         Node *parnode = currnode->get_parent();
854
855         if ((!parnode->backtrack_empty() ||
856                          !currnode->read_from_empty() ||
857                          !currnode->future_value_empty() ||
858                          !currnode->promise_empty() ||
859                          !currnode->relseq_break_empty())
860                         && (!priv->next_backtrack ||
861                                         *curr > *priv->next_backtrack)) {
862                 priv->next_backtrack = curr;
863         }
864 }
865
866 bool ModelChecker::promises_expired() {
867         for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
868                 Promise *promise = (*promises)[promise_index];
869                 if (promise->get_expiration()<priv->used_sequence_numbers) {
870                         return true;
871                 }
872         }
873         return false;
874 }
875
876 /** @return whether the current partial trace must be a prefix of a
877  * feasible trace. */
878 bool ModelChecker::isfeasibleprefix() {
879         return promises->size() == 0 && pending_rel_seqs->size() == 0;
880 }
881
882 /** @return whether the current partial trace is feasible. */
883 bool ModelChecker::isfeasible() {
884         if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
885                 DEBUG("Infeasible: RMW violation\n");
886
887         return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
888 }
889
890 /** @return whether the current partial trace is feasible other than
891  * multiple RMW reading from the same store. */
892 bool ModelChecker::isfeasibleotherthanRMW() {
893         if (DBG_ENABLED()) {
894                 if (mo_graph->checkForCycles())
895                         DEBUG("Infeasible: modification order cycles\n");
896                 if (failed_promise)
897                         DEBUG("Infeasible: failed promise\n");
898                 if (too_many_reads)
899                         DEBUG("Infeasible: too many reads\n");
900                 if (bad_synchronization)
901                         DEBUG("Infeasible: bad synchronization ordering\n");
902                 if (promises_expired())
903                         DEBUG("Infeasible: promises expired\n");
904         }
905         return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
906 }
907
908 /** Returns whether the current completed trace is feasible. */
909 bool ModelChecker::isfinalfeasible() {
910         if (DBG_ENABLED() && promises->size() != 0)
911                 DEBUG("Infeasible: unrevolved promises\n");
912
913         return isfeasible() && promises->size() == 0;
914 }
915
916 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
917 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
918         ModelAction *lastread = get_last_action(act->get_tid());
919         lastread->process_rmw(act);
920         if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
921                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
922                 mo_graph->commitChanges();
923         }
924         return lastread;
925 }
926
927 /**
928  * Checks whether a thread has read from the same write for too many times
929  * without seeing the effects of a later write.
930  *
931  * Basic idea:
932  * 1) there must a different write that we could read from that would satisfy the modification order,
933  * 2) we must have read from the same value in excess of maxreads times, and
934  * 3) that other write must have been in the reads_from set for maxreads times.
935  *
936  * If so, we decide that the execution is no longer feasible.
937  */
938 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
939         if (params.maxreads != 0) {
940
941                 if (curr->get_node()->get_read_from_size() <= 1)
942                         return;
943                 //Must make sure that execution is currently feasible...  We could
944                 //accidentally clear by rolling back
945                 if (!isfeasible())
946                         return;
947                 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
948                 int tid = id_to_int(curr->get_tid());
949
950                 /* Skip checks */
951                 if ((int)thrd_lists->size() <= tid)
952                         return;
953                 action_list_t *list = &(*thrd_lists)[tid];
954
955                 action_list_t::reverse_iterator rit = list->rbegin();
956                 /* Skip past curr */
957                 for (; (*rit) != curr; rit++)
958                         ;
959                 /* go past curr now */
960                 rit++;
961
962                 action_list_t::reverse_iterator ritcopy = rit;
963                 //See if we have enough reads from the same value
964                 int count = 0;
965                 for (; count < params.maxreads; rit++,count++) {
966                         if (rit==list->rend())
967                                 return;
968                         ModelAction *act = *rit;
969                         if (!act->is_read())
970                                 return;
971                         
972                         if (act->get_reads_from() != rf)
973                                 return;
974                         if (act->get_node()->get_read_from_size() <= 1)
975                                 return;
976                 }
977                 for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
978                         //Get write
979                         const ModelAction * write = curr->get_node()->get_read_from_at(i);
980
981                         //Need a different write
982                         if (write==rf)
983                                 continue;
984
985                         /* Test to see whether this is a feasible write to read from*/
986                         mo_graph->startChanges();
987                         r_modification_order(curr, write);
988                         bool feasiblereadfrom = isfeasible();
989                         mo_graph->rollbackChanges();
990
991                         if (!feasiblereadfrom)
992                                 continue;
993                         rit = ritcopy;
994
995                         bool feasiblewrite = true;
996                         //new we need to see if this write works for everyone
997
998                         for (int loop = count; loop>0; loop--,rit++) {
999                                 ModelAction *act=*rit;
1000                                 bool foundvalue = false;
1001                                 for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
1002                                         if (act->get_node()->get_read_from_at(i)==write) {
1003                                                 foundvalue = true;
1004                                                 break;
1005                                         }
1006                                 }
1007                                 if (!foundvalue) {
1008                                         feasiblewrite = false;
1009                                         break;
1010                                 }
1011                         }
1012                         if (feasiblewrite) {
1013                                 too_many_reads = true;
1014                                 return;
1015                         }
1016                 }
1017         }
1018 }
1019
1020 /**
1021  * Updates the mo_graph with the constraints imposed from the current
1022  * read.
1023  *
1024  * Basic idea is the following: Go through each other thread and find
1025  * the lastest action that happened before our read.  Two cases:
1026  *
1027  * (1) The action is a write => that write must either occur before
1028  * the write we read from or be the write we read from.
1029  *
1030  * (2) The action is a read => the write that that action read from
1031  * must occur before the write we read from or be the same write.
1032  *
1033  * @param curr The current action. Must be a read.
1034  * @param rf The action that curr reads from. Must be a write.
1035  * @return True if modification order edges were added; false otherwise
1036  */
1037 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
1038 {
1039         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1040         unsigned int i;
1041         bool added = false;
1042         ASSERT(curr->is_read());
1043
1044         /* Iterate over all threads */
1045         for (i = 0; i < thrd_lists->size(); i++) {
1046                 /* Iterate over actions in thread, starting from most recent */
1047                 action_list_t *list = &(*thrd_lists)[i];
1048                 action_list_t::reverse_iterator rit;
1049                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1050                         ModelAction *act = *rit;
1051
1052                         /*
1053                          * Include at most one act per-thread that "happens
1054                          * before" curr. Don't consider reflexively.
1055                          */
1056                         if (act->happens_before(curr) && act != curr) {
1057                                 if (act->is_write()) {
1058                                         if (rf != act) {
1059                                                 mo_graph->addEdge(act, rf);
1060                                                 added = true;
1061                                         }
1062                                 } else {
1063                                         const ModelAction *prevreadfrom = act->get_reads_from();
1064                                         //if the previous read is unresolved, keep going...
1065                                         if (prevreadfrom == NULL)
1066                                                 continue;
1067
1068                                         if (rf != prevreadfrom) {
1069                                                 mo_graph->addEdge(prevreadfrom, rf);
1070                                                 added = true;
1071                                         }
1072                                 }
1073                                 break;
1074                         }
1075                 }
1076         }
1077
1078         return added;
1079 }
1080
1081 /** This method fixes up the modification order when we resolve a
1082  *  promises.  The basic problem is that actions that occur after the
1083  *  read curr could not property add items to the modification order
1084  *  for our read.
1085  *
1086  *  So for each thread, we find the earliest item that happens after
1087  *  the read curr.  This is the item we have to fix up with additional
1088  *  constraints.  If that action is write, we add a MO edge between
1089  *  the Action rf and that action.  If the action is a read, we add a
1090  *  MO edge between the Action rf, and whatever the read accessed.
1091  *
1092  * @param curr is the read ModelAction that we are fixing up MO edges for.
1093  * @param rf is the write ModelAction that curr reads from.
1094  *
1095  */
1096 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1097 {
1098         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1099         unsigned int i;
1100         ASSERT(curr->is_read());
1101
1102         /* Iterate over all threads */
1103         for (i = 0; i < thrd_lists->size(); i++) {
1104                 /* Iterate over actions in thread, starting from most recent */
1105                 action_list_t *list = &(*thrd_lists)[i];
1106                 action_list_t::reverse_iterator rit;
1107                 ModelAction *lastact = NULL;
1108
1109                 /* Find last action that happens after curr that is either not curr or a rmw */
1110                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1111                         ModelAction *act = *rit;
1112                         if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1113                                 lastact = act;
1114                         } else
1115                                 break;
1116                 }
1117
1118                         /* Include at most one act per-thread that "happens before" curr */
1119                 if (lastact != NULL) {
1120                         if (lastact==curr) {
1121                                 //Case 1: The resolved read is a RMW, and we need to make sure
1122                                 //that the write portion of the RMW mod order after rf
1123
1124                                 mo_graph->addEdge(rf, lastact);
1125                         } else if (lastact->is_read()) {
1126                                 //Case 2: The resolved read is a normal read and the next
1127                                 //operation is a read, and we need to make sure the value read
1128                                 //is mod ordered after rf
1129
1130                                 const ModelAction *postreadfrom = lastact->get_reads_from();
1131                                 if (postreadfrom != NULL&&rf != postreadfrom)
1132                                         mo_graph->addEdge(rf, postreadfrom);
1133                         } else {
1134                                 //Case 3: The resolved read is a normal read and the next
1135                                 //operation is a write, and we need to make sure that the
1136                                 //write is mod ordered after rf
1137                                 if (lastact!=rf)
1138                                         mo_graph->addEdge(rf, lastact);
1139                         }
1140                         break;
1141                 }
1142         }
1143 }
1144
1145 /**
1146  * Updates the mo_graph with the constraints imposed from the current write.
1147  *
1148  * Basic idea is the following: Go through each other thread and find
1149  * the lastest action that happened before our write.  Two cases:
1150  *
1151  * (1) The action is a write => that write must occur before
1152  * the current write
1153  *
1154  * (2) The action is a read => the write that that action read from
1155  * must occur before the current write.
1156  *
1157  * This method also handles two other issues:
1158  *
1159  * (I) Sequential Consistency: Making sure that if the current write is
1160  * seq_cst, that it occurs after the previous seq_cst write.
1161  *
1162  * (II) Sending the write back to non-synchronizing reads.
1163  *
1164  * @param curr The current action. Must be a write.
1165  * @return True if modification order edges were added; false otherwise
1166  */
1167 bool ModelChecker::w_modification_order(ModelAction *curr)
1168 {
1169         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1170         unsigned int i;
1171         bool added = false;
1172         ASSERT(curr->is_write());
1173
1174         if (curr->is_seqcst()) {
1175                 /* We have to at least see the last sequentially consistent write,
1176                          so we are initialized. */
1177                 ModelAction *last_seq_cst = get_last_seq_cst(curr);
1178                 if (last_seq_cst != NULL) {
1179                         mo_graph->addEdge(last_seq_cst, curr);
1180                         added = true;
1181                 }
1182         }
1183
1184         /* Iterate over all threads */
1185         for (i = 0; i < thrd_lists->size(); i++) {
1186                 /* Iterate over actions in thread, starting from most recent */
1187                 action_list_t *list = &(*thrd_lists)[i];
1188                 action_list_t::reverse_iterator rit;
1189                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1190                         ModelAction *act = *rit;
1191                         if (act == curr) {
1192                                 /*
1193                                  * 1) If RMW and it actually read from something, then we
1194                                  * already have all relevant edges, so just skip to next
1195                                  * thread.
1196                                  * 
1197                                  * 2) If RMW and it didn't read from anything, we should
1198                                  * whatever edge we can get to speed up convergence.
1199                                  *
1200                                  * 3) If normal write, we need to look at earlier actions, so
1201                                  * continue processing list.
1202                                  */
1203                                 if (curr->is_rmw()) {
1204                                         if (curr->get_reads_from()!=NULL)
1205                                                 break;
1206                                         else 
1207                                                 continue;
1208                                 } else
1209                                         continue;
1210                         }
1211
1212                         /*
1213                          * Include at most one act per-thread that "happens
1214                          * before" curr
1215                          */
1216                         if (act->happens_before(curr)) {
1217                                 /*
1218                                  * Note: if act is RMW, just add edge:
1219                                  *   act --mo--> curr
1220                                  * The following edge should be handled elsewhere:
1221                                  *   readfrom(act) --mo--> act
1222                                  */
1223                                 if (act->is_write())
1224                                         mo_graph->addEdge(act, curr);
1225                                 else if (act->is_read()) { 
1226                                         //if previous read accessed a null, just keep going
1227                                         if (act->get_reads_from() == NULL)
1228                                                 continue;
1229                                         mo_graph->addEdge(act->get_reads_from(), curr);
1230                                 }
1231                                 added = true;
1232                                 break;
1233                         } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1234                                                      !act->same_thread(curr)) {
1235                                 /* We have an action that:
1236                                    (1) did not happen before us
1237                                    (2) is a read and we are a write
1238                                    (3) cannot synchronize with us
1239                                    (4) is in a different thread
1240                                    =>
1241                                    that read could potentially read from our write.  Note that
1242                                    these checks are overly conservative at this point, we'll
1243                                    do more checks before actually removing the
1244                                    pendingfuturevalue.
1245
1246                                  */
1247                                 if (thin_air_constraint_may_allow(curr, act)) {
1248                                         if (isfeasible() ||
1249                                                         (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
1250                                                 struct PendingFutureValue pfv = {curr,act};
1251                                                 futurevalues->push_back(pfv);
1252                                         }
1253                                 }
1254                         }
1255                 }
1256         }
1257
1258         return added;
1259 }
1260
1261 /** Arbitrary reads from the future are not allowed.  Section 29.3
1262  * part 9 places some constraints.  This method checks one result of constraint
1263  * constraint.  Others require compiler support. */
1264 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
1265         if (!writer->is_rmw())
1266                 return true;
1267
1268         if (!reader->is_rmw())
1269                 return true;
1270
1271         for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1272                 if (search == reader)
1273                         return false;
1274                 if (search->get_tid() == reader->get_tid() &&
1275                                 search->happens_before(reader))
1276                         break;
1277         }
1278
1279         return true;
1280 }
1281
1282 /** Arbitrary reads from the future are not allowed.  Section 29.3
1283  * part 9 places some constraints.  This method checks one result of constraint
1284  * constraint.  Others require compiler support. */
1285 bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
1286         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
1287
1288         //Get write that follows reader action
1289         action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
1290         action_list_t::reverse_iterator rit;
1291         ModelAction *first_write_after_read=NULL;
1292
1293         for (rit = list->rbegin(); rit != list->rend(); rit++) {
1294                 ModelAction *act = *rit;
1295                 if (act==reader)
1296                         break;
1297                 if (act->is_write())
1298                         first_write_after_read=act;
1299         }
1300
1301         if (first_write_after_read==NULL)
1302                 return true;
1303
1304         return !mo_graph->checkReachable(first_write_after_read, writer);
1305 }
1306
1307
1308
1309 /**
1310  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1311  * The ModelAction under consideration is expected to be taking part in
1312  * release/acquire synchronization as an object of the "reads from" relation.
1313  * Note that this can only provide release sequence support for RMW chains
1314  * which do not read from the future, as those actions cannot be traced until
1315  * their "promise" is fulfilled. Similarly, we may not even establish the
1316  * presence of a release sequence with certainty, as some modification order
1317  * constraints may be decided further in the future. Thus, this function
1318  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1319  * and a boolean representing certainty.
1320  *
1321  * @param rf The action that might be part of a release sequence. Must be a
1322  * write.
1323  * @param release_heads A pass-by-reference style return parameter. After
1324  * execution of this function, release_heads will contain the heads of all the
1325  * relevant release sequences, if any exists with certainty
1326  * @param pending A pass-by-reference style return parameter which is only used
1327  * when returning false (i.e., uncertain). Returns most information regarding
1328  * an uncertain release sequence, including any write operations that might
1329  * break the sequence.
1330  * @return true, if the ModelChecker is certain that release_heads is complete;
1331  * false otherwise
1332  */
1333 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1334                 rel_heads_list_t *release_heads,
1335                 struct release_seq *pending) const
1336 {
1337         /* Only check for release sequences if there are no cycles */
1338         if (mo_graph->checkForCycles())
1339                 return false;
1340
1341         while (rf) {
1342                 ASSERT(rf->is_write());
1343
1344                 if (rf->is_release())
1345                         release_heads->push_back(rf);
1346                 if (!rf->is_rmw())
1347                         break; /* End of RMW chain */
1348
1349                 /** @todo Need to be smarter here...  In the linux lock
1350                  * example, this will run to the beginning of the program for
1351                  * every acquire. */
1352                 /** @todo The way to be smarter here is to keep going until 1
1353                  * thread has a release preceded by an acquire and you've seen
1354                  *       both. */
1355
1356                 /* acq_rel RMW is a sufficient stopping condition */
1357                 if (rf->is_acquire() && rf->is_release())
1358                         return true; /* complete */
1359
1360                 rf = rf->get_reads_from();
1361         };
1362         if (!rf) {
1363                 /* read from future: need to settle this later */
1364                 pending->rf = NULL;
1365                 return false; /* incomplete */
1366         }
1367
1368         if (rf->is_release())
1369                 return true; /* complete */
1370
1371         /* else relaxed write; check modification order for contiguous subsequence
1372          * -> rf must be same thread as release */
1373         int tid = id_to_int(rf->get_tid());
1374         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
1375         action_list_t *list = &(*thrd_lists)[tid];
1376         action_list_t::const_reverse_iterator rit;
1377
1378         /* Find rf in the thread list */
1379         rit = std::find(list->rbegin(), list->rend(), rf);
1380         ASSERT(rit != list->rend());
1381
1382         /* Find the last write/release */
1383         for (; rit != list->rend(); rit++)
1384                 if ((*rit)->is_release())
1385                         break;
1386         if (rit == list->rend()) {
1387                 /* No write-release in this thread */
1388                 return true; /* complete */
1389         }
1390         ModelAction *release = *rit;
1391
1392         ASSERT(rf->same_thread(release));
1393
1394         pending->writes.clear();
1395
1396         bool certain = true;
1397         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1398                 if (id_to_int(rf->get_tid()) == (int)i)
1399                         continue;
1400                 list = &(*thrd_lists)[i];
1401
1402                 /* Can we ensure no future writes from this thread may break
1403                  * the release seq? */
1404                 bool future_ordered = false;
1405
1406                 ModelAction *last = get_last_action(int_to_id(i));
1407                 Thread *th = get_thread(int_to_id(i));
1408                 if ((last && rf->happens_before(last)) ||
1409                                 !scheduler->is_enabled(th) ||
1410                                 th->is_complete())
1411                         future_ordered = true;
1412
1413                 ASSERT(!th->is_model_thread() || future_ordered);
1414
1415                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1416                         const ModelAction *act = *rit;
1417                         /* Reach synchronization -> this thread is complete */
1418                         if (act->happens_before(release))
1419                                 break;
1420                         if (rf->happens_before(act)) {
1421                                 future_ordered = true;
1422                                 continue;
1423                         }
1424
1425                         /* Only writes can break release sequences */
1426                         if (!act->is_write())
1427                                 continue;
1428
1429                         /* Check modification order */
1430                         if (mo_graph->checkReachable(rf, act)) {
1431                                 /* rf --mo--> act */
1432                                 future_ordered = true;
1433                                 continue;
1434                         }
1435                         if (mo_graph->checkReachable(act, release))
1436                                 /* act --mo--> release */
1437                                 break;
1438                         if (mo_graph->checkReachable(release, act) &&
1439                                       mo_graph->checkReachable(act, rf)) {
1440                                 /* release --mo-> act --mo--> rf */
1441                                 return true; /* complete */
1442                         }
1443                         /* act may break release sequence */
1444                         pending->writes.push_back(act);
1445                         certain = false;
1446                 }
1447                 if (!future_ordered)
1448                         certain = false; /* This thread is uncertain */
1449         }
1450
1451         if (certain) {
1452                 release_heads->push_back(release);
1453                 pending->writes.clear();
1454         } else {
1455                 pending->release = release;
1456                 pending->rf = rf;
1457         }
1458         return certain;
1459 }
1460
1461 /**
1462  * A public interface for getting the release sequence head(s) with which a
1463  * given ModelAction must synchronize. This function only returns a non-empty
1464  * result when it can locate a release sequence head with certainty. Otherwise,
1465  * it may mark the internal state of the ModelChecker so that it will handle
1466  * the release sequence at a later time, causing @a act to update its
1467  * synchronization at some later point in execution.
1468  * @param act The 'acquire' action that may read from a release sequence
1469  * @param release_heads A pass-by-reference return parameter. Will be filled
1470  * with the head(s) of the release sequence(s), if they exists with certainty.
1471  * @see ModelChecker::release_seq_heads
1472  */
1473 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
1474 {
1475         const ModelAction *rf = act->get_reads_from();
1476         struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
1477         sequence->acquire = act;
1478
1479         if (!release_seq_heads(rf, release_heads, sequence)) {
1480                 /* add act to 'lazy checking' list */
1481                 pending_rel_seqs->push_back(sequence);
1482         } else {
1483                 snapshot_free(sequence);
1484         }
1485 }
1486
1487 /**
1488  * Attempt to resolve all stashed operations that might synchronize with a
1489  * release sequence for a given location. This implements the "lazy" portion of
1490  * determining whether or not a release sequence was contiguous, since not all
1491  * modification order information is present at the time an action occurs.
1492  *
1493  * @param location The location/object that should be checked for release
1494  * sequence resolutions. A NULL value means to check all locations.
1495  * @param work_queue The work queue to which to add work items as they are
1496  * generated
1497  * @return True if any updates occurred (new synchronization, new mo_graph
1498  * edges)
1499  */
1500 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
1501 {
1502         bool updated = false;
1503         std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
1504         while (it != pending_rel_seqs->end()) {
1505                 struct release_seq *pending = *it;
1506                 ModelAction *act = pending->acquire;
1507
1508                 /* Only resolve sequences on the given location, if provided */
1509                 if (location && act->get_location() != location) {
1510                         it++;
1511                         continue;
1512                 }
1513
1514                 const ModelAction *rf = act->get_reads_from();
1515                 rel_heads_list_t release_heads;
1516                 bool complete;
1517                 complete = release_seq_heads(rf, &release_heads, pending);
1518                 for (unsigned int i = 0; i < release_heads.size(); i++) {
1519                         if (!act->has_synchronized_with(release_heads[i])) {
1520                                 if (act->synchronize_with(release_heads[i]))
1521                                         updated = true;
1522                                 else
1523                                         set_bad_synchronization();
1524                         }
1525                 }
1526
1527                 if (updated) {
1528                         /* Re-check all pending release sequences */
1529                         work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1530                         /* Re-check act for mo_graph edges */
1531                         work_queue->push_back(MOEdgeWorkEntry(act));
1532
1533                         /* propagate synchronization to later actions */
1534                         action_list_t::reverse_iterator rit = action_trace->rbegin();
1535                         for (; (*rit) != act; rit++) {
1536                                 ModelAction *propagate = *rit;
1537                                 if (act->happens_before(propagate)) {
1538                                         propagate->synchronize_with(act);
1539                                         /* Re-check 'propagate' for mo_graph edges */
1540                                         work_queue->push_back(MOEdgeWorkEntry(propagate));
1541                                 }
1542                         }
1543                 }
1544                 if (complete) {
1545                         it = pending_rel_seqs->erase(it);
1546                         snapshot_free(pending);
1547                 } else {
1548                         it++;
1549                 }
1550         }
1551
1552         // If we resolved promises or data races, see if we have realized a data race.
1553         if (checkDataRaces()) {
1554                 set_assert();
1555         }
1556
1557         return updated;
1558 }
1559
1560 /**
1561  * Performs various bookkeeping operations for the current ModelAction. For
1562  * instance, adds action to the per-object, per-thread action vector and to the
1563  * action trace list of all thread actions.
1564  *
1565  * @param act is the ModelAction to add.
1566  */
1567 void ModelChecker::add_action_to_lists(ModelAction *act)
1568 {
1569         int tid = id_to_int(act->get_tid());
1570         action_trace->push_back(act);
1571
1572         obj_map->get_safe_ptr(act->get_location())->push_back(act);
1573
1574         std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
1575         if (tid >= (int)vec->size())
1576                 vec->resize(priv->next_thread_id);
1577         (*vec)[tid].push_back(act);
1578
1579         if ((int)thrd_last_action->size() <= tid)
1580                 thrd_last_action->resize(get_num_threads());
1581         (*thrd_last_action)[tid] = act;
1582 }
1583
1584 /**
1585  * @brief Get the last action performed by a particular Thread
1586  * @param tid The thread ID of the Thread in question
1587  * @return The last action in the thread
1588  */
1589 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
1590 {
1591         int threadid = id_to_int(tid);
1592         if (threadid < (int)thrd_last_action->size())
1593                 return (*thrd_last_action)[id_to_int(tid)];
1594         else
1595                 return NULL;
1596 }
1597
1598 /**
1599  * Gets the last memory_order_seq_cst write (in the total global sequence)
1600  * performed on a particular object (i.e., memory location), not including the
1601  * current action.
1602  * @param curr The current ModelAction; also denotes the object location to
1603  * check
1604  * @return The last seq_cst write
1605  */
1606 ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
1607 {
1608         void *location = curr->get_location();
1609         action_list_t *list = obj_map->get_safe_ptr(location);
1610         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1611         action_list_t::reverse_iterator rit;
1612         for (rit = list->rbegin(); rit != list->rend(); rit++)
1613                 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
1614                         return *rit;
1615         return NULL;
1616 }
1617
1618 /**
1619  * Gets the last unlock operation performed on a particular mutex (i.e., memory
1620  * location). This function identifies the mutex according to the current
1621  * action, which is presumed to perform on the same mutex.
1622  * @param curr The current ModelAction; also denotes the object location to
1623  * check
1624  * @return The last unlock operation
1625  */
1626 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
1627 {
1628         void *location = curr->get_location();
1629         action_list_t *list = obj_map->get_safe_ptr(location);
1630         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1631         action_list_t::reverse_iterator rit;
1632         for (rit = list->rbegin(); rit != list->rend(); rit++)
1633                 if ((*rit)->is_unlock())
1634                         return *rit;
1635         return NULL;
1636 }
1637
1638 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
1639 {
1640         ModelAction *parent = get_last_action(tid);
1641         if (!parent)
1642                 parent = get_thread(tid)->get_creation();
1643         return parent;
1644 }
1645
1646 /**
1647  * Returns the clock vector for a given thread.
1648  * @param tid The thread whose clock vector we want
1649  * @return Desired clock vector
1650  */
1651 ClockVector * ModelChecker::get_cv(thread_id_t tid)
1652 {
1653         return get_parent_action(tid)->get_cv();
1654 }
1655
1656 /**
1657  * Resolve a set of Promises with a current write. The set is provided in the
1658  * Node corresponding to @a write.
1659  * @param write The ModelAction that is fulfilling Promises
1660  * @return True if promises were resolved; false otherwise
1661  */
1662 bool ModelChecker::resolve_promises(ModelAction *write)
1663 {
1664         bool resolved = false;
1665         std::vector< thread_id_t, ModelAlloc<thread_id_t> > threads_to_check;
1666
1667         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
1668                 Promise *promise = (*promises)[promise_index];
1669                 if (write->get_node()->get_promise(i)) {
1670                         ModelAction *read = promise->get_action();
1671                         if (read->is_rmw()) {
1672                                 mo_graph->addRMWEdge(write, read);
1673                         }
1674                         read->read_from(write);
1675                         //First fix up the modification order for actions that happened
1676                         //before the read
1677                         r_modification_order(read, write);
1678                         //Next fix up the modification order for actions that happened
1679                         //after the read.
1680                         post_r_modification_order(read, write);
1681                         //Make sure the promise's value matches the write's value
1682                         ASSERT(promise->get_value() == write->get_value());
1683                         delete(promise);
1684                         
1685                         promises->erase(promises->begin() + promise_index);
1686                         threads_to_check.push_back(read->get_tid());
1687
1688                         resolved = true;
1689                 } else
1690                         promise_index++;
1691         }
1692
1693         //Check whether reading these writes has made threads unable to
1694         //resolve promises
1695
1696         for(unsigned int i=0;i<threads_to_check.size();i++)
1697                 mo_check_promises(threads_to_check[i], write);
1698
1699         return resolved;
1700 }
1701
1702 /**
1703  * Compute the set of promises that could potentially be satisfied by this
1704  * action. Note that the set computation actually appears in the Node, not in
1705  * ModelChecker.
1706  * @param curr The ModelAction that may satisfy promises
1707  */
1708 void ModelChecker::compute_promises(ModelAction *curr)
1709 {
1710         for (unsigned int i = 0; i < promises->size(); i++) {
1711                 Promise *promise = (*promises)[i];
1712                 const ModelAction *act = promise->get_action();
1713                 if (!act->happens_before(curr) &&
1714                                 act->is_read() &&
1715                                 !act->could_synchronize_with(curr) &&
1716                                 !act->same_thread(curr) &&
1717                                 promise->get_value() == curr->get_value()) {
1718                         curr->get_node()->set_promise(i);
1719                 }
1720         }
1721 }
1722
1723 /** Checks promises in response to change in ClockVector Threads. */
1724 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
1725 {
1726         for (unsigned int i = 0; i < promises->size(); i++) {
1727                 Promise *promise = (*promises)[i];
1728                 const ModelAction *act = promise->get_action();
1729                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
1730                                 merge_cv->synchronized_since(act)) {
1731                         if (promise->increment_threads(tid)) {
1732                                 //Promise has failed
1733                                 failed_promise = true;
1734                                 return;
1735                         }
1736                 }
1737         }
1738 }
1739
1740 /** Checks promises in response to addition to modification order for threads.
1741  * Definitions:
1742  * pthread is the thread that performed the read that created the promise
1743  * 
1744  * pread is the read that created the promise
1745  *
1746  * pwrite is either the first write to same location as pread by
1747  * pthread that is sequenced after pread or the value read by the
1748  * first read to the same lcoation as pread by pthread that is
1749  * sequenced after pread..
1750  *
1751  *      1. If tid=pthread, then we check what other threads are reachable
1752  * through the mode order starting with pwrite.  Those threads cannot
1753  * perform a write that will resolve the promise due to modification
1754  * order constraints.
1755  *
1756  * 2. If the tid is not pthread, we check whether pwrite can reach the
1757  * action write through the modification order.  If so, that thread
1758  * cannot perform a future write that will resolve the promise due to
1759  * modificatin order constraints.
1760  *
1761  *      @parem tid The thread that either read from the model action
1762  *      write, or actually did the model action write.
1763  *
1764  *      @parem write The ModelAction representing the relevant write.
1765  */
1766
1767 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
1768         void * location = write->get_location();
1769         for (unsigned int i = 0; i < promises->size(); i++) {
1770                 Promise *promise = (*promises)[i];
1771                 const ModelAction *act = promise->get_action();
1772                 
1773                 //Is this promise on the same location?
1774                 if ( act->get_location() != location )
1775                         continue;
1776
1777                 //same thread as the promise
1778                 if ( act->get_tid()==tid ) {
1779
1780                         //do we have a pwrite for the promise, if not, set it
1781                         if (promise->get_write() == NULL ) {
1782                                 promise->set_write(write);
1783                                 //The pwrite cannot happen before the promise
1784                                 if (write->happens_before(act) && (write != act)) {
1785                                         failed_promise = true;
1786                                         return;
1787                                 }
1788                         }
1789                         if (mo_graph->checkPromise(write, promise)) {
1790                                 failed_promise = true;
1791                                 return;
1792                         }
1793                 }
1794                 
1795                 //Don't do any lookups twice for the same thread
1796                 if (promise->has_sync_thread(tid))
1797                         continue;
1798                 
1799                 if (mo_graph->checkReachable(promise->get_write(), write)) {
1800                         if (promise->increment_threads(tid)) {
1801                                 failed_promise = true;
1802                                 return;
1803                         }
1804                 }
1805         }
1806 }
1807
1808 /**
1809  * Compute the set of writes that may break the current pending release
1810  * sequence. This information is extracted from previou release sequence
1811  * calculations.
1812  *
1813  * @param curr The current ModelAction. Must be a release sequence fixup
1814  * action.
1815  */
1816 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
1817 {
1818         if (pending_rel_seqs->empty())
1819                 return;
1820
1821         struct release_seq *pending = pending_rel_seqs->back();
1822         for (unsigned int i = 0; i < pending->writes.size(); i++) {
1823                 const ModelAction *write = pending->writes[i];
1824                 curr->get_node()->add_relseq_break(write);
1825         }
1826
1827         /* NULL means don't break the sequence; just synchronize */
1828         curr->get_node()->add_relseq_break(NULL);
1829 }
1830
1831 /**
1832  * Build up an initial set of all past writes that this 'read' action may read
1833  * from. This set is determined by the clock vector's "happens before"
1834  * relationship.
1835  * @param curr is the current ModelAction that we are exploring; it must be a
1836  * 'read' operation.
1837  */
1838 void ModelChecker::build_reads_from_past(ModelAction *curr)
1839 {
1840         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1841         unsigned int i;
1842         ASSERT(curr->is_read());
1843
1844         ModelAction *last_seq_cst = NULL;
1845
1846         /* Track whether this object has been initialized */
1847         bool initialized = false;
1848
1849         if (curr->is_seqcst()) {
1850                 last_seq_cst = get_last_seq_cst(curr);
1851                 /* We have to at least see the last sequentially consistent write,
1852                          so we are initialized. */
1853                 if (last_seq_cst != NULL)
1854                         initialized = true;
1855         }
1856
1857         /* Iterate over all threads */
1858         for (i = 0; i < thrd_lists->size(); i++) {
1859                 /* Iterate over actions in thread, starting from most recent */
1860                 action_list_t *list = &(*thrd_lists)[i];
1861                 action_list_t::reverse_iterator rit;
1862                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1863                         ModelAction *act = *rit;
1864
1865                         /* Only consider 'write' actions */
1866                         if (!act->is_write() || act == curr)
1867                                 continue;
1868
1869                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1870                         if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
1871                                 DEBUG("Adding action to may_read_from:\n");
1872                                 if (DBG_ENABLED()) {
1873                                         act->print();
1874                                         curr->print();
1875                                 }
1876
1877                                 if (curr->get_sleep_flag() && ! curr->is_seqcst()) {
1878                                         if (sleep_can_read_from(curr, act))
1879                                                 curr->get_node()->add_read_from(act);
1880                                 } else
1881                                         curr->get_node()->add_read_from(act);
1882                         }
1883
1884                         /* Include at most one act per-thread that "happens before" curr */
1885                         if (act->happens_before(curr)) {
1886                                 initialized = true;
1887                                 break;
1888                         }
1889                 }
1890         }
1891
1892         if (!initialized) {
1893                 /** @todo Need a more informative way of reporting errors. */
1894                 printf("ERROR: may read from uninitialized atomic\n");
1895         }
1896
1897         if (DBG_ENABLED() || !initialized) {
1898                 printf("Reached read action:\n");
1899                 curr->print();
1900                 printf("Printing may_read_from\n");
1901                 curr->get_node()->print_may_read_from();
1902                 printf("End printing may_read_from\n");
1903         }
1904
1905         ASSERT(initialized);
1906 }
1907
1908 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
1909         while(true) {
1910                 Node *prevnode=write->get_node()->get_parent();
1911                 bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
1912                 if (write->is_release()&&thread_sleep)
1913                         return true;
1914                 if (!write->is_rmw()) {
1915                         return false;
1916                 }
1917                 if (write->get_reads_from()==NULL)
1918                         return true;
1919                 write=write->get_reads_from();
1920         }
1921 }
1922
1923 static void print_list(action_list_t *list)
1924 {
1925         action_list_t::iterator it;
1926
1927         printf("---------------------------------------------------------------------\n");
1928         printf("Trace:\n");
1929         unsigned int hash=0;
1930         
1931         for (it = list->begin(); it != list->end(); it++) {
1932                 (*it)->print();
1933                 hash=hash^(hash<<3)^((*it)->hash());
1934         }
1935         printf("HASH %u\n", hash);
1936         printf("---------------------------------------------------------------------\n");
1937 }
1938
1939 #if SUPPORT_MOD_ORDER_DUMP
1940 void ModelChecker::dumpGraph(char *filename) {
1941         char buffer[200];
1942   sprintf(buffer, "%s.dot",filename);
1943   FILE *file=fopen(buffer, "w");
1944   fprintf(file, "digraph %s {\n",filename);
1945         mo_graph->dumpNodes(file);
1946         ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
1947         
1948         for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
1949                 ModelAction *action=*it;
1950                 if (action->is_read()) {
1951                         fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
1952                         if (action->get_reads_from()!=NULL)
1953                                 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
1954                 }
1955                 if (thread_array[action->get_tid()] != NULL) {
1956                         fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
1957                 }
1958                 
1959                 thread_array[action->get_tid()]=action;
1960         }
1961   fprintf(file,"}\n");
1962         model_free(thread_array);
1963   fclose(file); 
1964 }
1965 #endif
1966
1967 void ModelChecker::print_summary()
1968 {
1969         printf("\n");
1970         printf("Number of executions: %d\n", num_executions);
1971         printf("Number of feasible executions: %d\n", num_feasible_executions);
1972         printf("Total nodes created: %d\n", node_stack->get_total_nodes());
1973
1974 #if SUPPORT_MOD_ORDER_DUMP
1975         scheduler->print();
1976         char buffername[100];
1977         sprintf(buffername, "exec%04u", num_executions);
1978         mo_graph->dumpGraphToFile(buffername);
1979         sprintf(buffername, "graph%04u", num_executions);
1980   dumpGraph(buffername);
1981 #endif
1982
1983         if (!isfinalfeasible())
1984                 printf("INFEASIBLE EXECUTION!\n");
1985         print_list(action_trace);
1986         printf("\n");
1987 }
1988
1989 /**
1990  * Add a Thread to the system for the first time. Should only be called once
1991  * per thread.
1992  * @param t The Thread to add
1993  */
1994 void ModelChecker::add_thread(Thread *t)
1995 {
1996         thread_map->put(id_to_int(t->get_id()), t);
1997         scheduler->add_thread(t);
1998 }
1999
2000 /**
2001  * Removes a thread from the scheduler. 
2002  * @param the thread to remove.
2003  */
2004 void ModelChecker::remove_thread(Thread *t)
2005 {
2006         scheduler->remove_thread(t);
2007 }
2008
2009 /**
2010  * @brief Get a Thread reference by its ID
2011  * @param tid The Thread's ID
2012  * @return A Thread reference
2013  */
2014 Thread * ModelChecker::get_thread(thread_id_t tid) const
2015 {
2016         return thread_map->get(id_to_int(tid));
2017 }
2018
2019 /**
2020  * @brief Get a reference to the Thread in which a ModelAction was executed
2021  * @param act The ModelAction
2022  * @return A Thread reference
2023  */
2024 Thread * ModelChecker::get_thread(ModelAction *act) const
2025 {
2026         return get_thread(act->get_tid());
2027 }
2028
2029 /**
2030  * Switch from a user-context to the "master thread" context (a.k.a. system
2031  * context). This switch is made with the intention of exploring a particular
2032  * model-checking action (described by a ModelAction object). Must be called
2033  * from a user-thread context.
2034  *
2035  * @param act The current action that will be explored. May be NULL only if
2036  * trace is exiting via an assertion (see ModelChecker::set_assert and
2037  * ModelChecker::has_asserted).
2038  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
2039  */
2040 int ModelChecker::switch_to_master(ModelAction *act)
2041 {
2042         DBG();
2043         Thread *old = thread_current();
2044         set_current_action(act);
2045         old->set_state(THREAD_READY);
2046         return Thread::swap(old, &system_context);
2047 }
2048
2049 /**
2050  * Takes the next step in the execution, if possible.
2051  * @return Returns true (success) if a step was taken and false otherwise.
2052  */
2053 bool ModelChecker::take_step() {
2054         if (has_asserted())
2055                 return false;
2056
2057         Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
2058         if (curr) {
2059                 if (curr->get_state() == THREAD_READY) {
2060                         ASSERT(priv->current_action);
2061
2062                         priv->nextThread = check_current_action(priv->current_action);
2063                         priv->current_action = NULL;
2064
2065                         if (curr->is_blocked() || curr->is_complete())
2066                                 scheduler->remove_thread(curr);
2067                 } else {
2068                         ASSERT(false);
2069                 }
2070         }
2071         Thread *next = scheduler->next_thread(priv->nextThread);
2072
2073         /* Infeasible -> don't take any more steps */
2074         if (!isfeasible())
2075                 return false;
2076
2077         if (params.bound != 0) {
2078                 if (priv->used_sequence_numbers > params.bound) {
2079                         return false;
2080                 }
2081         }
2082
2083         DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
2084                         next ? id_to_int(next->get_id()) : -1);
2085
2086         /*
2087          * Launch end-of-execution release sequence fixups only when there are:
2088          *
2089          * (1) no more user threads to run (or when execution replay chooses
2090          *     the 'model_thread')
2091          * (2) pending release sequences
2092          * (3) pending assertions (i.e., data races)
2093          * (4) no pending promises
2094          */
2095         if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
2096                         isfinalfeasible() && !unrealizedraces.empty()) {
2097                 printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2098                                 pending_rel_seqs->size());
2099                 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2100                                 std::memory_order_seq_cst, NULL, VALUE_NONE,
2101                                 model_thread);
2102                 set_current_action(fixup);
2103                 return true;
2104         }
2105
2106         /* next == NULL -> don't take any more steps */
2107         if (!next)
2108                 return false;
2109
2110         next->set_state(THREAD_RUNNING);
2111
2112         if (next->get_pending() != NULL) {
2113                 /* restart a pending action */
2114                 set_current_action(next->get_pending());
2115                 next->set_pending(NULL);
2116                 next->set_state(THREAD_READY);
2117                 return true;
2118         }
2119
2120         /* Return false only if swap fails with an error */
2121         return (Thread::swap(&system_context, next) == 0);
2122 }
2123
2124 /** Runs the current execution until threre are no more steps to take. */
2125 void ModelChecker::finish_execution() {
2126         DBG();
2127
2128         while (take_step());
2129 }