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