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