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