9 #include "snapshot-interface.h"
11 #include "clockvector.h"
12 #include "cyclegraph.h"
15 #include "threads-model.h"
18 #define INITIAL_THREAD_ID 0
23 bug_message(const char *str) {
24 const char *fmt = " [BUG] %s\n";
25 msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
26 sprintf(msg, fmt, str);
28 ~bug_message() { if (msg) snapshot_free(msg); }
31 void print() { model_print("%s", msg); }
37 * Structure for holding small ModelChecker members that should be snapshotted
39 struct model_snapshot_members {
40 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),
51 ~model_snapshot_members() {
52 for (unsigned int i = 0; i < bugs.size(); i++)
57 ModelAction *current_action;
58 unsigned int next_thread_id;
59 modelclock_t used_sequence_numbers;
61 ModelAction *next_backtrack;
62 std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
63 struct execution_stats stats;
68 /** @brief Constructor */
69 ModelChecker::ModelChecker(struct model_params params) :
70 /* Initialize default scheduler */
72 scheduler(new Scheduler()),
74 earliest_diverge(NULL),
75 action_trace(new action_list_t()),
76 thread_map(new HashTable<int, Thread *, int>()),
77 obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
78 lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
79 condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
80 obj_thrd_map(new HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 >()),
81 promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
82 futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
83 pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
84 thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
85 node_stack(new NodeStack()),
86 priv(new struct model_snapshot_members()),
87 mo_graph(new CycleGraph()),
88 failed_promise(false),
89 too_many_reads(false),
91 bad_synchronization(false)
93 /* Initialize a model-checker thread, for special ModelActions */
94 model_thread = new Thread(get_next_id());
95 thread_map->put(id_to_int(model_thread->get_id()), model_thread);
98 /** @brief Destructor */
99 ModelChecker::~ModelChecker()
101 for (unsigned int i = 0; i < get_num_threads(); i++)
102 delete thread_map->get(i);
107 delete lock_waiters_map;
108 delete condvar_waiters_map;
111 for (unsigned int i = 0; i < promises->size(); i++)
112 delete (*promises)[i];
115 delete pending_rel_seqs;
117 delete thrd_last_action;
124 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
125 action_list_t * tmp=hash->get(ptr);
127 tmp=new action_list_t();
133 static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr) {
134 std::vector<action_list_t> * tmp=hash->get(ptr);
136 tmp=new std::vector<action_list_t>();
143 * Restores user program to initial state and resets all model-checker data
146 void ModelChecker::reset_to_initial_state()
148 DEBUG("+++ Resetting to initial state +++\n");
149 node_stack->reset_execution();
150 failed_promise = false;
151 too_many_reads = false;
152 bad_synchronization = false;
155 /* Print all model-checker output before rollback */
158 snapshotObject->backTrackBeforeStep(0);
161 /** @return a thread ID for a new Thread */
162 thread_id_t ModelChecker::get_next_id()
164 return priv->next_thread_id++;
167 /** @return the number of user threads created during this execution */
168 unsigned int ModelChecker::get_num_threads() const
170 return priv->next_thread_id;
173 /** @return The currently executing Thread. */
174 Thread * ModelChecker::get_current_thread()
176 return scheduler->get_current_thread();
179 /** @return a sequence number for a new ModelAction */
180 modelclock_t ModelChecker::get_next_seq_num()
182 return ++priv->used_sequence_numbers;
185 Node * ModelChecker::get_curr_node() {
186 return node_stack->get_head();
190 * @brief Choose the next thread to execute.
192 * This function chooses the next thread that should execute. It can force the
193 * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
194 * followed by a THREAD_START, or it can enforce execution replay/backtracking.
195 * The model-checker may have no preference regarding the next thread (i.e.,
196 * when exploring a new execution ordering), in which case this will return
198 * @param curr The current ModelAction. This action might guide the choice of
200 * @return The next thread to run. If the model-checker has no preference, NULL.
202 Thread * ModelChecker::get_next_thread(ModelAction *curr)
207 /* Do not split atomic actions. */
209 return thread_current();
210 /* The THREAD_CREATE action points to the created Thread */
211 else if (curr->get_type() == THREAD_CREATE)
212 return (Thread *)curr->get_location();
215 /* Have we completed exploring the preselected path? */
219 /* Else, we are trying to replay an execution */
220 ModelAction *next = node_stack->get_next()->get_action();
222 if (next == diverge) {
223 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
224 earliest_diverge=diverge;
226 Node *nextnode = next->get_node();
227 Node *prevnode = nextnode->get_parent();
228 scheduler->update_sleep_set(prevnode);
230 /* Reached divergence point */
231 if (nextnode->increment_misc()) {
232 /* The next node will try to satisfy a different misc_index values. */
233 tid = next->get_tid();
234 node_stack->pop_restofstack(2);
235 } else if (nextnode->increment_promise()) {
236 /* The next node will try to satisfy a different set of promises. */
237 tid = next->get_tid();
238 node_stack->pop_restofstack(2);
239 } else if (nextnode->increment_read_from()) {
240 /* The next node will read from a different value. */
241 tid = next->get_tid();
242 node_stack->pop_restofstack(2);
243 } else if (nextnode->increment_future_value()) {
244 /* The next node will try to read from a different future value. */
245 tid = next->get_tid();
246 node_stack->pop_restofstack(2);
247 } else if (nextnode->increment_relseq_break()) {
248 /* The next node will try to resolve a release sequence differently */
249 tid = next->get_tid();
250 node_stack->pop_restofstack(2);
252 /* Make a different thread execute for next step */
253 scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
254 tid = prevnode->get_next_backtrack();
255 /* Make sure the backtracked thread isn't sleeping. */
256 node_stack->pop_restofstack(1);
257 if (diverge==earliest_diverge) {
258 earliest_diverge=prevnode->get_action();
261 /* The correct sleep set is in the parent node. */
264 DEBUG("*** Divergence point ***\n");
268 tid = next->get_tid();
270 DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
271 ASSERT(tid != THREAD_ID_T_NONE);
272 return thread_map->get(id_to_int(tid));
276 * We need to know what the next actions of all threads in the sleep
277 * set will be. This method computes them and stores the actions at
278 * the corresponding thread object's pending action.
281 void ModelChecker::execute_sleep_set() {
282 for(unsigned int i=0;i<get_num_threads();i++) {
283 thread_id_t tid=int_to_id(i);
284 Thread *thr=get_thread(tid);
285 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
286 thr->get_pending() == NULL ) {
287 thr->set_state(THREAD_RUNNING);
288 scheduler->next_thread(thr);
289 Thread::swap(&system_context, thr);
290 priv->current_action->set_sleep_flag();
291 thr->set_pending(priv->current_action);
294 priv->current_action = NULL;
297 void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
298 for(unsigned int i=0;i<get_num_threads();i++) {
299 thread_id_t tid=int_to_id(i);
300 Thread *thr=get_thread(tid);
301 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
302 ModelAction *pending_act=thr->get_pending();
303 if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) {
304 //Remove this thread from sleep set
305 scheduler->remove_sleep(thr);
312 * Check if we are in a deadlock. Should only be called at the end of an
313 * execution, although it should not give false positives in the middle of an
314 * execution (there should be some ENABLED thread).
316 * @return True if program is in a deadlock; false otherwise
318 bool ModelChecker::is_deadlocked() const
320 bool blocking_threads = false;
321 for (unsigned int i = 0; i < get_num_threads(); i++) {
322 thread_id_t tid = int_to_id(i);
325 Thread *t = get_thread(tid);
326 if (!t->is_model_thread() && t->get_pending())
327 blocking_threads = true;
329 return blocking_threads;
333 * Check if this is a complete execution. That is, have all thread completed
334 * execution (rather than exiting because sleep sets have forced a redundant
337 * @return True if the execution is complete.
339 bool ModelChecker::is_complete_execution() const
341 for (unsigned int i = 0; i < get_num_threads(); i++)
342 if (is_enabled(int_to_id(i)))
348 * @brief Assert a bug in the executing program.
350 * Use this function to assert any sort of bug in the user program. If the
351 * current trace is feasible (actually, a prefix of some feasible execution),
352 * then this execution will be aborted, printing the appropriate message. If
353 * the current trace is not yet feasible, the error message will be stashed and
354 * printed if the execution ever becomes feasible.
356 * @param msg Descriptive message for the bug (do not include newline char)
357 * @return True if bug is immediately-feasible
359 bool ModelChecker::assert_bug(const char *msg)
361 priv->bugs.push_back(new bug_message(msg));
363 if (isfeasibleprefix()) {
371 * @brief Assert a bug in the executing program, asserted by a user thread
372 * @see ModelChecker::assert_bug
373 * @param msg Descriptive message for the bug (do not include newline char)
375 void ModelChecker::assert_user_bug(const char *msg)
377 /* If feasible bug, bail out now */
379 switch_to_master(NULL);
382 /** @return True, if any bugs have been reported for this execution */
383 bool ModelChecker::have_bug_reports() const
385 return priv->bugs.size() != 0;
388 /** @brief Print bug report listing for this execution (if any bugs exist) */
389 void ModelChecker::print_bugs() const
391 if (have_bug_reports()) {
392 model_print("Bug report: %zu bug%s detected\n",
394 priv->bugs.size() > 1 ? "s" : "");
395 for (unsigned int i = 0; i < priv->bugs.size(); i++)
396 priv->bugs[i]->print();
401 * @brief Record end-of-execution stats
403 * Must be run when exiting an execution. Records various stats.
404 * @see struct execution_stats
406 void ModelChecker::record_stats()
409 if (!isfinalfeasible())
410 stats.num_infeasible++;
411 else if (have_bug_reports())
412 stats.num_buggy_executions++;
413 else if (is_complete_execution())
414 stats.num_complete++;
416 stats.num_redundant++;
419 /** @brief Print execution stats */
420 void ModelChecker::print_stats() const
422 model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
423 model_print("Number of redundant executions: %d\n", stats.num_redundant);
424 model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
425 model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
426 model_print("Total executions: %d\n", stats.num_total);
427 model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
431 * @brief End-of-exeuction print
432 * @param printbugs Should any existing bugs be printed?
434 void ModelChecker::print_execution(bool printbugs) const
436 print_program_output();
438 if (DBG_ENABLED() || params.verbose) {
439 model_print("Earliest divergence point since last feasible execution:\n");
440 if (earliest_diverge)
441 earliest_diverge->print();
443 model_print("(Not set)\n");
449 /* Don't print invalid bugs */
458 * Queries the model-checker for more executions to explore and, if one
459 * exists, resets the model-checker state to execute a new execution.
461 * @return If there are more executions to explore, return true. Otherwise,
464 bool ModelChecker::next_execution()
467 /* Is this execution a feasible execution that's worth bug-checking? */
468 bool complete = isfinalfeasible() && (is_complete_execution() ||
471 /* End-of-execution bug checks */
474 assert_bug("Deadlock detected");
482 if (DBG_ENABLED() || params.verbose || have_bug_reports())
483 print_execution(complete);
485 clear_program_output();
488 earliest_diverge = NULL;
490 if ((diverge = get_next_backtrack()) == NULL)
494 model_print("Next execution will diverge at:\n");
498 reset_to_initial_state();
502 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
504 switch (act->get_type()) {
508 /* Optimization: relaxed operations don't need backtracking */
509 if (act->is_relaxed())
511 /* linear search: from most recent to oldest */
512 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
513 action_list_t::reverse_iterator rit;
514 for (rit = list->rbegin(); rit != list->rend(); rit++) {
515 ModelAction *prev = *rit;
516 if (prev->could_synchronize_with(act))
522 case ATOMIC_TRYLOCK: {
523 /* linear search: from most recent to oldest */
524 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
525 action_list_t::reverse_iterator rit;
526 for (rit = list->rbegin(); rit != list->rend(); rit++) {
527 ModelAction *prev = *rit;
528 if (act->is_conflicting_lock(prev))
533 case ATOMIC_UNLOCK: {
534 /* linear search: from most recent to oldest */
535 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
536 action_list_t::reverse_iterator rit;
537 for (rit = list->rbegin(); rit != list->rend(); rit++) {
538 ModelAction *prev = *rit;
539 if (!act->same_thread(prev)&&prev->is_failed_trylock())
545 /* linear search: from most recent to oldest */
546 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
547 action_list_t::reverse_iterator rit;
548 for (rit = list->rbegin(); rit != list->rend(); rit++) {
549 ModelAction *prev = *rit;
550 if (!act->same_thread(prev)&&prev->is_failed_trylock())
552 if (!act->same_thread(prev)&&prev->is_notify())
558 case ATOMIC_NOTIFY_ALL:
559 case ATOMIC_NOTIFY_ONE: {
560 /* linear search: from most recent to oldest */
561 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
562 action_list_t::reverse_iterator rit;
563 for (rit = list->rbegin(); rit != list->rend(); rit++) {
564 ModelAction *prev = *rit;
565 if (!act->same_thread(prev)&&prev->is_wait())
576 /** This method finds backtracking points where we should try to
577 * reorder the parameter ModelAction against.
579 * @param the ModelAction to find backtracking points for.
581 void ModelChecker::set_backtracking(ModelAction *act)
583 Thread *t = get_thread(act);
584 ModelAction * prev = get_last_conflict(act);
588 Node * node = prev->get_node()->get_parent();
590 int low_tid, high_tid;
591 if (node->is_enabled(t)) {
592 low_tid = id_to_int(act->get_tid());
593 high_tid = low_tid+1;
596 high_tid = get_num_threads();
599 for(int i = low_tid; i < high_tid; i++) {
600 thread_id_t tid = int_to_id(i);
602 /* Make sure this thread can be enabled here. */
603 if (i >= node->get_num_threads())
606 /* Don't backtrack into a point where the thread is disabled or sleeping. */
607 if (node->enabled_status(tid)!=THREAD_ENABLED)
610 /* Check if this has been explored already */
611 if (node->has_been_explored(tid))
614 /* See if fairness allows */
615 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
617 for(int t=0;t<node->get_num_threads();t++) {
618 thread_id_t tother=int_to_id(t);
619 if (node->is_enabled(tother) && node->has_priority(tother)) {
627 /* Cache the latest backtracking point */
628 if (!priv->next_backtrack || *prev > *priv->next_backtrack)
629 priv->next_backtrack = prev;
631 /* If this is a new backtracking point, mark the tree */
632 if (!node->set_backtrack(tid))
634 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
635 id_to_int(prev->get_tid()),
636 id_to_int(t->get_id()));
645 * Returns last backtracking point. The model checker will explore a different
646 * path for this point in the next execution.
647 * @return The ModelAction at which the next execution should diverge.
649 ModelAction * ModelChecker::get_next_backtrack()
651 ModelAction *next = priv->next_backtrack;
652 priv->next_backtrack = NULL;
657 * Processes a read or rmw model action.
658 * @param curr is the read model action to process.
659 * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
660 * @return True if processing this read updates the mo_graph.
662 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
664 uint64_t value = VALUE_NONE;
665 bool updated = false;
667 const ModelAction *reads_from = curr->get_node()->get_read_from();
668 if (reads_from != NULL) {
669 mo_graph->startChanges();
671 value = reads_from->get_value();
672 bool r_status = false;
674 if (!second_part_of_rmw) {
675 check_recency(curr, reads_from);
676 r_status = r_modification_order(curr, reads_from);
680 if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
681 mo_graph->rollbackChanges();
682 too_many_reads = false;
686 curr->read_from(reads_from);
687 mo_graph->commitChanges();
688 mo_check_promises(curr->get_tid(), reads_from);
691 } else if (!second_part_of_rmw) {
692 /* Read from future value */
693 value = curr->get_node()->get_future_value();
694 modelclock_t expiration = curr->get_node()->get_future_value_expiration();
695 curr->read_from(NULL);
696 Promise *valuepromise = new Promise(curr, value, expiration);
697 promises->push_back(valuepromise);
699 get_thread(curr)->set_return_value(value);
705 * Processes a lock, trylock, or unlock model action. @param curr is
706 * the read model action to process.
708 * The try lock operation checks whether the lock is taken. If not,
709 * it falls to the normal lock operation case. If so, it returns
712 * The lock operation has already been checked that it is enabled, so
713 * it just grabs the lock and synchronizes with the previous unlock.
715 * The unlock operation has to re-enable all of the threads that are
716 * waiting on the lock.
718 * @return True if synchronization was updated; false otherwise
720 bool ModelChecker::process_mutex(ModelAction *curr) {
721 std::mutex *mutex=NULL;
722 struct std::mutex_state *state=NULL;
724 if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
725 mutex = (std::mutex *)curr->get_location();
726 state = mutex->get_state();
727 } else if(curr->is_wait()) {
728 mutex = (std::mutex *)curr->get_value();
729 state = mutex->get_state();
732 switch (curr->get_type()) {
733 case ATOMIC_TRYLOCK: {
734 bool success = !state->islocked;
735 curr->set_try_lock(success);
737 get_thread(curr)->set_return_value(0);
740 get_thread(curr)->set_return_value(1);
742 //otherwise fall into the lock case
744 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
745 assert_bug("Lock access before initialization");
746 state->islocked = true;
747 ModelAction *unlock = get_last_unlock(curr);
748 //synchronize with the previous unlock statement
749 if (unlock != NULL) {
750 curr->synchronize_with(unlock);
755 case ATOMIC_UNLOCK: {
757 state->islocked = false;
758 //wake up the other threads
759 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
760 //activate all the waiting threads
761 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
762 scheduler->wake(get_thread(*rit));
769 state->islocked = false;
770 //wake up the other threads
771 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
772 //activate all the waiting threads
773 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
774 scheduler->wake(get_thread(*rit));
777 //check whether we should go to sleep or not...simulate spurious failures
778 if (curr->get_node()->get_misc()==0) {
779 get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
781 scheduler->sleep(get_current_thread());
785 case ATOMIC_NOTIFY_ALL: {
786 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
787 //activate all the waiting threads
788 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
789 scheduler->wake(get_thread(*rit));
794 case ATOMIC_NOTIFY_ONE: {
795 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
796 int wakeupthread=curr->get_node()->get_misc();
797 action_list_t::iterator it = waiters->begin();
798 advance(it, wakeupthread);
799 scheduler->wake(get_thread(*it));
811 * Process a write ModelAction
812 * @param curr The ModelAction to process
813 * @return True if the mo_graph was updated or promises were resolved
815 bool ModelChecker::process_write(ModelAction *curr)
817 bool updated_mod_order = w_modification_order(curr);
818 bool updated_promises = resolve_promises(curr);
820 if (promises->size() == 0) {
821 for (unsigned int i = 0; i < futurevalues->size(); i++) {
822 struct PendingFutureValue pfv = (*futurevalues)[i];
823 //Do more ambitious checks now that mo is more complete
824 if (mo_may_allow(pfv.writer, pfv.act)&&
825 pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
826 (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
827 priv->next_backtrack = pfv.act;
829 futurevalues->resize(0);
832 mo_graph->commitChanges();
833 mo_check_promises(curr->get_tid(), curr);
835 get_thread(curr)->set_return_value(VALUE_NONE);
836 return updated_mod_order || updated_promises;
840 * @brief Process the current action for thread-related activity
842 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
843 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
844 * synchronization, etc. This function is a no-op for non-THREAD actions
845 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
847 * @param curr The current action
848 * @return True if synchronization was updated or a thread completed
850 bool ModelChecker::process_thread_action(ModelAction *curr)
852 bool updated = false;
854 switch (curr->get_type()) {
855 case THREAD_CREATE: {
856 Thread *th = (Thread *)curr->get_location();
857 th->set_creation(curr);
861 Thread *blocking = (Thread *)curr->get_location();
862 ModelAction *act = get_last_action(blocking->get_id());
863 curr->synchronize_with(act);
864 updated = true; /* trigger rel-seq checks */
867 case THREAD_FINISH: {
868 Thread *th = get_thread(curr);
869 while (!th->wait_list_empty()) {
870 ModelAction *act = th->pop_wait_list();
871 scheduler->wake(get_thread(act));
874 updated = true; /* trigger rel-seq checks */
878 check_promises(curr->get_tid(), NULL, curr->get_cv());
889 * @brief Process the current action for release sequence fixup activity
891 * Performs model-checker release sequence fixups for the current action,
892 * forcing a single pending release sequence to break (with a given, potential
893 * "loose" write) or to complete (i.e., synchronize). If a pending release
894 * sequence forms a complete release sequence, then we must perform the fixup
895 * synchronization, mo_graph additions, etc.
897 * @param curr The current action; must be a release sequence fixup action
898 * @param work_queue The work queue to which to add work items as they are
901 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
903 const ModelAction *write = curr->get_node()->get_relseq_break();
904 struct release_seq *sequence = pending_rel_seqs->back();
905 pending_rel_seqs->pop_back();
907 ModelAction *acquire = sequence->acquire;
908 const ModelAction *rf = sequence->rf;
909 const ModelAction *release = sequence->release;
913 ASSERT(release->same_thread(rf));
917 * @todo Forcing a synchronization requires that we set
918 * modification order constraints. For instance, we can't allow
919 * a fixup sequence in which two separate read-acquire
920 * operations read from the same sequence, where the first one
921 * synchronizes and the other doesn't. Essentially, we can't
922 * allow any writes to insert themselves between 'release' and
926 /* Must synchronize */
927 if (!acquire->synchronize_with(release)) {
928 set_bad_synchronization();
931 /* Re-check all pending release sequences */
932 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
933 /* Re-check act for mo_graph edges */
934 work_queue->push_back(MOEdgeWorkEntry(acquire));
936 /* propagate synchronization to later actions */
937 action_list_t::reverse_iterator rit = action_trace->rbegin();
938 for (; (*rit) != acquire; rit++) {
939 ModelAction *propagate = *rit;
940 if (acquire->happens_before(propagate)) {
941 propagate->synchronize_with(acquire);
942 /* Re-check 'propagate' for mo_graph edges */
943 work_queue->push_back(MOEdgeWorkEntry(propagate));
947 /* Break release sequence with new edges:
948 * release --mo--> write --mo--> rf */
949 mo_graph->addEdge(release, write);
950 mo_graph->addEdge(write, rf);
953 /* See if we have realized a data race */
958 * Initialize the current action by performing one or more of the following
959 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
960 * in the NodeStack, manipulating backtracking sets, allocating and
961 * initializing clock vectors, and computing the promises to fulfill.
963 * @param curr The current action, as passed from the user context; may be
964 * freed/invalidated after the execution of this function, with a different
965 * action "returned" its place (pass-by-reference)
966 * @return True if curr is a newly-explored action; false otherwise
968 bool ModelChecker::initialize_curr_action(ModelAction **curr)
970 ModelAction *newcurr;
972 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
973 newcurr = process_rmw(*curr);
976 if (newcurr->is_rmw())
977 compute_promises(newcurr);
983 (*curr)->set_seq_number(get_next_seq_num());
985 newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
987 /* First restore type and order in case of RMW operation */
988 if ((*curr)->is_rmwr())
989 newcurr->copy_typeandorder(*curr);
991 ASSERT((*curr)->get_location() == newcurr->get_location());
992 newcurr->copy_from_new(*curr);
994 /* Discard duplicate ModelAction; use action from NodeStack */
997 /* Always compute new clock vector */
998 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1001 return false; /* Action was explored previously */
1005 /* Always compute new clock vector */
1006 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1008 * Perform one-time actions when pushing new ModelAction onto
1011 if (newcurr->is_write())
1012 compute_promises(newcurr);
1013 else if (newcurr->is_relseq_fixup())
1014 compute_relseq_breakwrites(newcurr);
1015 else if (newcurr->is_wait())
1016 newcurr->get_node()->set_misc_max(2);
1017 else if (newcurr->is_notify_one()) {
1018 newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
1020 return true; /* This was a new ModelAction */
1025 * @brief Check whether a model action is enabled.
1027 * Checks whether a lock or join operation would be successful (i.e., is the
1028 * lock already locked, or is the joined thread already complete). If not, put
1029 * the action in a waiter list.
1031 * @param curr is the ModelAction to check whether it is enabled.
1032 * @return a bool that indicates whether the action is enabled.
1034 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1035 if (curr->is_lock()) {
1036 std::mutex * lock = (std::mutex *)curr->get_location();
1037 struct std::mutex_state * state = lock->get_state();
1038 if (state->islocked) {
1039 //Stick the action in the appropriate waiting queue
1040 get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1043 } else if (curr->get_type() == THREAD_JOIN) {
1044 Thread *blocking = (Thread *)curr->get_location();
1045 if (!blocking->is_complete()) {
1046 blocking->push_wait_list(curr);
1055 * Stores the ModelAction for the current thread action. Call this
1056 * immediately before switching from user- to system-context to pass
1057 * data between them.
1058 * @param act The ModelAction created by the user-thread action
1060 void ModelChecker::set_current_action(ModelAction *act) {
1061 priv->current_action = act;
1065 * This is the heart of the model checker routine. It performs model-checking
1066 * actions corresponding to a given "current action." Among other processes, it
1067 * calculates reads-from relationships, updates synchronization clock vectors,
1068 * forms a memory_order constraints graph, and handles replay/backtrack
1069 * execution when running permutations of previously-observed executions.
1071 * @param curr The current action to process
1072 * @return The next Thread that must be executed. May be NULL if ModelChecker
1073 * makes no choice (e.g., according to replay execution, combining RMW actions,
1076 Thread * ModelChecker::check_current_action(ModelAction *curr)
1079 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1081 if (!check_action_enabled(curr)) {
1082 /* Make the execution look like we chose to run this action
1083 * much later, when a lock/join can succeed */
1084 get_current_thread()->set_pending(curr);
1085 scheduler->sleep(get_current_thread());
1086 return get_next_thread(NULL);
1089 bool newly_explored = initialize_curr_action(&curr);
1091 wake_up_sleeping_actions(curr);
1093 /* Add the action to lists before any other model-checking tasks */
1094 if (!second_part_of_rmw)
1095 add_action_to_lists(curr);
1097 /* Build may_read_from set for newly-created actions */
1098 if (newly_explored && curr->is_read())
1099 build_reads_from_past(curr);
1101 /* Initialize work_queue with the "current action" work */
1102 work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1103 while (!work_queue.empty() && !has_asserted()) {
1104 WorkQueueEntry work = work_queue.front();
1105 work_queue.pop_front();
1107 switch (work.type) {
1108 case WORK_CHECK_CURR_ACTION: {
1109 ModelAction *act = work.action;
1110 bool update = false; /* update this location's release seq's */
1111 bool update_all = false; /* update all release seq's */
1113 if (process_thread_action(curr))
1116 if (act->is_read() && process_read(act, second_part_of_rmw))
1119 if (act->is_write() && process_write(act))
1122 if (act->is_mutex_op() && process_mutex(act))
1125 if (act->is_relseq_fixup())
1126 process_relseq_fixup(curr, &work_queue);
1129 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1131 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1134 case WORK_CHECK_RELEASE_SEQ:
1135 resolve_release_sequences(work.location, &work_queue);
1137 case WORK_CHECK_MO_EDGES: {
1138 /** @todo Complete verification of work_queue */
1139 ModelAction *act = work.action;
1140 bool updated = false;
1142 if (act->is_read()) {
1143 const ModelAction *rf = act->get_reads_from();
1144 if (rf != NULL && r_modification_order(act, rf))
1147 if (act->is_write()) {
1148 if (w_modification_order(act))
1151 mo_graph->commitChanges();
1154 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1163 check_curr_backtracking(curr);
1164 set_backtracking(curr);
1165 return get_next_thread(curr);
1168 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
1169 Node *currnode = curr->get_node();
1170 Node *parnode = currnode->get_parent();
1172 if ((!parnode->backtrack_empty() ||
1173 !currnode->misc_empty() ||
1174 !currnode->read_from_empty() ||
1175 !currnode->future_value_empty() ||
1176 !currnode->promise_empty() ||
1177 !currnode->relseq_break_empty())
1178 && (!priv->next_backtrack ||
1179 *curr > *priv->next_backtrack)) {
1180 priv->next_backtrack = curr;
1184 bool ModelChecker::promises_expired() const
1186 for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
1187 Promise *promise = (*promises)[promise_index];
1188 if (promise->get_expiration()<priv->used_sequence_numbers) {
1195 /** @return whether the current partial trace must be a prefix of a
1196 * feasible trace. */
1197 bool ModelChecker::isfeasibleprefix() const
1199 return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
1202 /** @return whether the current partial trace is feasible. */
1203 bool ModelChecker::isfeasible() const
1205 if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
1206 DEBUG("Infeasible: RMW violation\n");
1208 return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
1211 /** @return whether the current partial trace is feasible other than
1212 * multiple RMW reading from the same store. */
1213 bool ModelChecker::isfeasibleotherthanRMW() const
1215 if (DBG_ENABLED()) {
1216 if (mo_graph->checkForCycles())
1217 DEBUG("Infeasible: modification order cycles\n");
1219 DEBUG("Infeasible: failed promise\n");
1221 DEBUG("Infeasible: too many reads\n");
1222 if (bad_synchronization)
1223 DEBUG("Infeasible: bad synchronization ordering\n");
1224 if (promises_expired())
1225 DEBUG("Infeasible: promises expired\n");
1227 return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
1230 /** Returns whether the current completed trace is feasible. */
1231 bool ModelChecker::isfinalfeasible() const
1233 if (DBG_ENABLED() && promises->size() != 0)
1234 DEBUG("Infeasible: unrevolved promises\n");
1236 return isfeasible() && promises->size() == 0;
1239 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1240 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1241 ModelAction *lastread = get_last_action(act->get_tid());
1242 lastread->process_rmw(act);
1243 if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
1244 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1245 mo_graph->commitChanges();
1251 * Checks whether a thread has read from the same write for too many times
1252 * without seeing the effects of a later write.
1255 * 1) there must a different write that we could read from that would satisfy the modification order,
1256 * 2) we must have read from the same value in excess of maxreads times, and
1257 * 3) that other write must have been in the reads_from set for maxreads times.
1259 * If so, we decide that the execution is no longer feasible.
1261 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
1262 if (params.maxreads != 0) {
1264 if (curr->get_node()->get_read_from_size() <= 1)
1266 //Must make sure that execution is currently feasible... We could
1267 //accidentally clear by rolling back
1270 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1271 int tid = id_to_int(curr->get_tid());
1274 if ((int)thrd_lists->size() <= tid)
1276 action_list_t *list = &(*thrd_lists)[tid];
1278 action_list_t::reverse_iterator rit = list->rbegin();
1279 /* Skip past curr */
1280 for (; (*rit) != curr; rit++)
1282 /* go past curr now */
1285 action_list_t::reverse_iterator ritcopy = rit;
1286 //See if we have enough reads from the same value
1288 for (; count < params.maxreads; rit++,count++) {
1289 if (rit==list->rend())
1291 ModelAction *act = *rit;
1292 if (!act->is_read())
1295 if (act->get_reads_from() != rf)
1297 if (act->get_node()->get_read_from_size() <= 1)
1300 for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
1302 const ModelAction * write = curr->get_node()->get_read_from_at(i);
1304 //Need a different write
1308 /* Test to see whether this is a feasible write to read from*/
1309 mo_graph->startChanges();
1310 r_modification_order(curr, write);
1311 bool feasiblereadfrom = isfeasible();
1312 mo_graph->rollbackChanges();
1314 if (!feasiblereadfrom)
1318 bool feasiblewrite = true;
1319 //new we need to see if this write works for everyone
1321 for (int loop = count; loop>0; loop--,rit++) {
1322 ModelAction *act=*rit;
1323 bool foundvalue = false;
1324 for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
1325 if (act->get_node()->get_read_from_at(j)==write) {
1331 feasiblewrite = false;
1335 if (feasiblewrite) {
1336 too_many_reads = true;
1344 * Updates the mo_graph with the constraints imposed from the current
1347 * Basic idea is the following: Go through each other thread and find
1348 * the lastest action that happened before our read. Two cases:
1350 * (1) The action is a write => that write must either occur before
1351 * the write we read from or be the write we read from.
1353 * (2) The action is a read => the write that that action read from
1354 * must occur before the write we read from or be the same write.
1356 * @param curr The current action. Must be a read.
1357 * @param rf The action that curr reads from. Must be a write.
1358 * @return True if modification order edges were added; false otherwise
1360 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
1362 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1365 ASSERT(curr->is_read());
1367 /* Iterate over all threads */
1368 for (i = 0; i < thrd_lists->size(); i++) {
1369 /* Iterate over actions in thread, starting from most recent */
1370 action_list_t *list = &(*thrd_lists)[i];
1371 action_list_t::reverse_iterator rit;
1372 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1373 ModelAction *act = *rit;
1376 * Include at most one act per-thread that "happens
1377 * before" curr. Don't consider reflexively.
1379 if (act->happens_before(curr) && act != curr) {
1380 if (act->is_write()) {
1382 mo_graph->addEdge(act, rf);
1386 const ModelAction *prevreadfrom = act->get_reads_from();
1387 //if the previous read is unresolved, keep going...
1388 if (prevreadfrom == NULL)
1391 if (rf != prevreadfrom) {
1392 mo_graph->addEdge(prevreadfrom, rf);
1404 /** This method fixes up the modification order when we resolve a
1405 * promises. The basic problem is that actions that occur after the
1406 * read curr could not property add items to the modification order
1409 * So for each thread, we find the earliest item that happens after
1410 * the read curr. This is the item we have to fix up with additional
1411 * constraints. If that action is write, we add a MO edge between
1412 * the Action rf and that action. If the action is a read, we add a
1413 * MO edge between the Action rf, and whatever the read accessed.
1415 * @param curr is the read ModelAction that we are fixing up MO edges for.
1416 * @param rf is the write ModelAction that curr reads from.
1419 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1421 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1423 ASSERT(curr->is_read());
1425 /* Iterate over all threads */
1426 for (i = 0; i < thrd_lists->size(); i++) {
1427 /* Iterate over actions in thread, starting from most recent */
1428 action_list_t *list = &(*thrd_lists)[i];
1429 action_list_t::reverse_iterator rit;
1430 ModelAction *lastact = NULL;
1432 /* Find last action that happens after curr that is either not curr or a rmw */
1433 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1434 ModelAction *act = *rit;
1435 if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1441 /* Include at most one act per-thread that "happens before" curr */
1442 if (lastact != NULL) {
1443 if (lastact==curr) {
1444 //Case 1: The resolved read is a RMW, and we need to make sure
1445 //that the write portion of the RMW mod order after rf
1447 mo_graph->addEdge(rf, lastact);
1448 } else if (lastact->is_read()) {
1449 //Case 2: The resolved read is a normal read and the next
1450 //operation is a read, and we need to make sure the value read
1451 //is mod ordered after rf
1453 const ModelAction *postreadfrom = lastact->get_reads_from();
1454 if (postreadfrom != NULL&&rf != postreadfrom)
1455 mo_graph->addEdge(rf, postreadfrom);
1457 //Case 3: The resolved read is a normal read and the next
1458 //operation is a write, and we need to make sure that the
1459 //write is mod ordered after rf
1461 mo_graph->addEdge(rf, lastact);
1469 * Updates the mo_graph with the constraints imposed from the current write.
1471 * Basic idea is the following: Go through each other thread and find
1472 * the lastest action that happened before our write. Two cases:
1474 * (1) The action is a write => that write must occur before
1477 * (2) The action is a read => the write that that action read from
1478 * must occur before the current write.
1480 * This method also handles two other issues:
1482 * (I) Sequential Consistency: Making sure that if the current write is
1483 * seq_cst, that it occurs after the previous seq_cst write.
1485 * (II) Sending the write back to non-synchronizing reads.
1487 * @param curr The current action. Must be a write.
1488 * @return True if modification order edges were added; false otherwise
1490 bool ModelChecker::w_modification_order(ModelAction *curr)
1492 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1495 ASSERT(curr->is_write());
1497 if (curr->is_seqcst()) {
1498 /* We have to at least see the last sequentially consistent write,
1499 so we are initialized. */
1500 ModelAction *last_seq_cst = get_last_seq_cst(curr);
1501 if (last_seq_cst != NULL) {
1502 mo_graph->addEdge(last_seq_cst, curr);
1507 /* Iterate over all threads */
1508 for (i = 0; i < thrd_lists->size(); i++) {
1509 /* Iterate over actions in thread, starting from most recent */
1510 action_list_t *list = &(*thrd_lists)[i];
1511 action_list_t::reverse_iterator rit;
1512 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1513 ModelAction *act = *rit;
1516 * 1) If RMW and it actually read from something, then we
1517 * already have all relevant edges, so just skip to next
1520 * 2) If RMW and it didn't read from anything, we should
1521 * whatever edge we can get to speed up convergence.
1523 * 3) If normal write, we need to look at earlier actions, so
1524 * continue processing list.
1526 if (curr->is_rmw()) {
1527 if (curr->get_reads_from()!=NULL)
1536 * Include at most one act per-thread that "happens
1539 if (act->happens_before(curr)) {
1541 * Note: if act is RMW, just add edge:
1543 * The following edge should be handled elsewhere:
1544 * readfrom(act) --mo--> act
1546 if (act->is_write())
1547 mo_graph->addEdge(act, curr);
1548 else if (act->is_read()) {
1549 //if previous read accessed a null, just keep going
1550 if (act->get_reads_from() == NULL)
1552 mo_graph->addEdge(act->get_reads_from(), curr);
1556 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1557 !act->same_thread(curr)) {
1558 /* We have an action that:
1559 (1) did not happen before us
1560 (2) is a read and we are a write
1561 (3) cannot synchronize with us
1562 (4) is in a different thread
1564 that read could potentially read from our write. Note that
1565 these checks are overly conservative at this point, we'll
1566 do more checks before actually removing the
1570 if (thin_air_constraint_may_allow(curr, act)) {
1572 (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
1573 struct PendingFutureValue pfv = {curr,act};
1574 futurevalues->push_back(pfv);
1584 /** Arbitrary reads from the future are not allowed. Section 29.3
1585 * part 9 places some constraints. This method checks one result of constraint
1586 * constraint. Others require compiler support. */
1587 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
1588 if (!writer->is_rmw())
1591 if (!reader->is_rmw())
1594 for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1595 if (search == reader)
1597 if (search->get_tid() == reader->get_tid() &&
1598 search->happens_before(reader))
1606 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1607 * some constraints. This method checks one the following constraint (others
1608 * require compiler support):
1610 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1612 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1614 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1616 /* Iterate over all threads */
1617 for (i = 0; i < thrd_lists->size(); i++) {
1618 const ModelAction *write_after_read = NULL;
1620 /* Iterate over actions in thread, starting from most recent */
1621 action_list_t *list = &(*thrd_lists)[i];
1622 action_list_t::reverse_iterator rit;
1623 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1624 ModelAction *act = *rit;
1626 if (!reader->happens_before(act))
1628 else if (act->is_write())
1629 write_after_read = act;
1630 else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
1631 write_after_read = act->get_reads_from();
1635 if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
1642 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1643 * The ModelAction under consideration is expected to be taking part in
1644 * release/acquire synchronization as an object of the "reads from" relation.
1645 * Note that this can only provide release sequence support for RMW chains
1646 * which do not read from the future, as those actions cannot be traced until
1647 * their "promise" is fulfilled. Similarly, we may not even establish the
1648 * presence of a release sequence with certainty, as some modification order
1649 * constraints may be decided further in the future. Thus, this function
1650 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1651 * and a boolean representing certainty.
1653 * @param rf The action that might be part of a release sequence. Must be a
1655 * @param release_heads A pass-by-reference style return parameter. After
1656 * execution of this function, release_heads will contain the heads of all the
1657 * relevant release sequences, if any exists with certainty
1658 * @param pending A pass-by-reference style return parameter which is only used
1659 * when returning false (i.e., uncertain). Returns most information regarding
1660 * an uncertain release sequence, including any write operations that might
1661 * break the sequence.
1662 * @return true, if the ModelChecker is certain that release_heads is complete;
1665 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1666 rel_heads_list_t *release_heads,
1667 struct release_seq *pending) const
1669 /* Only check for release sequences if there are no cycles */
1670 if (mo_graph->checkForCycles())
1674 ASSERT(rf->is_write());
1676 if (rf->is_release())
1677 release_heads->push_back(rf);
1679 break; /* End of RMW chain */
1681 /** @todo Need to be smarter here... In the linux lock
1682 * example, this will run to the beginning of the program for
1684 /** @todo The way to be smarter here is to keep going until 1
1685 * thread has a release preceded by an acquire and you've seen
1688 /* acq_rel RMW is a sufficient stopping condition */
1689 if (rf->is_acquire() && rf->is_release())
1690 return true; /* complete */
1692 rf = rf->get_reads_from();
1695 /* read from future: need to settle this later */
1697 return false; /* incomplete */
1700 if (rf->is_release())
1701 return true; /* complete */
1703 /* else relaxed write; check modification order for contiguous subsequence
1704 * -> rf must be same thread as release */
1705 int tid = id_to_int(rf->get_tid());
1706 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
1707 action_list_t *list = &(*thrd_lists)[tid];
1708 action_list_t::const_reverse_iterator rit;
1710 /* Find rf in the thread list */
1711 rit = std::find(list->rbegin(), list->rend(), rf);
1712 ASSERT(rit != list->rend());
1714 /* Find the last write/release */
1715 for (; rit != list->rend(); rit++)
1716 if ((*rit)->is_release())
1718 if (rit == list->rend()) {
1719 /* No write-release in this thread */
1720 return true; /* complete */
1722 ModelAction *release = *rit;
1724 ASSERT(rf->same_thread(release));
1726 pending->writes.clear();
1728 bool certain = true;
1729 for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1730 if (id_to_int(rf->get_tid()) == (int)i)
1732 list = &(*thrd_lists)[i];
1734 /* Can we ensure no future writes from this thread may break
1735 * the release seq? */
1736 bool future_ordered = false;
1738 ModelAction *last = get_last_action(int_to_id(i));
1739 Thread *th = get_thread(int_to_id(i));
1740 if ((last && rf->happens_before(last)) ||
1743 future_ordered = true;
1745 ASSERT(!th->is_model_thread() || future_ordered);
1747 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1748 const ModelAction *act = *rit;
1749 /* Reach synchronization -> this thread is complete */
1750 if (act->happens_before(release))
1752 if (rf->happens_before(act)) {
1753 future_ordered = true;
1757 /* Only non-RMW writes can break release sequences */
1758 if (!act->is_write() || act->is_rmw())
1761 /* Check modification order */
1762 if (mo_graph->checkReachable(rf, act)) {
1763 /* rf --mo--> act */
1764 future_ordered = true;
1767 if (mo_graph->checkReachable(act, release))
1768 /* act --mo--> release */
1770 if (mo_graph->checkReachable(release, act) &&
1771 mo_graph->checkReachable(act, rf)) {
1772 /* release --mo-> act --mo--> rf */
1773 return true; /* complete */
1775 /* act may break release sequence */
1776 pending->writes.push_back(act);
1779 if (!future_ordered)
1780 certain = false; /* This thread is uncertain */
1784 release_heads->push_back(release);
1785 pending->writes.clear();
1787 pending->release = release;
1794 * A public interface for getting the release sequence head(s) with which a
1795 * given ModelAction must synchronize. This function only returns a non-empty
1796 * result when it can locate a release sequence head with certainty. Otherwise,
1797 * it may mark the internal state of the ModelChecker so that it will handle
1798 * the release sequence at a later time, causing @a act to update its
1799 * synchronization at some later point in execution.
1800 * @param act The 'acquire' action that may read from a release sequence
1801 * @param release_heads A pass-by-reference return parameter. Will be filled
1802 * with the head(s) of the release sequence(s), if they exists with certainty.
1803 * @see ModelChecker::release_seq_heads
1805 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
1807 const ModelAction *rf = act->get_reads_from();
1808 struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
1809 sequence->acquire = act;
1811 if (!release_seq_heads(rf, release_heads, sequence)) {
1812 /* add act to 'lazy checking' list */
1813 pending_rel_seqs->push_back(sequence);
1815 snapshot_free(sequence);
1820 * Attempt to resolve all stashed operations that might synchronize with a
1821 * release sequence for a given location. This implements the "lazy" portion of
1822 * determining whether or not a release sequence was contiguous, since not all
1823 * modification order information is present at the time an action occurs.
1825 * @param location The location/object that should be checked for release
1826 * sequence resolutions. A NULL value means to check all locations.
1827 * @param work_queue The work queue to which to add work items as they are
1829 * @return True if any updates occurred (new synchronization, new mo_graph
1832 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
1834 bool updated = false;
1835 std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
1836 while (it != pending_rel_seqs->end()) {
1837 struct release_seq *pending = *it;
1838 ModelAction *act = pending->acquire;
1840 /* Only resolve sequences on the given location, if provided */
1841 if (location && act->get_location() != location) {
1846 const ModelAction *rf = act->get_reads_from();
1847 rel_heads_list_t release_heads;
1849 complete = release_seq_heads(rf, &release_heads, pending);
1850 for (unsigned int i = 0; i < release_heads.size(); i++) {
1851 if (!act->has_synchronized_with(release_heads[i])) {
1852 if (act->synchronize_with(release_heads[i]))
1855 set_bad_synchronization();
1860 /* Re-check all pending release sequences */
1861 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1862 /* Re-check act for mo_graph edges */
1863 work_queue->push_back(MOEdgeWorkEntry(act));
1865 /* propagate synchronization to later actions */
1866 action_list_t::reverse_iterator rit = action_trace->rbegin();
1867 for (; (*rit) != act; rit++) {
1868 ModelAction *propagate = *rit;
1869 if (act->happens_before(propagate)) {
1870 propagate->synchronize_with(act);
1871 /* Re-check 'propagate' for mo_graph edges */
1872 work_queue->push_back(MOEdgeWorkEntry(propagate));
1877 it = pending_rel_seqs->erase(it);
1878 snapshot_free(pending);
1884 // If we resolved promises or data races, see if we have realized a data race.
1891 * Performs various bookkeeping operations for the current ModelAction. For
1892 * instance, adds action to the per-object, per-thread action vector and to the
1893 * action trace list of all thread actions.
1895 * @param act is the ModelAction to add.
1897 void ModelChecker::add_action_to_lists(ModelAction *act)
1899 int tid = id_to_int(act->get_tid());
1900 action_trace->push_back(act);
1902 get_safe_ptr_action(obj_map, act->get_location())->push_back(act);
1904 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
1905 if (tid >= (int)vec->size())
1906 vec->resize(priv->next_thread_id);
1907 (*vec)[tid].push_back(act);
1909 if ((int)thrd_last_action->size() <= tid)
1910 thrd_last_action->resize(get_num_threads());
1911 (*thrd_last_action)[tid] = act;
1913 if (act->is_wait()) {
1914 void *mutex_loc=(void *) act->get_value();
1915 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
1917 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
1918 if (tid >= (int)vec->size())
1919 vec->resize(priv->next_thread_id);
1920 (*vec)[tid].push_back(act);
1922 if ((int)thrd_last_action->size() <= tid)
1923 thrd_last_action->resize(get_num_threads());
1924 (*thrd_last_action)[tid] = act;
1929 * @brief Get the last action performed by a particular Thread
1930 * @param tid The thread ID of the Thread in question
1931 * @return The last action in the thread
1933 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
1935 int threadid = id_to_int(tid);
1936 if (threadid < (int)thrd_last_action->size())
1937 return (*thrd_last_action)[id_to_int(tid)];
1943 * Gets the last memory_order_seq_cst write (in the total global sequence)
1944 * performed on a particular object (i.e., memory location), not including the
1946 * @param curr The current ModelAction; also denotes the object location to
1948 * @return The last seq_cst write
1950 ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
1952 void *location = curr->get_location();
1953 action_list_t *list = get_safe_ptr_action(obj_map, location);
1954 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1955 action_list_t::reverse_iterator rit;
1956 for (rit = list->rbegin(); rit != list->rend(); rit++)
1957 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
1963 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1964 * location). This function identifies the mutex according to the current
1965 * action, which is presumed to perform on the same mutex.
1966 * @param curr The current ModelAction; also denotes the object location to
1968 * @return The last unlock operation
1970 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
1972 void *location = curr->get_location();
1973 action_list_t *list = get_safe_ptr_action(obj_map, location);
1974 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1975 action_list_t::reverse_iterator rit;
1976 for (rit = list->rbegin(); rit != list->rend(); rit++)
1977 if ((*rit)->is_unlock() || (*rit)->is_wait())
1982 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
1984 ModelAction *parent = get_last_action(tid);
1986 parent = get_thread(tid)->get_creation();
1991 * Returns the clock vector for a given thread.
1992 * @param tid The thread whose clock vector we want
1993 * @return Desired clock vector
1995 ClockVector * ModelChecker::get_cv(thread_id_t tid)
1997 return get_parent_action(tid)->get_cv();
2001 * Resolve a set of Promises with a current write. The set is provided in the
2002 * Node corresponding to @a write.
2003 * @param write The ModelAction that is fulfilling Promises
2004 * @return True if promises were resolved; false otherwise
2006 bool ModelChecker::resolve_promises(ModelAction *write)
2008 bool resolved = false;
2009 std::vector< thread_id_t, ModelAlloc<thread_id_t> > threads_to_check;
2011 for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
2012 Promise *promise = (*promises)[promise_index];
2013 if (write->get_node()->get_promise(i)) {
2014 ModelAction *read = promise->get_action();
2015 if (read->is_rmw()) {
2016 mo_graph->addRMWEdge(write, read);
2018 read->read_from(write);
2019 //First fix up the modification order for actions that happened
2021 r_modification_order(read, write);
2022 //Next fix up the modification order for actions that happened
2024 post_r_modification_order(read, write);
2025 //Make sure the promise's value matches the write's value
2026 ASSERT(promise->get_value() == write->get_value());
2029 promises->erase(promises->begin() + promise_index);
2030 threads_to_check.push_back(read->get_tid());
2037 //Check whether reading these writes has made threads unable to
2040 for(unsigned int i=0;i<threads_to_check.size();i++)
2041 mo_check_promises(threads_to_check[i], write);
2047 * Compute the set of promises that could potentially be satisfied by this
2048 * action. Note that the set computation actually appears in the Node, not in
2050 * @param curr The ModelAction that may satisfy promises
2052 void ModelChecker::compute_promises(ModelAction *curr)
2054 for (unsigned int i = 0; i < promises->size(); i++) {
2055 Promise *promise = (*promises)[i];
2056 const ModelAction *act = promise->get_action();
2057 if (!act->happens_before(curr) &&
2059 !act->could_synchronize_with(curr) &&
2060 !act->same_thread(curr) &&
2061 act->get_location() == curr->get_location() &&
2062 promise->get_value() == curr->get_value()) {
2063 curr->get_node()->set_promise(i, act->is_rmw());
2068 /** Checks promises in response to change in ClockVector Threads. */
2069 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2071 for (unsigned int i = 0; i < promises->size(); i++) {
2072 Promise *promise = (*promises)[i];
2073 const ModelAction *act = promise->get_action();
2074 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2075 merge_cv->synchronized_since(act)) {
2076 if (promise->increment_threads(tid)) {
2077 //Promise has failed
2078 failed_promise = true;
2085 void ModelChecker::check_promises_thread_disabled() {
2086 for (unsigned int i = 0; i < promises->size(); i++) {
2087 Promise *promise = (*promises)[i];
2088 if (promise->check_promise()) {
2089 failed_promise = true;
2095 /** Checks promises in response to addition to modification order for threads.
2097 * pthread is the thread that performed the read that created the promise
2099 * pread is the read that created the promise
2101 * pwrite is either the first write to same location as pread by
2102 * pthread that is sequenced after pread or the value read by the
2103 * first read to the same lcoation as pread by pthread that is
2104 * sequenced after pread..
2106 * 1. If tid=pthread, then we check what other threads are reachable
2107 * through the mode order starting with pwrite. Those threads cannot
2108 * perform a write that will resolve the promise due to modification
2109 * order constraints.
2111 * 2. If the tid is not pthread, we check whether pwrite can reach the
2112 * action write through the modification order. If so, that thread
2113 * cannot perform a future write that will resolve the promise due to
2114 * modificatin order constraints.
2116 * @parem tid The thread that either read from the model action
2117 * write, or actually did the model action write.
2119 * @parem write The ModelAction representing the relevant write.
2122 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
2123 void * location = write->get_location();
2124 for (unsigned int i = 0; i < promises->size(); i++) {
2125 Promise *promise = (*promises)[i];
2126 const ModelAction *act = promise->get_action();
2128 //Is this promise on the same location?
2129 if ( act->get_location() != location )
2132 //same thread as the promise
2133 if ( act->get_tid()==tid ) {
2135 //do we have a pwrite for the promise, if not, set it
2136 if (promise->get_write() == NULL ) {
2137 promise->set_write(write);
2138 //The pwrite cannot happen before the promise
2139 if (write->happens_before(act) && (write != act)) {
2140 failed_promise = true;
2144 if (mo_graph->checkPromise(write, promise)) {
2145 failed_promise = true;
2150 //Don't do any lookups twice for the same thread
2151 if (promise->has_sync_thread(tid))
2154 if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
2155 if (promise->increment_threads(tid)) {
2156 failed_promise = true;
2164 * Compute the set of writes that may break the current pending release
2165 * sequence. This information is extracted from previou release sequence
2168 * @param curr The current ModelAction. Must be a release sequence fixup
2171 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2173 if (pending_rel_seqs->empty())
2176 struct release_seq *pending = pending_rel_seqs->back();
2177 for (unsigned int i = 0; i < pending->writes.size(); i++) {
2178 const ModelAction *write = pending->writes[i];
2179 curr->get_node()->add_relseq_break(write);
2182 /* NULL means don't break the sequence; just synchronize */
2183 curr->get_node()->add_relseq_break(NULL);
2187 * Build up an initial set of all past writes that this 'read' action may read
2188 * from. This set is determined by the clock vector's "happens before"
2190 * @param curr is the current ModelAction that we are exploring; it must be a
2193 void ModelChecker::build_reads_from_past(ModelAction *curr)
2195 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2197 ASSERT(curr->is_read());
2199 ModelAction *last_seq_cst = NULL;
2201 /* Track whether this object has been initialized */
2202 bool initialized = false;
2204 if (curr->is_seqcst()) {
2205 last_seq_cst = get_last_seq_cst(curr);
2206 /* We have to at least see the last sequentially consistent write,
2207 so we are initialized. */
2208 if (last_seq_cst != NULL)
2212 /* Iterate over all threads */
2213 for (i = 0; i < thrd_lists->size(); i++) {
2214 /* Iterate over actions in thread, starting from most recent */
2215 action_list_t *list = &(*thrd_lists)[i];
2216 action_list_t::reverse_iterator rit;
2217 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2218 ModelAction *act = *rit;
2220 /* Only consider 'write' actions */
2221 if (!act->is_write() || act == curr)
2224 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2225 if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
2226 if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
2227 DEBUG("Adding action to may_read_from:\n");
2228 if (DBG_ENABLED()) {
2232 curr->get_node()->add_read_from(act);
2236 /* Include at most one act per-thread that "happens before" curr */
2237 if (act->happens_before(curr)) {
2245 assert_bug("May read from uninitialized atomic");
2247 if (DBG_ENABLED() || !initialized) {
2248 model_print("Reached read action:\n");
2250 model_print("Printing may_read_from\n");
2251 curr->get_node()->print_may_read_from();
2252 model_print("End printing may_read_from\n");
2256 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
2258 Node *prevnode=write->get_node()->get_parent();
2260 bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
2261 if (write->is_release()&&thread_sleep)
2263 if (!write->is_rmw()) {
2266 if (write->get_reads_from()==NULL)
2268 write=write->get_reads_from();
2272 static void print_list(action_list_t *list, int exec_num = -1)
2274 action_list_t::iterator it;
2276 model_print("---------------------------------------------------------------------\n");
2278 model_print("Execution %d:\n", exec_num);
2280 unsigned int hash=0;
2282 for (it = list->begin(); it != list->end(); it++) {
2284 hash=hash^(hash<<3)^((*it)->hash());
2286 model_print("HASH %u\n", hash);
2287 model_print("---------------------------------------------------------------------\n");
2290 #if SUPPORT_MOD_ORDER_DUMP
2291 void ModelChecker::dumpGraph(char *filename) {
2293 sprintf(buffer, "%s.dot",filename);
2294 FILE *file=fopen(buffer, "w");
2295 fprintf(file, "digraph %s {\n",filename);
2296 mo_graph->dumpNodes(file);
2297 ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
2299 for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2300 ModelAction *action=*it;
2301 if (action->is_read()) {
2302 fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
2303 if (action->get_reads_from()!=NULL)
2304 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2306 if (thread_array[action->get_tid()] != NULL) {
2307 fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2310 thread_array[action->get_tid()]=action;
2312 fprintf(file,"}\n");
2313 model_free(thread_array);
2318 /** @brief Prints an execution trace summary. */
2319 void ModelChecker::print_summary() const
2321 #if SUPPORT_MOD_ORDER_DUMP
2323 char buffername[100];
2324 sprintf(buffername, "exec%04u", stats.num_total);
2325 mo_graph->dumpGraphToFile(buffername);
2326 sprintf(buffername, "graph%04u", stats.num_total);
2327 dumpGraph(buffername);
2330 if (!isfinalfeasible())
2331 model_print("INFEASIBLE EXECUTION!\n");
2332 print_list(action_trace, stats.num_total);
2337 * Add a Thread to the system for the first time. Should only be called once
2339 * @param t The Thread to add
2341 void ModelChecker::add_thread(Thread *t)
2343 thread_map->put(id_to_int(t->get_id()), t);
2344 scheduler->add_thread(t);
2348 * Removes a thread from the scheduler.
2349 * @param the thread to remove.
2351 void ModelChecker::remove_thread(Thread *t)
2353 scheduler->remove_thread(t);
2357 * @brief Get a Thread reference by its ID
2358 * @param tid The Thread's ID
2359 * @return A Thread reference
2361 Thread * ModelChecker::get_thread(thread_id_t tid) const
2363 return thread_map->get(id_to_int(tid));
2367 * @brief Get a reference to the Thread in which a ModelAction was executed
2368 * @param act The ModelAction
2369 * @return A Thread reference
2371 Thread * ModelChecker::get_thread(ModelAction *act) const
2373 return get_thread(act->get_tid());
2377 * @brief Check if a Thread is currently enabled
2378 * @param t The Thread to check
2379 * @return True if the Thread is currently enabled
2381 bool ModelChecker::is_enabled(Thread *t) const
2383 return scheduler->is_enabled(t);
2387 * @brief Check if a Thread is currently enabled
2388 * @param tid The ID of the Thread to check
2389 * @return True if the Thread is currently enabled
2391 bool ModelChecker::is_enabled(thread_id_t tid) const
2393 return scheduler->is_enabled(tid);
2397 * Switch from a user-context to the "master thread" context (a.k.a. system
2398 * context). This switch is made with the intention of exploring a particular
2399 * model-checking action (described by a ModelAction object). Must be called
2400 * from a user-thread context.
2402 * @param act The current action that will be explored. May be NULL only if
2403 * trace is exiting via an assertion (see ModelChecker::set_assert and
2404 * ModelChecker::has_asserted).
2405 * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
2407 int ModelChecker::switch_to_master(ModelAction *act)
2410 Thread *old = thread_current();
2411 set_current_action(act);
2412 old->set_state(THREAD_READY);
2413 return Thread::swap(old, &system_context);
2417 * Takes the next step in the execution, if possible.
2418 * @return Returns true (success) if a step was taken and false otherwise.
2420 bool ModelChecker::take_step() {
2424 Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
2426 if (curr->get_state() == THREAD_READY) {
2427 ASSERT(priv->current_action);
2429 priv->nextThread = check_current_action(priv->current_action);
2430 priv->current_action = NULL;
2432 if (curr->is_blocked() || curr->is_complete())
2433 scheduler->remove_thread(curr);
2438 Thread *next = scheduler->next_thread(priv->nextThread);
2440 /* Infeasible -> don't take any more steps */
2443 else if (isfeasibleprefix() && have_bug_reports()) {
2448 if (params.bound != 0) {
2449 if (priv->used_sequence_numbers > params.bound) {
2454 DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
2455 next ? id_to_int(next->get_id()) : -1);
2458 * Launch end-of-execution release sequence fixups only when there are:
2460 * (1) no more user threads to run (or when execution replay chooses
2461 * the 'model_thread')
2462 * (2) pending release sequences
2463 * (3) pending assertions (i.e., data races)
2464 * (4) no pending promises
2466 if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
2467 isfinalfeasible() && !unrealizedraces.empty()) {
2468 model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2469 pending_rel_seqs->size());
2470 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2471 std::memory_order_seq_cst, NULL, VALUE_NONE,
2473 set_current_action(fixup);
2477 /* next == NULL -> don't take any more steps */
2481 next->set_state(THREAD_RUNNING);
2483 if (next->get_pending() != NULL) {
2484 /* restart a pending action */
2485 set_current_action(next->get_pending());
2486 next->set_pending(NULL);
2487 next->set_state(THREAD_READY);
2491 /* Return false only if swap fails with an error */
2492 return (Thread::swap(&system_context, next) == 0);
2495 /** Runs the current execution until threre are no more steps to take. */
2496 void ModelChecker::finish_execution() {
2499 while (take_step());