8 #include "snapshot-interface.h"
10 #include "clockvector.h"
11 #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 obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
35 promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
36 futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
37 pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
38 thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
39 node_stack(new NodeStack()),
40 mo_graph(new CycleGraph()),
41 failed_promise(false),
42 too_many_reads(false),
44 bad_synchronization(false)
46 /* Allocate this "size" on the snapshotting heap */
47 priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
48 /* First thread created will have id INITIAL_THREAD_ID */
49 priv->next_thread_id = INITIAL_THREAD_ID;
51 /* Initialize a model-checker thread, for special ModelActions */
52 model_thread = new Thread(get_next_id());
53 thread_map->put(id_to_int(model_thread->get_id()), model_thread);
56 /** @brief Destructor */
57 ModelChecker::~ModelChecker()
59 for (unsigned int i = 0; i < get_num_threads(); i++)
60 delete thread_map->get(i);
65 delete lock_waiters_map;
68 for (unsigned int i = 0; i < promises->size(); i++)
69 delete (*promises)[i];
72 delete pending_rel_seqs;
74 delete thrd_last_action;
81 * Restores user program to initial state and resets all model-checker data
84 void ModelChecker::reset_to_initial_state()
86 DEBUG("+++ Resetting to initial state +++\n");
87 node_stack->reset_execution();
88 failed_promise = false;
89 too_many_reads = false;
90 bad_synchronization = false;
92 snapshotObject->backTrackBeforeStep(0);
95 /** @return a thread ID for a new Thread */
96 thread_id_t ModelChecker::get_next_id()
98 return priv->next_thread_id++;
101 /** @return the number of user threads created during this execution */
102 unsigned int ModelChecker::get_num_threads()
104 return priv->next_thread_id;
107 /** @return The currently executing Thread. */
108 Thread * ModelChecker::get_current_thread()
110 return scheduler->get_current_thread();
113 /** @return a sequence number for a new ModelAction */
114 modelclock_t ModelChecker::get_next_seq_num()
116 return ++priv->used_sequence_numbers;
119 Node * ModelChecker::get_curr_node() {
120 return node_stack->get_head();
124 * @brief Choose the next thread to execute.
126 * This function chooses the next thread that should execute. It can force the
127 * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
128 * followed by a THREAD_START, or it can enforce execution replay/backtracking.
129 * The model-checker may have no preference regarding the next thread (i.e.,
130 * when exploring a new execution ordering), in which case this will return
132 * @param curr The current ModelAction. This action might guide the choice of
134 * @return The next thread to run. If the model-checker has no preference, NULL.
136 Thread * ModelChecker::get_next_thread(ModelAction *curr)
141 /* Do not split atomic actions. */
143 return thread_current();
144 /* The THREAD_CREATE action points to the created Thread */
145 else if (curr->get_type() == THREAD_CREATE)
146 return (Thread *)curr->get_location();
149 /* Have we completed exploring the preselected path? */
153 /* Else, we are trying to replay an execution */
154 ModelAction *next = node_stack->get_next()->get_action();
156 if (next == diverge) {
157 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
158 earliest_diverge=diverge;
160 Node *nextnode = next->get_node();
161 Node *prevnode = nextnode->get_parent();
162 scheduler->update_sleep_set(prevnode);
164 /* Reached divergence point */
165 if (nextnode->increment_promise()) {
166 /* The next node will try to satisfy a different set of promises. */
167 tid = next->get_tid();
168 node_stack->pop_restofstack(2);
169 } else if (nextnode->increment_read_from()) {
170 /* The next node will read from a different value. */
171 tid = next->get_tid();
172 node_stack->pop_restofstack(2);
173 } else if (nextnode->increment_future_value()) {
174 /* The next node will try to read from a different future value. */
175 tid = next->get_tid();
176 node_stack->pop_restofstack(2);
177 } else if (nextnode->increment_relseq_break()) {
178 /* The next node will try to resolve a release sequence differently */
179 tid = next->get_tid();
180 node_stack->pop_restofstack(2);
182 /* Make a different thread execute for next step */
183 scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
184 tid = prevnode->get_next_backtrack();
185 /* Make sure the backtracked thread isn't sleeping. */
186 node_stack->pop_restofstack(1);
187 if (diverge==earliest_diverge) {
188 earliest_diverge=prevnode->get_action();
191 /* The correct sleep set is in the parent node. */
194 DEBUG("*** Divergence point ***\n");
198 tid = next->get_tid();
200 DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
201 ASSERT(tid != THREAD_ID_T_NONE);
202 return thread_map->get(id_to_int(tid));
206 * We need to know what the next actions of all threads in the sleep
207 * set will be. This method computes them and stores the actions at
208 * the corresponding thread object's pending action.
211 void ModelChecker::execute_sleep_set() {
212 for(unsigned int i=0;i<get_num_threads();i++) {
213 thread_id_t tid=int_to_id(i);
214 Thread *thr=get_thread(tid);
215 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
216 thr->set_state(THREAD_RUNNING);
217 scheduler->next_thread(thr);
218 Thread::swap(&system_context, thr);
219 priv->current_action->set_sleep_flag();
220 thr->set_pending(priv->current_action);
223 priv->current_action = NULL;
226 void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
227 for(unsigned int i=0;i<get_num_threads();i++) {
228 thread_id_t tid=int_to_id(i);
229 Thread *thr=get_thread(tid);
230 if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
231 ModelAction *pending_act=thr->get_pending();
232 if (pending_act->could_synchronize_with(curr)) {
233 //Remove this thread from sleep set
234 scheduler->remove_sleep(thr);
241 * Queries the model-checker for more executions to explore and, if one
242 * exists, resets the model-checker state to execute a new execution.
244 * @return If there are more executions to explore, return true. Otherwise,
247 bool ModelChecker::next_execution()
253 if (isfinalfeasible()) {
254 printf("Earliest divergence point since last feasible execution:\n");
255 if (earliest_diverge)
256 earliest_diverge->print();
258 printf("(Not set)\n");
260 earliest_diverge = NULL;
261 num_feasible_executions++;
264 DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
265 pending_rel_seqs->size());
268 if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
271 if ((diverge = get_next_backtrack()) == NULL)
275 printf("Next execution will diverge at:\n");
279 reset_to_initial_state();
283 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
285 switch (act->get_type()) {
289 /* linear search: from most recent to oldest */
290 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
291 action_list_t::reverse_iterator rit;
292 for (rit = list->rbegin(); rit != list->rend(); rit++) {
293 ModelAction *prev = *rit;
294 if (prev->could_synchronize_with(act))
300 case ATOMIC_TRYLOCK: {
301 /* linear search: from most recent to oldest */
302 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
303 action_list_t::reverse_iterator rit;
304 for (rit = list->rbegin(); rit != list->rend(); rit++) {
305 ModelAction *prev = *rit;
306 if (act->is_conflicting_lock(prev))
311 case ATOMIC_UNLOCK: {
312 /* linear search: from most recent to oldest */
313 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
314 action_list_t::reverse_iterator rit;
315 for (rit = list->rbegin(); rit != list->rend(); rit++) {
316 ModelAction *prev = *rit;
317 if (!act->same_thread(prev)&&prev->is_failed_trylock())
328 /** This method finds backtracking points where we should try to
329 * reorder the parameter ModelAction against.
331 * @param the ModelAction to find backtracking points for.
333 void ModelChecker::set_backtracking(ModelAction *act)
335 Thread *t = get_thread(act);
336 ModelAction * prev = get_last_conflict(act);
340 Node * node = prev->get_node()->get_parent();
342 int low_tid, high_tid;
343 if (node->is_enabled(t)) {
344 low_tid = id_to_int(act->get_tid());
345 high_tid = low_tid+1;
348 high_tid = get_num_threads();
351 for(int i = low_tid; i < high_tid; i++) {
352 thread_id_t tid = int_to_id(i);
354 /* Don't backtrack into a point where the thread is disabled or sleeping. */
355 if (node->get_enabled_array()[i]!=THREAD_ENABLED)
358 /* Check if this has been explored already */
359 if (node->has_been_explored(tid))
362 /* See if fairness allows */
363 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
365 for(int t=0;t<node->get_num_threads();t++) {
366 thread_id_t tother=int_to_id(t);
367 if (node->is_enabled(tother) && node->has_priority(tother)) {
375 /* Cache the latest backtracking point */
376 if (!priv->next_backtrack || *prev > *priv->next_backtrack)
377 priv->next_backtrack = prev;
379 /* If this is a new backtracking point, mark the tree */
380 if (!node->set_backtrack(tid))
382 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
383 id_to_int(prev->get_tid()),
384 id_to_int(t->get_id()));
393 * Returns last backtracking point. The model checker will explore a different
394 * path for this point in the next execution.
395 * @return The ModelAction at which the next execution should diverge.
397 ModelAction * ModelChecker::get_next_backtrack()
399 ModelAction *next = priv->next_backtrack;
400 priv->next_backtrack = NULL;
405 * Processes a read or rmw model action.
406 * @param curr is the read model action to process.
407 * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
408 * @return True if processing this read updates the mo_graph.
410 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
413 bool updated = false;
415 const ModelAction *reads_from = curr->get_node()->get_read_from();
416 if (reads_from != NULL) {
417 mo_graph->startChanges();
419 value = reads_from->get_value();
420 bool r_status = false;
422 if (!second_part_of_rmw) {
423 check_recency(curr, reads_from);
424 r_status = r_modification_order(curr, reads_from);
428 if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
429 mo_graph->rollbackChanges();
430 too_many_reads = false;
434 curr->read_from(reads_from);
435 mo_graph->commitChanges();
436 mo_check_promises(curr->get_tid(), reads_from);
439 } else if (!second_part_of_rmw) {
440 /* Read from future value */
441 value = curr->get_node()->get_future_value();
442 modelclock_t expiration = curr->get_node()->get_future_value_expiration();
443 curr->read_from(NULL);
444 Promise *valuepromise = new Promise(curr, value, expiration);
445 promises->push_back(valuepromise);
447 get_thread(curr)->set_return_value(value);
453 * Processes a lock, trylock, or unlock model action. @param curr is
454 * the read model action to process.
456 * The try lock operation checks whether the lock is taken. If not,
457 * it falls to the normal lock operation case. If so, it returns
460 * The lock operation has already been checked that it is enabled, so
461 * it just grabs the lock and synchronizes with the previous unlock.
463 * The unlock operation has to re-enable all of the threads that are
464 * waiting on the lock.
466 * @return True if synchronization was updated; false otherwise
468 bool ModelChecker::process_mutex(ModelAction *curr) {
469 std::mutex *mutex = (std::mutex *)curr->get_location();
470 struct std::mutex_state *state = mutex->get_state();
471 switch (curr->get_type()) {
472 case ATOMIC_TRYLOCK: {
473 bool success = !state->islocked;
474 curr->set_try_lock(success);
476 get_thread(curr)->set_return_value(0);
479 get_thread(curr)->set_return_value(1);
481 //otherwise fall into the lock case
483 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
484 printf("Lock access before initialization\n");
487 state->islocked = true;
488 ModelAction *unlock = get_last_unlock(curr);
489 //synchronize with the previous unlock statement
490 if (unlock != NULL) {
491 curr->synchronize_with(unlock);
496 case ATOMIC_UNLOCK: {
498 state->islocked = false;
499 //wake up the other threads
500 action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
501 //activate all the waiting threads
502 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
503 scheduler->wake(get_thread(*rit));
515 * Process a write ModelAction
516 * @param curr The ModelAction to process
517 * @return True if the mo_graph was updated or promises were resolved
519 bool ModelChecker::process_write(ModelAction *curr)
521 bool updated_mod_order = w_modification_order(curr);
522 bool updated_promises = resolve_promises(curr);
524 if (promises->size() == 0) {
525 for (unsigned int i = 0; i < futurevalues->size(); i++) {
526 struct PendingFutureValue pfv = (*futurevalues)[i];
527 //Do more ambitious checks now that mo is more complete
528 if (mo_may_allow(pfv.writer, pfv.act)&&
529 pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
530 (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
531 priv->next_backtrack = pfv.act;
533 futurevalues->resize(0);
536 mo_graph->commitChanges();
537 mo_check_promises(curr->get_tid(), curr);
539 get_thread(curr)->set_return_value(VALUE_NONE);
540 return updated_mod_order || updated_promises;
544 * @brief Process the current action for thread-related activity
546 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
547 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
548 * synchronization, etc. This function is a no-op for non-THREAD actions
549 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
551 * @param curr The current action
552 * @return True if synchronization was updated or a thread completed
554 bool ModelChecker::process_thread_action(ModelAction *curr)
556 bool updated = false;
558 switch (curr->get_type()) {
559 case THREAD_CREATE: {
560 Thread *th = (Thread *)curr->get_location();
561 th->set_creation(curr);
565 Thread *blocking = (Thread *)curr->get_location();
566 ModelAction *act = get_last_action(blocking->get_id());
567 curr->synchronize_with(act);
568 updated = true; /* trigger rel-seq checks */
571 case THREAD_FINISH: {
572 Thread *th = get_thread(curr);
573 while (!th->wait_list_empty()) {
574 ModelAction *act = th->pop_wait_list();
575 scheduler->wake(get_thread(act));
578 updated = true; /* trigger rel-seq checks */
582 check_promises(curr->get_tid(), NULL, curr->get_cv());
593 * @brief Process the current action for release sequence fixup activity
595 * Performs model-checker release sequence fixups for the current action,
596 * forcing a single pending release sequence to break (with a given, potential
597 * "loose" write) or to complete (i.e., synchronize). If a pending release
598 * sequence forms a complete release sequence, then we must perform the fixup
599 * synchronization, mo_graph additions, etc.
601 * @param curr The current action; must be a release sequence fixup action
602 * @param work_queue The work queue to which to add work items as they are
605 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
607 const ModelAction *write = curr->get_node()->get_relseq_break();
608 struct release_seq *sequence = pending_rel_seqs->back();
609 pending_rel_seqs->pop_back();
611 ModelAction *acquire = sequence->acquire;
612 const ModelAction *rf = sequence->rf;
613 const ModelAction *release = sequence->release;
617 ASSERT(release->same_thread(rf));
621 * @todo Forcing a synchronization requires that we set
622 * modification order constraints. For instance, we can't allow
623 * a fixup sequence in which two separate read-acquire
624 * operations read from the same sequence, where the first one
625 * synchronizes and the other doesn't. Essentially, we can't
626 * allow any writes to insert themselves between 'release' and
630 /* Must synchronize */
631 if (!acquire->synchronize_with(release)) {
632 set_bad_synchronization();
635 /* Re-check all pending release sequences */
636 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
637 /* Re-check act for mo_graph edges */
638 work_queue->push_back(MOEdgeWorkEntry(acquire));
640 /* propagate synchronization to later actions */
641 action_list_t::reverse_iterator rit = action_trace->rbegin();
642 for (; (*rit) != acquire; rit++) {
643 ModelAction *propagate = *rit;
644 if (acquire->happens_before(propagate)) {
645 propagate->synchronize_with(acquire);
646 /* Re-check 'propagate' for mo_graph edges */
647 work_queue->push_back(MOEdgeWorkEntry(propagate));
651 /* Break release sequence with new edges:
652 * release --mo--> write --mo--> rf */
653 mo_graph->addEdge(release, write);
654 mo_graph->addEdge(write, rf);
657 /* See if we have realized a data race */
658 if (checkDataRaces())
663 * Initialize the current action by performing one or more of the following
664 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
665 * in the NodeStack, manipulating backtracking sets, allocating and
666 * initializing clock vectors, and computing the promises to fulfill.
668 * @param curr The current action, as passed from the user context; may be
669 * freed/invalidated after the execution of this function
670 * @return The current action, as processed by the ModelChecker. Is only the
671 * same as the parameter @a curr if this is a newly-explored action.
673 ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
675 ModelAction *newcurr;
677 if (curr->is_rmwc() || curr->is_rmw()) {
678 newcurr = process_rmw(curr);
681 if (newcurr->is_rmw())
682 compute_promises(newcurr);
686 curr->set_seq_number(get_next_seq_num());
688 newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
690 /* First restore type and order in case of RMW operation */
692 newcurr->copy_typeandorder(curr);
694 ASSERT(curr->get_location() == newcurr->get_location());
695 newcurr->copy_from_new(curr);
697 /* Discard duplicate ModelAction; use action from NodeStack */
700 /* Always compute new clock vector */
701 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
705 /* Always compute new clock vector */
706 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
708 * Perform one-time actions when pushing new ModelAction onto
711 if (newcurr->is_write())
712 compute_promises(newcurr);
713 else if (newcurr->is_relseq_fixup())
714 compute_relseq_breakwrites(newcurr);
720 * @brief Check whether a model action is enabled.
722 * Checks whether a lock or join operation would be successful (i.e., is the
723 * lock already locked, or is the joined thread already complete). If not, put
724 * the action in a waiter list.
726 * @param curr is the ModelAction to check whether it is enabled.
727 * @return a bool that indicates whether the action is enabled.
729 bool ModelChecker::check_action_enabled(ModelAction *curr) {
730 if (curr->is_lock()) {
731 std::mutex * lock = (std::mutex *)curr->get_location();
732 struct std::mutex_state * state = lock->get_state();
733 if (state->islocked) {
734 //Stick the action in the appropriate waiting queue
735 lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
738 } else if (curr->get_type() == THREAD_JOIN) {
739 Thread *blocking = (Thread *)curr->get_location();
740 if (!blocking->is_complete()) {
741 blocking->push_wait_list(curr);
750 * This is the heart of the model checker routine. It performs model-checking
751 * actions corresponding to a given "current action." Among other processes, it
752 * calculates reads-from relationships, updates synchronization clock vectors,
753 * forms a memory_order constraints graph, and handles replay/backtrack
754 * execution when running permutations of previously-observed executions.
756 * @param curr The current action to process
757 * @return The next Thread that must be executed. May be NULL if ModelChecker
758 * makes no choice (e.g., according to replay execution, combining RMW actions,
761 Thread * ModelChecker::check_current_action(ModelAction *curr)
764 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
766 if (!check_action_enabled(curr)) {
767 /* Make the execution look like we chose to run this action
768 * much later, when a lock/join can succeed */
769 get_current_thread()->set_pending(curr);
770 scheduler->sleep(get_current_thread());
771 return get_next_thread(NULL);
774 ModelAction *newcurr = initialize_curr_action(curr);
776 wake_up_sleeping_actions(curr);
778 /* Add the action to lists before any other model-checking tasks */
779 if (!second_part_of_rmw)
780 add_action_to_lists(newcurr);
782 /* Build may_read_from set for newly-created actions */
783 if (curr == newcurr && curr->is_read())
784 build_reads_from_past(curr);
787 /* Initialize work_queue with the "current action" work */
788 work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
789 while (!work_queue.empty()) {
790 WorkQueueEntry work = work_queue.front();
791 work_queue.pop_front();
794 case WORK_CHECK_CURR_ACTION: {
795 ModelAction *act = work.action;
796 bool update = false; /* update this location's release seq's */
797 bool update_all = false; /* update all release seq's */
799 if (process_thread_action(curr))
802 if (act->is_read() && process_read(act, second_part_of_rmw))
805 if (act->is_write() && process_write(act))
808 if (act->is_mutex_op() && process_mutex(act))
811 if (act->is_relseq_fixup())
812 process_relseq_fixup(curr, &work_queue);
815 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
817 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
820 case WORK_CHECK_RELEASE_SEQ:
821 resolve_release_sequences(work.location, &work_queue);
823 case WORK_CHECK_MO_EDGES: {
824 /** @todo Complete verification of work_queue */
825 ModelAction *act = work.action;
826 bool updated = false;
828 if (act->is_read()) {
829 const ModelAction *rf = act->get_reads_from();
830 if (rf != NULL && r_modification_order(act, rf))
833 if (act->is_write()) {
834 if (w_modification_order(act))
837 mo_graph->commitChanges();
840 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
849 check_curr_backtracking(curr);
850 set_backtracking(curr);
851 return get_next_thread(curr);
854 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
855 Node *currnode = curr->get_node();
856 Node *parnode = currnode->get_parent();
858 if ((!parnode->backtrack_empty() ||
859 !currnode->read_from_empty() ||
860 !currnode->future_value_empty() ||
861 !currnode->promise_empty() ||
862 !currnode->relseq_break_empty())
863 && (!priv->next_backtrack ||
864 *curr > *priv->next_backtrack)) {
865 priv->next_backtrack = curr;
869 bool ModelChecker::promises_expired() {
870 for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
871 Promise *promise = (*promises)[promise_index];
872 if (promise->get_expiration()<priv->used_sequence_numbers) {
879 /** @return whether the current partial trace must be a prefix of a
881 bool ModelChecker::isfeasibleprefix() {
882 return promises->size() == 0 && pending_rel_seqs->size() == 0;
885 /** @return whether the current partial trace is feasible. */
886 bool ModelChecker::isfeasible() {
887 if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
888 DEBUG("Infeasible: RMW violation\n");
890 return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
893 /** @return whether the current partial trace is feasible other than
894 * multiple RMW reading from the same store. */
895 bool ModelChecker::isfeasibleotherthanRMW() {
897 if (mo_graph->checkForCycles())
898 DEBUG("Infeasible: modification order cycles\n");
900 DEBUG("Infeasible: failed promise\n");
902 DEBUG("Infeasible: too many reads\n");
903 if (bad_synchronization)
904 DEBUG("Infeasible: bad synchronization ordering\n");
905 if (promises_expired())
906 DEBUG("Infeasible: promises expired\n");
908 return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
911 /** Returns whether the current completed trace is feasible. */
912 bool ModelChecker::isfinalfeasible() {
913 if (DBG_ENABLED() && promises->size() != 0)
914 DEBUG("Infeasible: unrevolved promises\n");
916 return isfeasible() && promises->size() == 0;
919 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
920 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
921 ModelAction *lastread = get_last_action(act->get_tid());
922 lastread->process_rmw(act);
923 if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
924 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
925 mo_graph->commitChanges();
931 * Checks whether a thread has read from the same write for too many times
932 * without seeing the effects of a later write.
935 * 1) there must a different write that we could read from that would satisfy the modification order,
936 * 2) we must have read from the same value in excess of maxreads times, and
937 * 3) that other write must have been in the reads_from set for maxreads times.
939 * If so, we decide that the execution is no longer feasible.
941 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
942 if (params.maxreads != 0) {
944 if (curr->get_node()->get_read_from_size() <= 1)
946 //Must make sure that execution is currently feasible... We could
947 //accidentally clear by rolling back
950 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
951 int tid = id_to_int(curr->get_tid());
954 if ((int)thrd_lists->size() <= tid)
956 action_list_t *list = &(*thrd_lists)[tid];
958 action_list_t::reverse_iterator rit = list->rbegin();
960 for (; (*rit) != curr; rit++)
962 /* go past curr now */
965 action_list_t::reverse_iterator ritcopy = rit;
966 //See if we have enough reads from the same value
968 for (; count < params.maxreads; rit++,count++) {
969 if (rit==list->rend())
971 ModelAction *act = *rit;
975 if (act->get_reads_from() != rf)
977 if (act->get_node()->get_read_from_size() <= 1)
980 for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
982 const ModelAction * write = curr->get_node()->get_read_from_at(i);
984 //Need a different write
988 /* Test to see whether this is a feasible write to read from*/
989 mo_graph->startChanges();
990 r_modification_order(curr, write);
991 bool feasiblereadfrom = isfeasible();
992 mo_graph->rollbackChanges();
994 if (!feasiblereadfrom)
998 bool feasiblewrite = true;
999 //new we need to see if this write works for everyone
1001 for (int loop = count; loop>0; loop--,rit++) {
1002 ModelAction *act=*rit;
1003 bool foundvalue = false;
1004 for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
1005 if (act->get_node()->get_read_from_at(i)==write) {
1011 feasiblewrite = false;
1015 if (feasiblewrite) {
1016 too_many_reads = true;
1024 * Updates the mo_graph with the constraints imposed from the current
1027 * Basic idea is the following: Go through each other thread and find
1028 * the lastest action that happened before our read. Two cases:
1030 * (1) The action is a write => that write must either occur before
1031 * the write we read from or be the write we read from.
1033 * (2) The action is a read => the write that that action read from
1034 * must occur before the write we read from or be the same write.
1036 * @param curr The current action. Must be a read.
1037 * @param rf The action that curr reads from. Must be a write.
1038 * @return True if modification order edges were added; false otherwise
1040 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
1042 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1045 ASSERT(curr->is_read());
1047 /* Iterate over all threads */
1048 for (i = 0; i < thrd_lists->size(); i++) {
1049 /* Iterate over actions in thread, starting from most recent */
1050 action_list_t *list = &(*thrd_lists)[i];
1051 action_list_t::reverse_iterator rit;
1052 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1053 ModelAction *act = *rit;
1056 * Include at most one act per-thread that "happens
1057 * before" curr. Don't consider reflexively.
1059 if (act->happens_before(curr) && act != curr) {
1060 if (act->is_write()) {
1062 mo_graph->addEdge(act, rf);
1066 const ModelAction *prevreadfrom = act->get_reads_from();
1067 //if the previous read is unresolved, keep going...
1068 if (prevreadfrom == NULL)
1071 if (rf != prevreadfrom) {
1072 mo_graph->addEdge(prevreadfrom, rf);
1084 /** This method fixes up the modification order when we resolve a
1085 * promises. The basic problem is that actions that occur after the
1086 * read curr could not property add items to the modification order
1089 * So for each thread, we find the earliest item that happens after
1090 * the read curr. This is the item we have to fix up with additional
1091 * constraints. If that action is write, we add a MO edge between
1092 * the Action rf and that action. If the action is a read, we add a
1093 * MO edge between the Action rf, and whatever the read accessed.
1095 * @param curr is the read ModelAction that we are fixing up MO edges for.
1096 * @param rf is the write ModelAction that curr reads from.
1099 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1101 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1103 ASSERT(curr->is_read());
1105 /* Iterate over all threads */
1106 for (i = 0; i < thrd_lists->size(); i++) {
1107 /* Iterate over actions in thread, starting from most recent */
1108 action_list_t *list = &(*thrd_lists)[i];
1109 action_list_t::reverse_iterator rit;
1110 ModelAction *lastact = NULL;
1112 /* Find last action that happens after curr that is either not curr or a rmw */
1113 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1114 ModelAction *act = *rit;
1115 if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1121 /* Include at most one act per-thread that "happens before" curr */
1122 if (lastact != NULL) {
1123 if (lastact==curr) {
1124 //Case 1: The resolved read is a RMW, and we need to make sure
1125 //that the write portion of the RMW mod order after rf
1127 mo_graph->addEdge(rf, lastact);
1128 } else if (lastact->is_read()) {
1129 //Case 2: The resolved read is a normal read and the next
1130 //operation is a read, and we need to make sure the value read
1131 //is mod ordered after rf
1133 const ModelAction *postreadfrom = lastact->get_reads_from();
1134 if (postreadfrom != NULL&&rf != postreadfrom)
1135 mo_graph->addEdge(rf, postreadfrom);
1137 //Case 3: The resolved read is a normal read and the next
1138 //operation is a write, and we need to make sure that the
1139 //write is mod ordered after rf
1141 mo_graph->addEdge(rf, lastact);
1149 * Updates the mo_graph with the constraints imposed from the current write.
1151 * Basic idea is the following: Go through each other thread and find
1152 * the lastest action that happened before our write. Two cases:
1154 * (1) The action is a write => that write must occur before
1157 * (2) The action is a read => the write that that action read from
1158 * must occur before the current write.
1160 * This method also handles two other issues:
1162 * (I) Sequential Consistency: Making sure that if the current write is
1163 * seq_cst, that it occurs after the previous seq_cst write.
1165 * (II) Sending the write back to non-synchronizing reads.
1167 * @param curr The current action. Must be a write.
1168 * @return True if modification order edges were added; false otherwise
1170 bool ModelChecker::w_modification_order(ModelAction *curr)
1172 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1175 ASSERT(curr->is_write());
1177 if (curr->is_seqcst()) {
1178 /* We have to at least see the last sequentially consistent write,
1179 so we are initialized. */
1180 ModelAction *last_seq_cst = get_last_seq_cst(curr);
1181 if (last_seq_cst != NULL) {
1182 mo_graph->addEdge(last_seq_cst, curr);
1187 /* Iterate over all threads */
1188 for (i = 0; i < thrd_lists->size(); i++) {
1189 /* Iterate over actions in thread, starting from most recent */
1190 action_list_t *list = &(*thrd_lists)[i];
1191 action_list_t::reverse_iterator rit;
1192 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1193 ModelAction *act = *rit;
1196 * 1) If RMW and it actually read from something, then we
1197 * already have all relevant edges, so just skip to next
1200 * 2) If RMW and it didn't read from anything, we should
1201 * whatever edge we can get to speed up convergence.
1203 * 3) If normal write, we need to look at earlier actions, so
1204 * continue processing list.
1206 if (curr->is_rmw()) {
1207 if (curr->get_reads_from()!=NULL)
1216 * Include at most one act per-thread that "happens
1219 if (act->happens_before(curr)) {
1221 * Note: if act is RMW, just add edge:
1223 * The following edge should be handled elsewhere:
1224 * readfrom(act) --mo--> act
1226 if (act->is_write())
1227 mo_graph->addEdge(act, curr);
1228 else if (act->is_read()) {
1229 //if previous read accessed a null, just keep going
1230 if (act->get_reads_from() == NULL)
1232 mo_graph->addEdge(act->get_reads_from(), curr);
1236 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1237 !act->same_thread(curr)) {
1238 /* We have an action that:
1239 (1) did not happen before us
1240 (2) is a read and we are a write
1241 (3) cannot synchronize with us
1242 (4) is in a different thread
1244 that read could potentially read from our write. Note that
1245 these checks are overly conservative at this point, we'll
1246 do more checks before actually removing the
1250 if (thin_air_constraint_may_allow(curr, act)) {
1252 (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
1253 struct PendingFutureValue pfv = {curr,act};
1254 futurevalues->push_back(pfv);
1264 /** Arbitrary reads from the future are not allowed. Section 29.3
1265 * part 9 places some constraints. This method checks one result of constraint
1266 * constraint. Others require compiler support. */
1267 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
1268 if (!writer->is_rmw())
1271 if (!reader->is_rmw())
1274 for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1275 if (search == reader)
1277 if (search->get_tid() == reader->get_tid() &&
1278 search->happens_before(reader))
1285 /** Arbitrary reads from the future are not allowed. Section 29.3
1286 * part 9 places some constraints. This method checks one result of constraint
1287 * constraint. Others require compiler support. */
1288 bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
1289 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
1291 //Get write that follows reader action
1292 action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
1293 action_list_t::reverse_iterator rit;
1294 ModelAction *first_write_after_read=NULL;
1296 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1297 ModelAction *act = *rit;
1300 if (act->is_write())
1301 first_write_after_read=act;
1304 if (first_write_after_read==NULL)
1307 return !mo_graph->checkReachable(first_write_after_read, writer);
1313 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1314 * The ModelAction under consideration is expected to be taking part in
1315 * release/acquire synchronization as an object of the "reads from" relation.
1316 * Note that this can only provide release sequence support for RMW chains
1317 * which do not read from the future, as those actions cannot be traced until
1318 * their "promise" is fulfilled. Similarly, we may not even establish the
1319 * presence of a release sequence with certainty, as some modification order
1320 * constraints may be decided further in the future. Thus, this function
1321 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1322 * and a boolean representing certainty.
1324 * @param rf The action that might be part of a release sequence. Must be a
1326 * @param release_heads A pass-by-reference style return parameter. After
1327 * execution of this function, release_heads will contain the heads of all the
1328 * relevant release sequences, if any exists with certainty
1329 * @param pending A pass-by-reference style return parameter which is only used
1330 * when returning false (i.e., uncertain). Returns most information regarding
1331 * an uncertain release sequence, including any write operations that might
1332 * break the sequence.
1333 * @return true, if the ModelChecker is certain that release_heads is complete;
1336 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1337 rel_heads_list_t *release_heads,
1338 struct release_seq *pending) const
1340 /* Only check for release sequences if there are no cycles */
1341 if (mo_graph->checkForCycles())
1345 ASSERT(rf->is_write());
1347 if (rf->is_release())
1348 release_heads->push_back(rf);
1350 break; /* End of RMW chain */
1352 /** @todo Need to be smarter here... In the linux lock
1353 * example, this will run to the beginning of the program for
1355 /** @todo The way to be smarter here is to keep going until 1
1356 * thread has a release preceded by an acquire and you've seen
1359 /* acq_rel RMW is a sufficient stopping condition */
1360 if (rf->is_acquire() && rf->is_release())
1361 return true; /* complete */
1363 rf = rf->get_reads_from();
1366 /* read from future: need to settle this later */
1368 return false; /* incomplete */
1371 if (rf->is_release())
1372 return true; /* complete */
1374 /* else relaxed write; check modification order for contiguous subsequence
1375 * -> rf must be same thread as release */
1376 int tid = id_to_int(rf->get_tid());
1377 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
1378 action_list_t *list = &(*thrd_lists)[tid];
1379 action_list_t::const_reverse_iterator rit;
1381 /* Find rf in the thread list */
1382 rit = std::find(list->rbegin(), list->rend(), rf);
1383 ASSERT(rit != list->rend());
1385 /* Find the last write/release */
1386 for (; rit != list->rend(); rit++)
1387 if ((*rit)->is_release())
1389 if (rit == list->rend()) {
1390 /* No write-release in this thread */
1391 return true; /* complete */
1393 ModelAction *release = *rit;
1395 ASSERT(rf->same_thread(release));
1397 pending->writes.clear();
1399 bool certain = true;
1400 for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1401 if (id_to_int(rf->get_tid()) == (int)i)
1403 list = &(*thrd_lists)[i];
1405 /* Can we ensure no future writes from this thread may break
1406 * the release seq? */
1407 bool future_ordered = false;
1409 ModelAction *last = get_last_action(int_to_id(i));
1410 Thread *th = get_thread(int_to_id(i));
1411 if ((last && rf->happens_before(last)) ||
1412 !scheduler->is_enabled(th) ||
1414 future_ordered = true;
1416 ASSERT(!th->is_model_thread() || future_ordered);
1418 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1419 const ModelAction *act = *rit;
1420 /* Reach synchronization -> this thread is complete */
1421 if (act->happens_before(release))
1423 if (rf->happens_before(act)) {
1424 future_ordered = true;
1428 /* Only writes can break release sequences */
1429 if (!act->is_write())
1432 /* Check modification order */
1433 if (mo_graph->checkReachable(rf, act)) {
1434 /* rf --mo--> act */
1435 future_ordered = true;
1438 if (mo_graph->checkReachable(act, release))
1439 /* act --mo--> release */
1441 if (mo_graph->checkReachable(release, act) &&
1442 mo_graph->checkReachable(act, rf)) {
1443 /* release --mo-> act --mo--> rf */
1444 return true; /* complete */
1446 /* act may break release sequence */
1447 pending->writes.push_back(act);
1450 if (!future_ordered)
1451 certain = false; /* This thread is uncertain */
1455 release_heads->push_back(release);
1456 pending->writes.clear();
1458 pending->release = release;
1465 * A public interface for getting the release sequence head(s) with which a
1466 * given ModelAction must synchronize. This function only returns a non-empty
1467 * result when it can locate a release sequence head with certainty. Otherwise,
1468 * it may mark the internal state of the ModelChecker so that it will handle
1469 * the release sequence at a later time, causing @a act to update its
1470 * synchronization at some later point in execution.
1471 * @param act The 'acquire' action that may read from a release sequence
1472 * @param release_heads A pass-by-reference return parameter. Will be filled
1473 * with the head(s) of the release sequence(s), if they exists with certainty.
1474 * @see ModelChecker::release_seq_heads
1476 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
1478 const ModelAction *rf = act->get_reads_from();
1479 struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
1480 sequence->acquire = act;
1482 if (!release_seq_heads(rf, release_heads, sequence)) {
1483 /* add act to 'lazy checking' list */
1484 pending_rel_seqs->push_back(sequence);
1486 snapshot_free(sequence);
1491 * Attempt to resolve all stashed operations that might synchronize with a
1492 * release sequence for a given location. This implements the "lazy" portion of
1493 * determining whether or not a release sequence was contiguous, since not all
1494 * modification order information is present at the time an action occurs.
1496 * @param location The location/object that should be checked for release
1497 * sequence resolutions. A NULL value means to check all locations.
1498 * @param work_queue The work queue to which to add work items as they are
1500 * @return True if any updates occurred (new synchronization, new mo_graph
1503 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
1505 bool updated = false;
1506 std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
1507 while (it != pending_rel_seqs->end()) {
1508 struct release_seq *pending = *it;
1509 ModelAction *act = pending->acquire;
1511 /* Only resolve sequences on the given location, if provided */
1512 if (location && act->get_location() != location) {
1517 const ModelAction *rf = act->get_reads_from();
1518 rel_heads_list_t release_heads;
1520 complete = release_seq_heads(rf, &release_heads, pending);
1521 for (unsigned int i = 0; i < release_heads.size(); i++) {
1522 if (!act->has_synchronized_with(release_heads[i])) {
1523 if (act->synchronize_with(release_heads[i]))
1526 set_bad_synchronization();
1531 /* Re-check all pending release sequences */
1532 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1533 /* Re-check act for mo_graph edges */
1534 work_queue->push_back(MOEdgeWorkEntry(act));
1536 /* propagate synchronization to later actions */
1537 action_list_t::reverse_iterator rit = action_trace->rbegin();
1538 for (; (*rit) != act; rit++) {
1539 ModelAction *propagate = *rit;
1540 if (act->happens_before(propagate)) {
1541 propagate->synchronize_with(act);
1542 /* Re-check 'propagate' for mo_graph edges */
1543 work_queue->push_back(MOEdgeWorkEntry(propagate));
1548 it = pending_rel_seqs->erase(it);
1549 snapshot_free(pending);
1555 // If we resolved promises or data races, see if we have realized a data race.
1556 if (checkDataRaces()) {
1564 * Performs various bookkeeping operations for the current ModelAction. For
1565 * instance, adds action to the per-object, per-thread action vector and to the
1566 * action trace list of all thread actions.
1568 * @param act is the ModelAction to add.
1570 void ModelChecker::add_action_to_lists(ModelAction *act)
1572 int tid = id_to_int(act->get_tid());
1573 action_trace->push_back(act);
1575 obj_map->get_safe_ptr(act->get_location())->push_back(act);
1577 std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
1578 if (tid >= (int)vec->size())
1579 vec->resize(priv->next_thread_id);
1580 (*vec)[tid].push_back(act);
1582 if ((int)thrd_last_action->size() <= tid)
1583 thrd_last_action->resize(get_num_threads());
1584 (*thrd_last_action)[tid] = act;
1588 * @brief Get the last action performed by a particular Thread
1589 * @param tid The thread ID of the Thread in question
1590 * @return The last action in the thread
1592 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
1594 int threadid = id_to_int(tid);
1595 if (threadid < (int)thrd_last_action->size())
1596 return (*thrd_last_action)[id_to_int(tid)];
1602 * Gets the last memory_order_seq_cst write (in the total global sequence)
1603 * performed on a particular object (i.e., memory location), not including the
1605 * @param curr The current ModelAction; also denotes the object location to
1607 * @return The last seq_cst write
1609 ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
1611 void *location = curr->get_location();
1612 action_list_t *list = obj_map->get_safe_ptr(location);
1613 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1614 action_list_t::reverse_iterator rit;
1615 for (rit = list->rbegin(); rit != list->rend(); rit++)
1616 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
1622 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1623 * location). This function identifies the mutex according to the current
1624 * action, which is presumed to perform on the same mutex.
1625 * @param curr The current ModelAction; also denotes the object location to
1627 * @return The last unlock operation
1629 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
1631 void *location = curr->get_location();
1632 action_list_t *list = obj_map->get_safe_ptr(location);
1633 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1634 action_list_t::reverse_iterator rit;
1635 for (rit = list->rbegin(); rit != list->rend(); rit++)
1636 if ((*rit)->is_unlock())
1641 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
1643 ModelAction *parent = get_last_action(tid);
1645 parent = get_thread(tid)->get_creation();
1650 * Returns the clock vector for a given thread.
1651 * @param tid The thread whose clock vector we want
1652 * @return Desired clock vector
1654 ClockVector * ModelChecker::get_cv(thread_id_t tid)
1656 return get_parent_action(tid)->get_cv();
1660 * Resolve a set of Promises with a current write. The set is provided in the
1661 * Node corresponding to @a write.
1662 * @param write The ModelAction that is fulfilling Promises
1663 * @return True if promises were resolved; false otherwise
1665 bool ModelChecker::resolve_promises(ModelAction *write)
1667 bool resolved = false;
1668 std::vector< thread_id_t, ModelAlloc<thread_id_t> > threads_to_check;
1670 for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
1671 Promise *promise = (*promises)[promise_index];
1672 if (write->get_node()->get_promise(i)) {
1673 ModelAction *read = promise->get_action();
1674 if (read->is_rmw()) {
1675 mo_graph->addRMWEdge(write, read);
1677 read->read_from(write);
1678 //First fix up the modification order for actions that happened
1680 r_modification_order(read, write);
1681 //Next fix up the modification order for actions that happened
1683 post_r_modification_order(read, write);
1684 //Make sure the promise's value matches the write's value
1685 ASSERT(promise->get_value() == write->get_value());
1688 promises->erase(promises->begin() + promise_index);
1689 threads_to_check.push_back(read->get_tid());
1696 //Check whether reading these writes has made threads unable to
1699 for(unsigned int i=0;i<threads_to_check.size();i++)
1700 mo_check_promises(threads_to_check[i], write);
1706 * Compute the set of promises that could potentially be satisfied by this
1707 * action. Note that the set computation actually appears in the Node, not in
1709 * @param curr The ModelAction that may satisfy promises
1711 void ModelChecker::compute_promises(ModelAction *curr)
1713 for (unsigned int i = 0; i < promises->size(); i++) {
1714 Promise *promise = (*promises)[i];
1715 const ModelAction *act = promise->get_action();
1716 if (!act->happens_before(curr) &&
1718 !act->could_synchronize_with(curr) &&
1719 !act->same_thread(curr) &&
1720 promise->get_value() == curr->get_value()) {
1721 curr->get_node()->set_promise(i);
1726 /** Checks promises in response to change in ClockVector Threads. */
1727 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
1729 for (unsigned int i = 0; i < promises->size(); i++) {
1730 Promise *promise = (*promises)[i];
1731 const ModelAction *act = promise->get_action();
1732 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
1733 merge_cv->synchronized_since(act)) {
1734 if (promise->increment_threads(tid)) {
1735 //Promise has failed
1736 failed_promise = true;
1743 /** Checks promises in response to addition to modification order for threads.
1745 * pthread is the thread that performed the read that created the promise
1747 * pread is the read that created the promise
1749 * pwrite is either the first write to same location as pread by
1750 * pthread that is sequenced after pread or the value read by the
1751 * first read to the same lcoation as pread by pthread that is
1752 * sequenced after pread..
1754 * 1. If tid=pthread, then we check what other threads are reachable
1755 * through the mode order starting with pwrite. Those threads cannot
1756 * perform a write that will resolve the promise due to modification
1757 * order constraints.
1759 * 2. If the tid is not pthread, we check whether pwrite can reach the
1760 * action write through the modification order. If so, that thread
1761 * cannot perform a future write that will resolve the promise due to
1762 * modificatin order constraints.
1764 * @parem tid The thread that either read from the model action
1765 * write, or actually did the model action write.
1767 * @parem write The ModelAction representing the relevant write.
1770 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
1771 void * location = write->get_location();
1772 for (unsigned int i = 0; i < promises->size(); i++) {
1773 Promise *promise = (*promises)[i];
1774 const ModelAction *act = promise->get_action();
1776 //Is this promise on the same location?
1777 if ( act->get_location() != location )
1780 //same thread as the promise
1781 if ( act->get_tid()==tid ) {
1783 //do we have a pwrite for the promise, if not, set it
1784 if (promise->get_write() == NULL ) {
1785 promise->set_write(write);
1786 //The pwrite cannot happen before the promise
1787 if (write->happens_before(act) && (write != act)) {
1788 failed_promise = true;
1792 if (mo_graph->checkPromise(write, promise)) {
1793 failed_promise = true;
1798 //Don't do any lookups twice for the same thread
1799 if (promise->has_sync_thread(tid))
1802 if (mo_graph->checkReachable(promise->get_write(), write)) {
1803 if (promise->increment_threads(tid)) {
1804 failed_promise = true;
1812 * Compute the set of writes that may break the current pending release
1813 * sequence. This information is extracted from previou release sequence
1816 * @param curr The current ModelAction. Must be a release sequence fixup
1819 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
1821 if (pending_rel_seqs->empty())
1824 struct release_seq *pending = pending_rel_seqs->back();
1825 for (unsigned int i = 0; i < pending->writes.size(); i++) {
1826 const ModelAction *write = pending->writes[i];
1827 curr->get_node()->add_relseq_break(write);
1830 /* NULL means don't break the sequence; just synchronize */
1831 curr->get_node()->add_relseq_break(NULL);
1835 * Build up an initial set of all past writes that this 'read' action may read
1836 * from. This set is determined by the clock vector's "happens before"
1838 * @param curr is the current ModelAction that we are exploring; it must be a
1841 void ModelChecker::build_reads_from_past(ModelAction *curr)
1843 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1845 ASSERT(curr->is_read());
1847 ModelAction *last_seq_cst = NULL;
1849 /* Track whether this object has been initialized */
1850 bool initialized = false;
1852 if (curr->is_seqcst()) {
1853 last_seq_cst = get_last_seq_cst(curr);
1854 /* We have to at least see the last sequentially consistent write,
1855 so we are initialized. */
1856 if (last_seq_cst != NULL)
1860 /* Iterate over all threads */
1861 for (i = 0; i < thrd_lists->size(); i++) {
1862 /* Iterate over actions in thread, starting from most recent */
1863 action_list_t *list = &(*thrd_lists)[i];
1864 action_list_t::reverse_iterator rit;
1865 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1866 ModelAction *act = *rit;
1868 /* Only consider 'write' actions */
1869 if (!act->is_write() || act == curr)
1872 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1873 if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
1874 DEBUG("Adding action to may_read_from:\n");
1875 if (DBG_ENABLED()) {
1880 if (curr->get_sleep_flag() && ! curr->is_seqcst()) {
1881 if (sleep_can_read_from(curr, act))
1882 curr->get_node()->add_read_from(act);
1884 curr->get_node()->add_read_from(act);
1887 /* Include at most one act per-thread that "happens before" curr */
1888 if (act->happens_before(curr)) {
1896 /** @todo Need a more informative way of reporting errors. */
1897 printf("ERROR: may read from uninitialized atomic\n");
1900 if (DBG_ENABLED() || !initialized) {
1901 printf("Reached read action:\n");
1903 printf("Printing may_read_from\n");
1904 curr->get_node()->print_may_read_from();
1905 printf("End printing may_read_from\n");
1908 ASSERT(initialized);
1911 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
1913 Node *prevnode=write->get_node()->get_parent();
1914 bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
1915 if (write->is_release()&&thread_sleep)
1917 if (!write->is_rmw()) {
1920 if (write->get_reads_from()==NULL)
1922 write=write->get_reads_from();
1926 static void print_list(action_list_t *list)
1928 action_list_t::iterator it;
1930 printf("---------------------------------------------------------------------\n");
1932 unsigned int hash=0;
1934 for (it = list->begin(); it != list->end(); it++) {
1936 hash=hash^(hash<<3)^((*it)->hash());
1938 printf("HASH %u\n", hash);
1939 printf("---------------------------------------------------------------------\n");
1942 #if SUPPORT_MOD_ORDER_DUMP
1943 void ModelChecker::dumpGraph(char *filename) {
1945 sprintf(buffer, "%s.dot",filename);
1946 FILE *file=fopen(buffer, "w");
1947 fprintf(file, "digraph %s {\n",filename);
1948 mo_graph->dumpNodes(file);
1949 ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
1951 for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
1952 ModelAction *action=*it;
1953 if (action->is_read()) {
1954 fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
1955 if (action->get_reads_from()!=NULL)
1956 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
1958 if (thread_array[action->get_tid()] != NULL) {
1959 fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
1962 thread_array[action->get_tid()]=action;
1964 fprintf(file,"}\n");
1965 model_free(thread_array);
1970 void ModelChecker::print_summary()
1973 printf("Number of executions: %d\n", num_executions);
1974 printf("Number of feasible executions: %d\n", num_feasible_executions);
1975 printf("Total nodes created: %d\n", node_stack->get_total_nodes());
1977 #if SUPPORT_MOD_ORDER_DUMP
1979 char buffername[100];
1980 sprintf(buffername, "exec%04u", num_executions);
1981 mo_graph->dumpGraphToFile(buffername);
1982 sprintf(buffername, "graph%04u", num_executions);
1983 dumpGraph(buffername);
1986 if (!isfinalfeasible())
1987 printf("INFEASIBLE EXECUTION!\n");
1988 print_list(action_trace);
1993 * Add a Thread to the system for the first time. Should only be called once
1995 * @param t The Thread to add
1997 void ModelChecker::add_thread(Thread *t)
1999 thread_map->put(id_to_int(t->get_id()), t);
2000 scheduler->add_thread(t);
2004 * Removes a thread from the scheduler.
2005 * @param the thread to remove.
2007 void ModelChecker::remove_thread(Thread *t)
2009 scheduler->remove_thread(t);
2013 * @brief Get a Thread reference by its ID
2014 * @param tid The Thread's ID
2015 * @return A Thread reference
2017 Thread * ModelChecker::get_thread(thread_id_t tid) const
2019 return thread_map->get(id_to_int(tid));
2023 * @brief Get a reference to the Thread in which a ModelAction was executed
2024 * @param act The ModelAction
2025 * @return A Thread reference
2027 Thread * ModelChecker::get_thread(ModelAction *act) const
2029 return get_thread(act->get_tid());
2033 * Switch from a user-context to the "master thread" context (a.k.a. system
2034 * context). This switch is made with the intention of exploring a particular
2035 * model-checking action (described by a ModelAction object). Must be called
2036 * from a user-thread context.
2038 * @param act The current action that will be explored. May be NULL only if
2039 * trace is exiting via an assertion (see ModelChecker::set_assert and
2040 * ModelChecker::has_asserted).
2041 * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
2043 int ModelChecker::switch_to_master(ModelAction *act)
2046 Thread *old = thread_current();
2047 set_current_action(act);
2048 old->set_state(THREAD_READY);
2049 return Thread::swap(old, &system_context);
2053 * Takes the next step in the execution, if possible.
2054 * @return Returns true (success) if a step was taken and false otherwise.
2056 bool ModelChecker::take_step() {
2060 Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
2062 if (curr->get_state() == THREAD_READY) {
2063 ASSERT(priv->current_action);
2065 priv->nextThread = check_current_action(priv->current_action);
2066 priv->current_action = NULL;
2068 if (curr->is_blocked() || curr->is_complete())
2069 scheduler->remove_thread(curr);
2074 Thread *next = scheduler->next_thread(priv->nextThread);
2076 /* Infeasible -> don't take any more steps */
2080 if (params.bound != 0) {
2081 if (priv->used_sequence_numbers > params.bound) {
2086 DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
2087 next ? id_to_int(next->get_id()) : -1);
2090 * Launch end-of-execution release sequence fixups only when there are:
2092 * (1) no more user threads to run (or when execution replay chooses
2093 * the 'model_thread')
2094 * (2) pending release sequences
2095 * (3) pending assertions (i.e., data races)
2096 * (4) no pending promises
2098 if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
2099 isfinalfeasible() && !unrealizedraces.empty()) {
2100 printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2101 pending_rel_seqs->size());
2102 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2103 std::memory_order_seq_cst, NULL, VALUE_NONE,
2105 set_current_action(fixup);
2109 /* next == NULL -> don't take any more steps */
2113 next->set_state(THREAD_RUNNING);
2115 if (next->get_pending() != NULL) {
2116 /* restart a pending action */
2117 set_current_action(next->get_pending());
2118 next->set_pending(NULL);
2119 next->set_state(THREAD_READY);
2123 /* Return false only if swap fails with an error */
2124 return (Thread::swap(&system_context, next) == 0);
2127 /** Runs the current execution until threre are no more steps to take. */
2128 void ModelChecker::finish_execution() {
2131 while (take_step());