9 #include "snapshot-interface.h"
11 #include "clockvector.h"
12 #include "cyclegraph.h"
15 #include "threads-model.h"
17 #define INITIAL_THREAD_ID 0
22 bug_message(const char *str) {
23 const char *fmt = " [BUG] %s\n";
24 msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
25 sprintf(msg, fmt, str);
27 ~bug_message() { if (msg) snapshot_free(msg); }
30 void print() { printf("%s", msg); }
36 * Structure for holding small ModelChecker members that should be snapshotted
38 struct model_snapshot_members {
39 ModelAction *current_action;
40 unsigned int next_thread_id;
41 modelclock_t used_sequence_numbers;
43 ModelAction *next_backtrack;
44 std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
45 struct execution_stats stats;
48 /** @brief Constructor */
49 ModelChecker::ModelChecker(struct model_params params) :
50 /* Initialize default scheduler */
52 scheduler(new Scheduler()),
54 earliest_diverge(NULL),
55 action_trace(new action_list_t()),
56 thread_map(new HashTable<int, Thread *, int>()),
57 obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
58 lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
59 condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
60 obj_thrd_map(new HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 >()),
61 promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
62 futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
63 pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
64 thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
65 node_stack(new NodeStack()),
66 mo_graph(new CycleGraph()),
67 failed_promise(false),
68 too_many_reads(false),
70 bad_synchronization(false)
72 /* Allocate this "size" on the snapshotting heap */
73 priv = (struct model_snapshot_members *)snapshot_calloc(1, sizeof(*priv));
74 /* First thread created will have id INITIAL_THREAD_ID */
75 priv->next_thread_id = INITIAL_THREAD_ID;
77 /* Initialize a model-checker thread, for special ModelActions */
78 model_thread = new Thread(get_next_id());
79 thread_map->put(id_to_int(model_thread->get_id()), model_thread);
82 /** @brief Destructor */
83 ModelChecker::~ModelChecker()
85 for (unsigned int i = 0; i < get_num_threads(); i++)
86 delete thread_map->get(i);
91 delete lock_waiters_map;
92 delete condvar_waiters_map;
95 for (unsigned int i = 0; i < promises->size(); i++)
96 delete (*promises)[i];
99 delete pending_rel_seqs;
101 delete thrd_last_action;
106 for (unsigned int i = 0; i < priv->bugs.size(); i++)
107 delete priv->bugs[i];
112 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
113 action_list_t * tmp=hash->get(ptr);
115 tmp=new action_list_t();
121 static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr) {
122 std::vector<action_list_t> * tmp=hash->get(ptr);
124 tmp=new std::vector<action_list_t>();
131 * Restores user program to initial state and resets all model-checker data
134 void ModelChecker::reset_to_initial_state()
136 DEBUG("+++ Resetting to initial state +++\n");
137 node_stack->reset_execution();
138 failed_promise = false;
139 too_many_reads = false;
140 bad_synchronization = false;
142 snapshotObject->backTrackBeforeStep(0);
145 /** @return a thread ID for a new Thread */
146 thread_id_t ModelChecker::get_next_id()
148 return priv->next_thread_id++;
151 /** @return the number of user threads created during this execution */
152 unsigned int ModelChecker::get_num_threads() const
154 return priv->next_thread_id;
157 /** @return The currently executing Thread. */
158 Thread * ModelChecker::get_current_thread()
160 return scheduler->get_current_thread();
163 /** @return a sequence number for a new ModelAction */
164 modelclock_t ModelChecker::get_next_seq_num()
166 return ++priv->used_sequence_numbers;
169 Node * ModelChecker::get_curr_node() {
170 return node_stack->get_head();
174 * @brief Choose the next thread to execute.
176 * This function chooses the next thread that should execute. It can force the
177 * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
178 * followed by a THREAD_START, or it can enforce execution replay/backtracking.
179 * The model-checker may have no preference regarding the next thread (i.e.,
180 * when exploring a new execution ordering), in which case this will return
182 * @param curr The current ModelAction. This action might guide the choice of
184 * @return The next thread to run. If the model-checker has no preference, NULL.
186 Thread * ModelChecker::get_next_thread(ModelAction *curr)
191 /* Do not split atomic actions. */
193 return thread_current();
194 /* The THREAD_CREATE action points to the created Thread */
195 else if (curr->get_type() == THREAD_CREATE)
196 return (Thread *)curr->get_location();
199 /* Have we completed exploring the preselected path? */
203 /* Else, we are trying to replay an execution */
204 ModelAction *next = node_stack->get_next()->get_action();
206 if (next == diverge) {
207 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
208 earliest_diverge=diverge;
210 Node *nextnode = next->get_node();
211 Node *prevnode = nextnode->get_parent();
212 scheduler->update_sleep_set(prevnode);
214 /* Reached divergence point */
215 if (nextnode->increment_misc()) {
216 /* The next node will try to satisfy a different misc_index values. */
217 tid = next->get_tid();
218 node_stack->pop_restofstack(2);
219 } else if (nextnode->increment_promise()) {
220 /* The next node will try to satisfy a different set of promises. */
221 tid = next->get_tid();
222 node_stack->pop_restofstack(2);
223 } else if (nextnode->increment_read_from()) {
224 /* The next node will read from a different value. */
225 tid = next->get_tid();
226 node_stack->pop_restofstack(2);
227 } else if (nextnode->increment_future_value()) {
228 /* The next node will try to read from a different future value. */
229 tid = next->get_tid();
230 node_stack->pop_restofstack(2);
231 } else if (nextnode->increment_relseq_break()) {
232 /* The next node will try to resolve a release sequence differently */
233 tid = next->get_tid();
234 node_stack->pop_restofstack(2);
236 /* Make a different thread execute for next step */
237 scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
238 tid = prevnode->get_next_backtrack();
239 /* Make sure the backtracked thread isn't sleeping. */
240 node_stack->pop_restofstack(1);
241 if (diverge==earliest_diverge) {
242 earliest_diverge=prevnode->get_action();
245 /* The correct sleep set is in the parent node. */
248 DEBUG("*** Divergence point ***\n");
252 tid = next->get_tid();
254 DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
255 ASSERT(tid != THREAD_ID_T_NONE);
256 return thread_map->get(id_to_int(tid));
260 * We need to know what the next actions of all threads in the sleep
261 * set will be. This method computes them and stores the actions at
262 * the corresponding thread object's pending action.
265 void ModelChecker::execute_sleep_set() {
266 for(unsigned int i=0;i<get_num_threads();i++) {
267 thread_id_t tid=int_to_id(i);
268 Thread *thr=get_thread(tid);
269 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
270 thr->get_pending() == NULL ) {
271 thr->set_state(THREAD_RUNNING);
272 scheduler->next_thread(thr);
273 Thread::swap(&system_context, thr);
274 priv->current_action->set_sleep_flag();
275 thr->set_pending(priv->current_action);
278 priv->current_action = NULL;
281 void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
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 ModelAction *pending_act=thr->get_pending();
287 if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) {
288 //Remove this thread from sleep set
289 scheduler->remove_sleep(thr);
296 * Check if we are in a deadlock. Should only be called at the end of an
297 * execution, although it should not give false positives in the middle of an
298 * execution (there should be some ENABLED thread).
300 * @return True if program is in a deadlock; false otherwise
302 bool ModelChecker::is_deadlocked() const
304 bool blocking_threads = false;
305 for (unsigned int i = 0; i < get_num_threads(); i++) {
306 thread_id_t tid = int_to_id(i);
309 Thread *t = get_thread(tid);
310 if (!t->is_model_thread() && t->get_pending())
311 blocking_threads = true;
313 return blocking_threads;
317 * Check if this is a complete execution. That is, have all thread completed
318 * execution (rather than exiting because sleep sets have forced a redundant
321 * @return True if the execution is complete.
323 bool ModelChecker::is_complete_execution() const
325 for (unsigned int i = 0; i < get_num_threads(); i++)
326 if (is_enabled(int_to_id(i)))
332 * @brief Assert a bug in the executing program.
334 * Use this function to assert any sort of bug in the user program. If the
335 * current trace is feasible (actually, a prefix of some feasible execution),
336 * then this execution will be aborted, printing the appropriate message. If
337 * the current trace is not yet feasible, the error message will be stashed and
338 * printed if the execution ever becomes feasible.
340 * This function can also be used to immediately trigger the bug; that is, we
341 * don't wait for a feasible execution before aborting. Only use the
342 * "immediate" option when you know that the infeasibility is justified (e.g.,
343 * pending release sequences are not a problem)
345 * @param msg Descriptive message for the bug (do not include newline char)
346 * @param user_thread Was this assertion triggered from a user thread?
347 * @param immediate Should this bug be triggered immediately?
349 void ModelChecker::assert_bug(const char *msg, bool user_thread, bool immediate)
351 priv->bugs.push_back(new bug_message(msg));
353 if (immediate || isfeasibleprefix()) {
356 switch_to_master(NULL);
361 * @brief Assert a bug in the executing program, with a default message
362 * @see ModelChecker::assert_bug
363 * @param user_thread Was this assertion triggered from a user thread?
365 void ModelChecker::assert_bug(bool user_thread)
367 assert_bug("bug detected", user_thread);
371 * @brief Assert a bug in the executing program immediately
372 * @see ModelChecker::assert_bug
373 * @param msg Descriptive message for the bug (do not include newline char)
375 void ModelChecker::assert_bug_immediate(const char *msg)
377 printf("Feasible: %s\n", isfeasibleprefix() ? "yes" : "no");
378 assert_bug(msg, false, true);
381 /** @return True, if any bugs have been reported for this execution */
382 bool ModelChecker::have_bug_reports() const
384 return priv->bugs.size() != 0;
387 /** @brief Print bug report listing for this execution (if any bugs exist) */
388 void ModelChecker::print_bugs() const
390 if (have_bug_reports()) {
391 printf("Bug report: %zu bugs detected\n", priv->bugs.size());
392 for (unsigned int i = 0; i < priv->bugs.size(); i++)
393 priv->bugs[i]->print();
398 * @brief Record end-of-execution stats
400 * Must be run when exiting an execution. Records various stats.
401 * @see struct execution_stats
403 void ModelChecker::record_stats()
406 if (!isfinalfeasible())
407 stats.num_infeasible++;
408 else if (have_bug_reports())
409 stats.num_buggy_executions++;
410 else if (is_complete_execution())
411 stats.num_complete++;
414 /** @brief Print execution stats */
415 void ModelChecker::print_stats() const
417 printf("Number of complete, bug-free executions: %d\n", stats.num_complete);
418 printf("Number of buggy executions: %d\n", stats.num_buggy_executions);
419 printf("Number of infeasible executions: %d\n", stats.num_infeasible);
420 printf("Total executions: %d\n", stats.num_total);
421 printf("Total nodes created: %d\n", node_stack->get_total_nodes());
425 * Queries the model-checker for more executions to explore and, if one
426 * exists, resets the model-checker state to execute a new execution.
428 * @return If there are more executions to explore, return true. Otherwise,
431 bool ModelChecker::next_execution()
437 if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
438 printf("Earliest divergence point since last feasible execution:\n");
439 if (earliest_diverge)
440 earliest_diverge->print();
442 printf("(Not set)\n");
444 earliest_diverge = NULL;
447 assert_bug("Deadlock detected");
454 } else if (DBG_ENABLED()) {
459 if ((diverge = get_next_backtrack()) == NULL)
463 printf("Next execution will diverge at:\n");
467 reset_to_initial_state();
471 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
473 switch (act->get_type()) {
477 /* linear search: from most recent to oldest */
478 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
479 action_list_t::reverse_iterator rit;
480 for (rit = list->rbegin(); rit != list->rend(); rit++) {
481 ModelAction *prev = *rit;
482 if (prev->could_synchronize_with(act))
488 case ATOMIC_TRYLOCK: {
489 /* linear search: from most recent to oldest */
490 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
491 action_list_t::reverse_iterator rit;
492 for (rit = list->rbegin(); rit != list->rend(); rit++) {
493 ModelAction *prev = *rit;
494 if (act->is_conflicting_lock(prev))
499 case ATOMIC_UNLOCK: {
500 /* linear search: from most recent to oldest */
501 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
502 action_list_t::reverse_iterator rit;
503 for (rit = list->rbegin(); rit != list->rend(); rit++) {
504 ModelAction *prev = *rit;
505 if (!act->same_thread(prev)&&prev->is_failed_trylock())
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 (!act->same_thread(prev)&&prev->is_failed_trylock())
518 if (!act->same_thread(prev)&&prev->is_notify())
524 case ATOMIC_NOTIFY_ALL:
525 case ATOMIC_NOTIFY_ONE: {
526 /* linear search: from most recent to oldest */
527 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
528 action_list_t::reverse_iterator rit;
529 for (rit = list->rbegin(); rit != list->rend(); rit++) {
530 ModelAction *prev = *rit;
531 if (!act->same_thread(prev)&&prev->is_wait())
542 /** This method finds backtracking points where we should try to
543 * reorder the parameter ModelAction against.
545 * @param the ModelAction to find backtracking points for.
547 void ModelChecker::set_backtracking(ModelAction *act)
549 Thread *t = get_thread(act);
550 ModelAction * prev = get_last_conflict(act);
554 Node * node = prev->get_node()->get_parent();
556 int low_tid, high_tid;
557 if (node->is_enabled(t)) {
558 low_tid = id_to_int(act->get_tid());
559 high_tid = low_tid+1;
562 high_tid = get_num_threads();
565 for(int i = low_tid; i < high_tid; i++) {
566 thread_id_t tid = int_to_id(i);
568 /* Make sure this thread can be enabled here. */
569 if (i >= node->get_num_threads())
572 /* Don't backtrack into a point where the thread is disabled or sleeping. */
573 if (node->enabled_status(tid)!=THREAD_ENABLED)
576 /* Check if this has been explored already */
577 if (node->has_been_explored(tid))
580 /* See if fairness allows */
581 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
583 for(int t=0;t<node->get_num_threads();t++) {
584 thread_id_t tother=int_to_id(t);
585 if (node->is_enabled(tother) && node->has_priority(tother)) {
593 /* Cache the latest backtracking point */
594 if (!priv->next_backtrack || *prev > *priv->next_backtrack)
595 priv->next_backtrack = prev;
597 /* If this is a new backtracking point, mark the tree */
598 if (!node->set_backtrack(tid))
600 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
601 id_to_int(prev->get_tid()),
602 id_to_int(t->get_id()));
611 * Returns last backtracking point. The model checker will explore a different
612 * path for this point in the next execution.
613 * @return The ModelAction at which the next execution should diverge.
615 ModelAction * ModelChecker::get_next_backtrack()
617 ModelAction *next = priv->next_backtrack;
618 priv->next_backtrack = NULL;
623 * Processes a read or rmw model action.
624 * @param curr is the read model action to process.
625 * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
626 * @return True if processing this read updates the mo_graph.
628 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
630 uint64_t value = VALUE_NONE;
631 bool updated = false;
633 const ModelAction *reads_from = curr->get_node()->get_read_from();
634 if (reads_from != NULL) {
635 mo_graph->startChanges();
637 value = reads_from->get_value();
638 bool r_status = false;
640 if (!second_part_of_rmw) {
641 check_recency(curr, reads_from);
642 r_status = r_modification_order(curr, reads_from);
646 if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
647 mo_graph->rollbackChanges();
648 too_many_reads = false;
652 curr->read_from(reads_from);
653 mo_graph->commitChanges();
654 mo_check_promises(curr->get_tid(), reads_from);
657 } else if (!second_part_of_rmw) {
658 /* Read from future value */
659 value = curr->get_node()->get_future_value();
660 modelclock_t expiration = curr->get_node()->get_future_value_expiration();
661 curr->read_from(NULL);
662 Promise *valuepromise = new Promise(curr, value, expiration);
663 promises->push_back(valuepromise);
665 get_thread(curr)->set_return_value(value);
671 * Processes a lock, trylock, or unlock model action. @param curr is
672 * the read model action to process.
674 * The try lock operation checks whether the lock is taken. If not,
675 * it falls to the normal lock operation case. If so, it returns
678 * The lock operation has already been checked that it is enabled, so
679 * it just grabs the lock and synchronizes with the previous unlock.
681 * The unlock operation has to re-enable all of the threads that are
682 * waiting on the lock.
684 * @return True if synchronization was updated; false otherwise
686 bool ModelChecker::process_mutex(ModelAction *curr) {
687 std::mutex *mutex=NULL;
688 struct std::mutex_state *state=NULL;
690 if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
691 mutex = (std::mutex *)curr->get_location();
692 state = mutex->get_state();
693 } else if(curr->is_wait()) {
694 mutex = (std::mutex *)curr->get_value();
695 state = mutex->get_state();
698 switch (curr->get_type()) {
699 case ATOMIC_TRYLOCK: {
700 bool success = !state->islocked;
701 curr->set_try_lock(success);
703 get_thread(curr)->set_return_value(0);
706 get_thread(curr)->set_return_value(1);
708 //otherwise fall into the lock case
710 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
711 assert_bug("Lock access before initialization");
712 state->islocked = true;
713 ModelAction *unlock = get_last_unlock(curr);
714 //synchronize with the previous unlock statement
715 if (unlock != NULL) {
716 curr->synchronize_with(unlock);
721 case ATOMIC_UNLOCK: {
723 state->islocked = false;
724 //wake up the other threads
725 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
726 //activate all the waiting threads
727 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
728 scheduler->wake(get_thread(*rit));
735 state->islocked = false;
736 //wake up the other threads
737 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
738 //activate all the waiting threads
739 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
740 scheduler->wake(get_thread(*rit));
743 //check whether we should go to sleep or not...simulate spurious failures
744 if (curr->get_node()->get_misc()==0) {
745 get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
747 scheduler->sleep(get_current_thread());
751 case ATOMIC_NOTIFY_ALL: {
752 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
753 //activate all the waiting threads
754 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
755 scheduler->wake(get_thread(*rit));
760 case ATOMIC_NOTIFY_ONE: {
761 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
762 int wakeupthread=curr->get_node()->get_misc();
763 action_list_t::iterator it = waiters->begin();
764 advance(it, wakeupthread);
765 scheduler->wake(get_thread(*it));
777 * Process a write ModelAction
778 * @param curr The ModelAction to process
779 * @return True if the mo_graph was updated or promises were resolved
781 bool ModelChecker::process_write(ModelAction *curr)
783 bool updated_mod_order = w_modification_order(curr);
784 bool updated_promises = resolve_promises(curr);
786 if (promises->size() == 0) {
787 for (unsigned int i = 0; i < futurevalues->size(); i++) {
788 struct PendingFutureValue pfv = (*futurevalues)[i];
789 //Do more ambitious checks now that mo is more complete
790 if (mo_may_allow(pfv.writer, pfv.act)&&
791 pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
792 (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
793 priv->next_backtrack = pfv.act;
795 futurevalues->resize(0);
798 mo_graph->commitChanges();
799 mo_check_promises(curr->get_tid(), curr);
801 get_thread(curr)->set_return_value(VALUE_NONE);
802 return updated_mod_order || updated_promises;
806 * @brief Process the current action for thread-related activity
808 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
809 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
810 * synchronization, etc. This function is a no-op for non-THREAD actions
811 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
813 * @param curr The current action
814 * @return True if synchronization was updated or a thread completed
816 bool ModelChecker::process_thread_action(ModelAction *curr)
818 bool updated = false;
820 switch (curr->get_type()) {
821 case THREAD_CREATE: {
822 Thread *th = (Thread *)curr->get_location();
823 th->set_creation(curr);
827 Thread *blocking = (Thread *)curr->get_location();
828 ModelAction *act = get_last_action(blocking->get_id());
829 curr->synchronize_with(act);
830 updated = true; /* trigger rel-seq checks */
833 case THREAD_FINISH: {
834 Thread *th = get_thread(curr);
835 while (!th->wait_list_empty()) {
836 ModelAction *act = th->pop_wait_list();
837 scheduler->wake(get_thread(act));
840 updated = true; /* trigger rel-seq checks */
844 check_promises(curr->get_tid(), NULL, curr->get_cv());
855 * @brief Process the current action for release sequence fixup activity
857 * Performs model-checker release sequence fixups for the current action,
858 * forcing a single pending release sequence to break (with a given, potential
859 * "loose" write) or to complete (i.e., synchronize). If a pending release
860 * sequence forms a complete release sequence, then we must perform the fixup
861 * synchronization, mo_graph additions, etc.
863 * @param curr The current action; must be a release sequence fixup action
864 * @param work_queue The work queue to which to add work items as they are
867 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
869 const ModelAction *write = curr->get_node()->get_relseq_break();
870 struct release_seq *sequence = pending_rel_seqs->back();
871 pending_rel_seqs->pop_back();
873 ModelAction *acquire = sequence->acquire;
874 const ModelAction *rf = sequence->rf;
875 const ModelAction *release = sequence->release;
879 ASSERT(release->same_thread(rf));
883 * @todo Forcing a synchronization requires that we set
884 * modification order constraints. For instance, we can't allow
885 * a fixup sequence in which two separate read-acquire
886 * operations read from the same sequence, where the first one
887 * synchronizes and the other doesn't. Essentially, we can't
888 * allow any writes to insert themselves between 'release' and
892 /* Must synchronize */
893 if (!acquire->synchronize_with(release)) {
894 set_bad_synchronization();
897 /* Re-check all pending release sequences */
898 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
899 /* Re-check act for mo_graph edges */
900 work_queue->push_back(MOEdgeWorkEntry(acquire));
902 /* propagate synchronization to later actions */
903 action_list_t::reverse_iterator rit = action_trace->rbegin();
904 for (; (*rit) != acquire; rit++) {
905 ModelAction *propagate = *rit;
906 if (acquire->happens_before(propagate)) {
907 propagate->synchronize_with(acquire);
908 /* Re-check 'propagate' for mo_graph edges */
909 work_queue->push_back(MOEdgeWorkEntry(propagate));
913 /* Break release sequence with new edges:
914 * release --mo--> write --mo--> rf */
915 mo_graph->addEdge(release, write);
916 mo_graph->addEdge(write, rf);
919 /* See if we have realized a data race */
924 * Initialize the current action by performing one or more of the following
925 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
926 * in the NodeStack, manipulating backtracking sets, allocating and
927 * initializing clock vectors, and computing the promises to fulfill.
929 * @param curr The current action, as passed from the user context; may be
930 * freed/invalidated after the execution of this function, with a different
931 * action "returned" its place (pass-by-reference)
932 * @return True if curr is a newly-explored action; false otherwise
934 bool ModelChecker::initialize_curr_action(ModelAction **curr)
936 ModelAction *newcurr;
938 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
939 newcurr = process_rmw(*curr);
942 if (newcurr->is_rmw())
943 compute_promises(newcurr);
949 (*curr)->set_seq_number(get_next_seq_num());
951 newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
953 /* First restore type and order in case of RMW operation */
954 if ((*curr)->is_rmwr())
955 newcurr->copy_typeandorder(*curr);
957 ASSERT((*curr)->get_location() == newcurr->get_location());
958 newcurr->copy_from_new(*curr);
960 /* Discard duplicate ModelAction; use action from NodeStack */
963 /* Always compute new clock vector */
964 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
967 return false; /* Action was explored previously */
971 /* Always compute new clock vector */
972 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
974 * Perform one-time actions when pushing new ModelAction onto
977 if (newcurr->is_write())
978 compute_promises(newcurr);
979 else if (newcurr->is_relseq_fixup())
980 compute_relseq_breakwrites(newcurr);
981 else if (newcurr->is_wait())
982 newcurr->get_node()->set_misc_max(2);
983 else if (newcurr->is_notify_one()) {
984 newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
986 return true; /* This was a new ModelAction */
991 * @brief Check whether a model action is enabled.
993 * Checks whether a lock or join operation would be successful (i.e., is the
994 * lock already locked, or is the joined thread already complete). If not, put
995 * the action in a waiter list.
997 * @param curr is the ModelAction to check whether it is enabled.
998 * @return a bool that indicates whether the action is enabled.
1000 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1001 if (curr->is_lock()) {
1002 std::mutex * lock = (std::mutex *)curr->get_location();
1003 struct std::mutex_state * state = lock->get_state();
1004 if (state->islocked) {
1005 //Stick the action in the appropriate waiting queue
1006 get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1009 } else if (curr->get_type() == THREAD_JOIN) {
1010 Thread *blocking = (Thread *)curr->get_location();
1011 if (!blocking->is_complete()) {
1012 blocking->push_wait_list(curr);
1021 * Stores the ModelAction for the current thread action. Call this
1022 * immediately before switching from user- to system-context to pass
1023 * data between them.
1024 * @param act The ModelAction created by the user-thread action
1026 void ModelChecker::set_current_action(ModelAction *act) {
1027 priv->current_action = act;
1031 * This is the heart of the model checker routine. It performs model-checking
1032 * actions corresponding to a given "current action." Among other processes, it
1033 * calculates reads-from relationships, updates synchronization clock vectors,
1034 * forms a memory_order constraints graph, and handles replay/backtrack
1035 * execution when running permutations of previously-observed executions.
1037 * @param curr The current action to process
1038 * @return The next Thread that must be executed. May be NULL if ModelChecker
1039 * makes no choice (e.g., according to replay execution, combining RMW actions,
1042 Thread * ModelChecker::check_current_action(ModelAction *curr)
1045 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1047 if (!check_action_enabled(curr)) {
1048 /* Make the execution look like we chose to run this action
1049 * much later, when a lock/join can succeed */
1050 get_current_thread()->set_pending(curr);
1051 scheduler->sleep(get_current_thread());
1052 return get_next_thread(NULL);
1055 bool newly_explored = initialize_curr_action(&curr);
1057 wake_up_sleeping_actions(curr);
1059 /* Add the action to lists before any other model-checking tasks */
1060 if (!second_part_of_rmw)
1061 add_action_to_lists(curr);
1063 /* Build may_read_from set for newly-created actions */
1064 if (newly_explored && curr->is_read())
1065 build_reads_from_past(curr);
1067 /* Initialize work_queue with the "current action" work */
1068 work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1069 while (!work_queue.empty() && !has_asserted()) {
1070 WorkQueueEntry work = work_queue.front();
1071 work_queue.pop_front();
1073 switch (work.type) {
1074 case WORK_CHECK_CURR_ACTION: {
1075 ModelAction *act = work.action;
1076 bool update = false; /* update this location's release seq's */
1077 bool update_all = false; /* update all release seq's */
1079 if (process_thread_action(curr))
1082 if (act->is_read() && process_read(act, second_part_of_rmw))
1085 if (act->is_write() && process_write(act))
1088 if (act->is_mutex_op() && process_mutex(act))
1091 if (act->is_relseq_fixup())
1092 process_relseq_fixup(curr, &work_queue);
1095 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1097 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1100 case WORK_CHECK_RELEASE_SEQ:
1101 resolve_release_sequences(work.location, &work_queue);
1103 case WORK_CHECK_MO_EDGES: {
1104 /** @todo Complete verification of work_queue */
1105 ModelAction *act = work.action;
1106 bool updated = false;
1108 if (act->is_read()) {
1109 const ModelAction *rf = act->get_reads_from();
1110 if (rf != NULL && r_modification_order(act, rf))
1113 if (act->is_write()) {
1114 if (w_modification_order(act))
1117 mo_graph->commitChanges();
1120 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1129 check_curr_backtracking(curr);
1130 set_backtracking(curr);
1131 return get_next_thread(curr);
1134 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
1135 Node *currnode = curr->get_node();
1136 Node *parnode = currnode->get_parent();
1138 if ((!parnode->backtrack_empty() ||
1139 !currnode->misc_empty() ||
1140 !currnode->read_from_empty() ||
1141 !currnode->future_value_empty() ||
1142 !currnode->promise_empty() ||
1143 !currnode->relseq_break_empty())
1144 && (!priv->next_backtrack ||
1145 *curr > *priv->next_backtrack)) {
1146 priv->next_backtrack = curr;
1150 bool ModelChecker::promises_expired() const
1152 for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
1153 Promise *promise = (*promises)[promise_index];
1154 if (promise->get_expiration()<priv->used_sequence_numbers) {
1161 /** @return whether the current partial trace must be a prefix of a
1162 * feasible trace. */
1163 bool ModelChecker::isfeasibleprefix() const
1165 return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
1168 /** @return whether the current partial trace is feasible. */
1169 bool ModelChecker::isfeasible() const
1171 if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
1172 DEBUG("Infeasible: RMW violation\n");
1174 return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
1177 /** @return whether the current partial trace is feasible other than
1178 * multiple RMW reading from the same store. */
1179 bool ModelChecker::isfeasibleotherthanRMW() const
1181 if (DBG_ENABLED()) {
1182 if (mo_graph->checkForCycles())
1183 DEBUG("Infeasible: modification order cycles\n");
1185 DEBUG("Infeasible: failed promise\n");
1187 DEBUG("Infeasible: too many reads\n");
1188 if (bad_synchronization)
1189 DEBUG("Infeasible: bad synchronization ordering\n");
1190 if (promises_expired())
1191 DEBUG("Infeasible: promises expired\n");
1193 return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
1196 /** Returns whether the current completed trace is feasible. */
1197 bool ModelChecker::isfinalfeasible() const
1199 if (DBG_ENABLED() && promises->size() != 0)
1200 DEBUG("Infeasible: unrevolved promises\n");
1202 return isfeasible() && promises->size() == 0;
1205 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1206 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1207 ModelAction *lastread = get_last_action(act->get_tid());
1208 lastread->process_rmw(act);
1209 if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
1210 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1211 mo_graph->commitChanges();
1217 * Checks whether a thread has read from the same write for too many times
1218 * without seeing the effects of a later write.
1221 * 1) there must a different write that we could read from that would satisfy the modification order,
1222 * 2) we must have read from the same value in excess of maxreads times, and
1223 * 3) that other write must have been in the reads_from set for maxreads times.
1225 * If so, we decide that the execution is no longer feasible.
1227 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
1228 if (params.maxreads != 0) {
1230 if (curr->get_node()->get_read_from_size() <= 1)
1232 //Must make sure that execution is currently feasible... We could
1233 //accidentally clear by rolling back
1236 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1237 int tid = id_to_int(curr->get_tid());
1240 if ((int)thrd_lists->size() <= tid)
1242 action_list_t *list = &(*thrd_lists)[tid];
1244 action_list_t::reverse_iterator rit = list->rbegin();
1245 /* Skip past curr */
1246 for (; (*rit) != curr; rit++)
1248 /* go past curr now */
1251 action_list_t::reverse_iterator ritcopy = rit;
1252 //See if we have enough reads from the same value
1254 for (; count < params.maxreads; rit++,count++) {
1255 if (rit==list->rend())
1257 ModelAction *act = *rit;
1258 if (!act->is_read())
1261 if (act->get_reads_from() != rf)
1263 if (act->get_node()->get_read_from_size() <= 1)
1266 for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
1268 const ModelAction * write = curr->get_node()->get_read_from_at(i);
1270 //Need a different write
1274 /* Test to see whether this is a feasible write to read from*/
1275 mo_graph->startChanges();
1276 r_modification_order(curr, write);
1277 bool feasiblereadfrom = isfeasible();
1278 mo_graph->rollbackChanges();
1280 if (!feasiblereadfrom)
1284 bool feasiblewrite = true;
1285 //new we need to see if this write works for everyone
1287 for (int loop = count; loop>0; loop--,rit++) {
1288 ModelAction *act=*rit;
1289 bool foundvalue = false;
1290 for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
1291 if (act->get_node()->get_read_from_at(j)==write) {
1297 feasiblewrite = false;
1301 if (feasiblewrite) {
1302 too_many_reads = true;
1310 * Updates the mo_graph with the constraints imposed from the current
1313 * Basic idea is the following: Go through each other thread and find
1314 * the lastest action that happened before our read. Two cases:
1316 * (1) The action is a write => that write must either occur before
1317 * the write we read from or be the write we read from.
1319 * (2) The action is a read => the write that that action read from
1320 * must occur before the write we read from or be the same write.
1322 * @param curr The current action. Must be a read.
1323 * @param rf The action that curr reads from. Must be a write.
1324 * @return True if modification order edges were added; false otherwise
1326 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
1328 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1331 ASSERT(curr->is_read());
1333 /* Iterate over all threads */
1334 for (i = 0; i < thrd_lists->size(); i++) {
1335 /* Iterate over actions in thread, starting from most recent */
1336 action_list_t *list = &(*thrd_lists)[i];
1337 action_list_t::reverse_iterator rit;
1338 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1339 ModelAction *act = *rit;
1342 * Include at most one act per-thread that "happens
1343 * before" curr. Don't consider reflexively.
1345 if (act->happens_before(curr) && act != curr) {
1346 if (act->is_write()) {
1348 mo_graph->addEdge(act, rf);
1352 const ModelAction *prevreadfrom = act->get_reads_from();
1353 //if the previous read is unresolved, keep going...
1354 if (prevreadfrom == NULL)
1357 if (rf != prevreadfrom) {
1358 mo_graph->addEdge(prevreadfrom, rf);
1370 /** This method fixes up the modification order when we resolve a
1371 * promises. The basic problem is that actions that occur after the
1372 * read curr could not property add items to the modification order
1375 * So for each thread, we find the earliest item that happens after
1376 * the read curr. This is the item we have to fix up with additional
1377 * constraints. If that action is write, we add a MO edge between
1378 * the Action rf and that action. If the action is a read, we add a
1379 * MO edge between the Action rf, and whatever the read accessed.
1381 * @param curr is the read ModelAction that we are fixing up MO edges for.
1382 * @param rf is the write ModelAction that curr reads from.
1385 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1387 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1389 ASSERT(curr->is_read());
1391 /* Iterate over all threads */
1392 for (i = 0; i < thrd_lists->size(); i++) {
1393 /* Iterate over actions in thread, starting from most recent */
1394 action_list_t *list = &(*thrd_lists)[i];
1395 action_list_t::reverse_iterator rit;
1396 ModelAction *lastact = NULL;
1398 /* Find last action that happens after curr that is either not curr or a rmw */
1399 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1400 ModelAction *act = *rit;
1401 if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1407 /* Include at most one act per-thread that "happens before" curr */
1408 if (lastact != NULL) {
1409 if (lastact==curr) {
1410 //Case 1: The resolved read is a RMW, and we need to make sure
1411 //that the write portion of the RMW mod order after rf
1413 mo_graph->addEdge(rf, lastact);
1414 } else if (lastact->is_read()) {
1415 //Case 2: The resolved read is a normal read and the next
1416 //operation is a read, and we need to make sure the value read
1417 //is mod ordered after rf
1419 const ModelAction *postreadfrom = lastact->get_reads_from();
1420 if (postreadfrom != NULL&&rf != postreadfrom)
1421 mo_graph->addEdge(rf, postreadfrom);
1423 //Case 3: The resolved read is a normal read and the next
1424 //operation is a write, and we need to make sure that the
1425 //write is mod ordered after rf
1427 mo_graph->addEdge(rf, lastact);
1435 * Updates the mo_graph with the constraints imposed from the current write.
1437 * Basic idea is the following: Go through each other thread and find
1438 * the lastest action that happened before our write. Two cases:
1440 * (1) The action is a write => that write must occur before
1443 * (2) The action is a read => the write that that action read from
1444 * must occur before the current write.
1446 * This method also handles two other issues:
1448 * (I) Sequential Consistency: Making sure that if the current write is
1449 * seq_cst, that it occurs after the previous seq_cst write.
1451 * (II) Sending the write back to non-synchronizing reads.
1453 * @param curr The current action. Must be a write.
1454 * @return True if modification order edges were added; false otherwise
1456 bool ModelChecker::w_modification_order(ModelAction *curr)
1458 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1461 ASSERT(curr->is_write());
1463 if (curr->is_seqcst()) {
1464 /* We have to at least see the last sequentially consistent write,
1465 so we are initialized. */
1466 ModelAction *last_seq_cst = get_last_seq_cst(curr);
1467 if (last_seq_cst != NULL) {
1468 mo_graph->addEdge(last_seq_cst, curr);
1473 /* Iterate over all threads */
1474 for (i = 0; i < thrd_lists->size(); i++) {
1475 /* Iterate over actions in thread, starting from most recent */
1476 action_list_t *list = &(*thrd_lists)[i];
1477 action_list_t::reverse_iterator rit;
1478 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1479 ModelAction *act = *rit;
1482 * 1) If RMW and it actually read from something, then we
1483 * already have all relevant edges, so just skip to next
1486 * 2) If RMW and it didn't read from anything, we should
1487 * whatever edge we can get to speed up convergence.
1489 * 3) If normal write, we need to look at earlier actions, so
1490 * continue processing list.
1492 if (curr->is_rmw()) {
1493 if (curr->get_reads_from()!=NULL)
1502 * Include at most one act per-thread that "happens
1505 if (act->happens_before(curr)) {
1507 * Note: if act is RMW, just add edge:
1509 * The following edge should be handled elsewhere:
1510 * readfrom(act) --mo--> act
1512 if (act->is_write())
1513 mo_graph->addEdge(act, curr);
1514 else if (act->is_read()) {
1515 //if previous read accessed a null, just keep going
1516 if (act->get_reads_from() == NULL)
1518 mo_graph->addEdge(act->get_reads_from(), curr);
1522 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1523 !act->same_thread(curr)) {
1524 /* We have an action that:
1525 (1) did not happen before us
1526 (2) is a read and we are a write
1527 (3) cannot synchronize with us
1528 (4) is in a different thread
1530 that read could potentially read from our write. Note that
1531 these checks are overly conservative at this point, we'll
1532 do more checks before actually removing the
1536 if (thin_air_constraint_may_allow(curr, act)) {
1538 (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
1539 struct PendingFutureValue pfv = {curr,act};
1540 futurevalues->push_back(pfv);
1550 /** Arbitrary reads from the future are not allowed. Section 29.3
1551 * part 9 places some constraints. This method checks one result of constraint
1552 * constraint. Others require compiler support. */
1553 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
1554 if (!writer->is_rmw())
1557 if (!reader->is_rmw())
1560 for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1561 if (search == reader)
1563 if (search->get_tid() == reader->get_tid() &&
1564 search->happens_before(reader))
1572 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1573 * some constraints. This method checks one the following constraint (others
1574 * require compiler support):
1576 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1578 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1580 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1582 /* Iterate over all threads */
1583 for (i = 0; i < thrd_lists->size(); i++) {
1584 const ModelAction *write_after_read = NULL;
1586 /* Iterate over actions in thread, starting from most recent */
1587 action_list_t *list = &(*thrd_lists)[i];
1588 action_list_t::reverse_iterator rit;
1589 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1590 ModelAction *act = *rit;
1592 if (!reader->happens_before(act))
1594 else if (act->is_write())
1595 write_after_read = act;
1596 else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
1597 write_after_read = act->get_reads_from();
1601 if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
1608 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1609 * The ModelAction under consideration is expected to be taking part in
1610 * release/acquire synchronization as an object of the "reads from" relation.
1611 * Note that this can only provide release sequence support for RMW chains
1612 * which do not read from the future, as those actions cannot be traced until
1613 * their "promise" is fulfilled. Similarly, we may not even establish the
1614 * presence of a release sequence with certainty, as some modification order
1615 * constraints may be decided further in the future. Thus, this function
1616 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1617 * and a boolean representing certainty.
1619 * @param rf The action that might be part of a release sequence. Must be a
1621 * @param release_heads A pass-by-reference style return parameter. After
1622 * execution of this function, release_heads will contain the heads of all the
1623 * relevant release sequences, if any exists with certainty
1624 * @param pending A pass-by-reference style return parameter which is only used
1625 * when returning false (i.e., uncertain). Returns most information regarding
1626 * an uncertain release sequence, including any write operations that might
1627 * break the sequence.
1628 * @return true, if the ModelChecker is certain that release_heads is complete;
1631 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1632 rel_heads_list_t *release_heads,
1633 struct release_seq *pending) const
1635 /* Only check for release sequences if there are no cycles */
1636 if (mo_graph->checkForCycles())
1640 ASSERT(rf->is_write());
1642 if (rf->is_release())
1643 release_heads->push_back(rf);
1645 break; /* End of RMW chain */
1647 /** @todo Need to be smarter here... In the linux lock
1648 * example, this will run to the beginning of the program for
1650 /** @todo The way to be smarter here is to keep going until 1
1651 * thread has a release preceded by an acquire and you've seen
1654 /* acq_rel RMW is a sufficient stopping condition */
1655 if (rf->is_acquire() && rf->is_release())
1656 return true; /* complete */
1658 rf = rf->get_reads_from();
1661 /* read from future: need to settle this later */
1663 return false; /* incomplete */
1666 if (rf->is_release())
1667 return true; /* complete */
1669 /* else relaxed write; check modification order for contiguous subsequence
1670 * -> rf must be same thread as release */
1671 int tid = id_to_int(rf->get_tid());
1672 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
1673 action_list_t *list = &(*thrd_lists)[tid];
1674 action_list_t::const_reverse_iterator rit;
1676 /* Find rf in the thread list */
1677 rit = std::find(list->rbegin(), list->rend(), rf);
1678 ASSERT(rit != list->rend());
1680 /* Find the last write/release */
1681 for (; rit != list->rend(); rit++)
1682 if ((*rit)->is_release())
1684 if (rit == list->rend()) {
1685 /* No write-release in this thread */
1686 return true; /* complete */
1688 ModelAction *release = *rit;
1690 ASSERT(rf->same_thread(release));
1692 pending->writes.clear();
1694 bool certain = true;
1695 for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1696 if (id_to_int(rf->get_tid()) == (int)i)
1698 list = &(*thrd_lists)[i];
1700 /* Can we ensure no future writes from this thread may break
1701 * the release seq? */
1702 bool future_ordered = false;
1704 ModelAction *last = get_last_action(int_to_id(i));
1705 Thread *th = get_thread(int_to_id(i));
1706 if ((last && rf->happens_before(last)) ||
1709 future_ordered = true;
1711 ASSERT(!th->is_model_thread() || future_ordered);
1713 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1714 const ModelAction *act = *rit;
1715 /* Reach synchronization -> this thread is complete */
1716 if (act->happens_before(release))
1718 if (rf->happens_before(act)) {
1719 future_ordered = true;
1723 /* Only non-RMW writes can break release sequences */
1724 if (!act->is_write() || act->is_rmw())
1727 /* Check modification order */
1728 if (mo_graph->checkReachable(rf, act)) {
1729 /* rf --mo--> act */
1730 future_ordered = true;
1733 if (mo_graph->checkReachable(act, release))
1734 /* act --mo--> release */
1736 if (mo_graph->checkReachable(release, act) &&
1737 mo_graph->checkReachable(act, rf)) {
1738 /* release --mo-> act --mo--> rf */
1739 return true; /* complete */
1741 /* act may break release sequence */
1742 pending->writes.push_back(act);
1745 if (!future_ordered)
1746 certain = false; /* This thread is uncertain */
1750 release_heads->push_back(release);
1751 pending->writes.clear();
1753 pending->release = release;
1760 * A public interface for getting the release sequence head(s) with which a
1761 * given ModelAction must synchronize. This function only returns a non-empty
1762 * result when it can locate a release sequence head with certainty. Otherwise,
1763 * it may mark the internal state of the ModelChecker so that it will handle
1764 * the release sequence at a later time, causing @a act to update its
1765 * synchronization at some later point in execution.
1766 * @param act The 'acquire' action that may read from a release sequence
1767 * @param release_heads A pass-by-reference return parameter. Will be filled
1768 * with the head(s) of the release sequence(s), if they exists with certainty.
1769 * @see ModelChecker::release_seq_heads
1771 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
1773 const ModelAction *rf = act->get_reads_from();
1774 struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
1775 sequence->acquire = act;
1777 if (!release_seq_heads(rf, release_heads, sequence)) {
1778 /* add act to 'lazy checking' list */
1779 pending_rel_seqs->push_back(sequence);
1781 snapshot_free(sequence);
1786 * Attempt to resolve all stashed operations that might synchronize with a
1787 * release sequence for a given location. This implements the "lazy" portion of
1788 * determining whether or not a release sequence was contiguous, since not all
1789 * modification order information is present at the time an action occurs.
1791 * @param location The location/object that should be checked for release
1792 * sequence resolutions. A NULL value means to check all locations.
1793 * @param work_queue The work queue to which to add work items as they are
1795 * @return True if any updates occurred (new synchronization, new mo_graph
1798 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
1800 bool updated = false;
1801 std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
1802 while (it != pending_rel_seqs->end()) {
1803 struct release_seq *pending = *it;
1804 ModelAction *act = pending->acquire;
1806 /* Only resolve sequences on the given location, if provided */
1807 if (location && act->get_location() != location) {
1812 const ModelAction *rf = act->get_reads_from();
1813 rel_heads_list_t release_heads;
1815 complete = release_seq_heads(rf, &release_heads, pending);
1816 for (unsigned int i = 0; i < release_heads.size(); i++) {
1817 if (!act->has_synchronized_with(release_heads[i])) {
1818 if (act->synchronize_with(release_heads[i]))
1821 set_bad_synchronization();
1826 /* Re-check all pending release sequences */
1827 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1828 /* Re-check act for mo_graph edges */
1829 work_queue->push_back(MOEdgeWorkEntry(act));
1831 /* propagate synchronization to later actions */
1832 action_list_t::reverse_iterator rit = action_trace->rbegin();
1833 for (; (*rit) != act; rit++) {
1834 ModelAction *propagate = *rit;
1835 if (act->happens_before(propagate)) {
1836 propagate->synchronize_with(act);
1837 /* Re-check 'propagate' for mo_graph edges */
1838 work_queue->push_back(MOEdgeWorkEntry(propagate));
1843 it = pending_rel_seqs->erase(it);
1844 snapshot_free(pending);
1850 // If we resolved promises or data races, see if we have realized a data race.
1857 * Performs various bookkeeping operations for the current ModelAction. For
1858 * instance, adds action to the per-object, per-thread action vector and to the
1859 * action trace list of all thread actions.
1861 * @param act is the ModelAction to add.
1863 void ModelChecker::add_action_to_lists(ModelAction *act)
1865 int tid = id_to_int(act->get_tid());
1866 action_trace->push_back(act);
1868 get_safe_ptr_action(obj_map, act->get_location())->push_back(act);
1870 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
1871 if (tid >= (int)vec->size())
1872 vec->resize(priv->next_thread_id);
1873 (*vec)[tid].push_back(act);
1875 if ((int)thrd_last_action->size() <= tid)
1876 thrd_last_action->resize(get_num_threads());
1877 (*thrd_last_action)[tid] = act;
1879 if (act->is_wait()) {
1880 void *mutex_loc=(void *) act->get_value();
1881 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
1883 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
1884 if (tid >= (int)vec->size())
1885 vec->resize(priv->next_thread_id);
1886 (*vec)[tid].push_back(act);
1888 if ((int)thrd_last_action->size() <= tid)
1889 thrd_last_action->resize(get_num_threads());
1890 (*thrd_last_action)[tid] = act;
1895 * @brief Get the last action performed by a particular Thread
1896 * @param tid The thread ID of the Thread in question
1897 * @return The last action in the thread
1899 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
1901 int threadid = id_to_int(tid);
1902 if (threadid < (int)thrd_last_action->size())
1903 return (*thrd_last_action)[id_to_int(tid)];
1909 * Gets the last memory_order_seq_cst write (in the total global sequence)
1910 * performed on a particular object (i.e., memory location), not including the
1912 * @param curr The current ModelAction; also denotes the object location to
1914 * @return The last seq_cst write
1916 ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
1918 void *location = curr->get_location();
1919 action_list_t *list = get_safe_ptr_action(obj_map, location);
1920 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1921 action_list_t::reverse_iterator rit;
1922 for (rit = list->rbegin(); rit != list->rend(); rit++)
1923 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
1929 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1930 * location). This function identifies the mutex according to the current
1931 * action, which is presumed to perform on the same mutex.
1932 * @param curr The current ModelAction; also denotes the object location to
1934 * @return The last unlock operation
1936 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
1938 void *location = curr->get_location();
1939 action_list_t *list = get_safe_ptr_action(obj_map, location);
1940 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1941 action_list_t::reverse_iterator rit;
1942 for (rit = list->rbegin(); rit != list->rend(); rit++)
1943 if ((*rit)->is_unlock() || (*rit)->is_wait())
1948 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
1950 ModelAction *parent = get_last_action(tid);
1952 parent = get_thread(tid)->get_creation();
1957 * Returns the clock vector for a given thread.
1958 * @param tid The thread whose clock vector we want
1959 * @return Desired clock vector
1961 ClockVector * ModelChecker::get_cv(thread_id_t tid)
1963 return get_parent_action(tid)->get_cv();
1967 * Resolve a set of Promises with a current write. The set is provided in the
1968 * Node corresponding to @a write.
1969 * @param write The ModelAction that is fulfilling Promises
1970 * @return True if promises were resolved; false otherwise
1972 bool ModelChecker::resolve_promises(ModelAction *write)
1974 bool resolved = false;
1975 std::vector< thread_id_t, ModelAlloc<thread_id_t> > threads_to_check;
1977 for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
1978 Promise *promise = (*promises)[promise_index];
1979 if (write->get_node()->get_promise(i)) {
1980 ModelAction *read = promise->get_action();
1981 if (read->is_rmw()) {
1982 mo_graph->addRMWEdge(write, read);
1984 read->read_from(write);
1985 //First fix up the modification order for actions that happened
1987 r_modification_order(read, write);
1988 //Next fix up the modification order for actions that happened
1990 post_r_modification_order(read, write);
1991 //Make sure the promise's value matches the write's value
1992 ASSERT(promise->get_value() == write->get_value());
1995 promises->erase(promises->begin() + promise_index);
1996 threads_to_check.push_back(read->get_tid());
2003 //Check whether reading these writes has made threads unable to
2006 for(unsigned int i=0;i<threads_to_check.size();i++)
2007 mo_check_promises(threads_to_check[i], write);
2013 * Compute the set of promises that could potentially be satisfied by this
2014 * action. Note that the set computation actually appears in the Node, not in
2016 * @param curr The ModelAction that may satisfy promises
2018 void ModelChecker::compute_promises(ModelAction *curr)
2020 for (unsigned int i = 0; i < promises->size(); i++) {
2021 Promise *promise = (*promises)[i];
2022 const ModelAction *act = promise->get_action();
2023 if (!act->happens_before(curr) &&
2025 !act->could_synchronize_with(curr) &&
2026 !act->same_thread(curr) &&
2027 act->get_location() == curr->get_location() &&
2028 promise->get_value() == curr->get_value()) {
2029 curr->get_node()->set_promise(i, act->is_rmw());
2034 /** Checks promises in response to change in ClockVector Threads. */
2035 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2037 for (unsigned int i = 0; i < promises->size(); i++) {
2038 Promise *promise = (*promises)[i];
2039 const ModelAction *act = promise->get_action();
2040 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2041 merge_cv->synchronized_since(act)) {
2042 if (promise->increment_threads(tid)) {
2043 //Promise has failed
2044 failed_promise = true;
2051 void ModelChecker::check_promises_thread_disabled() {
2052 for (unsigned int i = 0; i < promises->size(); i++) {
2053 Promise *promise = (*promises)[i];
2054 if (promise->check_promise()) {
2055 failed_promise = true;
2061 /** Checks promises in response to addition to modification order for threads.
2063 * pthread is the thread that performed the read that created the promise
2065 * pread is the read that created the promise
2067 * pwrite is either the first write to same location as pread by
2068 * pthread that is sequenced after pread or the value read by the
2069 * first read to the same lcoation as pread by pthread that is
2070 * sequenced after pread..
2072 * 1. If tid=pthread, then we check what other threads are reachable
2073 * through the mode order starting with pwrite. Those threads cannot
2074 * perform a write that will resolve the promise due to modification
2075 * order constraints.
2077 * 2. If the tid is not pthread, we check whether pwrite can reach the
2078 * action write through the modification order. If so, that thread
2079 * cannot perform a future write that will resolve the promise due to
2080 * modificatin order constraints.
2082 * @parem tid The thread that either read from the model action
2083 * write, or actually did the model action write.
2085 * @parem write The ModelAction representing the relevant write.
2088 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
2089 void * location = write->get_location();
2090 for (unsigned int i = 0; i < promises->size(); i++) {
2091 Promise *promise = (*promises)[i];
2092 const ModelAction *act = promise->get_action();
2094 //Is this promise on the same location?
2095 if ( act->get_location() != location )
2098 //same thread as the promise
2099 if ( act->get_tid()==tid ) {
2101 //do we have a pwrite for the promise, if not, set it
2102 if (promise->get_write() == NULL ) {
2103 promise->set_write(write);
2104 //The pwrite cannot happen before the promise
2105 if (write->happens_before(act) && (write != act)) {
2106 failed_promise = true;
2110 if (mo_graph->checkPromise(write, promise)) {
2111 failed_promise = true;
2116 //Don't do any lookups twice for the same thread
2117 if (promise->has_sync_thread(tid))
2120 if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
2121 if (promise->increment_threads(tid)) {
2122 failed_promise = true;
2130 * Compute the set of writes that may break the current pending release
2131 * sequence. This information is extracted from previou release sequence
2134 * @param curr The current ModelAction. Must be a release sequence fixup
2137 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2139 if (pending_rel_seqs->empty())
2142 struct release_seq *pending = pending_rel_seqs->back();
2143 for (unsigned int i = 0; i < pending->writes.size(); i++) {
2144 const ModelAction *write = pending->writes[i];
2145 curr->get_node()->add_relseq_break(write);
2148 /* NULL means don't break the sequence; just synchronize */
2149 curr->get_node()->add_relseq_break(NULL);
2153 * Build up an initial set of all past writes that this 'read' action may read
2154 * from. This set is determined by the clock vector's "happens before"
2156 * @param curr is the current ModelAction that we are exploring; it must be a
2159 void ModelChecker::build_reads_from_past(ModelAction *curr)
2161 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2163 ASSERT(curr->is_read());
2165 ModelAction *last_seq_cst = NULL;
2167 /* Track whether this object has been initialized */
2168 bool initialized = false;
2170 if (curr->is_seqcst()) {
2171 last_seq_cst = get_last_seq_cst(curr);
2172 /* We have to at least see the last sequentially consistent write,
2173 so we are initialized. */
2174 if (last_seq_cst != NULL)
2178 /* Iterate over all threads */
2179 for (i = 0; i < thrd_lists->size(); i++) {
2180 /* Iterate over actions in thread, starting from most recent */
2181 action_list_t *list = &(*thrd_lists)[i];
2182 action_list_t::reverse_iterator rit;
2183 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2184 ModelAction *act = *rit;
2186 /* Only consider 'write' actions */
2187 if (!act->is_write() || act == curr)
2190 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2191 if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
2192 if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
2193 DEBUG("Adding action to may_read_from:\n");
2194 if (DBG_ENABLED()) {
2198 curr->get_node()->add_read_from(act);
2202 /* Include at most one act per-thread that "happens before" curr */
2203 if (act->happens_before(curr)) {
2211 assert_bug("May read from uninitialized atomic");
2213 if (DBG_ENABLED() || !initialized) {
2214 printf("Reached read action:\n");
2216 printf("Printing may_read_from\n");
2217 curr->get_node()->print_may_read_from();
2218 printf("End printing may_read_from\n");
2222 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
2224 Node *prevnode=write->get_node()->get_parent();
2226 bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
2227 if (write->is_release()&&thread_sleep)
2229 if (!write->is_rmw()) {
2232 if (write->get_reads_from()==NULL)
2234 write=write->get_reads_from();
2238 static void print_list(action_list_t *list)
2240 action_list_t::iterator it;
2242 printf("---------------------------------------------------------------------\n");
2244 unsigned int hash=0;
2246 for (it = list->begin(); it != list->end(); it++) {
2248 hash=hash^(hash<<3)^((*it)->hash());
2250 printf("HASH %u\n", hash);
2251 printf("---------------------------------------------------------------------\n");
2254 #if SUPPORT_MOD_ORDER_DUMP
2255 void ModelChecker::dumpGraph(char *filename) {
2257 sprintf(buffer, "%s.dot",filename);
2258 FILE *file=fopen(buffer, "w");
2259 fprintf(file, "digraph %s {\n",filename);
2260 mo_graph->dumpNodes(file);
2261 ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
2263 for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2264 ModelAction *action=*it;
2265 if (action->is_read()) {
2266 fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
2267 if (action->get_reads_from()!=NULL)
2268 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2270 if (thread_array[action->get_tid()] != NULL) {
2271 fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2274 thread_array[action->get_tid()]=action;
2276 fprintf(file,"}\n");
2277 model_free(thread_array);
2282 void ModelChecker::print_summary()
2284 #if SUPPORT_MOD_ORDER_DUMP
2286 char buffername[100];
2287 sprintf(buffername, "exec%04u", stats.num_total);
2288 mo_graph->dumpGraphToFile(buffername);
2289 sprintf(buffername, "graph%04u", stats.num_total);
2290 dumpGraph(buffername);
2293 if (!isfinalfeasible())
2294 printf("INFEASIBLE EXECUTION!\n");
2295 print_list(action_trace);
2300 * Add a Thread to the system for the first time. Should only be called once
2302 * @param t The Thread to add
2304 void ModelChecker::add_thread(Thread *t)
2306 thread_map->put(id_to_int(t->get_id()), t);
2307 scheduler->add_thread(t);
2311 * Removes a thread from the scheduler.
2312 * @param the thread to remove.
2314 void ModelChecker::remove_thread(Thread *t)
2316 scheduler->remove_thread(t);
2320 * @brief Get a Thread reference by its ID
2321 * @param tid The Thread's ID
2322 * @return A Thread reference
2324 Thread * ModelChecker::get_thread(thread_id_t tid) const
2326 return thread_map->get(id_to_int(tid));
2330 * @brief Get a reference to the Thread in which a ModelAction was executed
2331 * @param act The ModelAction
2332 * @return A Thread reference
2334 Thread * ModelChecker::get_thread(ModelAction *act) const
2336 return get_thread(act->get_tid());
2340 * @brief Check if a Thread is currently enabled
2341 * @param t The Thread to check
2342 * @return True if the Thread is currently enabled
2344 bool ModelChecker::is_enabled(Thread *t) const
2346 return scheduler->is_enabled(t);
2350 * @brief Check if a Thread is currently enabled
2351 * @param tid The ID of the Thread to check
2352 * @return True if the Thread is currently enabled
2354 bool ModelChecker::is_enabled(thread_id_t tid) const
2356 return scheduler->is_enabled(tid);
2360 * Switch from a user-context to the "master thread" context (a.k.a. system
2361 * context). This switch is made with the intention of exploring a particular
2362 * model-checking action (described by a ModelAction object). Must be called
2363 * from a user-thread context.
2365 * @param act The current action that will be explored. May be NULL only if
2366 * trace is exiting via an assertion (see ModelChecker::set_assert and
2367 * ModelChecker::has_asserted).
2368 * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
2370 int ModelChecker::switch_to_master(ModelAction *act)
2373 Thread *old = thread_current();
2374 set_current_action(act);
2375 old->set_state(THREAD_READY);
2376 return Thread::swap(old, &system_context);
2380 * Takes the next step in the execution, if possible.
2381 * @return Returns true (success) if a step was taken and false otherwise.
2383 bool ModelChecker::take_step() {
2387 Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
2389 if (curr->get_state() == THREAD_READY) {
2390 ASSERT(priv->current_action);
2392 priv->nextThread = check_current_action(priv->current_action);
2393 priv->current_action = NULL;
2395 if (curr->is_blocked() || curr->is_complete())
2396 scheduler->remove_thread(curr);
2401 Thread *next = scheduler->next_thread(priv->nextThread);
2403 /* Infeasible -> don't take any more steps */
2406 else if (isfeasibleprefix() && have_bug_reports()) {
2411 if (params.bound != 0) {
2412 if (priv->used_sequence_numbers > params.bound) {
2417 DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
2418 next ? id_to_int(next->get_id()) : -1);
2421 * Launch end-of-execution release sequence fixups only when there are:
2423 * (1) no more user threads to run (or when execution replay chooses
2424 * the 'model_thread')
2425 * (2) pending release sequences
2426 * (3) pending assertions (i.e., data races)
2427 * (4) no pending promises
2429 if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
2430 isfinalfeasible() && !unrealizedraces.empty()) {
2431 printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2432 pending_rel_seqs->size());
2433 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2434 std::memory_order_seq_cst, NULL, VALUE_NONE,
2436 set_current_action(fixup);
2440 /* next == NULL -> don't take any more steps */
2444 next->set_state(THREAD_RUNNING);
2446 if (next->get_pending() != NULL) {
2447 /* restart a pending action */
2448 set_current_action(next->get_pending());
2449 next->set_pending(NULL);
2450 next->set_state(THREAD_READY);
2454 /* Return false only if swap fails with an error */
2455 return (Thread::swap(&system_context, next) == 0);
2458 /** Runs the current execution until threre are no more steps to take. */
2459 void ModelChecker::finish_execution() {
2462 while (take_step());