9 #include "snapshot-interface.h"
11 #include "clockvector.h"
12 #include "cyclegraph.h"
15 #include "threads-model.h"
17 #define INITIAL_THREAD_ID 0
21 /** @brief Constructor */
22 ModelChecker::ModelChecker(struct model_params params) :
23 /* Initialize default scheduler */
25 scheduler(new Scheduler()),
27 num_feasible_executions(0),
29 earliest_diverge(NULL),
30 action_trace(new action_list_t()),
31 thread_map(new HashTable<int, Thread *, int>()),
32 obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
33 lock_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
34 condvar_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
35 obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
36 promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
37 futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
38 pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
39 thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
40 node_stack(new NodeStack()),
41 mo_graph(new CycleGraph()),
42 failed_promise(false),
43 too_many_reads(false),
45 bad_synchronization(false)
47 /* Allocate this "size" on the snapshotting heap */
48 priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
49 /* First thread created will have id INITIAL_THREAD_ID */
50 priv->next_thread_id = INITIAL_THREAD_ID;
52 /* Initialize a model-checker thread, for special ModelActions */
53 model_thread = new Thread(get_next_id());
54 thread_map->put(id_to_int(model_thread->get_id()), model_thread);
57 /** @brief Destructor */
58 ModelChecker::~ModelChecker()
60 for (unsigned int i = 0; i < get_num_threads(); i++)
61 delete thread_map->get(i);
66 delete lock_waiters_map;
67 delete condvar_waiters_map;
70 for (unsigned int i = 0; i < promises->size(); i++)
71 delete (*promises)[i];
74 delete pending_rel_seqs;
76 delete thrd_last_action;
83 * Restores user program to initial state and resets all model-checker data
86 void ModelChecker::reset_to_initial_state()
88 DEBUG("+++ Resetting to initial state +++\n");
89 node_stack->reset_execution();
90 failed_promise = false;
91 too_many_reads = false;
92 bad_synchronization = false;
94 snapshotObject->backTrackBeforeStep(0);
97 /** @return a thread ID for a new Thread */
98 thread_id_t ModelChecker::get_next_id()
100 return priv->next_thread_id++;
103 /** @return the number of user threads created during this execution */
104 unsigned int ModelChecker::get_num_threads() const
106 return priv->next_thread_id;
109 /** @return The currently executing Thread. */
110 Thread * ModelChecker::get_current_thread()
112 return scheduler->get_current_thread();
115 /** @return a sequence number for a new ModelAction */
116 modelclock_t ModelChecker::get_next_seq_num()
118 return ++priv->used_sequence_numbers;
121 Node * ModelChecker::get_curr_node() {
122 return node_stack->get_head();
126 * @brief Choose the next thread to execute.
128 * This function chooses the next thread that should execute. It can force the
129 * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
130 * followed by a THREAD_START, or it can enforce execution replay/backtracking.
131 * The model-checker may have no preference regarding the next thread (i.e.,
132 * when exploring a new execution ordering), in which case this will return
134 * @param curr The current ModelAction. This action might guide the choice of
136 * @return The next thread to run. If the model-checker has no preference, NULL.
138 Thread * ModelChecker::get_next_thread(ModelAction *curr)
143 /* Do not split atomic actions. */
145 return thread_current();
146 /* The THREAD_CREATE action points to the created Thread */
147 else if (curr->get_type() == THREAD_CREATE)
148 return (Thread *)curr->get_location();
151 /* Have we completed exploring the preselected path? */
155 /* Else, we are trying to replay an execution */
156 ModelAction *next = node_stack->get_next()->get_action();
158 if (next == diverge) {
159 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
160 earliest_diverge=diverge;
162 Node *nextnode = next->get_node();
163 Node *prevnode = nextnode->get_parent();
164 scheduler->update_sleep_set(prevnode);
166 /* Reached divergence point */
167 if (nextnode->increment_misc()) {
168 /* The next node will try to satisfy a different misc_index values. */
169 tid = next->get_tid();
170 node_stack->pop_restofstack(2);
171 } else if (nextnode->increment_promise()) {
172 /* The next node will try to satisfy a different set of promises. */
173 tid = next->get_tid();
174 node_stack->pop_restofstack(2);
175 } else if (nextnode->increment_read_from()) {
176 /* The next node will read from a different value. */
177 tid = next->get_tid();
178 node_stack->pop_restofstack(2);
179 } else if (nextnode->increment_future_value()) {
180 /* The next node will try to read from a different future value. */
181 tid = next->get_tid();
182 node_stack->pop_restofstack(2);
183 } else if (nextnode->increment_relseq_break()) {
184 /* The next node will try to resolve a release sequence differently */
185 tid = next->get_tid();
186 node_stack->pop_restofstack(2);
188 /* Make a different thread execute for next step */
189 scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
190 tid = prevnode->get_next_backtrack();
191 /* Make sure the backtracked thread isn't sleeping. */
192 node_stack->pop_restofstack(1);
193 if (diverge==earliest_diverge) {
194 earliest_diverge=prevnode->get_action();
197 /* The correct sleep set is in the parent node. */
200 DEBUG("*** Divergence point ***\n");
204 tid = next->get_tid();
206 DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
207 ASSERT(tid != THREAD_ID_T_NONE);
208 return thread_map->get(id_to_int(tid));
212 * We need to know what the next actions of all threads in the sleep
213 * set will be. This method computes them and stores the actions at
214 * the corresponding thread object's pending action.
217 void ModelChecker::execute_sleep_set() {
218 for(unsigned int i=0;i<get_num_threads();i++) {
219 thread_id_t tid=int_to_id(i);
220 Thread *thr=get_thread(tid);
221 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
222 thr->get_pending() == NULL ) {
223 thr->set_state(THREAD_RUNNING);
224 scheduler->next_thread(thr);
225 Thread::swap(&system_context, thr);
226 priv->current_action->set_sleep_flag();
227 thr->set_pending(priv->current_action);
230 priv->current_action = NULL;
233 void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
234 for(unsigned int i=0;i<get_num_threads();i++) {
235 thread_id_t tid=int_to_id(i);
236 Thread *thr=get_thread(tid);
237 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
238 ModelAction *pending_act=thr->get_pending();
239 if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) {
240 //Remove this thread from sleep set
241 scheduler->remove_sleep(thr);
248 * Check if we are in a deadlock. Should only be called at the end of an
249 * execution, although it should not give false positives in the middle of an
250 * execution (there should be some ENABLED thread).
252 * @return True if program is in a deadlock; false otherwise
254 bool ModelChecker::is_deadlocked() const
256 bool blocking_threads = false;
257 for (unsigned int i = 0; i < get_num_threads(); i++) {
258 Thread *t = get_thread(int_to_id(i));
259 if (scheduler->is_enabled(t) != THREAD_DISABLED)
261 else if (!t->is_model_thread() && t->get_pending())
262 blocking_threads = true;
264 return blocking_threads;
268 * Queries the model-checker for more executions to explore and, if one
269 * exists, resets the model-checker state to execute a new execution.
271 * @return If there are more executions to explore, return true. Otherwise,
274 bool ModelChecker::next_execution()
281 printf("ERROR: DEADLOCK\n");
282 if (isfinalfeasible()) {
283 printf("Earliest divergence point since last feasible execution:\n");
284 if (earliest_diverge)
285 earliest_diverge->print();
287 printf("(Not set)\n");
289 earliest_diverge = NULL;
290 num_feasible_executions++;
293 DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
294 pending_rel_seqs->size());
297 if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
302 if ((diverge = get_next_backtrack()) == NULL)
306 printf("Next execution will diverge at:\n");
310 reset_to_initial_state();
314 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
316 switch (act->get_type()) {
320 /* linear search: from most recent to oldest */
321 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
322 action_list_t::reverse_iterator rit;
323 for (rit = list->rbegin(); rit != list->rend(); rit++) {
324 ModelAction *prev = *rit;
325 if (prev->could_synchronize_with(act))
331 case ATOMIC_TRYLOCK: {
332 /* linear search: from most recent to oldest */
333 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
334 action_list_t::reverse_iterator rit;
335 for (rit = list->rbegin(); rit != list->rend(); rit++) {
336 ModelAction *prev = *rit;
337 if (act->is_conflicting_lock(prev))
342 case ATOMIC_UNLOCK: {
343 /* linear search: from most recent to oldest */
344 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
345 action_list_t::reverse_iterator rit;
346 for (rit = list->rbegin(); rit != list->rend(); rit++) {
347 ModelAction *prev = *rit;
348 if (!act->same_thread(prev)&&prev->is_failed_trylock())
354 /* linear search: from most recent to oldest */
355 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
356 action_list_t::reverse_iterator rit;
357 for (rit = list->rbegin(); rit != list->rend(); rit++) {
358 ModelAction *prev = *rit;
359 if (!act->same_thread(prev)&&prev->is_failed_trylock())
361 if (!act->same_thread(prev)&&prev->is_notify())
367 case ATOMIC_NOTIFY_ALL:
368 case ATOMIC_NOTIFY_ONE: {
369 /* linear search: from most recent to oldest */
370 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
371 action_list_t::reverse_iterator rit;
372 for (rit = list->rbegin(); rit != list->rend(); rit++) {
373 ModelAction *prev = *rit;
374 if (!act->same_thread(prev)&&prev->is_wait())
385 /** This method finds backtracking points where we should try to
386 * reorder the parameter ModelAction against.
388 * @param the ModelAction to find backtracking points for.
390 void ModelChecker::set_backtracking(ModelAction *act)
392 Thread *t = get_thread(act);
393 ModelAction * prev = get_last_conflict(act);
397 Node * node = prev->get_node()->get_parent();
399 int low_tid, high_tid;
400 if (node->is_enabled(t)) {
401 low_tid = id_to_int(act->get_tid());
402 high_tid = low_tid+1;
405 high_tid = get_num_threads();
408 for(int i = low_tid; i < high_tid; i++) {
409 thread_id_t tid = int_to_id(i);
411 /* Make sure this thread can be enabled here. */
412 if (i >= node->get_num_threads())
415 /* Don't backtrack into a point where the thread is disabled or sleeping. */
416 if (node->enabled_status(tid)!=THREAD_ENABLED)
419 /* Check if this has been explored already */
420 if (node->has_been_explored(tid))
423 /* See if fairness allows */
424 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
426 for(int t=0;t<node->get_num_threads();t++) {
427 thread_id_t tother=int_to_id(t);
428 if (node->is_enabled(tother) && node->has_priority(tother)) {
436 /* Cache the latest backtracking point */
437 if (!priv->next_backtrack || *prev > *priv->next_backtrack)
438 priv->next_backtrack = prev;
440 /* If this is a new backtracking point, mark the tree */
441 if (!node->set_backtrack(tid))
443 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
444 id_to_int(prev->get_tid()),
445 id_to_int(t->get_id()));
454 * Returns last backtracking point. The model checker will explore a different
455 * path for this point in the next execution.
456 * @return The ModelAction at which the next execution should diverge.
458 ModelAction * ModelChecker::get_next_backtrack()
460 ModelAction *next = priv->next_backtrack;
461 priv->next_backtrack = NULL;
466 * Processes a read or rmw model action.
467 * @param curr is the read model action to process.
468 * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
469 * @return True if processing this read updates the mo_graph.
471 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
473 uint64_t value = VALUE_NONE;
474 bool updated = false;
476 const ModelAction *reads_from = curr->get_node()->get_read_from();
477 if (reads_from != NULL) {
478 mo_graph->startChanges();
480 value = reads_from->get_value();
481 bool r_status = false;
483 if (!second_part_of_rmw) {
484 check_recency(curr, reads_from);
485 r_status = r_modification_order(curr, reads_from);
489 if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
490 mo_graph->rollbackChanges();
491 too_many_reads = false;
495 curr->read_from(reads_from);
496 mo_graph->commitChanges();
497 mo_check_promises(curr->get_tid(), reads_from);
500 } else if (!second_part_of_rmw) {
501 /* Read from future value */
502 value = curr->get_node()->get_future_value();
503 modelclock_t expiration = curr->get_node()->get_future_value_expiration();
504 curr->read_from(NULL);
505 Promise *valuepromise = new Promise(curr, value, expiration);
506 promises->push_back(valuepromise);
508 get_thread(curr)->set_return_value(value);
514 * Processes a lock, trylock, or unlock model action. @param curr is
515 * the read model action to process.
517 * The try lock operation checks whether the lock is taken. If not,
518 * it falls to the normal lock operation case. If so, it returns
521 * The lock operation has already been checked that it is enabled, so
522 * it just grabs the lock and synchronizes with the previous unlock.
524 * The unlock operation has to re-enable all of the threads that are
525 * waiting on the lock.
527 * @return True if synchronization was updated; false otherwise
529 bool ModelChecker::process_mutex(ModelAction *curr) {
530 std::mutex *mutex=NULL;
531 struct std::mutex_state *state=NULL;
533 if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
534 mutex = (std::mutex *)curr->get_location();
535 state = mutex->get_state();
536 } else if(curr->is_wait()) {
537 mutex = (std::mutex *)curr->get_value();
538 state = mutex->get_state();
541 switch (curr->get_type()) {
542 case ATOMIC_TRYLOCK: {
543 bool success = !state->islocked;
544 curr->set_try_lock(success);
546 get_thread(curr)->set_return_value(0);
549 get_thread(curr)->set_return_value(1);
551 //otherwise fall into the lock case
553 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
554 printf("Lock access before initialization\n");
557 state->islocked = true;
558 ModelAction *unlock = get_last_unlock(curr);
559 //synchronize with the previous unlock statement
560 if (unlock != NULL) {
561 curr->synchronize_with(unlock);
566 case ATOMIC_UNLOCK: {
568 state->islocked = false;
569 //wake up the other threads
570 action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
571 //activate all the waiting threads
572 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
573 scheduler->wake(get_thread(*rit));
580 state->islocked = false;
581 //wake up the other threads
582 action_list_t *waiters = lock_waiters_map->get_safe_ptr((void *) curr->get_value());
583 //activate all the waiting threads
584 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
585 scheduler->wake(get_thread(*rit));
588 //check whether we should go to sleep or not...simulate spurious failures
589 if (curr->get_node()->get_misc()==0) {
590 condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
592 scheduler->sleep(get_current_thread());
596 case ATOMIC_NOTIFY_ALL: {
597 action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location());
598 //activate all the waiting threads
599 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
600 scheduler->wake(get_thread(*rit));
605 case ATOMIC_NOTIFY_ONE: {
606 action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location());
607 int wakeupthread=curr->get_node()->get_misc();
608 action_list_t::iterator it = waiters->begin();
609 advance(it, wakeupthread);
610 scheduler->wake(get_thread(*it));
622 * Process a write ModelAction
623 * @param curr The ModelAction to process
624 * @return True if the mo_graph was updated or promises were resolved
626 bool ModelChecker::process_write(ModelAction *curr)
628 bool updated_mod_order = w_modification_order(curr);
629 bool updated_promises = resolve_promises(curr);
631 if (promises->size() == 0) {
632 for (unsigned int i = 0; i < futurevalues->size(); i++) {
633 struct PendingFutureValue pfv = (*futurevalues)[i];
634 //Do more ambitious checks now that mo is more complete
635 if (mo_may_allow(pfv.writer, pfv.act)&&
636 pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
637 (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
638 priv->next_backtrack = pfv.act;
640 futurevalues->resize(0);
643 mo_graph->commitChanges();
644 mo_check_promises(curr->get_tid(), curr);
646 get_thread(curr)->set_return_value(VALUE_NONE);
647 return updated_mod_order || updated_promises;
651 * @brief Process the current action for thread-related activity
653 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
654 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
655 * synchronization, etc. This function is a no-op for non-THREAD actions
656 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
658 * @param curr The current action
659 * @return True if synchronization was updated or a thread completed
661 bool ModelChecker::process_thread_action(ModelAction *curr)
663 bool updated = false;
665 switch (curr->get_type()) {
666 case THREAD_CREATE: {
667 Thread *th = (Thread *)curr->get_location();
668 th->set_creation(curr);
672 Thread *blocking = (Thread *)curr->get_location();
673 ModelAction *act = get_last_action(blocking->get_id());
674 curr->synchronize_with(act);
675 updated = true; /* trigger rel-seq checks */
678 case THREAD_FINISH: {
679 Thread *th = get_thread(curr);
680 while (!th->wait_list_empty()) {
681 ModelAction *act = th->pop_wait_list();
682 scheduler->wake(get_thread(act));
685 updated = true; /* trigger rel-seq checks */
689 check_promises(curr->get_tid(), NULL, curr->get_cv());
700 * @brief Process the current action for release sequence fixup activity
702 * Performs model-checker release sequence fixups for the current action,
703 * forcing a single pending release sequence to break (with a given, potential
704 * "loose" write) or to complete (i.e., synchronize). If a pending release
705 * sequence forms a complete release sequence, then we must perform the fixup
706 * synchronization, mo_graph additions, etc.
708 * @param curr The current action; must be a release sequence fixup action
709 * @param work_queue The work queue to which to add work items as they are
712 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
714 const ModelAction *write = curr->get_node()->get_relseq_break();
715 struct release_seq *sequence = pending_rel_seqs->back();
716 pending_rel_seqs->pop_back();
718 ModelAction *acquire = sequence->acquire;
719 const ModelAction *rf = sequence->rf;
720 const ModelAction *release = sequence->release;
724 ASSERT(release->same_thread(rf));
728 * @todo Forcing a synchronization requires that we set
729 * modification order constraints. For instance, we can't allow
730 * a fixup sequence in which two separate read-acquire
731 * operations read from the same sequence, where the first one
732 * synchronizes and the other doesn't. Essentially, we can't
733 * allow any writes to insert themselves between 'release' and
737 /* Must synchronize */
738 if (!acquire->synchronize_with(release)) {
739 set_bad_synchronization();
742 /* Re-check all pending release sequences */
743 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
744 /* Re-check act for mo_graph edges */
745 work_queue->push_back(MOEdgeWorkEntry(acquire));
747 /* propagate synchronization to later actions */
748 action_list_t::reverse_iterator rit = action_trace->rbegin();
749 for (; (*rit) != acquire; rit++) {
750 ModelAction *propagate = *rit;
751 if (acquire->happens_before(propagate)) {
752 propagate->synchronize_with(acquire);
753 /* Re-check 'propagate' for mo_graph edges */
754 work_queue->push_back(MOEdgeWorkEntry(propagate));
758 /* Break release sequence with new edges:
759 * release --mo--> write --mo--> rf */
760 mo_graph->addEdge(release, write);
761 mo_graph->addEdge(write, rf);
764 /* See if we have realized a data race */
765 if (checkDataRaces())
770 * Initialize the current action by performing one or more of the following
771 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
772 * in the NodeStack, manipulating backtracking sets, allocating and
773 * initializing clock vectors, and computing the promises to fulfill.
775 * @param curr The current action, as passed from the user context; may be
776 * freed/invalidated after the execution of this function, with a different
777 * action "returned" its place (pass-by-reference)
778 * @return True if curr is a newly-explored action; false otherwise
780 bool ModelChecker::initialize_curr_action(ModelAction **curr)
782 ModelAction *newcurr;
784 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
785 newcurr = process_rmw(*curr);
788 if (newcurr->is_rmw())
789 compute_promises(newcurr);
795 (*curr)->set_seq_number(get_next_seq_num());
797 newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
799 /* First restore type and order in case of RMW operation */
800 if ((*curr)->is_rmwr())
801 newcurr->copy_typeandorder(*curr);
803 ASSERT((*curr)->get_location() == newcurr->get_location());
804 newcurr->copy_from_new(*curr);
806 /* Discard duplicate ModelAction; use action from NodeStack */
809 /* Always compute new clock vector */
810 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
813 return false; /* Action was explored previously */
817 /* Always compute new clock vector */
818 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
820 * Perform one-time actions when pushing new ModelAction onto
823 if (newcurr->is_write())
824 compute_promises(newcurr);
825 else if (newcurr->is_relseq_fixup())
826 compute_relseq_breakwrites(newcurr);
827 else if (newcurr->is_wait())
828 newcurr->get_node()->set_misc_max(2);
829 else if (newcurr->is_notify_one()) {
830 newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
832 return true; /* This was a new ModelAction */
837 * @brief Check whether a model action is enabled.
839 * Checks whether a lock or join operation would be successful (i.e., is the
840 * lock already locked, or is the joined thread already complete). If not, put
841 * the action in a waiter list.
843 * @param curr is the ModelAction to check whether it is enabled.
844 * @return a bool that indicates whether the action is enabled.
846 bool ModelChecker::check_action_enabled(ModelAction *curr) {
847 if (curr->is_lock()) {
848 std::mutex * lock = (std::mutex *)curr->get_location();
849 struct std::mutex_state * state = lock->get_state();
850 if (state->islocked) {
851 //Stick the action in the appropriate waiting queue
852 lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
855 } else if (curr->get_type() == THREAD_JOIN) {
856 Thread *blocking = (Thread *)curr->get_location();
857 if (!blocking->is_complete()) {
858 blocking->push_wait_list(curr);
867 * This is the heart of the model checker routine. It performs model-checking
868 * actions corresponding to a given "current action." Among other processes, it
869 * calculates reads-from relationships, updates synchronization clock vectors,
870 * forms a memory_order constraints graph, and handles replay/backtrack
871 * execution when running permutations of previously-observed executions.
873 * @param curr The current action to process
874 * @return The next Thread that must be executed. May be NULL if ModelChecker
875 * makes no choice (e.g., according to replay execution, combining RMW actions,
878 Thread * ModelChecker::check_current_action(ModelAction *curr)
881 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
883 if (!check_action_enabled(curr)) {
884 /* Make the execution look like we chose to run this action
885 * much later, when a lock/join can succeed */
886 get_current_thread()->set_pending(curr);
887 scheduler->sleep(get_current_thread());
888 return get_next_thread(NULL);
891 bool newly_explored = initialize_curr_action(&curr);
893 wake_up_sleeping_actions(curr);
895 /* Add the action to lists before any other model-checking tasks */
896 if (!second_part_of_rmw)
897 add_action_to_lists(curr);
899 /* Build may_read_from set for newly-created actions */
900 if (newly_explored && curr->is_read())
901 build_reads_from_past(curr);
903 /* Initialize work_queue with the "current action" work */
904 work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
905 while (!work_queue.empty()) {
906 WorkQueueEntry work = work_queue.front();
907 work_queue.pop_front();
910 case WORK_CHECK_CURR_ACTION: {
911 ModelAction *act = work.action;
912 bool update = false; /* update this location's release seq's */
913 bool update_all = false; /* update all release seq's */
915 if (process_thread_action(curr))
918 if (act->is_read() && process_read(act, second_part_of_rmw))
921 if (act->is_write() && process_write(act))
924 if (act->is_mutex_op() && process_mutex(act))
927 if (act->is_relseq_fixup())
928 process_relseq_fixup(curr, &work_queue);
931 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
933 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
936 case WORK_CHECK_RELEASE_SEQ:
937 resolve_release_sequences(work.location, &work_queue);
939 case WORK_CHECK_MO_EDGES: {
940 /** @todo Complete verification of work_queue */
941 ModelAction *act = work.action;
942 bool updated = false;
944 if (act->is_read()) {
945 const ModelAction *rf = act->get_reads_from();
946 if (rf != NULL && r_modification_order(act, rf))
949 if (act->is_write()) {
950 if (w_modification_order(act))
953 mo_graph->commitChanges();
956 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
965 check_curr_backtracking(curr);
966 set_backtracking(curr);
967 return get_next_thread(curr);
970 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
971 Node *currnode = curr->get_node();
972 Node *parnode = currnode->get_parent();
974 if ((!parnode->backtrack_empty() ||
975 !currnode->misc_empty() ||
976 !currnode->read_from_empty() ||
977 !currnode->future_value_empty() ||
978 !currnode->promise_empty() ||
979 !currnode->relseq_break_empty())
980 && (!priv->next_backtrack ||
981 *curr > *priv->next_backtrack)) {
982 priv->next_backtrack = curr;
986 bool ModelChecker::promises_expired() {
987 for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
988 Promise *promise = (*promises)[promise_index];
989 if (promise->get_expiration()<priv->used_sequence_numbers) {
996 /** @return whether the current partial trace must be a prefix of a
998 bool ModelChecker::isfeasibleprefix() {
999 return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
1002 /** @return whether the current partial trace is feasible. */
1003 bool ModelChecker::isfeasible() {
1004 if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
1005 DEBUG("Infeasible: RMW violation\n");
1007 return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
1010 /** @return whether the current partial trace is feasible other than
1011 * multiple RMW reading from the same store. */
1012 bool ModelChecker::isfeasibleotherthanRMW() {
1013 if (DBG_ENABLED()) {
1014 if (mo_graph->checkForCycles())
1015 DEBUG("Infeasible: modification order cycles\n");
1017 DEBUG("Infeasible: failed promise\n");
1019 DEBUG("Infeasible: too many reads\n");
1020 if (bad_synchronization)
1021 DEBUG("Infeasible: bad synchronization ordering\n");
1022 if (promises_expired())
1023 DEBUG("Infeasible: promises expired\n");
1025 return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
1028 /** Returns whether the current completed trace is feasible. */
1029 bool ModelChecker::isfinalfeasible() {
1030 if (DBG_ENABLED() && promises->size() != 0)
1031 DEBUG("Infeasible: unrevolved promises\n");
1033 return isfeasible() && promises->size() == 0;
1036 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1037 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1038 ModelAction *lastread = get_last_action(act->get_tid());
1039 lastread->process_rmw(act);
1040 if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
1041 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1042 mo_graph->commitChanges();
1048 * Checks whether a thread has read from the same write for too many times
1049 * without seeing the effects of a later write.
1052 * 1) there must a different write that we could read from that would satisfy the modification order,
1053 * 2) we must have read from the same value in excess of maxreads times, and
1054 * 3) that other write must have been in the reads_from set for maxreads times.
1056 * If so, we decide that the execution is no longer feasible.
1058 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
1059 if (params.maxreads != 0) {
1061 if (curr->get_node()->get_read_from_size() <= 1)
1063 //Must make sure that execution is currently feasible... We could
1064 //accidentally clear by rolling back
1067 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1068 int tid = id_to_int(curr->get_tid());
1071 if ((int)thrd_lists->size() <= tid)
1073 action_list_t *list = &(*thrd_lists)[tid];
1075 action_list_t::reverse_iterator rit = list->rbegin();
1076 /* Skip past curr */
1077 for (; (*rit) != curr; rit++)
1079 /* go past curr now */
1082 action_list_t::reverse_iterator ritcopy = rit;
1083 //See if we have enough reads from the same value
1085 for (; count < params.maxreads; rit++,count++) {
1086 if (rit==list->rend())
1088 ModelAction *act = *rit;
1089 if (!act->is_read())
1092 if (act->get_reads_from() != rf)
1094 if (act->get_node()->get_read_from_size() <= 1)
1097 for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
1099 const ModelAction * write = curr->get_node()->get_read_from_at(i);
1101 //Need a different write
1105 /* Test to see whether this is a feasible write to read from*/
1106 mo_graph->startChanges();
1107 r_modification_order(curr, write);
1108 bool feasiblereadfrom = isfeasible();
1109 mo_graph->rollbackChanges();
1111 if (!feasiblereadfrom)
1115 bool feasiblewrite = true;
1116 //new we need to see if this write works for everyone
1118 for (int loop = count; loop>0; loop--,rit++) {
1119 ModelAction *act=*rit;
1120 bool foundvalue = false;
1121 for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
1122 if (act->get_node()->get_read_from_at(j)==write) {
1128 feasiblewrite = false;
1132 if (feasiblewrite) {
1133 too_many_reads = true;
1141 * Updates the mo_graph with the constraints imposed from the current
1144 * Basic idea is the following: Go through each other thread and find
1145 * the lastest action that happened before our read. Two cases:
1147 * (1) The action is a write => that write must either occur before
1148 * the write we read from or be the write we read from.
1150 * (2) The action is a read => the write that that action read from
1151 * must occur before the write we read from or be the same write.
1153 * @param curr The current action. Must be a read.
1154 * @param rf The action that curr reads from. Must be a write.
1155 * @return True if modification order edges were added; false otherwise
1157 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
1159 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1162 ASSERT(curr->is_read());
1164 /* Iterate over all threads */
1165 for (i = 0; i < thrd_lists->size(); i++) {
1166 /* Iterate over actions in thread, starting from most recent */
1167 action_list_t *list = &(*thrd_lists)[i];
1168 action_list_t::reverse_iterator rit;
1169 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1170 ModelAction *act = *rit;
1173 * Include at most one act per-thread that "happens
1174 * before" curr. Don't consider reflexively.
1176 if (act->happens_before(curr) && act != curr) {
1177 if (act->is_write()) {
1179 mo_graph->addEdge(act, rf);
1183 const ModelAction *prevreadfrom = act->get_reads_from();
1184 //if the previous read is unresolved, keep going...
1185 if (prevreadfrom == NULL)
1188 if (rf != prevreadfrom) {
1189 mo_graph->addEdge(prevreadfrom, rf);
1201 /** This method fixes up the modification order when we resolve a
1202 * promises. The basic problem is that actions that occur after the
1203 * read curr could not property add items to the modification order
1206 * So for each thread, we find the earliest item that happens after
1207 * the read curr. This is the item we have to fix up with additional
1208 * constraints. If that action is write, we add a MO edge between
1209 * the Action rf and that action. If the action is a read, we add a
1210 * MO edge between the Action rf, and whatever the read accessed.
1212 * @param curr is the read ModelAction that we are fixing up MO edges for.
1213 * @param rf is the write ModelAction that curr reads from.
1216 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1218 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1220 ASSERT(curr->is_read());
1222 /* Iterate over all threads */
1223 for (i = 0; i < thrd_lists->size(); i++) {
1224 /* Iterate over actions in thread, starting from most recent */
1225 action_list_t *list = &(*thrd_lists)[i];
1226 action_list_t::reverse_iterator rit;
1227 ModelAction *lastact = NULL;
1229 /* Find last action that happens after curr that is either not curr or a rmw */
1230 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1231 ModelAction *act = *rit;
1232 if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1238 /* Include at most one act per-thread that "happens before" curr */
1239 if (lastact != NULL) {
1240 if (lastact==curr) {
1241 //Case 1: The resolved read is a RMW, and we need to make sure
1242 //that the write portion of the RMW mod order after rf
1244 mo_graph->addEdge(rf, lastact);
1245 } else if (lastact->is_read()) {
1246 //Case 2: The resolved read is a normal read and the next
1247 //operation is a read, and we need to make sure the value read
1248 //is mod ordered after rf
1250 const ModelAction *postreadfrom = lastact->get_reads_from();
1251 if (postreadfrom != NULL&&rf != postreadfrom)
1252 mo_graph->addEdge(rf, postreadfrom);
1254 //Case 3: The resolved read is a normal read and the next
1255 //operation is a write, and we need to make sure that the
1256 //write is mod ordered after rf
1258 mo_graph->addEdge(rf, lastact);
1266 * Updates the mo_graph with the constraints imposed from the current write.
1268 * Basic idea is the following: Go through each other thread and find
1269 * the lastest action that happened before our write. Two cases:
1271 * (1) The action is a write => that write must occur before
1274 * (2) The action is a read => the write that that action read from
1275 * must occur before the current write.
1277 * This method also handles two other issues:
1279 * (I) Sequential Consistency: Making sure that if the current write is
1280 * seq_cst, that it occurs after the previous seq_cst write.
1282 * (II) Sending the write back to non-synchronizing reads.
1284 * @param curr The current action. Must be a write.
1285 * @return True if modification order edges were added; false otherwise
1287 bool ModelChecker::w_modification_order(ModelAction *curr)
1289 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1292 ASSERT(curr->is_write());
1294 if (curr->is_seqcst()) {
1295 /* We have to at least see the last sequentially consistent write,
1296 so we are initialized. */
1297 ModelAction *last_seq_cst = get_last_seq_cst(curr);
1298 if (last_seq_cst != NULL) {
1299 mo_graph->addEdge(last_seq_cst, curr);
1304 /* Iterate over all threads */
1305 for (i = 0; i < thrd_lists->size(); i++) {
1306 /* Iterate over actions in thread, starting from most recent */
1307 action_list_t *list = &(*thrd_lists)[i];
1308 action_list_t::reverse_iterator rit;
1309 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1310 ModelAction *act = *rit;
1313 * 1) If RMW and it actually read from something, then we
1314 * already have all relevant edges, so just skip to next
1317 * 2) If RMW and it didn't read from anything, we should
1318 * whatever edge we can get to speed up convergence.
1320 * 3) If normal write, we need to look at earlier actions, so
1321 * continue processing list.
1323 if (curr->is_rmw()) {
1324 if (curr->get_reads_from()!=NULL)
1333 * Include at most one act per-thread that "happens
1336 if (act->happens_before(curr)) {
1338 * Note: if act is RMW, just add edge:
1340 * The following edge should be handled elsewhere:
1341 * readfrom(act) --mo--> act
1343 if (act->is_write())
1344 mo_graph->addEdge(act, curr);
1345 else if (act->is_read()) {
1346 //if previous read accessed a null, just keep going
1347 if (act->get_reads_from() == NULL)
1349 mo_graph->addEdge(act->get_reads_from(), curr);
1353 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1354 !act->same_thread(curr)) {
1355 /* We have an action that:
1356 (1) did not happen before us
1357 (2) is a read and we are a write
1358 (3) cannot synchronize with us
1359 (4) is in a different thread
1361 that read could potentially read from our write. Note that
1362 these checks are overly conservative at this point, we'll
1363 do more checks before actually removing the
1367 if (thin_air_constraint_may_allow(curr, act)) {
1369 (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
1370 struct PendingFutureValue pfv = {curr,act};
1371 futurevalues->push_back(pfv);
1381 /** Arbitrary reads from the future are not allowed. Section 29.3
1382 * part 9 places some constraints. This method checks one result of constraint
1383 * constraint. Others require compiler support. */
1384 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
1385 if (!writer->is_rmw())
1388 if (!reader->is_rmw())
1391 for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1392 if (search == reader)
1394 if (search->get_tid() == reader->get_tid() &&
1395 search->happens_before(reader))
1403 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1404 * some constraints. This method checks one the following constraint (others
1405 * require compiler support):
1407 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1409 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1411 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
1413 /* Iterate over all threads */
1414 for (i = 0; i < thrd_lists->size(); i++) {
1415 const ModelAction *write_after_read = NULL;
1417 /* Iterate over actions in thread, starting from most recent */
1418 action_list_t *list = &(*thrd_lists)[i];
1419 action_list_t::reverse_iterator rit;
1420 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1421 ModelAction *act = *rit;
1423 if (!reader->happens_before(act))
1425 else if (act->is_write())
1426 write_after_read = act;
1427 else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
1428 write_after_read = act->get_reads_from();
1432 if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
1439 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1440 * The ModelAction under consideration is expected to be taking part in
1441 * release/acquire synchronization as an object of the "reads from" relation.
1442 * Note that this can only provide release sequence support for RMW chains
1443 * which do not read from the future, as those actions cannot be traced until
1444 * their "promise" is fulfilled. Similarly, we may not even establish the
1445 * presence of a release sequence with certainty, as some modification order
1446 * constraints may be decided further in the future. Thus, this function
1447 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1448 * and a boolean representing certainty.
1450 * @param rf The action that might be part of a release sequence. Must be a
1452 * @param release_heads A pass-by-reference style return parameter. After
1453 * execution of this function, release_heads will contain the heads of all the
1454 * relevant release sequences, if any exists with certainty
1455 * @param pending A pass-by-reference style return parameter which is only used
1456 * when returning false (i.e., uncertain). Returns most information regarding
1457 * an uncertain release sequence, including any write operations that might
1458 * break the sequence.
1459 * @return true, if the ModelChecker is certain that release_heads is complete;
1462 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1463 rel_heads_list_t *release_heads,
1464 struct release_seq *pending) const
1466 /* Only check for release sequences if there are no cycles */
1467 if (mo_graph->checkForCycles())
1471 ASSERT(rf->is_write());
1473 if (rf->is_release())
1474 release_heads->push_back(rf);
1476 break; /* End of RMW chain */
1478 /** @todo Need to be smarter here... In the linux lock
1479 * example, this will run to the beginning of the program for
1481 /** @todo The way to be smarter here is to keep going until 1
1482 * thread has a release preceded by an acquire and you've seen
1485 /* acq_rel RMW is a sufficient stopping condition */
1486 if (rf->is_acquire() && rf->is_release())
1487 return true; /* complete */
1489 rf = rf->get_reads_from();
1492 /* read from future: need to settle this later */
1494 return false; /* incomplete */
1497 if (rf->is_release())
1498 return true; /* complete */
1500 /* else relaxed write; check modification order for contiguous subsequence
1501 * -> rf must be same thread as release */
1502 int tid = id_to_int(rf->get_tid());
1503 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
1504 action_list_t *list = &(*thrd_lists)[tid];
1505 action_list_t::const_reverse_iterator rit;
1507 /* Find rf in the thread list */
1508 rit = std::find(list->rbegin(), list->rend(), rf);
1509 ASSERT(rit != list->rend());
1511 /* Find the last write/release */
1512 for (; rit != list->rend(); rit++)
1513 if ((*rit)->is_release())
1515 if (rit == list->rend()) {
1516 /* No write-release in this thread */
1517 return true; /* complete */
1519 ModelAction *release = *rit;
1521 ASSERT(rf->same_thread(release));
1523 pending->writes.clear();
1525 bool certain = true;
1526 for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1527 if (id_to_int(rf->get_tid()) == (int)i)
1529 list = &(*thrd_lists)[i];
1531 /* Can we ensure no future writes from this thread may break
1532 * the release seq? */
1533 bool future_ordered = false;
1535 ModelAction *last = get_last_action(int_to_id(i));
1536 Thread *th = get_thread(int_to_id(i));
1537 if ((last && rf->happens_before(last)) ||
1538 !scheduler->is_enabled(th) ||
1540 future_ordered = true;
1542 ASSERT(!th->is_model_thread() || future_ordered);
1544 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1545 const ModelAction *act = *rit;
1546 /* Reach synchronization -> this thread is complete */
1547 if (act->happens_before(release))
1549 if (rf->happens_before(act)) {
1550 future_ordered = true;
1554 /* Only non-RMW writes can break release sequences */
1555 if (!act->is_write() || act->is_rmw())
1558 /* Check modification order */
1559 if (mo_graph->checkReachable(rf, act)) {
1560 /* rf --mo--> act */
1561 future_ordered = true;
1564 if (mo_graph->checkReachable(act, release))
1565 /* act --mo--> release */
1567 if (mo_graph->checkReachable(release, act) &&
1568 mo_graph->checkReachable(act, rf)) {
1569 /* release --mo-> act --mo--> rf */
1570 return true; /* complete */
1572 /* act may break release sequence */
1573 pending->writes.push_back(act);
1576 if (!future_ordered)
1577 certain = false; /* This thread is uncertain */
1581 release_heads->push_back(release);
1582 pending->writes.clear();
1584 pending->release = release;
1591 * A public interface for getting the release sequence head(s) with which a
1592 * given ModelAction must synchronize. This function only returns a non-empty
1593 * result when it can locate a release sequence head with certainty. Otherwise,
1594 * it may mark the internal state of the ModelChecker so that it will handle
1595 * the release sequence at a later time, causing @a act to update its
1596 * synchronization at some later point in execution.
1597 * @param act The 'acquire' action that may read from a release sequence
1598 * @param release_heads A pass-by-reference return parameter. Will be filled
1599 * with the head(s) of the release sequence(s), if they exists with certainty.
1600 * @see ModelChecker::release_seq_heads
1602 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
1604 const ModelAction *rf = act->get_reads_from();
1605 struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
1606 sequence->acquire = act;
1608 if (!release_seq_heads(rf, release_heads, sequence)) {
1609 /* add act to 'lazy checking' list */
1610 pending_rel_seqs->push_back(sequence);
1612 snapshot_free(sequence);
1617 * Attempt to resolve all stashed operations that might synchronize with a
1618 * release sequence for a given location. This implements the "lazy" portion of
1619 * determining whether or not a release sequence was contiguous, since not all
1620 * modification order information is present at the time an action occurs.
1622 * @param location The location/object that should be checked for release
1623 * sequence resolutions. A NULL value means to check all locations.
1624 * @param work_queue The work queue to which to add work items as they are
1626 * @return True if any updates occurred (new synchronization, new mo_graph
1629 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
1631 bool updated = false;
1632 std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
1633 while (it != pending_rel_seqs->end()) {
1634 struct release_seq *pending = *it;
1635 ModelAction *act = pending->acquire;
1637 /* Only resolve sequences on the given location, if provided */
1638 if (location && act->get_location() != location) {
1643 const ModelAction *rf = act->get_reads_from();
1644 rel_heads_list_t release_heads;
1646 complete = release_seq_heads(rf, &release_heads, pending);
1647 for (unsigned int i = 0; i < release_heads.size(); i++) {
1648 if (!act->has_synchronized_with(release_heads[i])) {
1649 if (act->synchronize_with(release_heads[i]))
1652 set_bad_synchronization();
1657 /* Re-check all pending release sequences */
1658 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1659 /* Re-check act for mo_graph edges */
1660 work_queue->push_back(MOEdgeWorkEntry(act));
1662 /* propagate synchronization to later actions */
1663 action_list_t::reverse_iterator rit = action_trace->rbegin();
1664 for (; (*rit) != act; rit++) {
1665 ModelAction *propagate = *rit;
1666 if (act->happens_before(propagate)) {
1667 propagate->synchronize_with(act);
1668 /* Re-check 'propagate' for mo_graph edges */
1669 work_queue->push_back(MOEdgeWorkEntry(propagate));
1674 it = pending_rel_seqs->erase(it);
1675 snapshot_free(pending);
1681 // If we resolved promises or data races, see if we have realized a data race.
1682 if (checkDataRaces()) {
1690 * Performs various bookkeeping operations for the current ModelAction. For
1691 * instance, adds action to the per-object, per-thread action vector and to the
1692 * action trace list of all thread actions.
1694 * @param act is the ModelAction to add.
1696 void ModelChecker::add_action_to_lists(ModelAction *act)
1698 int tid = id_to_int(act->get_tid());
1699 action_trace->push_back(act);
1701 obj_map->get_safe_ptr(act->get_location())->push_back(act);
1703 std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
1704 if (tid >= (int)vec->size())
1705 vec->resize(priv->next_thread_id);
1706 (*vec)[tid].push_back(act);
1708 if ((int)thrd_last_action->size() <= tid)
1709 thrd_last_action->resize(get_num_threads());
1710 (*thrd_last_action)[tid] = act;
1712 if (act->is_wait()) {
1713 void *mutex_loc=(void *) act->get_value();
1714 obj_map->get_safe_ptr(mutex_loc)->push_back(act);
1716 std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
1717 if (tid >= (int)vec->size())
1718 vec->resize(priv->next_thread_id);
1719 (*vec)[tid].push_back(act);
1721 if ((int)thrd_last_action->size() <= tid)
1722 thrd_last_action->resize(get_num_threads());
1723 (*thrd_last_action)[tid] = act;
1728 * @brief Get the last action performed by a particular Thread
1729 * @param tid The thread ID of the Thread in question
1730 * @return The last action in the thread
1732 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
1734 int threadid = id_to_int(tid);
1735 if (threadid < (int)thrd_last_action->size())
1736 return (*thrd_last_action)[id_to_int(tid)];
1742 * Gets the last memory_order_seq_cst write (in the total global sequence)
1743 * performed on a particular object (i.e., memory location), not including the
1745 * @param curr The current ModelAction; also denotes the object location to
1747 * @return The last seq_cst write
1749 ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
1751 void *location = curr->get_location();
1752 action_list_t *list = obj_map->get_safe_ptr(location);
1753 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1754 action_list_t::reverse_iterator rit;
1755 for (rit = list->rbegin(); rit != list->rend(); rit++)
1756 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
1762 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1763 * location). This function identifies the mutex according to the current
1764 * action, which is presumed to perform on the same mutex.
1765 * @param curr The current ModelAction; also denotes the object location to
1767 * @return The last unlock operation
1769 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
1771 void *location = curr->get_location();
1772 action_list_t *list = obj_map->get_safe_ptr(location);
1773 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1774 action_list_t::reverse_iterator rit;
1775 for (rit = list->rbegin(); rit != list->rend(); rit++)
1776 if ((*rit)->is_unlock() || (*rit)->is_wait())
1781 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
1783 ModelAction *parent = get_last_action(tid);
1785 parent = get_thread(tid)->get_creation();
1790 * Returns the clock vector for a given thread.
1791 * @param tid The thread whose clock vector we want
1792 * @return Desired clock vector
1794 ClockVector * ModelChecker::get_cv(thread_id_t tid)
1796 return get_parent_action(tid)->get_cv();
1800 * Resolve a set of Promises with a current write. The set is provided in the
1801 * Node corresponding to @a write.
1802 * @param write The ModelAction that is fulfilling Promises
1803 * @return True if promises were resolved; false otherwise
1805 bool ModelChecker::resolve_promises(ModelAction *write)
1807 bool resolved = false;
1808 std::vector< thread_id_t, ModelAlloc<thread_id_t> > threads_to_check;
1810 for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
1811 Promise *promise = (*promises)[promise_index];
1812 if (write->get_node()->get_promise(i)) {
1813 ModelAction *read = promise->get_action();
1814 if (read->is_rmw()) {
1815 mo_graph->addRMWEdge(write, read);
1817 read->read_from(write);
1818 //First fix up the modification order for actions that happened
1820 r_modification_order(read, write);
1821 //Next fix up the modification order for actions that happened
1823 post_r_modification_order(read, write);
1824 //Make sure the promise's value matches the write's value
1825 ASSERT(promise->get_value() == write->get_value());
1828 promises->erase(promises->begin() + promise_index);
1829 threads_to_check.push_back(read->get_tid());
1836 //Check whether reading these writes has made threads unable to
1839 for(unsigned int i=0;i<threads_to_check.size();i++)
1840 mo_check_promises(threads_to_check[i], write);
1846 * Compute the set of promises that could potentially be satisfied by this
1847 * action. Note that the set computation actually appears in the Node, not in
1849 * @param curr The ModelAction that may satisfy promises
1851 void ModelChecker::compute_promises(ModelAction *curr)
1853 for (unsigned int i = 0; i < promises->size(); i++) {
1854 Promise *promise = (*promises)[i];
1855 const ModelAction *act = promise->get_action();
1856 if (!act->happens_before(curr) &&
1858 !act->could_synchronize_with(curr) &&
1859 !act->same_thread(curr) &&
1860 act->get_location() == curr->get_location() &&
1861 promise->get_value() == curr->get_value()) {
1862 curr->get_node()->set_promise(i, act->is_rmw());
1867 /** Checks promises in response to change in ClockVector Threads. */
1868 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
1870 for (unsigned int i = 0; i < promises->size(); i++) {
1871 Promise *promise = (*promises)[i];
1872 const ModelAction *act = promise->get_action();
1873 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
1874 merge_cv->synchronized_since(act)) {
1875 if (promise->increment_threads(tid)) {
1876 //Promise has failed
1877 failed_promise = true;
1884 void ModelChecker::check_promises_thread_disabled() {
1885 for (unsigned int i = 0; i < promises->size(); i++) {
1886 Promise *promise = (*promises)[i];
1887 if (promise->check_promise()) {
1888 failed_promise = true;
1894 /** Checks promises in response to addition to modification order for threads.
1896 * pthread is the thread that performed the read that created the promise
1898 * pread is the read that created the promise
1900 * pwrite is either the first write to same location as pread by
1901 * pthread that is sequenced after pread or the value read by the
1902 * first read to the same lcoation as pread by pthread that is
1903 * sequenced after pread..
1905 * 1. If tid=pthread, then we check what other threads are reachable
1906 * through the mode order starting with pwrite. Those threads cannot
1907 * perform a write that will resolve the promise due to modification
1908 * order constraints.
1910 * 2. If the tid is not pthread, we check whether pwrite can reach the
1911 * action write through the modification order. If so, that thread
1912 * cannot perform a future write that will resolve the promise due to
1913 * modificatin order constraints.
1915 * @parem tid The thread that either read from the model action
1916 * write, or actually did the model action write.
1918 * @parem write The ModelAction representing the relevant write.
1921 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
1922 void * location = write->get_location();
1923 for (unsigned int i = 0; i < promises->size(); i++) {
1924 Promise *promise = (*promises)[i];
1925 const ModelAction *act = promise->get_action();
1927 //Is this promise on the same location?
1928 if ( act->get_location() != location )
1931 //same thread as the promise
1932 if ( act->get_tid()==tid ) {
1934 //do we have a pwrite for the promise, if not, set it
1935 if (promise->get_write() == NULL ) {
1936 promise->set_write(write);
1937 //The pwrite cannot happen before the promise
1938 if (write->happens_before(act) && (write != act)) {
1939 failed_promise = true;
1943 if (mo_graph->checkPromise(write, promise)) {
1944 failed_promise = true;
1949 //Don't do any lookups twice for the same thread
1950 if (promise->has_sync_thread(tid))
1953 if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
1954 if (promise->increment_threads(tid)) {
1955 failed_promise = true;
1963 * Compute the set of writes that may break the current pending release
1964 * sequence. This information is extracted from previou release sequence
1967 * @param curr The current ModelAction. Must be a release sequence fixup
1970 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
1972 if (pending_rel_seqs->empty())
1975 struct release_seq *pending = pending_rel_seqs->back();
1976 for (unsigned int i = 0; i < pending->writes.size(); i++) {
1977 const ModelAction *write = pending->writes[i];
1978 curr->get_node()->add_relseq_break(write);
1981 /* NULL means don't break the sequence; just synchronize */
1982 curr->get_node()->add_relseq_break(NULL);
1986 * Build up an initial set of all past writes that this 'read' action may read
1987 * from. This set is determined by the clock vector's "happens before"
1989 * @param curr is the current ModelAction that we are exploring; it must be a
1992 void ModelChecker::build_reads_from_past(ModelAction *curr)
1994 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1996 ASSERT(curr->is_read());
1998 ModelAction *last_seq_cst = NULL;
2000 /* Track whether this object has been initialized */
2001 bool initialized = false;
2003 if (curr->is_seqcst()) {
2004 last_seq_cst = get_last_seq_cst(curr);
2005 /* We have to at least see the last sequentially consistent write,
2006 so we are initialized. */
2007 if (last_seq_cst != NULL)
2011 /* Iterate over all threads */
2012 for (i = 0; i < thrd_lists->size(); i++) {
2013 /* Iterate over actions in thread, starting from most recent */
2014 action_list_t *list = &(*thrd_lists)[i];
2015 action_list_t::reverse_iterator rit;
2016 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2017 ModelAction *act = *rit;
2019 /* Only consider 'write' actions */
2020 if (!act->is_write() || act == curr)
2023 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2024 if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
2025 DEBUG("Adding action to may_read_from:\n");
2026 if (DBG_ENABLED()) {
2031 if (curr->get_sleep_flag() && ! curr->is_seqcst()) {
2032 if (sleep_can_read_from(curr, act))
2033 curr->get_node()->add_read_from(act);
2035 curr->get_node()->add_read_from(act);
2038 /* Include at most one act per-thread that "happens before" curr */
2039 if (act->happens_before(curr)) {
2047 /** @todo Need a more informative way of reporting errors. */
2048 printf("ERROR: may read from uninitialized atomic\n");
2052 if (DBG_ENABLED() || !initialized) {
2053 printf("Reached read action:\n");
2055 printf("Printing may_read_from\n");
2056 curr->get_node()->print_may_read_from();
2057 printf("End printing may_read_from\n");
2061 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
2063 Node *prevnode=write->get_node()->get_parent();
2065 bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
2066 if (write->is_release()&&thread_sleep)
2068 if (!write->is_rmw()) {
2071 if (write->get_reads_from()==NULL)
2073 write=write->get_reads_from();
2077 static void print_list(action_list_t *list)
2079 action_list_t::iterator it;
2081 printf("---------------------------------------------------------------------\n");
2083 unsigned int hash=0;
2085 for (it = list->begin(); it != list->end(); it++) {
2087 hash=hash^(hash<<3)^((*it)->hash());
2089 printf("HASH %u\n", hash);
2090 printf("---------------------------------------------------------------------\n");
2093 #if SUPPORT_MOD_ORDER_DUMP
2094 void ModelChecker::dumpGraph(char *filename) {
2096 sprintf(buffer, "%s.dot",filename);
2097 FILE *file=fopen(buffer, "w");
2098 fprintf(file, "digraph %s {\n",filename);
2099 mo_graph->dumpNodes(file);
2100 ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
2102 for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2103 ModelAction *action=*it;
2104 if (action->is_read()) {
2105 fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
2106 if (action->get_reads_from()!=NULL)
2107 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2109 if (thread_array[action->get_tid()] != NULL) {
2110 fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2113 thread_array[action->get_tid()]=action;
2115 fprintf(file,"}\n");
2116 model_free(thread_array);
2121 void ModelChecker::print_summary()
2124 printf("Number of executions: %d\n", num_executions);
2125 printf("Number of feasible executions: %d\n", num_feasible_executions);
2126 printf("Total nodes created: %d\n", node_stack->get_total_nodes());
2128 #if SUPPORT_MOD_ORDER_DUMP
2130 char buffername[100];
2131 sprintf(buffername, "exec%04u", num_executions);
2132 mo_graph->dumpGraphToFile(buffername);
2133 sprintf(buffername, "graph%04u", num_executions);
2134 dumpGraph(buffername);
2137 if (!isfinalfeasible())
2138 printf("INFEASIBLE EXECUTION!\n");
2139 print_list(action_trace);
2144 * Add a Thread to the system for the first time. Should only be called once
2146 * @param t The Thread to add
2148 void ModelChecker::add_thread(Thread *t)
2150 thread_map->put(id_to_int(t->get_id()), t);
2151 scheduler->add_thread(t);
2155 * Removes a thread from the scheduler.
2156 * @param the thread to remove.
2158 void ModelChecker::remove_thread(Thread *t)
2160 scheduler->remove_thread(t);
2164 * @brief Get a Thread reference by its ID
2165 * @param tid The Thread's ID
2166 * @return A Thread reference
2168 Thread * ModelChecker::get_thread(thread_id_t tid) const
2170 return thread_map->get(id_to_int(tid));
2174 * @brief Get a reference to the Thread in which a ModelAction was executed
2175 * @param act The ModelAction
2176 * @return A Thread reference
2178 Thread * ModelChecker::get_thread(ModelAction *act) const
2180 return get_thread(act->get_tid());
2184 * Switch from a user-context to the "master thread" context (a.k.a. system
2185 * context). This switch is made with the intention of exploring a particular
2186 * model-checking action (described by a ModelAction object). Must be called
2187 * from a user-thread context.
2189 * @param act The current action that will be explored. May be NULL only if
2190 * trace is exiting via an assertion (see ModelChecker::set_assert and
2191 * ModelChecker::has_asserted).
2192 * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
2194 int ModelChecker::switch_to_master(ModelAction *act)
2197 Thread *old = thread_current();
2198 set_current_action(act);
2199 old->set_state(THREAD_READY);
2200 return Thread::swap(old, &system_context);
2204 * Takes the next step in the execution, if possible.
2205 * @return Returns true (success) if a step was taken and false otherwise.
2207 bool ModelChecker::take_step() {
2211 Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
2213 if (curr->get_state() == THREAD_READY) {
2214 ASSERT(priv->current_action);
2216 priv->nextThread = check_current_action(priv->current_action);
2217 priv->current_action = NULL;
2219 if (curr->is_blocked() || curr->is_complete())
2220 scheduler->remove_thread(curr);
2225 Thread *next = scheduler->next_thread(priv->nextThread);
2227 /* Infeasible -> don't take any more steps */
2231 if (params.bound != 0) {
2232 if (priv->used_sequence_numbers > params.bound) {
2237 DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
2238 next ? id_to_int(next->get_id()) : -1);
2241 * Launch end-of-execution release sequence fixups only when there are:
2243 * (1) no more user threads to run (or when execution replay chooses
2244 * the 'model_thread')
2245 * (2) pending release sequences
2246 * (3) pending assertions (i.e., data races)
2247 * (4) no pending promises
2249 if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
2250 isfinalfeasible() && !unrealizedraces.empty()) {
2251 printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2252 pending_rel_seqs->size());
2253 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2254 std::memory_order_seq_cst, NULL, VALUE_NONE,
2256 set_current_action(fixup);
2260 /* next == NULL -> don't take any more steps */
2264 next->set_state(THREAD_RUNNING);
2266 if (next->get_pending() != NULL) {
2267 /* restart a pending action */
2268 set_current_action(next->get_pending());
2269 next->set_pending(NULL);
2270 next->set_state(THREAD_READY);
2274 /* Return false only if swap fails with an error */
2275 return (Thread::swap(&system_context, next) == 0);
2278 /** Runs the current execution until threre are no more steps to take. */
2279 void ModelChecker::finish_execution() {
2282 while (take_step());