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() :
43 /* First thread created will have id INITIAL_THREAD_ID */
44 next_thread_id(INITIAL_THREAD_ID),
45 used_sequence_numbers(0),
49 failed_promise(false),
50 too_many_reads(false),
51 no_valid_reads(false),
52 bad_synchronization(false),
56 ~model_snapshot_members() {
57 for (unsigned int i = 0; i < bugs.size(); i++)
62 ModelAction *current_action;
63 unsigned int next_thread_id;
64 modelclock_t used_sequence_numbers;
65 ModelAction *next_backtrack;
66 std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
67 struct execution_stats stats;
71 /** @brief Incorrectly-ordered synchronization was made */
72 bool bad_synchronization;
78 /** @brief Constructor */
79 ModelChecker::ModelChecker(struct model_params params) :
80 /* Initialize default scheduler */
82 scheduler(new Scheduler()),
84 earliest_diverge(NULL),
85 action_trace(new action_list_t()),
86 thread_map(new HashTable<int, Thread *, int>()),
87 obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
88 lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
89 condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
90 obj_thrd_map(new HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 >()),
91 promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
92 futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
93 pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
94 thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
95 thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
96 node_stack(new NodeStack()),
97 priv(new struct model_snapshot_members()),
98 mo_graph(new CycleGraph())
100 /* Initialize a model-checker thread, for special ModelActions */
101 model_thread = new Thread(get_next_id());
102 thread_map->put(id_to_int(model_thread->get_id()), model_thread);
105 /** @brief Destructor */
106 ModelChecker::~ModelChecker()
108 for (unsigned int i = 0; i < get_num_threads(); i++)
109 delete thread_map->get(i);
114 delete lock_waiters_map;
115 delete condvar_waiters_map;
118 for (unsigned int i = 0; i < promises->size(); i++)
119 delete (*promises)[i];
122 delete pending_rel_seqs;
124 delete thrd_last_action;
125 delete thrd_last_fence_release;
132 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
134 action_list_t *tmp = hash->get(ptr);
136 tmp = new action_list_t();
142 static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
144 std::vector<action_list_t> *tmp = hash->get(ptr);
146 tmp = new std::vector<action_list_t>();
153 * Restores user program to initial state and resets all model-checker data
156 void ModelChecker::reset_to_initial_state()
158 DEBUG("+++ Resetting to initial state +++\n");
159 node_stack->reset_execution();
161 /* Print all model-checker output before rollback */
164 snapshot_backtrack_before(0);
167 /** @return a thread ID for a new Thread */
168 thread_id_t ModelChecker::get_next_id()
170 return priv->next_thread_id++;
173 /** @return the number of user threads created during this execution */
174 unsigned int ModelChecker::get_num_threads() const
176 return priv->next_thread_id;
180 * Must be called from user-thread context (e.g., through the global
181 * thread_current() interface)
183 * @return The currently executing Thread.
185 Thread * ModelChecker::get_current_thread() const
187 return scheduler->get_current_thread();
190 /** @return a sequence number for a new ModelAction */
191 modelclock_t ModelChecker::get_next_seq_num()
193 return ++priv->used_sequence_numbers;
196 Node * ModelChecker::get_curr_node() const
198 return node_stack->get_head();
202 * @brief Choose the next thread to execute.
204 * This function chooses the next thread that should execute. It can force the
205 * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
206 * followed by a THREAD_START, or it can enforce execution replay/backtracking.
207 * The model-checker may have no preference regarding the next thread (i.e.,
208 * when exploring a new execution ordering), in which case this will return
210 * @param curr The current ModelAction. This action might guide the choice of
212 * @return The next thread to run. If the model-checker has no preference, NULL.
214 Thread * ModelChecker::get_next_thread(ModelAction *curr)
219 /* Do not split atomic actions. */
221 return thread_current();
222 else if (curr->get_type() == THREAD_CREATE)
223 return curr->get_thread_operand();
226 /* Have we completed exploring the preselected path? */
230 /* Else, we are trying to replay an execution */
231 ModelAction *next = node_stack->get_next()->get_action();
233 if (next == diverge) {
234 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
235 earliest_diverge = diverge;
237 Node *nextnode = next->get_node();
238 Node *prevnode = nextnode->get_parent();
239 scheduler->update_sleep_set(prevnode);
241 /* Reached divergence point */
242 if (nextnode->increment_misc()) {
243 /* The next node will try to satisfy a different misc_index values. */
244 tid = next->get_tid();
245 node_stack->pop_restofstack(2);
246 } else if (nextnode->increment_promise()) {
247 /* The next node will try to satisfy a different set of promises. */
248 tid = next->get_tid();
249 node_stack->pop_restofstack(2);
250 } else if (nextnode->increment_read_from()) {
251 /* The next node will read from a different value. */
252 tid = next->get_tid();
253 node_stack->pop_restofstack(2);
254 } else if (nextnode->increment_future_value()) {
255 /* The next node will try to read from a different future value. */
256 tid = next->get_tid();
257 node_stack->pop_restofstack(2);
258 } else if (nextnode->increment_relseq_break()) {
259 /* The next node will try to resolve a release sequence differently */
260 tid = next->get_tid();
261 node_stack->pop_restofstack(2);
264 /* Make a different thread execute for next step */
265 scheduler->add_sleep(get_thread(next->get_tid()));
266 tid = prevnode->get_next_backtrack();
267 /* Make sure the backtracked thread isn't sleeping. */
268 node_stack->pop_restofstack(1);
269 if (diverge == earliest_diverge) {
270 earliest_diverge = prevnode->get_action();
273 /* The correct sleep set is in the parent node. */
276 DEBUG("*** Divergence point ***\n");
280 tid = next->get_tid();
282 DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
283 ASSERT(tid != THREAD_ID_T_NONE);
284 return thread_map->get(id_to_int(tid));
288 * We need to know what the next actions of all threads in the sleep
289 * set will be. This method computes them and stores the actions at
290 * the corresponding thread object's pending action.
293 void ModelChecker::execute_sleep_set()
295 for (unsigned int i = 0; i < get_num_threads(); i++) {
296 thread_id_t tid = int_to_id(i);
297 Thread *thr = get_thread(tid);
298 if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
299 scheduler->next_thread(thr);
300 Thread::swap(&system_context, thr);
301 priv->current_action->set_sleep_flag();
302 thr->set_pending(priv->current_action);
307 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
309 for (unsigned int i = 0; i < get_num_threads(); i++) {
310 Thread *thr = get_thread(int_to_id(i));
311 if (scheduler->is_sleep_set(thr)) {
312 ModelAction *pending_act = thr->get_pending();
313 if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
314 //Remove this thread from sleep set
315 scheduler->remove_sleep(thr);
320 /** @brief Alert the model-checker that an incorrectly-ordered
321 * synchronization was made */
322 void ModelChecker::set_bad_synchronization()
324 priv->bad_synchronization = true;
327 bool ModelChecker::has_asserted() const
329 return priv->asserted;
332 void ModelChecker::set_assert()
334 priv->asserted = true;
338 * Check if we are in a deadlock. Should only be called at the end of an
339 * execution, although it should not give false positives in the middle of an
340 * execution (there should be some ENABLED thread).
342 * @return True if program is in a deadlock; false otherwise
344 bool ModelChecker::is_deadlocked() const
346 bool blocking_threads = false;
347 for (unsigned int i = 0; i < get_num_threads(); i++) {
348 thread_id_t tid = int_to_id(i);
351 Thread *t = get_thread(tid);
352 if (!t->is_model_thread() && t->get_pending())
353 blocking_threads = true;
355 return blocking_threads;
359 * Check if this is a complete execution. That is, have all thread completed
360 * execution (rather than exiting because sleep sets have forced a redundant
363 * @return True if the execution is complete.
365 bool ModelChecker::is_complete_execution() const
367 for (unsigned int i = 0; i < get_num_threads(); i++)
368 if (is_enabled(int_to_id(i)))
374 * @brief Assert a bug in the executing program.
376 * Use this function to assert any sort of bug in the user program. If the
377 * current trace is feasible (actually, a prefix of some feasible execution),
378 * then this execution will be aborted, printing the appropriate message. If
379 * the current trace is not yet feasible, the error message will be stashed and
380 * printed if the execution ever becomes feasible.
382 * @param msg Descriptive message for the bug (do not include newline char)
383 * @return True if bug is immediately-feasible
385 bool ModelChecker::assert_bug(const char *msg)
387 priv->bugs.push_back(new bug_message(msg));
389 if (isfeasibleprefix()) {
397 * @brief Assert a bug in the executing program, asserted by a user thread
398 * @see ModelChecker::assert_bug
399 * @param msg Descriptive message for the bug (do not include newline char)
401 void ModelChecker::assert_user_bug(const char *msg)
403 /* If feasible bug, bail out now */
405 switch_to_master(NULL);
408 /** @return True, if any bugs have been reported for this execution */
409 bool ModelChecker::have_bug_reports() const
411 return priv->bugs.size() != 0;
414 /** @brief Print bug report listing for this execution (if any bugs exist) */
415 void ModelChecker::print_bugs() const
417 if (have_bug_reports()) {
418 model_print("Bug report: %zu bug%s detected\n",
420 priv->bugs.size() > 1 ? "s" : "");
421 for (unsigned int i = 0; i < priv->bugs.size(); i++)
422 priv->bugs[i]->print();
427 * @brief Record end-of-execution stats
429 * Must be run when exiting an execution. Records various stats.
430 * @see struct execution_stats
432 void ModelChecker::record_stats()
435 if (!isfeasibleprefix())
436 stats.num_infeasible++;
437 else if (have_bug_reports())
438 stats.num_buggy_executions++;
439 else if (is_complete_execution())
440 stats.num_complete++;
442 stats.num_redundant++;
445 /** @brief Print execution stats */
446 void ModelChecker::print_stats() const
448 model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
449 model_print("Number of redundant executions: %d\n", stats.num_redundant);
450 model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
451 model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
452 model_print("Total executions: %d\n", stats.num_total);
453 model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
457 * @brief End-of-exeuction print
458 * @param printbugs Should any existing bugs be printed?
460 void ModelChecker::print_execution(bool printbugs) const
462 print_program_output();
464 if (DBG_ENABLED() || params.verbose) {
465 model_print("Earliest divergence point since last feasible execution:\n");
466 if (earliest_diverge)
467 earliest_diverge->print();
469 model_print("(Not set)\n");
475 /* Don't print invalid bugs */
484 * Queries the model-checker for more executions to explore and, if one
485 * exists, resets the model-checker state to execute a new execution.
487 * @return If there are more executions to explore, return true. Otherwise,
490 bool ModelChecker::next_execution()
493 /* Is this execution a feasible execution that's worth bug-checking? */
494 bool complete = isfeasibleprefix() && (is_complete_execution() ||
497 /* End-of-execution bug checks */
500 assert_bug("Deadlock detected");
508 if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
509 print_execution(complete);
511 clear_program_output();
514 earliest_diverge = NULL;
516 if ((diverge = get_next_backtrack()) == NULL)
520 model_print("Next execution will diverge at:\n");
524 reset_to_initial_state();
528 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
530 switch (act->get_type()) {
535 /* Optimization: relaxed operations don't need backtracking */
536 if (act->is_relaxed())
538 /* linear search: from most recent to oldest */
539 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
540 action_list_t::reverse_iterator rit;
541 for (rit = list->rbegin(); rit != list->rend(); rit++) {
542 ModelAction *prev = *rit;
543 if (prev->could_synchronize_with(act))
549 case ATOMIC_TRYLOCK: {
550 /* linear search: from most recent to oldest */
551 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
552 action_list_t::reverse_iterator rit;
553 for (rit = list->rbegin(); rit != list->rend(); rit++) {
554 ModelAction *prev = *rit;
555 if (act->is_conflicting_lock(prev))
560 case ATOMIC_UNLOCK: {
561 /* linear search: from most recent to oldest */
562 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
563 action_list_t::reverse_iterator rit;
564 for (rit = list->rbegin(); rit != list->rend(); rit++) {
565 ModelAction *prev = *rit;
566 if (!act->same_thread(prev) && prev->is_failed_trylock())
572 /* linear search: from most recent to oldest */
573 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
574 action_list_t::reverse_iterator rit;
575 for (rit = list->rbegin(); rit != list->rend(); rit++) {
576 ModelAction *prev = *rit;
577 if (!act->same_thread(prev) && prev->is_failed_trylock())
579 if (!act->same_thread(prev) && prev->is_notify())
585 case ATOMIC_NOTIFY_ALL:
586 case ATOMIC_NOTIFY_ONE: {
587 /* linear search: from most recent to oldest */
588 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
589 action_list_t::reverse_iterator rit;
590 for (rit = list->rbegin(); rit != list->rend(); rit++) {
591 ModelAction *prev = *rit;
592 if (!act->same_thread(prev) && prev->is_wait())
603 /** This method finds backtracking points where we should try to
604 * reorder the parameter ModelAction against.
606 * @param the ModelAction to find backtracking points for.
608 void ModelChecker::set_backtracking(ModelAction *act)
610 Thread *t = get_thread(act);
611 ModelAction *prev = get_last_conflict(act);
615 Node *node = prev->get_node()->get_parent();
617 int low_tid, high_tid;
618 if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
619 low_tid = id_to_int(act->get_tid());
620 high_tid = low_tid + 1;
623 high_tid = get_num_threads();
626 for (int i = low_tid; i < high_tid; i++) {
627 thread_id_t tid = int_to_id(i);
629 /* Make sure this thread can be enabled here. */
630 if (i >= node->get_num_threads())
633 /* Don't backtrack into a point where the thread is disabled or sleeping. */
634 if (node->enabled_status(tid) != THREAD_ENABLED)
637 /* Check if this has been explored already */
638 if (node->has_been_explored(tid))
641 /* See if fairness allows */
642 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
644 for (int t = 0; t < node->get_num_threads(); t++) {
645 thread_id_t tother = int_to_id(t);
646 if (node->is_enabled(tother) && node->has_priority(tother)) {
654 /* Cache the latest backtracking point */
655 set_latest_backtrack(prev);
657 /* If this is a new backtracking point, mark the tree */
658 if (!node->set_backtrack(tid))
660 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
661 id_to_int(prev->get_tid()),
662 id_to_int(t->get_id()));
671 * @brief Cache the a backtracking point as the "most recent", if eligible
673 * Note that this does not prepare the NodeStack for this backtracking
674 * operation, it only caches the action on a per-execution basis
676 * @param act The operation at which we should explore a different next action
677 * (i.e., backtracking point)
678 * @return True, if this action is now the most recent backtracking point;
681 bool ModelChecker::set_latest_backtrack(ModelAction *act)
683 if (!priv->next_backtrack || *act > *priv->next_backtrack) {
684 priv->next_backtrack = act;
691 * Returns last backtracking point. The model checker will explore a different
692 * path for this point in the next execution.
693 * @return The ModelAction at which the next execution should diverge.
695 ModelAction * ModelChecker::get_next_backtrack()
697 ModelAction *next = priv->next_backtrack;
698 priv->next_backtrack = NULL;
703 * Processes a read or rmw model action.
704 * @param curr is the read model action to process.
705 * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
706 * @return True if processing this read updates the mo_graph.
708 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
710 uint64_t value = VALUE_NONE;
711 bool updated = false;
713 const ModelAction *reads_from = curr->get_node()->get_read_from();
714 if (reads_from != NULL) {
715 mo_graph->startChanges();
717 value = reads_from->get_value();
718 bool r_status = false;
720 if (!second_part_of_rmw) {
721 check_recency(curr, reads_from);
722 r_status = r_modification_order(curr, reads_from);
725 if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
726 mo_graph->rollbackChanges();
727 priv->too_many_reads = false;
731 read_from(curr, reads_from);
732 mo_graph->commitChanges();
733 mo_check_promises(curr, true);
736 } else if (!second_part_of_rmw) {
737 /* Read from future value */
738 struct future_value fv = curr->get_node()->get_future_value();
739 Promise *promise = new Promise(curr, fv);
741 curr->set_read_from_promise(promise);
742 promises->push_back(promise);
743 mo_graph->startChanges();
744 updated = r_modification_order(curr, promise);
745 mo_graph->commitChanges();
747 get_thread(curr)->set_return_value(value);
753 * Processes a lock, trylock, or unlock model action. @param curr is
754 * the read model action to process.
756 * The try lock operation checks whether the lock is taken. If not,
757 * it falls to the normal lock operation case. If so, it returns
760 * The lock operation has already been checked that it is enabled, so
761 * it just grabs the lock and synchronizes with the previous unlock.
763 * The unlock operation has to re-enable all of the threads that are
764 * waiting on the lock.
766 * @return True if synchronization was updated; false otherwise
768 bool ModelChecker::process_mutex(ModelAction *curr)
770 std::mutex *mutex = NULL;
771 struct std::mutex_state *state = NULL;
773 if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
774 mutex = (std::mutex *)curr->get_location();
775 state = mutex->get_state();
776 } else if (curr->is_wait()) {
777 mutex = (std::mutex *)curr->get_value();
778 state = mutex->get_state();
781 switch (curr->get_type()) {
782 case ATOMIC_TRYLOCK: {
783 bool success = !state->islocked;
784 curr->set_try_lock(success);
786 get_thread(curr)->set_return_value(0);
789 get_thread(curr)->set_return_value(1);
791 //otherwise fall into the lock case
793 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
794 assert_bug("Lock access before initialization");
795 state->islocked = true;
796 ModelAction *unlock = get_last_unlock(curr);
797 //synchronize with the previous unlock statement
798 if (unlock != NULL) {
799 curr->synchronize_with(unlock);
804 case ATOMIC_UNLOCK: {
806 state->islocked = false;
807 //wake up the other threads
808 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
809 //activate all the waiting threads
810 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
811 scheduler->wake(get_thread(*rit));
818 state->islocked = false;
819 //wake up the other threads
820 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
821 //activate all the waiting threads
822 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
823 scheduler->wake(get_thread(*rit));
826 //check whether we should go to sleep or not...simulate spurious failures
827 if (curr->get_node()->get_misc() == 0) {
828 get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
830 scheduler->sleep(get_thread(curr));
834 case ATOMIC_NOTIFY_ALL: {
835 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
836 //activate all the waiting threads
837 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
838 scheduler->wake(get_thread(*rit));
843 case ATOMIC_NOTIFY_ONE: {
844 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
845 int wakeupthread = curr->get_node()->get_misc();
846 action_list_t::iterator it = waiters->begin();
847 advance(it, wakeupthread);
848 scheduler->wake(get_thread(*it));
859 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
861 /* Do more ambitious checks now that mo is more complete */
862 if (mo_may_allow(writer, reader)) {
863 Node *node = reader->get_node();
865 /* Find an ancestor thread which exists at the time of the reader */
866 Thread *write_thread = get_thread(writer);
867 while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
868 write_thread = write_thread->get_parent();
870 struct future_value fv = {
872 writer->get_seq_number() + params.maxfuturedelay,
873 write_thread->get_id(),
875 if (node->add_future_value(fv))
876 set_latest_backtrack(reader);
881 * Process a write ModelAction
882 * @param curr The ModelAction to process
883 * @return True if the mo_graph was updated or promises were resolved
885 bool ModelChecker::process_write(ModelAction *curr)
887 bool updated_mod_order = w_modification_order(curr);
888 bool updated_promises = resolve_promises(curr);
890 if (promises->size() == 0) {
891 for (unsigned int i = 0; i < futurevalues->size(); i++) {
892 struct PendingFutureValue pfv = (*futurevalues)[i];
893 add_future_value(pfv.writer, pfv.act);
895 futurevalues->clear();
898 mo_graph->commitChanges();
899 mo_check_promises(curr, false);
901 get_thread(curr)->set_return_value(VALUE_NONE);
902 return updated_mod_order || updated_promises;
906 * Process a fence ModelAction
907 * @param curr The ModelAction to process
908 * @return True if synchronization was updated
910 bool ModelChecker::process_fence(ModelAction *curr)
913 * fence-relaxed: no-op
914 * fence-release: only log the occurence (not in this function), for
915 * use in later synchronization
916 * fence-acquire (this function): search for hypothetical release
919 bool updated = false;
920 if (curr->is_acquire()) {
921 action_list_t *list = action_trace;
922 action_list_t::reverse_iterator rit;
923 /* Find X : is_read(X) && X --sb-> curr */
924 for (rit = list->rbegin(); rit != list->rend(); rit++) {
925 ModelAction *act = *rit;
928 if (act->get_tid() != curr->get_tid())
930 /* Stop at the beginning of the thread */
931 if (act->is_thread_start())
933 /* Stop once we reach a prior fence-acquire */
934 if (act->is_fence() && act->is_acquire())
938 /* read-acquire will find its own release sequences */
939 if (act->is_acquire())
942 /* Establish hypothetical release sequences */
943 rel_heads_list_t release_heads;
944 get_release_seq_heads(curr, act, &release_heads);
945 for (unsigned int i = 0; i < release_heads.size(); i++)
946 if (!curr->synchronize_with(release_heads[i]))
947 set_bad_synchronization();
948 if (release_heads.size() != 0)
956 * @brief Process the current action for thread-related activity
958 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
959 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
960 * synchronization, etc. This function is a no-op for non-THREAD actions
961 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
963 * @param curr The current action
964 * @return True if synchronization was updated or a thread completed
966 bool ModelChecker::process_thread_action(ModelAction *curr)
968 bool updated = false;
970 switch (curr->get_type()) {
971 case THREAD_CREATE: {
972 thrd_t *thrd = (thrd_t *)curr->get_location();
973 struct thread_params *params = (struct thread_params *)curr->get_value();
974 Thread *th = new Thread(thrd, params->func, params->arg);
976 th->set_creation(curr);
977 /* Promises can be satisfied by children */
978 for (unsigned int i = 0; i < promises->size(); i++) {
979 Promise *promise = (*promises)[i];
980 if (promise->thread_is_available(curr->get_tid()))
981 promise->add_thread(th->get_id());
986 Thread *blocking = curr->get_thread_operand();
987 ModelAction *act = get_last_action(blocking->get_id());
988 curr->synchronize_with(act);
989 updated = true; /* trigger rel-seq checks */
992 case THREAD_FINISH: {
993 Thread *th = get_thread(curr);
994 while (!th->wait_list_empty()) {
995 ModelAction *act = th->pop_wait_list();
996 scheduler->wake(get_thread(act));
999 /* Completed thread can't satisfy promises */
1000 for (unsigned int i = 0; i < promises->size(); i++) {
1001 Promise *promise = (*promises)[i];
1002 if (promise->thread_is_available(th->get_id()))
1003 if (promise->eliminate_thread(th->get_id()))
1004 priv->failed_promise = true;
1006 updated = true; /* trigger rel-seq checks */
1009 case THREAD_START: {
1010 check_promises(curr->get_tid(), NULL, curr->get_cv());
1021 * @brief Process the current action for release sequence fixup activity
1023 * Performs model-checker release sequence fixups for the current action,
1024 * forcing a single pending release sequence to break (with a given, potential
1025 * "loose" write) or to complete (i.e., synchronize). If a pending release
1026 * sequence forms a complete release sequence, then we must perform the fixup
1027 * synchronization, mo_graph additions, etc.
1029 * @param curr The current action; must be a release sequence fixup action
1030 * @param work_queue The work queue to which to add work items as they are
1033 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
1035 const ModelAction *write = curr->get_node()->get_relseq_break();
1036 struct release_seq *sequence = pending_rel_seqs->back();
1037 pending_rel_seqs->pop_back();
1039 ModelAction *acquire = sequence->acquire;
1040 const ModelAction *rf = sequence->rf;
1041 const ModelAction *release = sequence->release;
1045 ASSERT(release->same_thread(rf));
1047 if (write == NULL) {
1049 * @todo Forcing a synchronization requires that we set
1050 * modification order constraints. For instance, we can't allow
1051 * a fixup sequence in which two separate read-acquire
1052 * operations read from the same sequence, where the first one
1053 * synchronizes and the other doesn't. Essentially, we can't
1054 * allow any writes to insert themselves between 'release' and
1058 /* Must synchronize */
1059 if (!acquire->synchronize_with(release)) {
1060 set_bad_synchronization();
1063 /* Re-check all pending release sequences */
1064 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1065 /* Re-check act for mo_graph edges */
1066 work_queue->push_back(MOEdgeWorkEntry(acquire));
1068 /* propagate synchronization to later actions */
1069 action_list_t::reverse_iterator rit = action_trace->rbegin();
1070 for (; (*rit) != acquire; rit++) {
1071 ModelAction *propagate = *rit;
1072 if (acquire->happens_before(propagate)) {
1073 propagate->synchronize_with(acquire);
1074 /* Re-check 'propagate' for mo_graph edges */
1075 work_queue->push_back(MOEdgeWorkEntry(propagate));
1079 /* Break release sequence with new edges:
1080 * release --mo--> write --mo--> rf */
1081 mo_graph->addEdge(release, write);
1082 mo_graph->addEdge(write, rf);
1085 /* See if we have realized a data race */
1090 * Initialize the current action by performing one or more of the following
1091 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
1092 * in the NodeStack, manipulating backtracking sets, allocating and
1093 * initializing clock vectors, and computing the promises to fulfill.
1095 * @param curr The current action, as passed from the user context; may be
1096 * freed/invalidated after the execution of this function, with a different
1097 * action "returned" its place (pass-by-reference)
1098 * @return True if curr is a newly-explored action; false otherwise
1100 bool ModelChecker::initialize_curr_action(ModelAction **curr)
1102 ModelAction *newcurr;
1104 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
1105 newcurr = process_rmw(*curr);
1108 if (newcurr->is_rmw())
1109 compute_promises(newcurr);
1115 (*curr)->set_seq_number(get_next_seq_num());
1117 newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
1119 /* First restore type and order in case of RMW operation */
1120 if ((*curr)->is_rmwr())
1121 newcurr->copy_typeandorder(*curr);
1123 ASSERT((*curr)->get_location() == newcurr->get_location());
1124 newcurr->copy_from_new(*curr);
1126 /* Discard duplicate ModelAction; use action from NodeStack */
1129 /* Always compute new clock vector */
1130 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1133 return false; /* Action was explored previously */
1137 /* Always compute new clock vector */
1138 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1140 /* Assign most recent release fence */
1141 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
1144 * Perform one-time actions when pushing new ModelAction onto
1147 if (newcurr->is_write())
1148 compute_promises(newcurr);
1149 else if (newcurr->is_relseq_fixup())
1150 compute_relseq_breakwrites(newcurr);
1151 else if (newcurr->is_wait())
1152 newcurr->get_node()->set_misc_max(2);
1153 else if (newcurr->is_notify_one()) {
1154 newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
1156 return true; /* This was a new ModelAction */
1161 * @brief Establish reads-from relation between two actions
1163 * Perform basic operations involved with establishing a concrete rf relation,
1164 * including setting the ModelAction data and checking for release sequences.
1166 * @param act The action that is reading (must be a read)
1167 * @param rf The action from which we are reading (must be a write)
1169 * @return True if this read established synchronization
1171 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
1173 act->set_read_from(rf);
1174 if (rf != NULL && act->is_acquire()) {
1175 rel_heads_list_t release_heads;
1176 get_release_seq_heads(act, act, &release_heads);
1177 int num_heads = release_heads.size();
1178 for (unsigned int i = 0; i < release_heads.size(); i++)
1179 if (!act->synchronize_with(release_heads[i])) {
1180 set_bad_synchronization();
1183 return num_heads > 0;
1189 * @brief Check whether a model action is enabled.
1191 * Checks whether a lock or join operation would be successful (i.e., is the
1192 * lock already locked, or is the joined thread already complete). If not, put
1193 * the action in a waiter list.
1195 * @param curr is the ModelAction to check whether it is enabled.
1196 * @return a bool that indicates whether the action is enabled.
1198 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1199 if (curr->is_lock()) {
1200 std::mutex *lock = (std::mutex *)curr->get_location();
1201 struct std::mutex_state *state = lock->get_state();
1202 if (state->islocked) {
1203 //Stick the action in the appropriate waiting queue
1204 get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1207 } else if (curr->get_type() == THREAD_JOIN) {
1208 Thread *blocking = (Thread *)curr->get_location();
1209 if (!blocking->is_complete()) {
1210 blocking->push_wait_list(curr);
1219 * Stores the ModelAction for the current thread action. Call this
1220 * immediately before switching from user- to system-context to pass
1221 * data between them.
1222 * @param act The ModelAction created by the user-thread action
1224 void ModelChecker::set_current_action(ModelAction *act) {
1225 priv->current_action = act;
1229 * This is the heart of the model checker routine. It performs model-checking
1230 * actions corresponding to a given "current action." Among other processes, it
1231 * calculates reads-from relationships, updates synchronization clock vectors,
1232 * forms a memory_order constraints graph, and handles replay/backtrack
1233 * execution when running permutations of previously-observed executions.
1235 * @param curr The current action to process
1236 * @return The ModelAction that is actually executed; may be different than
1237 * curr; may be NULL, if the current action is not enabled to run
1239 ModelAction * ModelChecker::check_current_action(ModelAction *curr)
1242 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1244 if (!check_action_enabled(curr)) {
1245 /* Make the execution look like we chose to run this action
1246 * much later, when a lock/join can succeed */
1247 get_thread(curr)->set_pending(curr);
1248 scheduler->sleep(get_thread(curr));
1252 bool newly_explored = initialize_curr_action(&curr);
1258 wake_up_sleeping_actions(curr);
1260 /* Add the action to lists before any other model-checking tasks */
1261 if (!second_part_of_rmw)
1262 add_action_to_lists(curr);
1264 /* Build may_read_from set for newly-created actions */
1265 if (newly_explored && curr->is_read())
1266 build_reads_from_past(curr);
1268 /* Initialize work_queue with the "current action" work */
1269 work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1270 while (!work_queue.empty() && !has_asserted()) {
1271 WorkQueueEntry work = work_queue.front();
1272 work_queue.pop_front();
1274 switch (work.type) {
1275 case WORK_CHECK_CURR_ACTION: {
1276 ModelAction *act = work.action;
1277 bool update = false; /* update this location's release seq's */
1278 bool update_all = false; /* update all release seq's */
1280 if (process_thread_action(curr))
1283 if (act->is_read() && process_read(act, second_part_of_rmw))
1286 if (act->is_write() && process_write(act))
1289 if (act->is_fence() && process_fence(act))
1292 if (act->is_mutex_op() && process_mutex(act))
1295 if (act->is_relseq_fixup())
1296 process_relseq_fixup(curr, &work_queue);
1299 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1301 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1304 case WORK_CHECK_RELEASE_SEQ:
1305 resolve_release_sequences(work.location, &work_queue);
1307 case WORK_CHECK_MO_EDGES: {
1308 /** @todo Complete verification of work_queue */
1309 ModelAction *act = work.action;
1310 bool updated = false;
1312 if (act->is_read()) {
1313 const ModelAction *rf = act->get_reads_from();
1314 const Promise *promise = act->get_reads_from_promise();
1316 if (r_modification_order(act, rf))
1318 } else if (promise) {
1319 if (r_modification_order(act, promise))
1323 if (act->is_write()) {
1324 if (w_modification_order(act))
1327 mo_graph->commitChanges();
1330 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1339 check_curr_backtracking(curr);
1340 set_backtracking(curr);
1344 void ModelChecker::check_curr_backtracking(ModelAction *curr)
1346 Node *currnode = curr->get_node();
1347 Node *parnode = currnode->get_parent();
1349 if ((parnode && !parnode->backtrack_empty()) ||
1350 !currnode->misc_empty() ||
1351 !currnode->read_from_empty() ||
1352 !currnode->future_value_empty() ||
1353 !currnode->promise_empty() ||
1354 !currnode->relseq_break_empty()) {
1355 set_latest_backtrack(curr);
1359 bool ModelChecker::promises_expired() const
1361 for (unsigned int i = 0; i < promises->size(); i++) {
1362 Promise *promise = (*promises)[i];
1363 if (promise->get_expiration() < priv->used_sequence_numbers)
1370 * This is the strongest feasibility check available.
1371 * @return whether the current trace (partial or complete) must be a prefix of
1374 bool ModelChecker::isfeasibleprefix() const
1376 return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
1380 * Print disagnostic information about an infeasible execution
1381 * @param prefix A string to prefix the output with; if NULL, then a default
1382 * message prefix will be provided
1384 void ModelChecker::print_infeasibility(const char *prefix) const
1388 if (mo_graph->checkForCycles())
1389 ptr += sprintf(ptr, "[mo cycle]");
1390 if (priv->failed_promise)
1391 ptr += sprintf(ptr, "[failed promise]");
1392 if (priv->too_many_reads)
1393 ptr += sprintf(ptr, "[too many reads]");
1394 if (priv->no_valid_reads)
1395 ptr += sprintf(ptr, "[no valid reads-from]");
1396 if (priv->bad_synchronization)
1397 ptr += sprintf(ptr, "[bad sw ordering]");
1398 if (promises_expired())
1399 ptr += sprintf(ptr, "[promise expired]");
1400 if (promises->size() != 0)
1401 ptr += sprintf(ptr, "[unresolved promise]");
1403 model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
1407 * Returns whether the current completed trace is feasible, except for pending
1408 * release sequences.
1410 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
1412 return !is_infeasible() && promises->size() == 0;
1416 * Check if the current partial trace is infeasible. Does not check any
1417 * end-of-execution flags, which might rule out the execution. Thus, this is
1418 * useful only for ruling an execution as infeasible.
1419 * @return whether the current partial trace is infeasible.
1421 bool ModelChecker::is_infeasible() const
1423 return mo_graph->checkForCycles() ||
1424 priv->no_valid_reads ||
1425 priv->failed_promise ||
1426 priv->too_many_reads ||
1427 priv->bad_synchronization ||
1431 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1432 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1433 ModelAction *lastread = get_last_action(act->get_tid());
1434 lastread->process_rmw(act);
1435 if (act->is_rmw()) {
1436 if (lastread->get_reads_from())
1437 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1439 mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread);
1440 mo_graph->commitChanges();
1446 * Checks whether a thread has read from the same write for too many times
1447 * without seeing the effects of a later write.
1450 * 1) there must a different write that we could read from that would satisfy the modification order,
1451 * 2) we must have read from the same value in excess of maxreads times, and
1452 * 3) that other write must have been in the reads_from set for maxreads times.
1454 * If so, we decide that the execution is no longer feasible.
1456 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
1458 if (params.maxreads != 0) {
1459 if (curr->get_node()->get_read_from_size() <= 1)
1461 //Must make sure that execution is currently feasible... We could
1462 //accidentally clear by rolling back
1463 if (is_infeasible())
1465 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1466 int tid = id_to_int(curr->get_tid());
1469 if ((int)thrd_lists->size() <= tid)
1471 action_list_t *list = &(*thrd_lists)[tid];
1473 action_list_t::reverse_iterator rit = list->rbegin();
1474 /* Skip past curr */
1475 for (; (*rit) != curr; rit++)
1477 /* go past curr now */
1480 action_list_t::reverse_iterator ritcopy = rit;
1481 //See if we have enough reads from the same value
1483 for (; count < params.maxreads; rit++, count++) {
1484 if (rit == list->rend())
1486 ModelAction *act = *rit;
1487 if (!act->is_read())
1490 if (act->get_reads_from() != rf)
1492 if (act->get_node()->get_read_from_size() <= 1)
1495 for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
1497 const ModelAction *write = curr->get_node()->get_read_from_at(i);
1499 /* Need a different write */
1503 /* Test to see whether this is a feasible write to read from */
1504 /** NOTE: all members of read-from set should be
1505 * feasible, so we no longer check it here **/
1509 bool feasiblewrite = true;
1510 //new we need to see if this write works for everyone
1512 for (int loop = count; loop > 0; loop--, rit++) {
1513 ModelAction *act = *rit;
1514 bool foundvalue = false;
1515 for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
1516 if (act->get_node()->get_read_from_at(j) == write) {
1522 feasiblewrite = false;
1526 if (feasiblewrite) {
1527 priv->too_many_reads = true;
1535 * Updates the mo_graph with the constraints imposed from the current
1538 * Basic idea is the following: Go through each other thread and find
1539 * the last action that happened before our read. Two cases:
1541 * (1) The action is a write => that write must either occur before
1542 * the write we read from or be the write we read from.
1544 * (2) The action is a read => the write that that action read from
1545 * must occur before the write we read from or be the same write.
1547 * @param curr The current action. Must be a read.
1548 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
1549 * @return True if modification order edges were added; false otherwise
1551 template <typename rf_type>
1552 bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
1554 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1557 ASSERT(curr->is_read());
1559 /* Last SC fence in the current thread */
1560 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1562 /* Iterate over all threads */
1563 for (i = 0; i < thrd_lists->size(); i++) {
1564 /* Last SC fence in thread i */
1565 ModelAction *last_sc_fence_thread_local = NULL;
1566 if (int_to_id((int)i) != curr->get_tid())
1567 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
1569 /* Last SC fence in thread i, before last SC fence in current thread */
1570 ModelAction *last_sc_fence_thread_before = NULL;
1571 if (last_sc_fence_local)
1572 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1574 /* Iterate over actions in thread, starting from most recent */
1575 action_list_t *list = &(*thrd_lists)[i];
1576 action_list_t::reverse_iterator rit;
1577 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1578 ModelAction *act = *rit;
1580 if (act->is_write() && !act->equals(rf) && act != curr) {
1581 /* C++, Section 29.3 statement 5 */
1582 if (curr->is_seqcst() && last_sc_fence_thread_local &&
1583 *act < *last_sc_fence_thread_local) {
1584 added = mo_graph->addEdge(act, rf) || added;
1587 /* C++, Section 29.3 statement 4 */
1588 else if (act->is_seqcst() && last_sc_fence_local &&
1589 *act < *last_sc_fence_local) {
1590 added = mo_graph->addEdge(act, rf) || added;
1593 /* C++, Section 29.3 statement 6 */
1594 else if (last_sc_fence_thread_before &&
1595 *act < *last_sc_fence_thread_before) {
1596 added = mo_graph->addEdge(act, rf) || added;
1602 * Include at most one act per-thread that "happens
1603 * before" curr. Don't consider reflexively.
1605 if (act->happens_before(curr) && act != curr) {
1606 if (act->is_write()) {
1607 if (!act->equals(rf)) {
1608 added = mo_graph->addEdge(act, rf) || added;
1611 const ModelAction *prevreadfrom = act->get_reads_from();
1612 //if the previous read is unresolved, keep going...
1613 if (prevreadfrom == NULL)
1616 if (!prevreadfrom->equals(rf)) {
1617 added = mo_graph->addEdge(prevreadfrom, rf) || added;
1626 * All compatible, thread-exclusive promises must be ordered after any
1627 * concrete loads from the same thread
1629 for (unsigned int i = 0; i < promises->size(); i++)
1630 if ((*promises)[i]->is_compatible_exclusive(curr))
1631 added = mo_graph->addEdge(rf, (*promises)[i]) || added;
1637 * Updates the mo_graph with the constraints imposed from the current write.
1639 * Basic idea is the following: Go through each other thread and find
1640 * the lastest action that happened before our write. Two cases:
1642 * (1) The action is a write => that write must occur before
1645 * (2) The action is a read => the write that that action read from
1646 * must occur before the current write.
1648 * This method also handles two other issues:
1650 * (I) Sequential Consistency: Making sure that if the current write is
1651 * seq_cst, that it occurs after the previous seq_cst write.
1653 * (II) Sending the write back to non-synchronizing reads.
1655 * @param curr The current action. Must be a write.
1656 * @return True if modification order edges were added; false otherwise
1658 bool ModelChecker::w_modification_order(ModelAction *curr)
1660 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1663 ASSERT(curr->is_write());
1665 if (curr->is_seqcst()) {
1666 /* We have to at least see the last sequentially consistent write,
1667 so we are initialized. */
1668 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
1669 if (last_seq_cst != NULL) {
1670 added = mo_graph->addEdge(last_seq_cst, curr) || added;
1674 /* Last SC fence in the current thread */
1675 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1677 /* Iterate over all threads */
1678 for (i = 0; i < thrd_lists->size(); i++) {
1679 /* Last SC fence in thread i, before last SC fence in current thread */
1680 ModelAction *last_sc_fence_thread_before = NULL;
1681 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
1682 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1684 /* Iterate over actions in thread, starting from most recent */
1685 action_list_t *list = &(*thrd_lists)[i];
1686 action_list_t::reverse_iterator rit;
1687 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1688 ModelAction *act = *rit;
1691 * 1) If RMW and it actually read from something, then we
1692 * already have all relevant edges, so just skip to next
1695 * 2) If RMW and it didn't read from anything, we should
1696 * whatever edge we can get to speed up convergence.
1698 * 3) If normal write, we need to look at earlier actions, so
1699 * continue processing list.
1701 if (curr->is_rmw()) {
1702 if (curr->get_reads_from() != NULL)
1710 /* C++, Section 29.3 statement 7 */
1711 if (last_sc_fence_thread_before && act->is_write() &&
1712 *act < *last_sc_fence_thread_before) {
1713 added = mo_graph->addEdge(act, curr) || added;
1718 * Include at most one act per-thread that "happens
1721 if (act->happens_before(curr)) {
1723 * Note: if act is RMW, just add edge:
1725 * The following edge should be handled elsewhere:
1726 * readfrom(act) --mo--> act
1728 if (act->is_write())
1729 added = mo_graph->addEdge(act, curr) || added;
1730 else if (act->is_read()) {
1731 //if previous read accessed a null, just keep going
1732 if (act->get_reads_from() == NULL)
1734 added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
1737 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1738 !act->same_thread(curr)) {
1739 /* We have an action that:
1740 (1) did not happen before us
1741 (2) is a read and we are a write
1742 (3) cannot synchronize with us
1743 (4) is in a different thread
1745 that read could potentially read from our write. Note that
1746 these checks are overly conservative at this point, we'll
1747 do more checks before actually removing the
1751 if (thin_air_constraint_may_allow(curr, act)) {
1752 if (!is_infeasible())
1753 futurevalues->push_back(PendingFutureValue(curr, act));
1754 else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
1755 add_future_value(curr, act);
1762 * All compatible, thread-exclusive promises must be ordered after any
1763 * concrete stores to the same thread, or else they can be merged with
1766 for (unsigned int i = 0; i < promises->size(); i++)
1767 if ((*promises)[i]->is_compatible_exclusive(curr))
1768 added = mo_graph->addEdge(curr, (*promises)[i]) || added;
1773 /** Arbitrary reads from the future are not allowed. Section 29.3
1774 * part 9 places some constraints. This method checks one result of constraint
1775 * constraint. Others require compiler support. */
1776 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
1778 if (!writer->is_rmw())
1781 if (!reader->is_rmw())
1784 for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1785 if (search == reader)
1787 if (search->get_tid() == reader->get_tid() &&
1788 search->happens_before(reader))
1796 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1797 * some constraints. This method checks one the following constraint (others
1798 * require compiler support):
1800 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1802 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1804 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1806 /* Iterate over all threads */
1807 for (i = 0; i < thrd_lists->size(); i++) {
1808 const ModelAction *write_after_read = NULL;
1810 /* Iterate over actions in thread, starting from most recent */
1811 action_list_t *list = &(*thrd_lists)[i];
1812 action_list_t::reverse_iterator rit;
1813 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1814 ModelAction *act = *rit;
1816 /* Don't disallow due to act == reader */
1817 if (!reader->happens_before(act) || reader == act)
1819 else if (act->is_write())
1820 write_after_read = act;
1821 else if (act->is_read() && act->get_reads_from() != NULL)
1822 write_after_read = act->get_reads_from();
1825 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1832 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1833 * The ModelAction under consideration is expected to be taking part in
1834 * release/acquire synchronization as an object of the "reads from" relation.
1835 * Note that this can only provide release sequence support for RMW chains
1836 * which do not read from the future, as those actions cannot be traced until
1837 * their "promise" is fulfilled. Similarly, we may not even establish the
1838 * presence of a release sequence with certainty, as some modification order
1839 * constraints may be decided further in the future. Thus, this function
1840 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1841 * and a boolean representing certainty.
1843 * @param rf The action that might be part of a release sequence. Must be a
1845 * @param release_heads A pass-by-reference style return parameter. After
1846 * execution of this function, release_heads will contain the heads of all the
1847 * relevant release sequences, if any exists with certainty
1848 * @param pending A pass-by-reference style return parameter which is only used
1849 * when returning false (i.e., uncertain). Returns most information regarding
1850 * an uncertain release sequence, including any write operations that might
1851 * break the sequence.
1852 * @return true, if the ModelChecker is certain that release_heads is complete;
1855 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1856 rel_heads_list_t *release_heads,
1857 struct release_seq *pending) const
1859 /* Only check for release sequences if there are no cycles */
1860 if (mo_graph->checkForCycles())
1864 ASSERT(rf->is_write());
1866 if (rf->is_release())
1867 release_heads->push_back(rf);
1868 else if (rf->get_last_fence_release())
1869 release_heads->push_back(rf->get_last_fence_release());
1871 break; /* End of RMW chain */
1873 /** @todo Need to be smarter here... In the linux lock
1874 * example, this will run to the beginning of the program for
1876 /** @todo The way to be smarter here is to keep going until 1
1877 * thread has a release preceded by an acquire and you've seen
1880 /* acq_rel RMW is a sufficient stopping condition */
1881 if (rf->is_acquire() && rf->is_release())
1882 return true; /* complete */
1884 rf = rf->get_reads_from();
1887 /* read from future: need to settle this later */
1889 return false; /* incomplete */
1892 if (rf->is_release())
1893 return true; /* complete */
1895 /* else relaxed write
1896 * - check for fence-release in the same thread (29.8, stmt. 3)
1897 * - check modification order for contiguous subsequence
1898 * -> rf must be same thread as release */
1900 const ModelAction *fence_release = rf->get_last_fence_release();
1901 /* Synchronize with a fence-release unconditionally; we don't need to
1902 * find any more "contiguous subsequence..." for it */
1904 release_heads->push_back(fence_release);
1906 int tid = id_to_int(rf->get_tid());
1907 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
1908 action_list_t *list = &(*thrd_lists)[tid];
1909 action_list_t::const_reverse_iterator rit;
1911 /* Find rf in the thread list */
1912 rit = std::find(list->rbegin(), list->rend(), rf);
1913 ASSERT(rit != list->rend());
1915 /* Find the last {write,fence}-release */
1916 for (; rit != list->rend(); rit++) {
1917 if (fence_release && *(*rit) < *fence_release)
1919 if ((*rit)->is_release())
1922 if (rit == list->rend()) {
1923 /* No write-release in this thread */
1924 return true; /* complete */
1925 } else if (fence_release && *(*rit) < *fence_release) {
1926 /* The fence-release is more recent (and so, "stronger") than
1927 * the most recent write-release */
1928 return true; /* complete */
1929 } /* else, need to establish contiguous release sequence */
1930 ModelAction *release = *rit;
1932 ASSERT(rf->same_thread(release));
1934 pending->writes.clear();
1936 bool certain = true;
1937 for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1938 if (id_to_int(rf->get_tid()) == (int)i)
1940 list = &(*thrd_lists)[i];
1942 /* Can we ensure no future writes from this thread may break
1943 * the release seq? */
1944 bool future_ordered = false;
1946 ModelAction *last = get_last_action(int_to_id(i));
1947 Thread *th = get_thread(int_to_id(i));
1948 if ((last && rf->happens_before(last)) ||
1951 future_ordered = true;
1953 ASSERT(!th->is_model_thread() || future_ordered);
1955 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1956 const ModelAction *act = *rit;
1957 /* Reach synchronization -> this thread is complete */
1958 if (act->happens_before(release))
1960 if (rf->happens_before(act)) {
1961 future_ordered = true;
1965 /* Only non-RMW writes can break release sequences */
1966 if (!act->is_write() || act->is_rmw())
1969 /* Check modification order */
1970 if (mo_graph->checkReachable(rf, act)) {
1971 /* rf --mo--> act */
1972 future_ordered = true;
1975 if (mo_graph->checkReachable(act, release))
1976 /* act --mo--> release */
1978 if (mo_graph->checkReachable(release, act) &&
1979 mo_graph->checkReachable(act, rf)) {
1980 /* release --mo-> act --mo--> rf */
1981 return true; /* complete */
1983 /* act may break release sequence */
1984 pending->writes.push_back(act);
1987 if (!future_ordered)
1988 certain = false; /* This thread is uncertain */
1992 release_heads->push_back(release);
1993 pending->writes.clear();
1995 pending->release = release;
2002 * An interface for getting the release sequence head(s) with which a
2003 * given ModelAction must synchronize. This function only returns a non-empty
2004 * result when it can locate a release sequence head with certainty. Otherwise,
2005 * it may mark the internal state of the ModelChecker so that it will handle
2006 * the release sequence at a later time, causing @a acquire to update its
2007 * synchronization at some later point in execution.
2009 * @param acquire The 'acquire' action that may synchronize with a release
2011 * @param read The read action that may read from a release sequence; this may
2012 * be the same as acquire, or else an earlier action in the same thread (i.e.,
2013 * when 'acquire' is a fence-acquire)
2014 * @param release_heads A pass-by-reference return parameter. Will be filled
2015 * with the head(s) of the release sequence(s), if they exists with certainty.
2016 * @see ModelChecker::release_seq_heads
2018 void ModelChecker::get_release_seq_heads(ModelAction *acquire,
2019 ModelAction *read, rel_heads_list_t *release_heads)
2021 const ModelAction *rf = read->get_reads_from();
2022 struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
2023 sequence->acquire = acquire;
2024 sequence->read = read;
2026 if (!release_seq_heads(rf, release_heads, sequence)) {
2027 /* add act to 'lazy checking' list */
2028 pending_rel_seqs->push_back(sequence);
2030 snapshot_free(sequence);
2035 * Attempt to resolve all stashed operations that might synchronize with a
2036 * release sequence for a given location. This implements the "lazy" portion of
2037 * determining whether or not a release sequence was contiguous, since not all
2038 * modification order information is present at the time an action occurs.
2040 * @param location The location/object that should be checked for release
2041 * sequence resolutions. A NULL value means to check all locations.
2042 * @param work_queue The work queue to which to add work items as they are
2044 * @return True if any updates occurred (new synchronization, new mo_graph
2047 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
2049 bool updated = false;
2050 std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
2051 while (it != pending_rel_seqs->end()) {
2052 struct release_seq *pending = *it;
2053 ModelAction *acquire = pending->acquire;
2054 const ModelAction *read = pending->read;
2056 /* Only resolve sequences on the given location, if provided */
2057 if (location && read->get_location() != location) {
2062 const ModelAction *rf = read->get_reads_from();
2063 rel_heads_list_t release_heads;
2065 complete = release_seq_heads(rf, &release_heads, pending);
2066 for (unsigned int i = 0; i < release_heads.size(); i++) {
2067 if (!acquire->has_synchronized_with(release_heads[i])) {
2068 if (acquire->synchronize_with(release_heads[i]))
2071 set_bad_synchronization();
2076 /* Re-check all pending release sequences */
2077 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
2078 /* Re-check read-acquire for mo_graph edges */
2079 if (acquire->is_read())
2080 work_queue->push_back(MOEdgeWorkEntry(acquire));
2082 /* propagate synchronization to later actions */
2083 action_list_t::reverse_iterator rit = action_trace->rbegin();
2084 for (; (*rit) != acquire; rit++) {
2085 ModelAction *propagate = *rit;
2086 if (acquire->happens_before(propagate)) {
2087 propagate->synchronize_with(acquire);
2088 /* Re-check 'propagate' for mo_graph edges */
2089 work_queue->push_back(MOEdgeWorkEntry(propagate));
2094 it = pending_rel_seqs->erase(it);
2095 snapshot_free(pending);
2101 // If we resolved promises or data races, see if we have realized a data race.
2108 * Performs various bookkeeping operations for the current ModelAction. For
2109 * instance, adds action to the per-object, per-thread action vector and to the
2110 * action trace list of all thread actions.
2112 * @param act is the ModelAction to add.
2114 void ModelChecker::add_action_to_lists(ModelAction *act)
2116 int tid = id_to_int(act->get_tid());
2117 ModelAction *uninit = NULL;
2119 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
2120 if (list->empty() && act->is_atomic_var()) {
2121 uninit = new_uninitialized_action(act->get_location());
2122 uninit_id = id_to_int(uninit->get_tid());
2123 list->push_back(uninit);
2125 list->push_back(act);
2127 action_trace->push_back(act);
2129 action_trace->push_front(uninit);
2131 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
2132 if (tid >= (int)vec->size())
2133 vec->resize(priv->next_thread_id);
2134 (*vec)[tid].push_back(act);
2136 (*vec)[uninit_id].push_front(uninit);
2138 if ((int)thrd_last_action->size() <= tid)
2139 thrd_last_action->resize(get_num_threads());
2140 (*thrd_last_action)[tid] = act;
2142 (*thrd_last_action)[uninit_id] = uninit;
2144 if (act->is_fence() && act->is_release()) {
2145 if ((int)thrd_last_fence_release->size() <= tid)
2146 thrd_last_fence_release->resize(get_num_threads());
2147 (*thrd_last_fence_release)[tid] = act;
2150 if (act->is_wait()) {
2151 void *mutex_loc = (void *) act->get_value();
2152 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
2154 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
2155 if (tid >= (int)vec->size())
2156 vec->resize(priv->next_thread_id);
2157 (*vec)[tid].push_back(act);
2162 * @brief Get the last action performed by a particular Thread
2163 * @param tid The thread ID of the Thread in question
2164 * @return The last action in the thread
2166 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
2168 int threadid = id_to_int(tid);
2169 if (threadid < (int)thrd_last_action->size())
2170 return (*thrd_last_action)[id_to_int(tid)];
2176 * @brief Get the last fence release performed by a particular Thread
2177 * @param tid The thread ID of the Thread in question
2178 * @return The last fence release in the thread, if one exists; NULL otherwise
2180 ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
2182 int threadid = id_to_int(tid);
2183 if (threadid < (int)thrd_last_fence_release->size())
2184 return (*thrd_last_fence_release)[id_to_int(tid)];
2190 * Gets the last memory_order_seq_cst write (in the total global sequence)
2191 * performed on a particular object (i.e., memory location), not including the
2193 * @param curr The current ModelAction; also denotes the object location to
2195 * @return The last seq_cst write
2197 ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
2199 void *location = curr->get_location();
2200 action_list_t *list = get_safe_ptr_action(obj_map, location);
2201 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
2202 action_list_t::reverse_iterator rit;
2203 for (rit = list->rbegin(); rit != list->rend(); rit++)
2204 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
2210 * Gets the last memory_order_seq_cst fence (in the total global sequence)
2211 * performed in a particular thread, prior to a particular fence.
2212 * @param tid The ID of the thread to check
2213 * @param before_fence The fence from which to begin the search; if NULL, then
2214 * search for the most recent fence in the thread.
2215 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
2217 ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
2219 /* All fences should have NULL location */
2220 action_list_t *list = get_safe_ptr_action(obj_map, NULL);
2221 action_list_t::reverse_iterator rit = list->rbegin();
2224 for (; rit != list->rend(); rit++)
2225 if (*rit == before_fence)
2228 ASSERT(*rit == before_fence);
2232 for (; rit != list->rend(); rit++)
2233 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
2239 * Gets the last unlock operation performed on a particular mutex (i.e., memory
2240 * location). This function identifies the mutex according to the current
2241 * action, which is presumed to perform on the same mutex.
2242 * @param curr The current ModelAction; also denotes the object location to
2244 * @return The last unlock operation
2246 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
2248 void *location = curr->get_location();
2249 action_list_t *list = get_safe_ptr_action(obj_map, location);
2250 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
2251 action_list_t::reverse_iterator rit;
2252 for (rit = list->rbegin(); rit != list->rend(); rit++)
2253 if ((*rit)->is_unlock() || (*rit)->is_wait())
2258 ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
2260 ModelAction *parent = get_last_action(tid);
2262 parent = get_thread(tid)->get_creation();
2267 * Returns the clock vector for a given thread.
2268 * @param tid The thread whose clock vector we want
2269 * @return Desired clock vector
2271 ClockVector * ModelChecker::get_cv(thread_id_t tid) const
2273 return get_parent_action(tid)->get_cv();
2277 * Resolve a set of Promises with a current write. The set is provided in the
2278 * Node corresponding to @a write.
2279 * @param write The ModelAction that is fulfilling Promises
2280 * @return True if promises were resolved; false otherwise
2282 bool ModelChecker::resolve_promises(ModelAction *write)
2284 bool haveResolved = false;
2285 std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
2286 promise_list_t mustResolve, resolved;
2288 for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
2289 Promise *promise = (*promises)[promise_index];
2290 if (write->get_node()->get_promise(i)) {
2291 ModelAction *read = promise->get_action();
2292 read_from(read, write);
2293 //Make sure the promise's value matches the write's value
2294 ASSERT(promise->is_compatible(write));
2295 mo_graph->resolvePromise(read, write, &mustResolve);
2297 resolved.push_back(promise);
2298 promises->erase(promises->begin() + promise_index);
2299 actions_to_check.push_back(read);
2301 haveResolved = true;
2306 for (unsigned int i = 0; i < mustResolve.size(); i++) {
2307 if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
2309 priv->failed_promise = true;
2311 for (unsigned int i = 0; i < resolved.size(); i++)
2313 //Check whether reading these writes has made threads unable to
2316 for (unsigned int i = 0; i < actions_to_check.size(); i++) {
2317 ModelAction *read = actions_to_check[i];
2318 mo_check_promises(read, true);
2321 return haveResolved;
2325 * Compute the set of promises that could potentially be satisfied by this
2326 * action. Note that the set computation actually appears in the Node, not in
2328 * @param curr The ModelAction that may satisfy promises
2330 void ModelChecker::compute_promises(ModelAction *curr)
2332 for (unsigned int i = 0; i < promises->size(); i++) {
2333 Promise *promise = (*promises)[i];
2334 const ModelAction *act = promise->get_action();
2335 if (!act->happens_before(curr) &&
2337 !act->could_synchronize_with(curr) &&
2338 !act->same_thread(curr) &&
2339 act->get_location() == curr->get_location() &&
2340 promise->get_value() == curr->get_value()) {
2341 curr->get_node()->set_promise(i, act->is_rmw());
2346 /** Checks promises in response to change in ClockVector Threads. */
2347 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2349 for (unsigned int i = 0; i < promises->size(); i++) {
2350 Promise *promise = (*promises)[i];
2351 const ModelAction *act = promise->get_action();
2352 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2353 merge_cv->synchronized_since(act)) {
2354 if (promise->eliminate_thread(tid)) {
2355 //Promise has failed
2356 priv->failed_promise = true;
2363 void ModelChecker::check_promises_thread_disabled()
2365 for (unsigned int i = 0; i < promises->size(); i++) {
2366 Promise *promise = (*promises)[i];
2367 if (promise->has_failed()) {
2368 priv->failed_promise = true;
2375 * @brief Checks promises in response to addition to modification order for
2378 * We test whether threads are still available for satisfying promises after an
2379 * addition to our modification order constraints. Those that are unavailable
2380 * are "eliminated". Once all threads are eliminated from satisfying a promise,
2381 * that promise has failed.
2383 * @param act The ModelAction which updated the modification order
2384 * @param is_read_check Should be true if act is a read and we must check for
2385 * updates to the store from which it read (there is a distinction here for
2386 * RMW's, which are both a load and a store)
2388 void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
2390 const ModelAction *write = is_read_check ? act->get_reads_from() : act;
2392 for (unsigned int i = 0; i < promises->size(); i++) {
2393 Promise *promise = (*promises)[i];
2394 const ModelAction *pread = promise->get_action();
2396 // Is this promise on the same location?
2397 if (!pread->same_var(write))
2400 if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
2401 priv->failed_promise = true;
2405 // Don't do any lookups twice for the same thread
2406 if (!promise->thread_is_available(act->get_tid()))
2409 if (mo_graph->checkReachable(promise, write)) {
2410 if (mo_graph->checkPromise(write, promise)) {
2411 priv->failed_promise = true;
2419 * Compute the set of writes that may break the current pending release
2420 * sequence. This information is extracted from previou release sequence
2423 * @param curr The current ModelAction. Must be a release sequence fixup
2426 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2428 if (pending_rel_seqs->empty())
2431 struct release_seq *pending = pending_rel_seqs->back();
2432 for (unsigned int i = 0; i < pending->writes.size(); i++) {
2433 const ModelAction *write = pending->writes[i];
2434 curr->get_node()->add_relseq_break(write);
2437 /* NULL means don't break the sequence; just synchronize */
2438 curr->get_node()->add_relseq_break(NULL);
2442 * Build up an initial set of all past writes that this 'read' action may read
2443 * from. This set is determined by the clock vector's "happens before"
2445 * @param curr is the current ModelAction that we are exploring; it must be a
2448 void ModelChecker::build_reads_from_past(ModelAction *curr)
2450 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2452 ASSERT(curr->is_read());
2454 ModelAction *last_sc_write = NULL;
2456 if (curr->is_seqcst())
2457 last_sc_write = get_last_seq_cst_write(curr);
2459 /* Iterate over all threads */
2460 for (i = 0; i < thrd_lists->size(); i++) {
2461 /* Iterate over actions in thread, starting from most recent */
2462 action_list_t *list = &(*thrd_lists)[i];
2463 action_list_t::reverse_iterator rit;
2464 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2465 ModelAction *act = *rit;
2467 /* Only consider 'write' actions */
2468 if (!act->is_write() || act == curr)
2471 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2472 bool allow_read = true;
2474 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
2476 else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
2480 /* Only add feasible reads */
2481 mo_graph->startChanges();
2482 r_modification_order(curr, act);
2483 if (!is_infeasible())
2484 curr->get_node()->add_read_from(act);
2485 mo_graph->rollbackChanges();
2488 /* Include at most one act per-thread that "happens before" curr */
2489 if (act->happens_before(curr))
2493 /* We may find no valid may-read-from only if the execution is doomed */
2494 if (!curr->get_node()->get_read_from_size()) {
2495 priv->no_valid_reads = true;
2499 if (DBG_ENABLED()) {
2500 model_print("Reached read action:\n");
2502 model_print("Printing may_read_from\n");
2503 curr->get_node()->print_may_read_from();
2504 model_print("End printing may_read_from\n");
2508 bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
2511 /* UNINIT actions don't have a Node, and they never sleep */
2512 if (write->is_uninitialized())
2514 Node *prevnode = write->get_node()->get_parent();
2516 bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
2517 if (write->is_release() && thread_sleep)
2519 if (!write->is_rmw()) {
2522 if (write->get_reads_from() == NULL)
2524 write = write->get_reads_from();
2529 * @brief Create a new action representing an uninitialized atomic
2530 * @param location The memory location of the atomic object
2531 * @return A pointer to a new ModelAction
2533 ModelAction * ModelChecker::new_uninitialized_action(void *location) const
2535 ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
2536 act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
2537 act->create_cv(NULL);
2541 static void print_list(action_list_t *list)
2543 action_list_t::iterator it;
2545 model_print("---------------------------------------------------------------------\n");
2547 unsigned int hash = 0;
2549 for (it = list->begin(); it != list->end(); it++) {
2551 hash = hash^(hash<<3)^((*it)->hash());
2553 model_print("HASH %u\n", hash);
2554 model_print("---------------------------------------------------------------------\n");
2557 #if SUPPORT_MOD_ORDER_DUMP
2558 void ModelChecker::dumpGraph(char *filename) const
2561 sprintf(buffer, "%s.dot", filename);
2562 FILE *file = fopen(buffer, "w");
2563 fprintf(file, "digraph %s {\n", filename);
2564 mo_graph->dumpNodes(file);
2565 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
2567 for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2568 ModelAction *action = *it;
2569 if (action->is_read()) {
2570 fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
2571 if (action->get_reads_from() != NULL)
2572 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2574 if (thread_array[action->get_tid()] != NULL) {
2575 fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2578 thread_array[action->get_tid()] = action;
2580 fprintf(file, "}\n");
2581 model_free(thread_array);
2586 /** @brief Prints an execution trace summary. */
2587 void ModelChecker::print_summary() const
2589 #if SUPPORT_MOD_ORDER_DUMP
2590 char buffername[100];
2591 sprintf(buffername, "exec%04u", stats.num_total);
2592 mo_graph->dumpGraphToFile(buffername);
2593 sprintf(buffername, "graph%04u", stats.num_total);
2594 dumpGraph(buffername);
2597 model_print("Execution %d:", stats.num_total);
2598 if (isfeasibleprefix())
2601 print_infeasibility(" INFEASIBLE");
2602 print_list(action_trace);
2607 * Add a Thread to the system for the first time. Should only be called once
2609 * @param t The Thread to add
2611 void ModelChecker::add_thread(Thread *t)
2613 thread_map->put(id_to_int(t->get_id()), t);
2614 scheduler->add_thread(t);
2618 * Removes a thread from the scheduler.
2619 * @param the thread to remove.
2621 void ModelChecker::remove_thread(Thread *t)
2623 scheduler->remove_thread(t);
2627 * @brief Get a Thread reference by its ID
2628 * @param tid The Thread's ID
2629 * @return A Thread reference
2631 Thread * ModelChecker::get_thread(thread_id_t tid) const
2633 return thread_map->get(id_to_int(tid));
2637 * @brief Get a reference to the Thread in which a ModelAction was executed
2638 * @param act The ModelAction
2639 * @return A Thread reference
2641 Thread * ModelChecker::get_thread(const ModelAction *act) const
2643 return get_thread(act->get_tid());
2647 * @brief Check if a Thread is currently enabled
2648 * @param t The Thread to check
2649 * @return True if the Thread is currently enabled
2651 bool ModelChecker::is_enabled(Thread *t) const
2653 return scheduler->is_enabled(t);
2657 * @brief Check if a Thread is currently enabled
2658 * @param tid The ID of the Thread to check
2659 * @return True if the Thread is currently enabled
2661 bool ModelChecker::is_enabled(thread_id_t tid) const
2663 return scheduler->is_enabled(tid);
2667 * Switch from a user-context to the "master thread" context (a.k.a. system
2668 * context). This switch is made with the intention of exploring a particular
2669 * model-checking action (described by a ModelAction object). Must be called
2670 * from a user-thread context.
2672 * @param act The current action that will be explored. May be NULL only if
2673 * trace is exiting via an assertion (see ModelChecker::set_assert and
2674 * ModelChecker::has_asserted).
2675 * @return Return the value returned by the current action
2677 uint64_t ModelChecker::switch_to_master(ModelAction *act)
2680 Thread *old = thread_current();
2681 set_current_action(act);
2682 if (Thread::swap(old, &system_context) < 0) {
2683 perror("swap threads");
2686 return old->get_return_value();
2690 * Takes the next step in the execution, if possible.
2691 * @param curr The current step to take
2692 * @return Returns true (success) if a step was taken and false otherwise.
2694 bool ModelChecker::take_step(ModelAction *curr)
2699 Thread *curr_thrd = get_thread(curr);
2700 ASSERT(curr_thrd->get_state() == THREAD_READY);
2702 curr = check_current_action(curr);
2704 /* Infeasible -> don't take any more steps */
2705 if (is_infeasible())
2707 else if (isfeasibleprefix() && have_bug_reports()) {
2712 if (params.bound != 0)
2713 if (priv->used_sequence_numbers > params.bound)
2716 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
2717 scheduler->remove_thread(curr_thrd);
2719 Thread *next_thrd = get_next_thread(curr);
2720 next_thrd = scheduler->next_thread(next_thrd);
2722 DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
2723 next_thrd ? id_to_int(next_thrd->get_id()) : -1);
2726 * Launch end-of-execution release sequence fixups only when there are:
2728 * (1) no more user threads to run (or when execution replay chooses
2729 * the 'model_thread')
2730 * (2) pending release sequences
2731 * (3) pending assertions (i.e., data races)
2732 * (4) no pending promises
2734 if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
2735 is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
2736 model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2737 pending_rel_seqs->size());
2738 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2739 std::memory_order_seq_cst, NULL, VALUE_NONE,
2741 set_current_action(fixup);
2745 /* next_thrd == NULL -> don't take any more steps */
2749 if (next_thrd->get_pending() != NULL) {
2750 /* restart a pending action */
2751 set_current_action(next_thrd->get_pending());
2752 next_thrd->set_pending(NULL);
2756 /* Return false only if swap fails with an error */
2757 return (Thread::swap(&system_context, next_thrd) == 0);
2760 /** Wrapper to run the user's main function, with appropriate arguments */
2761 void user_main_wrapper(void *)
2763 user_main(model->params.argc, model->params.argv);
2766 /** @brief Run ModelChecker for the user program */
2767 void ModelChecker::run()
2771 Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
2775 /* Run user thread up to its first action */
2776 scheduler->next_thread(t);
2777 Thread::swap(&system_context, t);
2779 /* Wait for all threads to complete */
2780 while (take_step(priv->current_action));
2781 } while (next_execution());