10 #include "snapshot-interface.h"
12 #include "clockvector.h"
13 #include "cyclegraph.h"
16 #include "threads-model.h"
19 #define INITIAL_THREAD_ID 0
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);
29 ~bug_message() { if (msg) snapshot_free(msg); }
32 void print() { model_print("%s", msg); }
38 * Structure for holding small ModelChecker members that should be snapshotted
40 struct model_snapshot_members {
41 model_snapshot_members() :
42 /* First thread created will have id INITIAL_THREAD_ID */
43 next_thread_id(INITIAL_THREAD_ID),
44 used_sequence_numbers(0),
48 failed_promise(false),
49 too_many_reads(false),
50 no_valid_reads(false),
51 bad_synchronization(false),
55 ~model_snapshot_members() {
56 for (unsigned int i = 0; i < bugs.size(); i++)
61 unsigned int next_thread_id;
62 modelclock_t used_sequence_numbers;
63 ModelAction *next_backtrack;
64 std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
65 struct execution_stats stats;
69 /** @brief Incorrectly-ordered synchronization was made */
70 bool bad_synchronization;
76 /** @brief Constructor */
77 ModelChecker::ModelChecker(struct model_params params) :
78 /* Initialize default scheduler */
80 scheduler(new Scheduler()),
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())
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);
103 /** @brief Destructor */
104 ModelChecker::~ModelChecker()
106 for (unsigned int i = 0; i < get_num_threads(); i++)
107 delete thread_map->get(i);
112 delete lock_waiters_map;
113 delete condvar_waiters_map;
116 for (unsigned int i = 0; i < promises->size(); i++)
117 delete (*promises)[i];
120 delete pending_rel_seqs;
122 delete thrd_last_action;
123 delete thrd_last_fence_release;
130 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
132 action_list_t *tmp = hash->get(ptr);
134 tmp = new action_list_t();
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)
142 std::vector<action_list_t> *tmp = hash->get(ptr);
144 tmp = new std::vector<action_list_t>();
151 * Restores user program to initial state and resets all model-checker data
154 void ModelChecker::reset_to_initial_state()
156 DEBUG("+++ Resetting to initial state +++\n");
157 node_stack->reset_execution();
159 /* Print all model-checker output before rollback */
163 * FIXME: if we utilize partial rollback, we will need to free only
164 * those pending actions which were NOT pending before the rollback
167 for (unsigned int i = 0; i < get_num_threads(); i++)
168 delete get_thread(int_to_id(i))->get_pending();
170 snapshot_backtrack_before(0);
173 /** @return a thread ID for a new Thread */
174 thread_id_t ModelChecker::get_next_id()
176 return priv->next_thread_id++;
179 /** @return the number of user threads created during this execution */
180 unsigned int ModelChecker::get_num_threads() const
182 return priv->next_thread_id;
186 * Must be called from user-thread context (e.g., through the global
187 * thread_current() interface)
189 * @return The currently executing Thread.
191 Thread * ModelChecker::get_current_thread() const
193 return scheduler->get_current_thread();
196 /** @return a sequence number for a new ModelAction */
197 modelclock_t ModelChecker::get_next_seq_num()
199 return ++priv->used_sequence_numbers;
202 Node * ModelChecker::get_curr_node() const
204 return node_stack->get_head();
208 * @brief Choose the next thread to execute.
210 * This function chooses the next thread that should execute. It can force the
211 * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
212 * followed by a THREAD_START, or it can enforce execution replay/backtracking.
213 * The model-checker may have no preference regarding the next thread (i.e.,
214 * when exploring a new execution ordering), in which case we defer to the
217 * @param curr Optional: The current ModelAction. Only used if non-NULL and it
218 * might guide the choice of next thread (i.e., THREAD_CREATE should be
219 * followed by THREAD_START, or ATOMIC_RMWR followed by ATOMIC_{RMW,RMWC})
220 * @return The next chosen thread to run, if any exist. Or else if no threads
221 * remain to be executed, return NULL.
223 Thread * ModelChecker::get_next_thread(ModelAction *curr)
228 /* Do not split atomic actions. */
230 return get_thread(curr);
231 else if (curr->get_type() == THREAD_CREATE)
232 return curr->get_thread_operand();
236 * Have we completed exploring the preselected path? Then let the
240 return scheduler->select_next_thread();
242 /* Else, we are trying to replay an execution */
243 ModelAction *next = node_stack->get_next()->get_action();
245 if (next == diverge) {
246 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
247 earliest_diverge = diverge;
249 Node *nextnode = next->get_node();
250 Node *prevnode = nextnode->get_parent();
251 scheduler->update_sleep_set(prevnode);
253 /* Reached divergence point */
254 if (nextnode->increment_misc()) {
255 /* The next node will try to satisfy a different misc_index values. */
256 tid = next->get_tid();
257 node_stack->pop_restofstack(2);
258 } else if (nextnode->increment_promise()) {
259 /* The next node will try to satisfy a different set of promises. */
260 tid = next->get_tid();
261 node_stack->pop_restofstack(2);
262 } else if (nextnode->increment_read_from()) {
263 /* The next node will read from a different value. */
264 tid = next->get_tid();
265 node_stack->pop_restofstack(2);
266 } else if (nextnode->increment_future_value()) {
267 /* The next node will try to read from a different future value. */
268 tid = next->get_tid();
269 node_stack->pop_restofstack(2);
270 } else if (nextnode->increment_relseq_break()) {
271 /* The next node will try to resolve a release sequence differently */
272 tid = next->get_tid();
273 node_stack->pop_restofstack(2);
276 /* Make a different thread execute for next step */
277 scheduler->add_sleep(get_thread(next->get_tid()));
278 tid = prevnode->get_next_backtrack();
279 /* Make sure the backtracked thread isn't sleeping. */
280 node_stack->pop_restofstack(1);
281 if (diverge == earliest_diverge) {
282 earliest_diverge = prevnode->get_action();
285 /* Start the round robin scheduler from this thread id */
286 scheduler->set_scheduler_thread(tid);
287 /* The correct sleep set is in the parent node. */
290 DEBUG("*** Divergence point ***\n");
294 tid = next->get_tid();
296 DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
297 ASSERT(tid != THREAD_ID_T_NONE);
298 return thread_map->get(id_to_int(tid));
302 * We need to know what the next actions of all threads in the sleep
303 * set will be. This method computes them and stores the actions at
304 * the corresponding thread object's pending action.
307 void ModelChecker::execute_sleep_set()
309 for (unsigned int i = 0; i < get_num_threads(); i++) {
310 thread_id_t tid = int_to_id(i);
311 Thread *thr = get_thread(tid);
312 if (scheduler->is_sleep_set(thr) && thr->get_pending()) {
313 thr->get_pending()->set_sleep_flag();
319 * @brief Should the current action wake up a given thread?
321 * @param curr The current action
322 * @param thread The thread that we might wake up
323 * @return True, if we should wake up the sleeping thread; false otherwise
325 bool ModelChecker::should_wake_up(const ModelAction *curr, const Thread *thread) const
327 const ModelAction *asleep = thread->get_pending();
328 /* Don't allow partial RMW to wake anyone up */
331 /* Synchronizing actions may have been backtracked */
332 if (asleep->could_synchronize_with(curr))
334 /* All acquire/release fences and fence-acquire/store-release */
335 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
337 /* Fence-release + store can awake load-acquire on the same location */
338 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
339 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
340 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
346 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
348 for (unsigned int i = 0; i < get_num_threads(); i++) {
349 Thread *thr = get_thread(int_to_id(i));
350 if (scheduler->is_sleep_set(thr)) {
351 if (should_wake_up(curr, thr))
352 /* Remove this thread from sleep set */
353 scheduler->remove_sleep(thr);
358 /** @brief Alert the model-checker that an incorrectly-ordered
359 * synchronization was made */
360 void ModelChecker::set_bad_synchronization()
362 priv->bad_synchronization = true;
366 * Check whether the current trace has triggered an assertion which should halt
369 * @return True, if the execution should be aborted; false otherwise
371 bool ModelChecker::has_asserted() const
373 return priv->asserted;
377 * Trigger a trace assertion which should cause this execution to be halted.
378 * This can be due to a detected bug or due to an infeasibility that should
381 void ModelChecker::set_assert()
383 priv->asserted = true;
387 * Check if we are in a deadlock. Should only be called at the end of an
388 * execution, although it should not give false positives in the middle of an
389 * execution (there should be some ENABLED thread).
391 * @return True if program is in a deadlock; false otherwise
393 bool ModelChecker::is_deadlocked() const
395 bool blocking_threads = false;
396 for (unsigned int i = 0; i < get_num_threads(); i++) {
397 thread_id_t tid = int_to_id(i);
400 Thread *t = get_thread(tid);
401 if (!t->is_model_thread() && t->get_pending())
402 blocking_threads = true;
404 return blocking_threads;
408 * Check if this is a complete execution. That is, have all thread completed
409 * execution (rather than exiting because sleep sets have forced a redundant
412 * @return True if the execution is complete.
414 bool ModelChecker::is_complete_execution() const
416 for (unsigned int i = 0; i < get_num_threads(); i++)
417 if (is_enabled(int_to_id(i)))
423 * @brief Assert a bug in the executing program.
425 * Use this function to assert any sort of bug in the user program. If the
426 * current trace is feasible (actually, a prefix of some feasible execution),
427 * then this execution will be aborted, printing the appropriate message. If
428 * the current trace is not yet feasible, the error message will be stashed and
429 * printed if the execution ever becomes feasible.
431 * @param msg Descriptive message for the bug (do not include newline char)
432 * @return True if bug is immediately-feasible
434 bool ModelChecker::assert_bug(const char *msg)
436 priv->bugs.push_back(new bug_message(msg));
438 if (isfeasibleprefix()) {
446 * @brief Assert a bug in the executing program, asserted by a user thread
447 * @see ModelChecker::assert_bug
448 * @param msg Descriptive message for the bug (do not include newline char)
450 void ModelChecker::assert_user_bug(const char *msg)
452 /* If feasible bug, bail out now */
454 switch_to_master(NULL);
457 /** @return True, if any bugs have been reported for this execution */
458 bool ModelChecker::have_bug_reports() const
460 return priv->bugs.size() != 0;
463 /** @brief Print bug report listing for this execution (if any bugs exist) */
464 void ModelChecker::print_bugs() const
466 if (have_bug_reports()) {
467 model_print("Bug report: %zu bug%s detected\n",
469 priv->bugs.size() > 1 ? "s" : "");
470 for (unsigned int i = 0; i < priv->bugs.size(); i++)
471 priv->bugs[i]->print();
476 * @brief Record end-of-execution stats
478 * Must be run when exiting an execution. Records various stats.
479 * @see struct execution_stats
481 void ModelChecker::record_stats()
484 if (!isfeasibleprefix())
485 stats.num_infeasible++;
486 else if (have_bug_reports())
487 stats.num_buggy_executions++;
488 else if (is_complete_execution())
489 stats.num_complete++;
491 stats.num_redundant++;
494 /** @brief Print execution stats */
495 void ModelChecker::print_stats() const
497 model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
498 model_print("Number of redundant executions: %d\n", stats.num_redundant);
499 model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
500 model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
501 model_print("Total executions: %d\n", stats.num_total);
502 model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
506 * @brief End-of-exeuction print
507 * @param printbugs Should any existing bugs be printed?
509 void ModelChecker::print_execution(bool printbugs) const
511 print_program_output();
513 if (DBG_ENABLED() || params.verbose) {
514 model_print("Earliest divergence point since last feasible execution:\n");
515 if (earliest_diverge)
516 earliest_diverge->print();
518 model_print("(Not set)\n");
524 /* Don't print invalid bugs */
533 * Queries the model-checker for more executions to explore and, if one
534 * exists, resets the model-checker state to execute a new execution.
536 * @return If there are more executions to explore, return true. Otherwise,
539 bool ModelChecker::next_execution()
542 /* Is this execution a feasible execution that's worth bug-checking? */
543 bool complete = isfeasibleprefix() && (is_complete_execution() ||
546 /* End-of-execution bug checks */
549 assert_bug("Deadlock detected");
557 if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
558 print_execution(complete);
560 clear_program_output();
563 earliest_diverge = NULL;
565 if ((diverge = get_next_backtrack()) == NULL)
569 model_print("Next execution will diverge at:\n");
573 reset_to_initial_state();
578 * @brief Find the last fence-related backtracking conflict for a ModelAction
580 * This function performs the search for the most recent conflicting action
581 * against which we should perform backtracking, as affected by fence
582 * operations. This includes pairs of potentially-synchronizing actions which
583 * occur due to fence-acquire or fence-release, and hence should be explored in
584 * the opposite execution order.
586 * @param act The current action
587 * @return The most recent action which conflicts with act due to fences
589 ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
591 /* Only perform release/acquire fence backtracking for stores */
592 if (!act->is_write())
595 /* Find a fence-release (or, act is a release) */
596 ModelAction *last_release;
597 if (act->is_release())
600 last_release = get_last_fence_release(act->get_tid());
604 /* Skip past the release */
605 action_list_t *list = action_trace;
606 action_list_t::reverse_iterator rit;
607 for (rit = list->rbegin(); rit != list->rend(); rit++)
608 if (*rit == last_release)
610 ASSERT(rit != list->rend());
615 * load --sb-> fence-acquire */
616 std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
617 std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
618 bool found_acquire_fences = false;
619 for ( ; rit != list->rend(); rit++) {
620 ModelAction *prev = *rit;
621 if (act->same_thread(prev))
624 int tid = id_to_int(prev->get_tid());
626 if (prev->is_read() && act->same_var(prev)) {
627 if (prev->is_acquire()) {
628 /* Found most recent load-acquire, don't need
629 * to search for more fences */
630 if (!found_acquire_fences)
633 prior_loads[tid] = prev;
636 if (prev->is_acquire() && prev->is_fence() && !acquire_fences[tid]) {
637 found_acquire_fences = true;
638 acquire_fences[tid] = prev;
642 ModelAction *latest_backtrack = NULL;
643 for (unsigned int i = 0; i < acquire_fences.size(); i++)
644 if (acquire_fences[i] && prior_loads[i])
645 if (!latest_backtrack || *latest_backtrack < *acquire_fences[i])
646 latest_backtrack = acquire_fences[i];
647 return latest_backtrack;
651 * @brief Find the last backtracking conflict for a ModelAction
653 * This function performs the search for the most recent conflicting action
654 * against which we should perform backtracking. This primary includes pairs of
655 * synchronizing actions which should be explored in the opposite execution
658 * @param act The current action
659 * @return The most recent action which conflicts with act
661 ModelAction * ModelChecker::get_last_conflict(ModelAction *act) const
663 switch (act->get_type()) {
664 /* case ATOMIC_FENCE: fences don't directly cause backtracking */
668 ModelAction *ret = NULL;
670 /* linear search: from most recent to oldest */
671 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
672 action_list_t::reverse_iterator rit;
673 for (rit = list->rbegin(); rit != list->rend(); rit++) {
674 ModelAction *prev = *rit;
675 if (prev->could_synchronize_with(act)) {
681 ModelAction *ret2 = get_last_fence_conflict(act);
691 case ATOMIC_TRYLOCK: {
692 /* linear search: from most recent to oldest */
693 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
694 action_list_t::reverse_iterator rit;
695 for (rit = list->rbegin(); rit != list->rend(); rit++) {
696 ModelAction *prev = *rit;
697 if (act->is_conflicting_lock(prev))
702 case ATOMIC_UNLOCK: {
703 /* linear search: from most recent to oldest */
704 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
705 action_list_t::reverse_iterator rit;
706 for (rit = list->rbegin(); rit != list->rend(); rit++) {
707 ModelAction *prev = *rit;
708 if (!act->same_thread(prev) && prev->is_failed_trylock())
714 /* linear search: from most recent to oldest */
715 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
716 action_list_t::reverse_iterator rit;
717 for (rit = list->rbegin(); rit != list->rend(); rit++) {
718 ModelAction *prev = *rit;
719 if (!act->same_thread(prev) && prev->is_failed_trylock())
721 if (!act->same_thread(prev) && prev->is_notify())
727 case ATOMIC_NOTIFY_ALL:
728 case ATOMIC_NOTIFY_ONE: {
729 /* linear search: from most recent to oldest */
730 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
731 action_list_t::reverse_iterator rit;
732 for (rit = list->rbegin(); rit != list->rend(); rit++) {
733 ModelAction *prev = *rit;
734 if (!act->same_thread(prev) && prev->is_wait())
745 /** This method finds backtracking points where we should try to
746 * reorder the parameter ModelAction against.
748 * @param the ModelAction to find backtracking points for.
750 void ModelChecker::set_backtracking(ModelAction *act)
752 Thread *t = get_thread(act);
753 ModelAction *prev = get_last_conflict(act);
757 Node *node = prev->get_node()->get_parent();
759 int low_tid, high_tid;
760 if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
761 low_tid = id_to_int(act->get_tid());
762 high_tid = low_tid + 1;
765 high_tid = get_num_threads();
768 for (int i = low_tid; i < high_tid; i++) {
769 thread_id_t tid = int_to_id(i);
771 /* Make sure this thread can be enabled here. */
772 if (i >= node->get_num_threads())
775 /* Don't backtrack into a point where the thread is disabled or sleeping. */
776 if (node->enabled_status(tid) != THREAD_ENABLED)
779 /* Check if this has been explored already */
780 if (node->has_been_explored(tid))
783 /* See if fairness allows */
784 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
786 for (int t = 0; t < node->get_num_threads(); t++) {
787 thread_id_t tother = int_to_id(t);
788 if (node->is_enabled(tother) && node->has_priority(tother)) {
796 /* Cache the latest backtracking point */
797 set_latest_backtrack(prev);
799 /* If this is a new backtracking point, mark the tree */
800 if (!node->set_backtrack(tid))
802 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
803 id_to_int(prev->get_tid()),
804 id_to_int(t->get_id()));
813 * @brief Cache the a backtracking point as the "most recent", if eligible
815 * Note that this does not prepare the NodeStack for this backtracking
816 * operation, it only caches the action on a per-execution basis
818 * @param act The operation at which we should explore a different next action
819 * (i.e., backtracking point)
820 * @return True, if this action is now the most recent backtracking point;
823 bool ModelChecker::set_latest_backtrack(ModelAction *act)
825 if (!priv->next_backtrack || *act > *priv->next_backtrack) {
826 priv->next_backtrack = act;
833 * Returns last backtracking point. The model checker will explore a different
834 * path for this point in the next execution.
835 * @return The ModelAction at which the next execution should diverge.
837 ModelAction * ModelChecker::get_next_backtrack()
839 ModelAction *next = priv->next_backtrack;
840 priv->next_backtrack = NULL;
845 * Processes a read model action.
846 * @param curr is the read model action to process.
847 * @return True if processing this read updates the mo_graph.
849 bool ModelChecker::process_read(ModelAction *curr)
851 uint64_t value = VALUE_NONE;
852 bool updated = false;
854 const ModelAction *reads_from = curr->get_node()->get_read_from();
855 if (reads_from != NULL) {
856 mo_graph->startChanges();
858 value = reads_from->get_value();
860 check_recency(curr, reads_from);
861 bool r_status = r_modification_order(curr, reads_from);
863 if (is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
864 mo_graph->rollbackChanges();
865 priv->too_many_reads = false;
869 read_from(curr, reads_from);
870 mo_graph->commitChanges();
871 mo_check_promises(curr, true);
875 /* Read from future value */
876 struct future_value fv = curr->get_node()->get_future_value();
877 Promise *promise = new Promise(curr, fv);
879 curr->set_read_from_promise(promise);
880 promises->push_back(promise);
881 mo_graph->startChanges();
882 updated = r_modification_order(curr, promise);
883 mo_graph->commitChanges();
885 get_thread(curr)->set_return_value(value);
891 * Processes a lock, trylock, or unlock model action. @param curr is
892 * the read model action to process.
894 * The try lock operation checks whether the lock is taken. If not,
895 * it falls to the normal lock operation case. If so, it returns
898 * The lock operation has already been checked that it is enabled, so
899 * it just grabs the lock and synchronizes with the previous unlock.
901 * The unlock operation has to re-enable all of the threads that are
902 * waiting on the lock.
904 * @return True if synchronization was updated; false otherwise
906 bool ModelChecker::process_mutex(ModelAction *curr)
908 std::mutex *mutex = NULL;
909 struct std::mutex_state *state = NULL;
911 if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
912 mutex = (std::mutex *)curr->get_location();
913 state = mutex->get_state();
914 } else if (curr->is_wait()) {
915 mutex = (std::mutex *)curr->get_value();
916 state = mutex->get_state();
919 switch (curr->get_type()) {
920 case ATOMIC_TRYLOCK: {
921 bool success = !state->islocked;
922 curr->set_try_lock(success);
924 get_thread(curr)->set_return_value(0);
927 get_thread(curr)->set_return_value(1);
929 //otherwise fall into the lock case
931 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
932 assert_bug("Lock access before initialization");
933 state->islocked = true;
934 ModelAction *unlock = get_last_unlock(curr);
935 //synchronize with the previous unlock statement
936 if (unlock != NULL) {
937 curr->synchronize_with(unlock);
942 case ATOMIC_UNLOCK: {
944 state->islocked = false;
945 //wake up the other threads
946 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
947 //activate all the waiting threads
948 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
949 scheduler->wake(get_thread(*rit));
956 state->islocked = false;
957 //wake up the other threads
958 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
959 //activate all the waiting threads
960 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
961 scheduler->wake(get_thread(*rit));
964 //check whether we should go to sleep or not...simulate spurious failures
965 if (curr->get_node()->get_misc() == 0) {
966 get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
968 scheduler->sleep(get_thread(curr));
972 case ATOMIC_NOTIFY_ALL: {
973 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
974 //activate all the waiting threads
975 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
976 scheduler->wake(get_thread(*rit));
981 case ATOMIC_NOTIFY_ONE: {
982 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
983 int wakeupthread = curr->get_node()->get_misc();
984 action_list_t::iterator it = waiters->begin();
985 advance(it, wakeupthread);
986 scheduler->wake(get_thread(*it));
997 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
999 /* Do more ambitious checks now that mo is more complete */
1000 if (mo_may_allow(writer, reader)) {
1001 Node *node = reader->get_node();
1003 /* Find an ancestor thread which exists at the time of the reader */
1004 Thread *write_thread = get_thread(writer);
1005 while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
1006 write_thread = write_thread->get_parent();
1008 struct future_value fv = {
1009 writer->get_value(),
1010 writer->get_seq_number() + params.maxfuturedelay,
1011 write_thread->get_id(),
1013 if (node->add_future_value(fv))
1014 set_latest_backtrack(reader);
1019 * Process a write ModelAction
1020 * @param curr The ModelAction to process
1021 * @return True if the mo_graph was updated or promises were resolved
1023 bool ModelChecker::process_write(ModelAction *curr)
1025 bool updated_mod_order = w_modification_order(curr);
1026 bool updated_promises = resolve_promises(curr);
1028 if (promises->size() == 0) {
1029 for (unsigned int i = 0; i < futurevalues->size(); i++) {
1030 struct PendingFutureValue pfv = (*futurevalues)[i];
1031 add_future_value(pfv.writer, pfv.act);
1033 futurevalues->clear();
1036 mo_graph->commitChanges();
1037 mo_check_promises(curr, false);
1039 get_thread(curr)->set_return_value(VALUE_NONE);
1040 return updated_mod_order || updated_promises;
1044 * Process a fence ModelAction
1045 * @param curr The ModelAction to process
1046 * @return True if synchronization was updated
1048 bool ModelChecker::process_fence(ModelAction *curr)
1051 * fence-relaxed: no-op
1052 * fence-release: only log the occurence (not in this function), for
1053 * use in later synchronization
1054 * fence-acquire (this function): search for hypothetical release
1057 bool updated = false;
1058 if (curr->is_acquire()) {
1059 action_list_t *list = action_trace;
1060 action_list_t::reverse_iterator rit;
1061 /* Find X : is_read(X) && X --sb-> curr */
1062 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1063 ModelAction *act = *rit;
1066 if (act->get_tid() != curr->get_tid())
1068 /* Stop at the beginning of the thread */
1069 if (act->is_thread_start())
1071 /* Stop once we reach a prior fence-acquire */
1072 if (act->is_fence() && act->is_acquire())
1074 if (!act->is_read())
1076 /* read-acquire will find its own release sequences */
1077 if (act->is_acquire())
1080 /* Establish hypothetical release sequences */
1081 rel_heads_list_t release_heads;
1082 get_release_seq_heads(curr, act, &release_heads);
1083 for (unsigned int i = 0; i < release_heads.size(); i++)
1084 if (!curr->synchronize_with(release_heads[i]))
1085 set_bad_synchronization();
1086 if (release_heads.size() != 0)
1094 * @brief Process the current action for thread-related activity
1096 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
1097 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
1098 * synchronization, etc. This function is a no-op for non-THREAD actions
1099 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
1101 * @param curr The current action
1102 * @return True if synchronization was updated or a thread completed
1104 bool ModelChecker::process_thread_action(ModelAction *curr)
1106 bool updated = false;
1108 switch (curr->get_type()) {
1109 case THREAD_CREATE: {
1110 thrd_t *thrd = (thrd_t *)curr->get_location();
1111 struct thread_params *params = (struct thread_params *)curr->get_value();
1112 Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr));
1114 th->set_creation(curr);
1115 /* Promises can be satisfied by children */
1116 for (unsigned int i = 0; i < promises->size(); i++) {
1117 Promise *promise = (*promises)[i];
1118 if (promise->thread_is_available(curr->get_tid()))
1119 promise->add_thread(th->get_id());
1124 Thread *blocking = curr->get_thread_operand();
1125 ModelAction *act = get_last_action(blocking->get_id());
1126 curr->synchronize_with(act);
1127 updated = true; /* trigger rel-seq checks */
1130 case THREAD_FINISH: {
1131 Thread *th = get_thread(curr);
1132 while (!th->wait_list_empty()) {
1133 ModelAction *act = th->pop_wait_list();
1134 scheduler->wake(get_thread(act));
1137 /* Completed thread can't satisfy promises */
1138 for (unsigned int i = 0; i < promises->size(); i++) {
1139 Promise *promise = (*promises)[i];
1140 if (promise->thread_is_available(th->get_id()))
1141 if (promise->eliminate_thread(th->get_id()))
1142 priv->failed_promise = true;
1144 updated = true; /* trigger rel-seq checks */
1147 case THREAD_START: {
1148 check_promises(curr->get_tid(), NULL, curr->get_cv());
1159 * @brief Process the current action for release sequence fixup activity
1161 * Performs model-checker release sequence fixups for the current action,
1162 * forcing a single pending release sequence to break (with a given, potential
1163 * "loose" write) or to complete (i.e., synchronize). If a pending release
1164 * sequence forms a complete release sequence, then we must perform the fixup
1165 * synchronization, mo_graph additions, etc.
1167 * @param curr The current action; must be a release sequence fixup action
1168 * @param work_queue The work queue to which to add work items as they are
1171 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
1173 const ModelAction *write = curr->get_node()->get_relseq_break();
1174 struct release_seq *sequence = pending_rel_seqs->back();
1175 pending_rel_seqs->pop_back();
1177 ModelAction *acquire = sequence->acquire;
1178 const ModelAction *rf = sequence->rf;
1179 const ModelAction *release = sequence->release;
1183 ASSERT(release->same_thread(rf));
1185 if (write == NULL) {
1187 * @todo Forcing a synchronization requires that we set
1188 * modification order constraints. For instance, we can't allow
1189 * a fixup sequence in which two separate read-acquire
1190 * operations read from the same sequence, where the first one
1191 * synchronizes and the other doesn't. Essentially, we can't
1192 * allow any writes to insert themselves between 'release' and
1196 /* Must synchronize */
1197 if (!acquire->synchronize_with(release)) {
1198 set_bad_synchronization();
1201 /* Re-check all pending release sequences */
1202 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1203 /* Re-check act for mo_graph edges */
1204 work_queue->push_back(MOEdgeWorkEntry(acquire));
1206 /* propagate synchronization to later actions */
1207 action_list_t::reverse_iterator rit = action_trace->rbegin();
1208 for (; (*rit) != acquire; rit++) {
1209 ModelAction *propagate = *rit;
1210 if (acquire->happens_before(propagate)) {
1211 propagate->synchronize_with(acquire);
1212 /* Re-check 'propagate' for mo_graph edges */
1213 work_queue->push_back(MOEdgeWorkEntry(propagate));
1217 /* Break release sequence with new edges:
1218 * release --mo--> write --mo--> rf */
1219 mo_graph->addEdge(release, write);
1220 mo_graph->addEdge(write, rf);
1223 /* See if we have realized a data race */
1228 * Initialize the current action by performing one or more of the following
1229 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
1230 * in the NodeStack, manipulating backtracking sets, allocating and
1231 * initializing clock vectors, and computing the promises to fulfill.
1233 * @param curr The current action, as passed from the user context; may be
1234 * freed/invalidated after the execution of this function, with a different
1235 * action "returned" its place (pass-by-reference)
1236 * @return True if curr is a newly-explored action; false otherwise
1238 bool ModelChecker::initialize_curr_action(ModelAction **curr)
1240 ModelAction *newcurr;
1242 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
1243 newcurr = process_rmw(*curr);
1246 if (newcurr->is_rmw())
1247 compute_promises(newcurr);
1253 (*curr)->set_seq_number(get_next_seq_num());
1255 newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
1257 /* First restore type and order in case of RMW operation */
1258 if ((*curr)->is_rmwr())
1259 newcurr->copy_typeandorder(*curr);
1261 ASSERT((*curr)->get_location() == newcurr->get_location());
1262 newcurr->copy_from_new(*curr);
1264 /* Discard duplicate ModelAction; use action from NodeStack */
1267 /* Always compute new clock vector */
1268 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1271 return false; /* Action was explored previously */
1275 /* Always compute new clock vector */
1276 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1278 /* Assign most recent release fence */
1279 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
1282 * Perform one-time actions when pushing new ModelAction onto
1285 if (newcurr->is_write())
1286 compute_promises(newcurr);
1287 else if (newcurr->is_relseq_fixup())
1288 compute_relseq_breakwrites(newcurr);
1289 else if (newcurr->is_wait())
1290 newcurr->get_node()->set_misc_max(2);
1291 else if (newcurr->is_notify_one()) {
1292 newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
1294 return true; /* This was a new ModelAction */
1299 * @brief Establish reads-from relation between two actions
1301 * Perform basic operations involved with establishing a concrete rf relation,
1302 * including setting the ModelAction data and checking for release sequences.
1304 * @param act The action that is reading (must be a read)
1305 * @param rf The action from which we are reading (must be a write)
1307 * @return True if this read established synchronization
1309 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
1311 act->set_read_from(rf);
1312 if (rf != NULL && act->is_acquire()) {
1313 rel_heads_list_t release_heads;
1314 get_release_seq_heads(act, act, &release_heads);
1315 int num_heads = release_heads.size();
1316 for (unsigned int i = 0; i < release_heads.size(); i++)
1317 if (!act->synchronize_with(release_heads[i])) {
1318 set_bad_synchronization();
1321 return num_heads > 0;
1327 * Check promises and eliminate potentially-satisfying threads when a thread is
1328 * blocked (e.g., join, lock). A thread which is waiting on another thread can
1329 * no longer satisfy a promise generated from that thread.
1331 * @param blocker The thread on which a thread is waiting
1332 * @param waiting The waiting thread
1334 void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
1336 for (unsigned int i = 0; i < promises->size(); i++) {
1337 Promise *promise = (*promises)[i];
1338 ModelAction *reader = promise->get_action();
1339 if (reader->get_tid() != blocker->get_id())
1341 if (!promise->thread_is_available(waiting->get_id()))
1343 if (promise->eliminate_thread(waiting->get_id())) {
1344 /* Promise has failed */
1345 priv->failed_promise = true;
1351 * @brief Check whether a model action is enabled.
1353 * Checks whether a lock or join operation would be successful (i.e., is the
1354 * lock already locked, or is the joined thread already complete). If not, put
1355 * the action in a waiter list.
1357 * @param curr is the ModelAction to check whether it is enabled.
1358 * @return a bool that indicates whether the action is enabled.
1360 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1361 if (curr->is_lock()) {
1362 std::mutex *lock = (std::mutex *)curr->get_location();
1363 struct std::mutex_state *state = lock->get_state();
1364 if (state->islocked) {
1365 //Stick the action in the appropriate waiting queue
1366 get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1369 } else if (curr->get_type() == THREAD_JOIN) {
1370 Thread *blocking = (Thread *)curr->get_location();
1371 if (!blocking->is_complete()) {
1372 blocking->push_wait_list(curr);
1373 thread_blocking_check_promises(blocking, get_thread(curr));
1382 * This is the heart of the model checker routine. It performs model-checking
1383 * actions corresponding to a given "current action." Among other processes, it
1384 * calculates reads-from relationships, updates synchronization clock vectors,
1385 * forms a memory_order constraints graph, and handles replay/backtrack
1386 * execution when running permutations of previously-observed executions.
1388 * @param curr The current action to process
1389 * @return The ModelAction that is actually executed; may be different than
1390 * curr; may be NULL, if the current action is not enabled to run
1392 ModelAction * ModelChecker::check_current_action(ModelAction *curr)
1395 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1397 if (!check_action_enabled(curr)) {
1398 /* Make the execution look like we chose to run this action
1399 * much later, when a lock/join can succeed */
1400 get_thread(curr)->set_pending(curr);
1401 scheduler->sleep(get_thread(curr));
1405 bool newly_explored = initialize_curr_action(&curr);
1411 wake_up_sleeping_actions(curr);
1413 /* Add the action to lists before any other model-checking tasks */
1414 if (!second_part_of_rmw)
1415 add_action_to_lists(curr);
1417 /* Build may_read_from set for newly-created actions */
1418 if (newly_explored && curr->is_read())
1419 build_may_read_from(curr);
1421 /* Initialize work_queue with the "current action" work */
1422 work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1423 while (!work_queue.empty() && !has_asserted()) {
1424 WorkQueueEntry work = work_queue.front();
1425 work_queue.pop_front();
1427 switch (work.type) {
1428 case WORK_CHECK_CURR_ACTION: {
1429 ModelAction *act = work.action;
1430 bool update = false; /* update this location's release seq's */
1431 bool update_all = false; /* update all release seq's */
1433 if (process_thread_action(curr))
1436 if (act->is_read() && !second_part_of_rmw && process_read(act))
1439 if (act->is_write() && process_write(act))
1442 if (act->is_fence() && process_fence(act))
1445 if (act->is_mutex_op() && process_mutex(act))
1448 if (act->is_relseq_fixup())
1449 process_relseq_fixup(curr, &work_queue);
1452 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1454 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1457 case WORK_CHECK_RELEASE_SEQ:
1458 resolve_release_sequences(work.location, &work_queue);
1460 case WORK_CHECK_MO_EDGES: {
1461 /** @todo Complete verification of work_queue */
1462 ModelAction *act = work.action;
1463 bool updated = false;
1465 if (act->is_read()) {
1466 const ModelAction *rf = act->get_reads_from();
1467 const Promise *promise = act->get_reads_from_promise();
1469 if (r_modification_order(act, rf))
1471 } else if (promise) {
1472 if (r_modification_order(act, promise))
1476 if (act->is_write()) {
1477 if (w_modification_order(act))
1480 mo_graph->commitChanges();
1483 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1492 check_curr_backtracking(curr);
1493 set_backtracking(curr);
1497 void ModelChecker::check_curr_backtracking(ModelAction *curr)
1499 Node *currnode = curr->get_node();
1500 Node *parnode = currnode->get_parent();
1502 if ((parnode && !parnode->backtrack_empty()) ||
1503 !currnode->misc_empty() ||
1504 !currnode->read_from_empty() ||
1505 !currnode->future_value_empty() ||
1506 !currnode->promise_empty() ||
1507 !currnode->relseq_break_empty()) {
1508 set_latest_backtrack(curr);
1512 bool ModelChecker::promises_expired() const
1514 for (unsigned int i = 0; i < promises->size(); i++) {
1515 Promise *promise = (*promises)[i];
1516 if (promise->get_expiration() < priv->used_sequence_numbers)
1523 * This is the strongest feasibility check available.
1524 * @return whether the current trace (partial or complete) must be a prefix of
1527 bool ModelChecker::isfeasibleprefix() const
1529 return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
1533 * Print disagnostic information about an infeasible execution
1534 * @param prefix A string to prefix the output with; if NULL, then a default
1535 * message prefix will be provided
1537 void ModelChecker::print_infeasibility(const char *prefix) const
1541 if (mo_graph->checkForCycles())
1542 ptr += sprintf(ptr, "[mo cycle]");
1543 if (priv->failed_promise)
1544 ptr += sprintf(ptr, "[failed promise]");
1545 if (priv->too_many_reads)
1546 ptr += sprintf(ptr, "[too many reads]");
1547 if (priv->no_valid_reads)
1548 ptr += sprintf(ptr, "[no valid reads-from]");
1549 if (priv->bad_synchronization)
1550 ptr += sprintf(ptr, "[bad sw ordering]");
1551 if (promises_expired())
1552 ptr += sprintf(ptr, "[promise expired]");
1553 if (promises->size() != 0)
1554 ptr += sprintf(ptr, "[unresolved promise]");
1556 model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
1560 * Returns whether the current completed trace is feasible, except for pending
1561 * release sequences.
1563 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
1565 return !is_infeasible() && promises->size() == 0;
1569 * Check if the current partial trace is infeasible. Does not check any
1570 * end-of-execution flags, which might rule out the execution. Thus, this is
1571 * useful only for ruling an execution as infeasible.
1572 * @return whether the current partial trace is infeasible.
1574 bool ModelChecker::is_infeasible() const
1576 return mo_graph->checkForCycles() ||
1577 priv->no_valid_reads ||
1578 priv->failed_promise ||
1579 priv->too_many_reads ||
1580 priv->bad_synchronization ||
1584 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1585 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1586 ModelAction *lastread = get_last_action(act->get_tid());
1587 lastread->process_rmw(act);
1588 if (act->is_rmw()) {
1589 if (lastread->get_reads_from())
1590 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1592 mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread);
1593 mo_graph->commitChanges();
1599 * Checks whether a thread has read from the same write for too many times
1600 * without seeing the effects of a later write.
1603 * 1) there must a different write that we could read from that would satisfy the modification order,
1604 * 2) we must have read from the same value in excess of maxreads times, and
1605 * 3) that other write must have been in the reads_from set for maxreads times.
1607 * If so, we decide that the execution is no longer feasible.
1609 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
1611 if (params.maxreads != 0) {
1612 if (curr->get_node()->get_read_from_size() <= 1)
1614 //Must make sure that execution is currently feasible... We could
1615 //accidentally clear by rolling back
1616 if (is_infeasible())
1618 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1619 int tid = id_to_int(curr->get_tid());
1622 if ((int)thrd_lists->size() <= tid)
1624 action_list_t *list = &(*thrd_lists)[tid];
1626 action_list_t::reverse_iterator rit = list->rbegin();
1627 /* Skip past curr */
1628 for (; (*rit) != curr; rit++)
1630 /* go past curr now */
1633 action_list_t::reverse_iterator ritcopy = rit;
1634 //See if we have enough reads from the same value
1636 for (; count < params.maxreads; rit++, count++) {
1637 if (rit == list->rend())
1639 ModelAction *act = *rit;
1640 if (!act->is_read())
1643 if (act->get_reads_from() != rf)
1645 if (act->get_node()->get_read_from_size() <= 1)
1648 for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
1650 const ModelAction *write = curr->get_node()->get_read_from_at(i);
1652 /* Need a different write */
1656 /* Test to see whether this is a feasible write to read from */
1657 /** NOTE: all members of read-from set should be
1658 * feasible, so we no longer check it here **/
1662 bool feasiblewrite = true;
1663 //new we need to see if this write works for everyone
1665 for (int loop = count; loop > 0; loop--, rit++) {
1666 ModelAction *act = *rit;
1667 bool foundvalue = false;
1668 for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
1669 if (act->get_node()->get_read_from_at(j) == write) {
1675 feasiblewrite = false;
1679 if (feasiblewrite) {
1680 priv->too_many_reads = true;
1688 * Updates the mo_graph with the constraints imposed from the current
1691 * Basic idea is the following: Go through each other thread and find
1692 * the last action that happened before our read. Two cases:
1694 * (1) The action is a write => that write must either occur before
1695 * the write we read from or be the write we read from.
1697 * (2) The action is a read => the write that that action read from
1698 * must occur before the write we read from or be the same write.
1700 * @param curr The current action. Must be a read.
1701 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
1702 * @return True if modification order edges were added; false otherwise
1704 template <typename rf_type>
1705 bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
1707 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1710 ASSERT(curr->is_read());
1712 /* Last SC fence in the current thread */
1713 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1715 /* Iterate over all threads */
1716 for (i = 0; i < thrd_lists->size(); i++) {
1717 /* Last SC fence in thread i */
1718 ModelAction *last_sc_fence_thread_local = NULL;
1719 if (int_to_id((int)i) != curr->get_tid())
1720 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
1722 /* Last SC fence in thread i, before last SC fence in current thread */
1723 ModelAction *last_sc_fence_thread_before = NULL;
1724 if (last_sc_fence_local)
1725 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1727 /* Iterate over actions in thread, starting from most recent */
1728 action_list_t *list = &(*thrd_lists)[i];
1729 action_list_t::reverse_iterator rit;
1730 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1731 ModelAction *act = *rit;
1733 if (act->is_write() && !act->equals(rf) && act != curr) {
1734 /* C++, Section 29.3 statement 5 */
1735 if (curr->is_seqcst() && last_sc_fence_thread_local &&
1736 *act < *last_sc_fence_thread_local) {
1737 added = mo_graph->addEdge(act, rf) || added;
1740 /* C++, Section 29.3 statement 4 */
1741 else if (act->is_seqcst() && last_sc_fence_local &&
1742 *act < *last_sc_fence_local) {
1743 added = mo_graph->addEdge(act, rf) || added;
1746 /* C++, Section 29.3 statement 6 */
1747 else if (last_sc_fence_thread_before &&
1748 *act < *last_sc_fence_thread_before) {
1749 added = mo_graph->addEdge(act, rf) || added;
1755 * Include at most one act per-thread that "happens
1756 * before" curr. Don't consider reflexively.
1758 if (act->happens_before(curr) && act != curr) {
1759 if (act->is_write()) {
1760 if (!act->equals(rf)) {
1761 added = mo_graph->addEdge(act, rf) || added;
1764 const ModelAction *prevrf = act->get_reads_from();
1765 const Promise *prevrf_promise = act->get_reads_from_promise();
1767 if (!prevrf->equals(rf))
1768 added = mo_graph->addEdge(prevrf, rf) || added;
1769 } else if (!prevrf_promise->equals(rf)) {
1770 added = mo_graph->addEdge(prevrf_promise, rf) || added;
1779 * All compatible, thread-exclusive promises must be ordered after any
1780 * concrete loads from the same thread
1782 for (unsigned int i = 0; i < promises->size(); i++)
1783 if ((*promises)[i]->is_compatible_exclusive(curr))
1784 added = mo_graph->addEdge(rf, (*promises)[i]) || added;
1790 * Updates the mo_graph with the constraints imposed from the current write.
1792 * Basic idea is the following: Go through each other thread and find
1793 * the lastest action that happened before our write. Two cases:
1795 * (1) The action is a write => that write must occur before
1798 * (2) The action is a read => the write that that action read from
1799 * must occur before the current write.
1801 * This method also handles two other issues:
1803 * (I) Sequential Consistency: Making sure that if the current write is
1804 * seq_cst, that it occurs after the previous seq_cst write.
1806 * (II) Sending the write back to non-synchronizing reads.
1808 * @param curr The current action. Must be a write.
1809 * @return True if modification order edges were added; false otherwise
1811 bool ModelChecker::w_modification_order(ModelAction *curr)
1813 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1816 ASSERT(curr->is_write());
1818 if (curr->is_seqcst()) {
1819 /* We have to at least see the last sequentially consistent write,
1820 so we are initialized. */
1821 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
1822 if (last_seq_cst != NULL) {
1823 added = mo_graph->addEdge(last_seq_cst, curr) || added;
1827 /* Last SC fence in the current thread */
1828 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1830 /* Iterate over all threads */
1831 for (i = 0; i < thrd_lists->size(); i++) {
1832 /* Last SC fence in thread i, before last SC fence in current thread */
1833 ModelAction *last_sc_fence_thread_before = NULL;
1834 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
1835 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1837 /* Iterate over actions in thread, starting from most recent */
1838 action_list_t *list = &(*thrd_lists)[i];
1839 action_list_t::reverse_iterator rit;
1840 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1841 ModelAction *act = *rit;
1844 * 1) If RMW and it actually read from something, then we
1845 * already have all relevant edges, so just skip to next
1848 * 2) If RMW and it didn't read from anything, we should
1849 * whatever edge we can get to speed up convergence.
1851 * 3) If normal write, we need to look at earlier actions, so
1852 * continue processing list.
1854 if (curr->is_rmw()) {
1855 if (curr->get_reads_from() != NULL)
1863 /* C++, Section 29.3 statement 7 */
1864 if (last_sc_fence_thread_before && act->is_write() &&
1865 *act < *last_sc_fence_thread_before) {
1866 added = mo_graph->addEdge(act, curr) || added;
1871 * Include at most one act per-thread that "happens
1874 if (act->happens_before(curr)) {
1876 * Note: if act is RMW, just add edge:
1878 * The following edge should be handled elsewhere:
1879 * readfrom(act) --mo--> act
1881 if (act->is_write())
1882 added = mo_graph->addEdge(act, curr) || added;
1883 else if (act->is_read()) {
1884 //if previous read accessed a null, just keep going
1885 if (act->get_reads_from() == NULL)
1887 added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
1890 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1891 !act->same_thread(curr)) {
1892 /* We have an action that:
1893 (1) did not happen before us
1894 (2) is a read and we are a write
1895 (3) cannot synchronize with us
1896 (4) is in a different thread
1898 that read could potentially read from our write. Note that
1899 these checks are overly conservative at this point, we'll
1900 do more checks before actually removing the
1904 if (thin_air_constraint_may_allow(curr, act)) {
1905 if (!is_infeasible())
1906 futurevalues->push_back(PendingFutureValue(curr, act));
1907 else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
1908 add_future_value(curr, act);
1915 * All compatible, thread-exclusive promises must be ordered after any
1916 * concrete stores to the same thread, or else they can be merged with
1919 for (unsigned int i = 0; i < promises->size(); i++)
1920 if ((*promises)[i]->is_compatible_exclusive(curr))
1921 added = mo_graph->addEdge(curr, (*promises)[i]) || added;
1926 /** Arbitrary reads from the future are not allowed. Section 29.3
1927 * part 9 places some constraints. This method checks one result of constraint
1928 * constraint. Others require compiler support. */
1929 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
1931 if (!writer->is_rmw())
1934 if (!reader->is_rmw())
1937 for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1938 if (search == reader)
1940 if (search->get_tid() == reader->get_tid() &&
1941 search->happens_before(reader))
1949 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1950 * some constraints. This method checks one the following constraint (others
1951 * require compiler support):
1953 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1955 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1957 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1959 /* Iterate over all threads */
1960 for (i = 0; i < thrd_lists->size(); i++) {
1961 const ModelAction *write_after_read = NULL;
1963 /* Iterate over actions in thread, starting from most recent */
1964 action_list_t *list = &(*thrd_lists)[i];
1965 action_list_t::reverse_iterator rit;
1966 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1967 ModelAction *act = *rit;
1969 /* Don't disallow due to act == reader */
1970 if (!reader->happens_before(act) || reader == act)
1972 else if (act->is_write())
1973 write_after_read = act;
1974 else if (act->is_read() && act->get_reads_from() != NULL)
1975 write_after_read = act->get_reads_from();
1978 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1985 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1986 * The ModelAction under consideration is expected to be taking part in
1987 * release/acquire synchronization as an object of the "reads from" relation.
1988 * Note that this can only provide release sequence support for RMW chains
1989 * which do not read from the future, as those actions cannot be traced until
1990 * their "promise" is fulfilled. Similarly, we may not even establish the
1991 * presence of a release sequence with certainty, as some modification order
1992 * constraints may be decided further in the future. Thus, this function
1993 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1994 * and a boolean representing certainty.
1996 * @param rf The action that might be part of a release sequence. Must be a
1998 * @param release_heads A pass-by-reference style return parameter. After
1999 * execution of this function, release_heads will contain the heads of all the
2000 * relevant release sequences, if any exists with certainty
2001 * @param pending A pass-by-reference style return parameter which is only used
2002 * when returning false (i.e., uncertain). Returns most information regarding
2003 * an uncertain release sequence, including any write operations that might
2004 * break the sequence.
2005 * @return true, if the ModelChecker is certain that release_heads is complete;
2008 bool ModelChecker::release_seq_heads(const ModelAction *rf,
2009 rel_heads_list_t *release_heads,
2010 struct release_seq *pending) const
2012 /* Only check for release sequences if there are no cycles */
2013 if (mo_graph->checkForCycles())
2016 for ( ; rf != NULL; rf = rf->get_reads_from()) {
2017 ASSERT(rf->is_write());
2019 if (rf->is_release())
2020 release_heads->push_back(rf);
2021 else if (rf->get_last_fence_release())
2022 release_heads->push_back(rf->get_last_fence_release());
2024 break; /* End of RMW chain */
2026 /** @todo Need to be smarter here... In the linux lock
2027 * example, this will run to the beginning of the program for
2029 /** @todo The way to be smarter here is to keep going until 1
2030 * thread has a release preceded by an acquire and you've seen
2033 /* acq_rel RMW is a sufficient stopping condition */
2034 if (rf->is_acquire() && rf->is_release())
2035 return true; /* complete */
2038 /* read from future: need to settle this later */
2040 return false; /* incomplete */
2043 if (rf->is_release())
2044 return true; /* complete */
2046 /* else relaxed write
2047 * - check for fence-release in the same thread (29.8, stmt. 3)
2048 * - check modification order for contiguous subsequence
2049 * -> rf must be same thread as release */
2051 const ModelAction *fence_release = rf->get_last_fence_release();
2052 /* Synchronize with a fence-release unconditionally; we don't need to
2053 * find any more "contiguous subsequence..." for it */
2055 release_heads->push_back(fence_release);
2057 int tid = id_to_int(rf->get_tid());
2058 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
2059 action_list_t *list = &(*thrd_lists)[tid];
2060 action_list_t::const_reverse_iterator rit;
2062 /* Find rf in the thread list */
2063 rit = std::find(list->rbegin(), list->rend(), rf);
2064 ASSERT(rit != list->rend());
2066 /* Find the last {write,fence}-release */
2067 for (; rit != list->rend(); rit++) {
2068 if (fence_release && *(*rit) < *fence_release)
2070 if ((*rit)->is_release())
2073 if (rit == list->rend()) {
2074 /* No write-release in this thread */
2075 return true; /* complete */
2076 } else if (fence_release && *(*rit) < *fence_release) {
2077 /* The fence-release is more recent (and so, "stronger") than
2078 * the most recent write-release */
2079 return true; /* complete */
2080 } /* else, need to establish contiguous release sequence */
2081 ModelAction *release = *rit;
2083 ASSERT(rf->same_thread(release));
2085 pending->writes.clear();
2087 bool certain = true;
2088 for (unsigned int i = 0; i < thrd_lists->size(); i++) {
2089 if (id_to_int(rf->get_tid()) == (int)i)
2091 list = &(*thrd_lists)[i];
2093 /* Can we ensure no future writes from this thread may break
2094 * the release seq? */
2095 bool future_ordered = false;
2097 ModelAction *last = get_last_action(int_to_id(i));
2098 Thread *th = get_thread(int_to_id(i));
2099 if ((last && rf->happens_before(last)) ||
2102 future_ordered = true;
2104 ASSERT(!th->is_model_thread() || future_ordered);
2106 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2107 const ModelAction *act = *rit;
2108 /* Reach synchronization -> this thread is complete */
2109 if (act->happens_before(release))
2111 if (rf->happens_before(act)) {
2112 future_ordered = true;
2116 /* Only non-RMW writes can break release sequences */
2117 if (!act->is_write() || act->is_rmw())
2120 /* Check modification order */
2121 if (mo_graph->checkReachable(rf, act)) {
2122 /* rf --mo--> act */
2123 future_ordered = true;
2126 if (mo_graph->checkReachable(act, release))
2127 /* act --mo--> release */
2129 if (mo_graph->checkReachable(release, act) &&
2130 mo_graph->checkReachable(act, rf)) {
2131 /* release --mo-> act --mo--> rf */
2132 return true; /* complete */
2134 /* act may break release sequence */
2135 pending->writes.push_back(act);
2138 if (!future_ordered)
2139 certain = false; /* This thread is uncertain */
2143 release_heads->push_back(release);
2144 pending->writes.clear();
2146 pending->release = release;
2153 * An interface for getting the release sequence head(s) with which a
2154 * given ModelAction must synchronize. This function only returns a non-empty
2155 * result when it can locate a release sequence head with certainty. Otherwise,
2156 * it may mark the internal state of the ModelChecker so that it will handle
2157 * the release sequence at a later time, causing @a acquire to update its
2158 * synchronization at some later point in execution.
2160 * @param acquire The 'acquire' action that may synchronize with a release
2162 * @param read The read action that may read from a release sequence; this may
2163 * be the same as acquire, or else an earlier action in the same thread (i.e.,
2164 * when 'acquire' is a fence-acquire)
2165 * @param release_heads A pass-by-reference return parameter. Will be filled
2166 * with the head(s) of the release sequence(s), if they exists with certainty.
2167 * @see ModelChecker::release_seq_heads
2169 void ModelChecker::get_release_seq_heads(ModelAction *acquire,
2170 ModelAction *read, rel_heads_list_t *release_heads)
2172 const ModelAction *rf = read->get_reads_from();
2173 struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
2174 sequence->acquire = acquire;
2175 sequence->read = read;
2177 if (!release_seq_heads(rf, release_heads, sequence)) {
2178 /* add act to 'lazy checking' list */
2179 pending_rel_seqs->push_back(sequence);
2181 snapshot_free(sequence);
2186 * Attempt to resolve all stashed operations that might synchronize with a
2187 * release sequence for a given location. This implements the "lazy" portion of
2188 * determining whether or not a release sequence was contiguous, since not all
2189 * modification order information is present at the time an action occurs.
2191 * @param location The location/object that should be checked for release
2192 * sequence resolutions. A NULL value means to check all locations.
2193 * @param work_queue The work queue to which to add work items as they are
2195 * @return True if any updates occurred (new synchronization, new mo_graph
2198 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
2200 bool updated = false;
2201 std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
2202 while (it != pending_rel_seqs->end()) {
2203 struct release_seq *pending = *it;
2204 ModelAction *acquire = pending->acquire;
2205 const ModelAction *read = pending->read;
2207 /* Only resolve sequences on the given location, if provided */
2208 if (location && read->get_location() != location) {
2213 const ModelAction *rf = read->get_reads_from();
2214 rel_heads_list_t release_heads;
2216 complete = release_seq_heads(rf, &release_heads, pending);
2217 for (unsigned int i = 0; i < release_heads.size(); i++) {
2218 if (!acquire->has_synchronized_with(release_heads[i])) {
2219 if (acquire->synchronize_with(release_heads[i]))
2222 set_bad_synchronization();
2227 /* Re-check all pending release sequences */
2228 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
2229 /* Re-check read-acquire for mo_graph edges */
2230 if (acquire->is_read())
2231 work_queue->push_back(MOEdgeWorkEntry(acquire));
2233 /* propagate synchronization to later actions */
2234 action_list_t::reverse_iterator rit = action_trace->rbegin();
2235 for (; (*rit) != acquire; rit++) {
2236 ModelAction *propagate = *rit;
2237 if (acquire->happens_before(propagate)) {
2238 propagate->synchronize_with(acquire);
2239 /* Re-check 'propagate' for mo_graph edges */
2240 work_queue->push_back(MOEdgeWorkEntry(propagate));
2245 it = pending_rel_seqs->erase(it);
2246 snapshot_free(pending);
2252 // If we resolved promises or data races, see if we have realized a data race.
2259 * Performs various bookkeeping operations for the current ModelAction. For
2260 * instance, adds action to the per-object, per-thread action vector and to the
2261 * action trace list of all thread actions.
2263 * @param act is the ModelAction to add.
2265 void ModelChecker::add_action_to_lists(ModelAction *act)
2267 int tid = id_to_int(act->get_tid());
2268 ModelAction *uninit = NULL;
2270 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
2271 if (list->empty() && act->is_atomic_var()) {
2272 uninit = new_uninitialized_action(act->get_location());
2273 uninit_id = id_to_int(uninit->get_tid());
2274 list->push_back(uninit);
2276 list->push_back(act);
2278 action_trace->push_back(act);
2280 action_trace->push_front(uninit);
2282 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
2283 if (tid >= (int)vec->size())
2284 vec->resize(priv->next_thread_id);
2285 (*vec)[tid].push_back(act);
2287 (*vec)[uninit_id].push_front(uninit);
2289 if ((int)thrd_last_action->size() <= tid)
2290 thrd_last_action->resize(get_num_threads());
2291 (*thrd_last_action)[tid] = act;
2293 (*thrd_last_action)[uninit_id] = uninit;
2295 if (act->is_fence() && act->is_release()) {
2296 if ((int)thrd_last_fence_release->size() <= tid)
2297 thrd_last_fence_release->resize(get_num_threads());
2298 (*thrd_last_fence_release)[tid] = act;
2301 if (act->is_wait()) {
2302 void *mutex_loc = (void *) act->get_value();
2303 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
2305 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
2306 if (tid >= (int)vec->size())
2307 vec->resize(priv->next_thread_id);
2308 (*vec)[tid].push_back(act);
2313 * @brief Get the last action performed by a particular Thread
2314 * @param tid The thread ID of the Thread in question
2315 * @return The last action in the thread
2317 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
2319 int threadid = id_to_int(tid);
2320 if (threadid < (int)thrd_last_action->size())
2321 return (*thrd_last_action)[id_to_int(tid)];
2327 * @brief Get the last fence release performed by a particular Thread
2328 * @param tid The thread ID of the Thread in question
2329 * @return The last fence release in the thread, if one exists; NULL otherwise
2331 ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
2333 int threadid = id_to_int(tid);
2334 if (threadid < (int)thrd_last_fence_release->size())
2335 return (*thrd_last_fence_release)[id_to_int(tid)];
2341 * Gets the last memory_order_seq_cst write (in the total global sequence)
2342 * performed on a particular object (i.e., memory location), not including the
2344 * @param curr The current ModelAction; also denotes the object location to
2346 * @return The last seq_cst write
2348 ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
2350 void *location = curr->get_location();
2351 action_list_t *list = get_safe_ptr_action(obj_map, location);
2352 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
2353 action_list_t::reverse_iterator rit;
2354 for (rit = list->rbegin(); rit != list->rend(); rit++)
2355 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
2361 * Gets the last memory_order_seq_cst fence (in the total global sequence)
2362 * performed in a particular thread, prior to a particular fence.
2363 * @param tid The ID of the thread to check
2364 * @param before_fence The fence from which to begin the search; if NULL, then
2365 * search for the most recent fence in the thread.
2366 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
2368 ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
2370 /* All fences should have NULL location */
2371 action_list_t *list = get_safe_ptr_action(obj_map, NULL);
2372 action_list_t::reverse_iterator rit = list->rbegin();
2375 for (; rit != list->rend(); rit++)
2376 if (*rit == before_fence)
2379 ASSERT(*rit == before_fence);
2383 for (; rit != list->rend(); rit++)
2384 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
2390 * Gets the last unlock operation performed on a particular mutex (i.e., memory
2391 * location). This function identifies the mutex according to the current
2392 * action, which is presumed to perform on the same mutex.
2393 * @param curr The current ModelAction; also denotes the object location to
2395 * @return The last unlock operation
2397 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
2399 void *location = curr->get_location();
2400 action_list_t *list = get_safe_ptr_action(obj_map, location);
2401 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
2402 action_list_t::reverse_iterator rit;
2403 for (rit = list->rbegin(); rit != list->rend(); rit++)
2404 if ((*rit)->is_unlock() || (*rit)->is_wait())
2409 ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
2411 ModelAction *parent = get_last_action(tid);
2413 parent = get_thread(tid)->get_creation();
2418 * Returns the clock vector for a given thread.
2419 * @param tid The thread whose clock vector we want
2420 * @return Desired clock vector
2422 ClockVector * ModelChecker::get_cv(thread_id_t tid) const
2424 return get_parent_action(tid)->get_cv();
2428 * Resolve a set of Promises with a current write. The set is provided in the
2429 * Node corresponding to @a write.
2430 * @param write The ModelAction that is fulfilling Promises
2431 * @return True if promises were resolved; false otherwise
2433 bool ModelChecker::resolve_promises(ModelAction *write)
2435 bool haveResolved = false;
2436 std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
2437 promise_list_t mustResolve, resolved;
2439 for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
2440 Promise *promise = (*promises)[promise_index];
2441 if (write->get_node()->get_promise(i)) {
2442 ModelAction *read = promise->get_action();
2443 read_from(read, write);
2444 //Make sure the promise's value matches the write's value
2445 ASSERT(promise->is_compatible(write));
2446 mo_graph->resolvePromise(promise, write, &mustResolve);
2448 resolved.push_back(promise);
2449 promises->erase(promises->begin() + promise_index);
2450 actions_to_check.push_back(read);
2452 haveResolved = true;
2457 for (unsigned int i = 0; i < mustResolve.size(); i++) {
2458 if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
2460 priv->failed_promise = true;
2462 for (unsigned int i = 0; i < resolved.size(); i++)
2464 //Check whether reading these writes has made threads unable to
2467 for (unsigned int i = 0; i < actions_to_check.size(); i++) {
2468 ModelAction *read = actions_to_check[i];
2469 mo_check_promises(read, true);
2472 return haveResolved;
2476 * Compute the set of promises that could potentially be satisfied by this
2477 * action. Note that the set computation actually appears in the Node, not in
2479 * @param curr The ModelAction that may satisfy promises
2481 void ModelChecker::compute_promises(ModelAction *curr)
2483 for (unsigned int i = 0; i < promises->size(); i++) {
2484 Promise *promise = (*promises)[i];
2485 const ModelAction *act = promise->get_action();
2486 ASSERT(act->is_read());
2487 if (!act->happens_before(curr) &&
2488 !act->could_synchronize_with(curr) &&
2489 promise->is_compatible(curr) &&
2490 promise->get_value() == curr->get_value()) {
2491 curr->get_node()->set_promise(i, act->is_rmw());
2496 /** Checks promises in response to change in ClockVector Threads. */
2497 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2499 for (unsigned int i = 0; i < promises->size(); i++) {
2500 Promise *promise = (*promises)[i];
2501 const ModelAction *act = promise->get_action();
2502 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2503 merge_cv->synchronized_since(act)) {
2504 if (promise->eliminate_thread(tid)) {
2505 //Promise has failed
2506 priv->failed_promise = true;
2513 void ModelChecker::check_promises_thread_disabled()
2515 for (unsigned int i = 0; i < promises->size(); i++) {
2516 Promise *promise = (*promises)[i];
2517 if (promise->has_failed()) {
2518 priv->failed_promise = true;
2525 * @brief Checks promises in response to addition to modification order for
2528 * We test whether threads are still available for satisfying promises after an
2529 * addition to our modification order constraints. Those that are unavailable
2530 * are "eliminated". Once all threads are eliminated from satisfying a promise,
2531 * that promise has failed.
2533 * @param act The ModelAction which updated the modification order
2534 * @param is_read_check Should be true if act is a read and we must check for
2535 * updates to the store from which it read (there is a distinction here for
2536 * RMW's, which are both a load and a store)
2538 void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
2540 const ModelAction *write = is_read_check ? act->get_reads_from() : act;
2542 for (unsigned int i = 0; i < promises->size(); i++) {
2543 Promise *promise = (*promises)[i];
2544 const ModelAction *pread = promise->get_action();
2546 // Is this promise on the same location?
2547 if (!pread->same_var(write))
2550 if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
2551 priv->failed_promise = true;
2555 // Don't do any lookups twice for the same thread
2556 if (!promise->thread_is_available(act->get_tid()))
2559 if (mo_graph->checkReachable(promise, write)) {
2560 if (mo_graph->checkPromise(write, promise)) {
2561 priv->failed_promise = true;
2569 * Compute the set of writes that may break the current pending release
2570 * sequence. This information is extracted from previou release sequence
2573 * @param curr The current ModelAction. Must be a release sequence fixup
2576 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2578 if (pending_rel_seqs->empty())
2581 struct release_seq *pending = pending_rel_seqs->back();
2582 for (unsigned int i = 0; i < pending->writes.size(); i++) {
2583 const ModelAction *write = pending->writes[i];
2584 curr->get_node()->add_relseq_break(write);
2587 /* NULL means don't break the sequence; just synchronize */
2588 curr->get_node()->add_relseq_break(NULL);
2592 * Build up an initial set of all past writes that this 'read' action may read
2593 * from, as well as any previously-observed future values that must still be valid.
2595 * @param curr is the current ModelAction that we are exploring; it must be a
2598 void ModelChecker::build_may_read_from(ModelAction *curr)
2600 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2602 ASSERT(curr->is_read());
2604 ModelAction *last_sc_write = NULL;
2606 if (curr->is_seqcst())
2607 last_sc_write = get_last_seq_cst_write(curr);
2609 /* Iterate over all threads */
2610 for (i = 0; i < thrd_lists->size(); i++) {
2611 /* Iterate over actions in thread, starting from most recent */
2612 action_list_t *list = &(*thrd_lists)[i];
2613 action_list_t::reverse_iterator rit;
2614 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2615 ModelAction *act = *rit;
2617 /* Only consider 'write' actions */
2618 if (!act->is_write() || act == curr)
2621 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2622 bool allow_read = true;
2624 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
2626 else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
2630 /* Only add feasible reads */
2631 mo_graph->startChanges();
2632 r_modification_order(curr, act);
2633 if (!is_infeasible())
2634 curr->get_node()->add_read_from(act);
2635 mo_graph->rollbackChanges();
2638 /* Include at most one act per-thread that "happens before" curr */
2639 if (act->happens_before(curr))
2644 /* Inherit existing, promised future values */
2645 for (i = 0; i < promises->size(); i++) {
2646 const Promise *promise = (*promises)[i];
2647 const ModelAction *promise_read = promise->get_action();
2648 if (promise_read->same_var(curr)) {
2649 /* Only add feasible future-values */
2650 mo_graph->startChanges();
2651 r_modification_order(curr, promise);
2652 if (!is_infeasible()) {
2653 const struct future_value fv = promise->get_fv();
2654 curr->get_node()->add_future_value(fv);
2656 mo_graph->rollbackChanges();
2660 /* We may find no valid may-read-from only if the execution is doomed */
2661 if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) {
2662 priv->no_valid_reads = true;
2666 if (DBG_ENABLED()) {
2667 model_print("Reached read action:\n");
2669 model_print("Printing may_read_from\n");
2670 curr->get_node()->print_may_read_from();
2671 model_print("End printing may_read_from\n");
2675 bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
2677 for ( ; write != NULL; write = write->get_reads_from()) {
2678 /* UNINIT actions don't have a Node, and they never sleep */
2679 if (write->is_uninitialized())
2681 Node *prevnode = write->get_node()->get_parent();
2683 bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
2684 if (write->is_release() && thread_sleep)
2686 if (!write->is_rmw())
2693 * @brief Create a new action representing an uninitialized atomic
2694 * @param location The memory location of the atomic object
2695 * @return A pointer to a new ModelAction
2697 ModelAction * ModelChecker::new_uninitialized_action(void *location) const
2699 ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
2700 act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
2701 act->create_cv(NULL);
2705 static void print_list(action_list_t *list)
2707 action_list_t::iterator it;
2709 model_print("---------------------------------------------------------------------\n");
2711 unsigned int hash = 0;
2713 for (it = list->begin(); it != list->end(); it++) {
2715 hash = hash^(hash<<3)^((*it)->hash());
2717 model_print("HASH %u\n", hash);
2718 model_print("---------------------------------------------------------------------\n");
2721 #if SUPPORT_MOD_ORDER_DUMP
2722 void ModelChecker::dumpGraph(char *filename) const
2725 sprintf(buffer, "%s.dot", filename);
2726 FILE *file = fopen(buffer, "w");
2727 fprintf(file, "digraph %s {\n", filename);
2728 mo_graph->dumpNodes(file);
2729 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
2731 for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2732 ModelAction *action = *it;
2733 if (action->is_read()) {
2734 fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
2735 if (action->get_reads_from() != NULL)
2736 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2738 if (thread_array[action->get_tid()] != NULL) {
2739 fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2742 thread_array[action->get_tid()] = action;
2744 fprintf(file, "}\n");
2745 model_free(thread_array);
2750 /** @brief Prints an execution trace summary. */
2751 void ModelChecker::print_summary() const
2753 #if SUPPORT_MOD_ORDER_DUMP
2754 char buffername[100];
2755 sprintf(buffername, "exec%04u", stats.num_total);
2756 mo_graph->dumpGraphToFile(buffername);
2757 sprintf(buffername, "graph%04u", stats.num_total);
2758 dumpGraph(buffername);
2761 model_print("Execution %d:", stats.num_total);
2762 if (isfeasibleprefix())
2765 print_infeasibility(" INFEASIBLE");
2766 print_list(action_trace);
2771 * Add a Thread to the system for the first time. Should only be called once
2773 * @param t The Thread to add
2775 void ModelChecker::add_thread(Thread *t)
2777 thread_map->put(id_to_int(t->get_id()), t);
2778 scheduler->add_thread(t);
2782 * Removes a thread from the scheduler.
2783 * @param the thread to remove.
2785 void ModelChecker::remove_thread(Thread *t)
2787 scheduler->remove_thread(t);
2791 * @brief Get a Thread reference by its ID
2792 * @param tid The Thread's ID
2793 * @return A Thread reference
2795 Thread * ModelChecker::get_thread(thread_id_t tid) const
2797 return thread_map->get(id_to_int(tid));
2801 * @brief Get a reference to the Thread in which a ModelAction was executed
2802 * @param act The ModelAction
2803 * @return A Thread reference
2805 Thread * ModelChecker::get_thread(const ModelAction *act) const
2807 return get_thread(act->get_tid());
2811 * @brief Check if a Thread is currently enabled
2812 * @param t The Thread to check
2813 * @return True if the Thread is currently enabled
2815 bool ModelChecker::is_enabled(Thread *t) const
2817 return scheduler->is_enabled(t);
2821 * @brief Check if a Thread is currently enabled
2822 * @param tid The ID of the Thread to check
2823 * @return True if the Thread is currently enabled
2825 bool ModelChecker::is_enabled(thread_id_t tid) const
2827 return scheduler->is_enabled(tid);
2831 * Switch from a model-checker context to a user-thread context. This is the
2832 * complement of ModelChecker::switch_to_master and must be called from the
2833 * model-checker context
2835 * @param thread The user-thread to switch to
2837 void ModelChecker::switch_from_master(Thread *thread)
2839 scheduler->set_current_thread(thread);
2840 Thread::swap(&system_context, thread);
2844 * Switch from a user-context to the "master thread" context (a.k.a. system
2845 * context). This switch is made with the intention of exploring a particular
2846 * model-checking action (described by a ModelAction object). Must be called
2847 * from a user-thread context.
2849 * @param act The current action that will be explored. May be NULL only if
2850 * trace is exiting via an assertion (see ModelChecker::set_assert and
2851 * ModelChecker::has_asserted).
2852 * @return Return the value returned by the current action
2854 uint64_t ModelChecker::switch_to_master(ModelAction *act)
2857 Thread *old = thread_current();
2858 ASSERT(!old->get_pending());
2859 old->set_pending(act);
2860 if (Thread::swap(old, &system_context) < 0) {
2861 perror("swap threads");
2864 return old->get_return_value();
2868 * Takes the next step in the execution, if possible.
2869 * @param curr The current step to take
2870 * @return Returns the next Thread to run, if any; NULL if this execution
2873 Thread * ModelChecker::take_step(ModelAction *curr)
2875 Thread *curr_thrd = get_thread(curr);
2876 ASSERT(curr_thrd->get_state() == THREAD_READY);
2878 curr = check_current_action(curr);
2880 /* Infeasible -> don't take any more steps */
2881 if (is_infeasible())
2883 else if (isfeasibleprefix() && have_bug_reports()) {
2888 if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
2891 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
2892 scheduler->remove_thread(curr_thrd);
2894 Thread *next_thrd = get_next_thread(curr);
2896 DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
2897 next_thrd ? id_to_int(next_thrd->get_id()) : -1);
2902 /** Wrapper to run the user's main function, with appropriate arguments */
2903 void user_main_wrapper(void *)
2905 user_main(model->params.argc, model->params.argv);
2908 /** @brief Run ModelChecker for the user program */
2909 void ModelChecker::run()
2913 Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL, NULL);
2918 * Stash next pending action(s) for thread(s). There
2919 * should only need to stash one thread's action--the
2920 * thread which just took a step--plus the first step
2921 * for any newly-created thread
2923 for (unsigned int i = 0; i < get_num_threads(); i++) {
2924 thread_id_t tid = int_to_id(i);
2925 Thread *thr = get_thread(tid);
2926 if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
2927 switch_from_master(thr);
2931 /* Catch assertions from prior take_step or from
2932 * between-ModelAction bugs (e.g., data races) */
2936 /* Consume the next action for a Thread */
2937 ModelAction *curr = t->get_pending();
2938 t->set_pending(NULL);
2939 t = take_step(curr);
2940 } while (t && !t->is_model_thread());
2943 * Launch end-of-execution release sequence fixups only when
2944 * the execution is otherwise feasible AND there are:
2946 * (1) pending release sequences
2947 * (2) pending assertions that could be invalidated by a change
2948 * in clock vectors (i.e., data races)
2949 * (3) no pending promises
2951 while (!pending_rel_seqs->empty() &&
2952 is_feasible_prefix_ignore_relseq() &&
2953 !unrealizedraces.empty()) {
2954 model_print("*** WARNING: release sequence fixup action "
2955 "(%zu pending release seuqence(s)) ***\n",
2956 pending_rel_seqs->size());
2957 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2958 std::memory_order_seq_cst, NULL, VALUE_NONE,
2962 } while (next_execution());
2964 model_print("******* Model-checking complete: *******\n");