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