12 #include "clockvector.h"
13 #include "cyclegraph.h"
15 #include "threads-model.h"
16 #include "bugmessage.h"
19 #define INITIAL_THREAD_ID 0
22 * Structure for holding small ModelChecker members that should be snapshotted
24 struct model_snapshot_members {
25 model_snapshot_members() :
26 /* First thread created will have id INITIAL_THREAD_ID */
27 next_thread_id(INITIAL_THREAD_ID),
28 used_sequence_numbers(0),
30 bad_synchronization(false),
35 ~model_snapshot_members() {
36 for (unsigned int i = 0;i < bugs.size();i++)
41 unsigned int next_thread_id;
42 modelclock_t used_sequence_numbers;
43 SnapVector<bug_message *> bugs;
44 /** @brief Incorrectly-ordered synchronization was made */
45 bool bad_synchronization;
52 /** @brief Constructor */
53 ModelExecution::ModelExecution(ModelChecker *m,
55 NodeStack *node_stack) :
60 thread_map(2), /* We'll always need at least 2 threads */
64 condvar_waiters_map(),
68 thrd_last_fence_release(),
69 node_stack(node_stack),
70 priv(new struct model_snapshot_members ()),
71 mo_graph(new CycleGraph()),
74 /* Initialize a model-checker thread, for special ModelActions */
75 model_thread = new Thread(get_next_id());
76 add_thread(model_thread);
77 scheduler->register_engine(this);
78 node_stack->register_engine(this);
81 /** @brief Destructor */
82 ModelExecution::~ModelExecution()
84 for (unsigned int i = 0;i < get_num_threads();i++)
85 delete get_thread(int_to_id(i));
91 int ModelExecution::get_execution_number() const
93 return model->get_execution_number();
96 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
98 action_list_t *tmp = hash->get(ptr);
100 tmp = new action_list_t();
106 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
108 SnapVector<action_list_t> *tmp = hash->get(ptr);
110 tmp = new SnapVector<action_list_t>();
116 action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
118 SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
121 unsigned int thread=id_to_int(tid);
122 if (thread < wrv->size())
123 return &(*wrv)[thread];
128 /** @return a thread ID for a new Thread */
129 thread_id_t ModelExecution::get_next_id()
131 return priv->next_thread_id++;
134 /** @return the number of user threads created during this execution */
135 unsigned int ModelExecution::get_num_threads() const
137 return priv->next_thread_id;
140 /** @return a sequence number for a new ModelAction */
141 modelclock_t ModelExecution::get_next_seq_num()
143 return ++priv->used_sequence_numbers;
147 * @brief Should the current action wake up a given thread?
149 * @param curr The current action
150 * @param thread The thread that we might wake up
151 * @return True, if we should wake up the sleeping thread; false otherwise
153 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
155 const ModelAction *asleep = thread->get_pending();
156 /* Don't allow partial RMW to wake anyone up */
159 /* Synchronizing actions may have been backtracked */
160 if (asleep->could_synchronize_with(curr))
162 /* All acquire/release fences and fence-acquire/store-release */
163 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
165 /* Fence-release + store can awake load-acquire on the same location */
166 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
167 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
168 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
174 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
176 for (unsigned int i = 0;i < get_num_threads();i++) {
177 Thread *thr = get_thread(int_to_id(i));
178 if (scheduler->is_sleep_set(thr)) {
179 if (should_wake_up(curr, thr))
180 /* Remove this thread from sleep set */
181 scheduler->remove_sleep(thr);
186 /** @brief Alert the model-checker that an incorrectly-ordered
187 * synchronization was made */
188 void ModelExecution::set_bad_synchronization()
190 priv->bad_synchronization = true;
193 /** @brief Alert the model-checker that an incorrectly-ordered
194 * synchronization was made */
195 void ModelExecution::set_bad_sc_read()
197 priv->bad_sc_read = true;
200 bool ModelExecution::assert_bug(const char *msg)
202 priv->bugs.push_back(new bug_message(msg));
204 if (isfeasibleprefix()) {
211 /** @return True, if any bugs have been reported for this execution */
212 bool ModelExecution::have_bug_reports() const
214 return priv->bugs.size() != 0;
217 SnapVector<bug_message *> * ModelExecution::get_bugs() const
223 * Check whether the current trace has triggered an assertion which should halt
226 * @return True, if the execution should be aborted; false otherwise
228 bool ModelExecution::has_asserted() const
230 return priv->asserted;
234 * Trigger a trace assertion which should cause this execution to be halted.
235 * This can be due to a detected bug or due to an infeasibility that should
238 void ModelExecution::set_assert()
240 priv->asserted = true;
244 * Check if we are in a deadlock. Should only be called at the end of an
245 * execution, although it should not give false positives in the middle of an
246 * execution (there should be some ENABLED thread).
248 * @return True if program is in a deadlock; false otherwise
250 bool ModelExecution::is_deadlocked() const
252 bool blocking_threads = false;
253 for (unsigned int i = 0;i < get_num_threads();i++) {
254 thread_id_t tid = int_to_id(i);
257 Thread *t = get_thread(tid);
258 if (!t->is_model_thread() && t->get_pending())
259 blocking_threads = true;
261 return blocking_threads;
265 * Check if this is a complete execution. That is, have all thread completed
266 * execution (rather than exiting because sleep sets have forced a redundant
269 * @return True if the execution is complete.
271 bool ModelExecution::is_complete_execution() const
273 for (unsigned int i = 0;i < get_num_threads();i++)
274 if (is_enabled(int_to_id(i)))
281 * Processes a read model action.
282 * @param curr is the read model action to process.
283 * @param rf_set is the set of model actions we can possibly read from
284 * @return True if processing this read updates the mo_graph.
286 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
290 int index = fuzzer->selectWrite(curr, rf_set);
291 const ModelAction *rf = (*rf_set)[index];
296 mo_graph->startChanges();
297 bool updated = r_modification_order(curr, rf);
298 if (!is_infeasible()) {
300 mo_graph->commitChanges();
301 get_thread(curr)->set_return_value(curr->get_return_value());
304 mo_graph->rollbackChanges();
305 (*rf_set)[index] = rf_set->back();
311 * Processes a lock, trylock, or unlock model action. @param curr is
312 * the read model action to process.
314 * The try lock operation checks whether the lock is taken. If not,
315 * it falls to the normal lock operation case. If so, it returns
318 * The lock operation has already been checked that it is enabled, so
319 * it just grabs the lock and synchronizes with the previous unlock.
321 * The unlock operation has to re-enable all of the threads that are
322 * waiting on the lock.
324 * @return True if synchronization was updated; false otherwise
326 bool ModelExecution::process_mutex(ModelAction *curr)
328 cdsc::mutex *mutex = curr->get_mutex();
329 struct cdsc::mutex_state *state = NULL;
332 state = mutex->get_state();
334 switch (curr->get_type()) {
335 case ATOMIC_TRYLOCK: {
336 bool success = !state->locked;
337 curr->set_try_lock(success);
339 get_thread(curr)->set_return_value(0);
342 get_thread(curr)->set_return_value(1);
344 //otherwise fall into the lock case
346 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
347 assert_bug("Lock access before initialization");
348 state->locked = get_thread(curr);
349 ModelAction *unlock = get_last_unlock(curr);
350 //synchronize with the previous unlock statement
351 if (unlock != NULL) {
352 synchronize(unlock, curr);
358 case ATOMIC_UNLOCK: {
359 /* wake up the other threads */
360 for (unsigned int i = 0;i < get_num_threads();i++) {
361 Thread *t = get_thread(int_to_id(i));
362 Thread *curr_thrd = get_thread(curr);
363 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
367 /* unlock the lock - after checking who was waiting on it */
368 state->locked = NULL;
370 if (!curr->is_wait())
371 break;/* The rest is only for ATOMIC_WAIT */
375 case ATOMIC_NOTIFY_ALL: {
376 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
377 //activate all the waiting threads
378 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
379 scheduler->wake(get_thread(*rit));
384 case ATOMIC_NOTIFY_ONE: {
385 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
386 Thread * thread = fuzzer->selectNotify(waiters);
387 scheduler->wake(thread);
398 * Process a write ModelAction
399 * @param curr The ModelAction to process
400 * @return True if the mo_graph was updated or promises were resolved
402 bool ModelExecution::process_write(ModelAction *curr)
405 bool updated_mod_order = w_modification_order(curr);
407 mo_graph->commitChanges();
409 get_thread(curr)->set_return_value(VALUE_NONE);
410 return updated_mod_order;
414 * Process a fence ModelAction
415 * @param curr The ModelAction to process
416 * @return True if synchronization was updated
418 bool ModelExecution::process_fence(ModelAction *curr)
421 * fence-relaxed: no-op
422 * fence-release: only log the occurence (not in this function), for
423 * use in later synchronization
424 * fence-acquire (this function): search for hypothetical release
426 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
428 bool updated = false;
429 if (curr->is_acquire()) {
430 action_list_t *list = &action_trace;
431 action_list_t::reverse_iterator rit;
432 /* Find X : is_read(X) && X --sb-> curr */
433 for (rit = list->rbegin();rit != list->rend();rit++) {
434 ModelAction *act = *rit;
437 if (act->get_tid() != curr->get_tid())
439 /* Stop at the beginning of the thread */
440 if (act->is_thread_start())
442 /* Stop once we reach a prior fence-acquire */
443 if (act->is_fence() && act->is_acquire())
447 /* read-acquire will find its own release sequences */
448 if (act->is_acquire())
451 /* Establish hypothetical release sequences */
452 rel_heads_list_t release_heads;
453 get_release_seq_heads(curr, act, &release_heads);
454 for (unsigned int i = 0;i < release_heads.size();i++)
455 synchronize(release_heads[i], curr);
456 if (release_heads.size() != 0)
464 * @brief Process the current action for thread-related activity
466 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
467 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
468 * synchronization, etc. This function is a no-op for non-THREAD actions
469 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
471 * @param curr The current action
472 * @return True if synchronization was updated or a thread completed
474 bool ModelExecution::process_thread_action(ModelAction *curr)
476 bool updated = false;
478 switch (curr->get_type()) {
479 case THREAD_CREATE: {
480 thrd_t *thrd = (thrd_t *)curr->get_location();
481 struct thread_params *params = (struct thread_params *)curr->get_value();
482 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
483 curr->set_thread_operand(th);
485 th->set_creation(curr);
488 case PTHREAD_CREATE: {
489 (*(uint32_t *)curr->get_location()) = pthread_counter++;
491 struct pthread_params *params = (struct pthread_params *)curr->get_value();
492 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
493 curr->set_thread_operand(th);
495 th->set_creation(curr);
497 if ( pthread_map.size() < pthread_counter )
498 pthread_map.resize( pthread_counter );
499 pthread_map[ pthread_counter-1 ] = th;
504 Thread *blocking = curr->get_thread_operand();
505 ModelAction *act = get_last_action(blocking->get_id());
506 synchronize(act, curr);
507 updated = true; /* trigger rel-seq checks */
511 Thread *blocking = curr->get_thread_operand();
512 ModelAction *act = get_last_action(blocking->get_id());
513 synchronize(act, curr);
514 updated = true; /* trigger rel-seq checks */
515 break; // WL: to be add (modified)
518 case THREAD_FINISH: {
519 Thread *th = get_thread(curr);
520 /* Wake up any joining threads */
521 for (unsigned int i = 0;i < get_num_threads();i++) {
522 Thread *waiting = get_thread(int_to_id(i));
523 if (waiting->waiting_on() == th &&
524 waiting->get_pending()->is_thread_join())
525 scheduler->wake(waiting);
528 updated = true; /* trigger rel-seq checks */
542 * Initialize the current action by performing one or more of the following
543 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
544 * in the NodeStack, manipulating backtracking sets, allocating and
545 * initializing clock vectors, and computing the promises to fulfill.
547 * @param curr The current action, as passed from the user context; may be
548 * freed/invalidated after the execution of this function, with a different
549 * action "returned" its place (pass-by-reference)
550 * @return True if curr is a newly-explored action; false otherwise
552 bool ModelExecution::initialize_curr_action(ModelAction **curr)
554 ModelAction *newcurr;
556 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
557 newcurr = process_rmw(*curr);
564 (*curr)->set_seq_number(get_next_seq_num());
566 newcurr = node_stack->explore_action(*curr);
568 /* First restore type and order in case of RMW operation */
569 if ((*curr)->is_rmwr())
570 newcurr->copy_typeandorder(*curr);
572 ASSERT((*curr)->get_location() == newcurr->get_location());
573 newcurr->copy_from_new(*curr);
575 /* Discard duplicate ModelAction; use action from NodeStack */
578 /* Always compute new clock vector */
579 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
582 return false; /* Action was explored previously */
586 /* Always compute new clock vector */
587 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
589 /* Assign most recent release fence */
590 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
592 return true; /* This was a new ModelAction */
597 * @brief Establish reads-from relation between two actions
599 * Perform basic operations involved with establishing a concrete rf relation,
600 * including setting the ModelAction data and checking for release sequences.
602 * @param act The action that is reading (must be a read)
603 * @param rf The action from which we are reading (must be a write)
605 * @return True if this read established synchronization
608 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
611 ASSERT(rf->is_write());
613 act->set_read_from(rf);
614 if (act->is_acquire()) {
615 rel_heads_list_t release_heads;
616 get_release_seq_heads(act, act, &release_heads);
617 int num_heads = release_heads.size();
618 for (unsigned int i = 0;i < release_heads.size();i++)
619 if (!synchronize(release_heads[i], act))
621 return num_heads > 0;
627 * @brief Synchronizes two actions
629 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
630 * This function performs the synchronization as well as providing other hooks
631 * for other checks along with synchronization.
633 * @param first The left-hand side of the synchronizes-with relation
634 * @param second The right-hand side of the synchronizes-with relation
635 * @return True if the synchronization was successful (i.e., was consistent
636 * with the execution order); false otherwise
638 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
640 if (*second < *first) {
641 set_bad_synchronization();
644 return second->synchronize_with(first);
648 * @brief Check whether a model action is enabled.
650 * Checks whether an operation would be successful (i.e., is a lock already
651 * locked, or is the joined thread already complete).
653 * For yield-blocking, yields are never enabled.
655 * @param curr is the ModelAction to check whether it is enabled.
656 * @return a bool that indicates whether the action is enabled.
658 bool ModelExecution::check_action_enabled(ModelAction *curr) {
659 if (curr->is_lock()) {
660 cdsc::mutex *lock = curr->get_mutex();
661 struct cdsc::mutex_state *state = lock->get_state();
664 } else if (curr->is_thread_join()) {
665 Thread *blocking = curr->get_thread_operand();
666 if (!blocking->is_complete()) {
675 * This is the heart of the model checker routine. It performs model-checking
676 * actions corresponding to a given "current action." Among other processes, it
677 * calculates reads-from relationships, updates synchronization clock vectors,
678 * forms a memory_order constraints graph, and handles replay/backtrack
679 * execution when running permutations of previously-observed executions.
681 * @param curr The current action to process
682 * @return The ModelAction that is actually executed; may be different than
685 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
688 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
689 bool newly_explored = initialize_curr_action(&curr);
693 wake_up_sleeping_actions(curr);
695 /* Add the action to lists before any other model-checking tasks */
696 if (!second_part_of_rmw)
697 add_action_to_lists(curr);
699 ModelVector<ModelAction *> * rf_set = NULL;
700 /* Build may_read_from set for newly-created actions */
701 if (newly_explored && curr->is_read())
702 rf_set = build_may_read_from(curr);
704 process_thread_action(curr);
706 if (curr->is_read() && !second_part_of_rmw) {
707 process_read(curr, rf_set);
710 ASSERT(rf_set == NULL);
713 if (curr->is_write())
716 if (curr->is_fence())
719 if (curr->is_mutex_op())
726 * This is the strongest feasibility check available.
727 * @return whether the current trace (partial or complete) must be a prefix of
730 bool ModelExecution::isfeasibleprefix() const
732 return !is_infeasible();
736 * Print disagnostic information about an infeasible execution
737 * @param prefix A string to prefix the output with; if NULL, then a default
738 * message prefix will be provided
740 void ModelExecution::print_infeasibility(const char *prefix) const
744 if (mo_graph->checkForCycles())
745 ptr += sprintf(ptr, "[mo cycle]");
746 if (priv->bad_synchronization)
747 ptr += sprintf(ptr, "[bad sw ordering]");
748 if (priv->bad_sc_read)
749 ptr += sprintf(ptr, "[bad sc read]");
751 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
755 * Check if the current partial trace is infeasible. Does not check any
756 * end-of-execution flags, which might rule out the execution. Thus, this is
757 * useful only for ruling an execution as infeasible.
758 * @return whether the current partial trace is infeasible.
760 bool ModelExecution::is_infeasible() const
762 return mo_graph->checkForCycles() ||
763 priv->bad_synchronization ||
767 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
768 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
769 ModelAction *lastread = get_last_action(act->get_tid());
770 lastread->process_rmw(act);
772 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
773 mo_graph->commitChanges();
779 * @brief Updates the mo_graph with the constraints imposed from the current
782 * Basic idea is the following: Go through each other thread and find
783 * the last action that happened before our read. Two cases:
785 * -# The action is a write: that write must either occur before
786 * the write we read from or be the write we read from.
787 * -# The action is a read: the write that that action read from
788 * must occur before the write we read from or be the same write.
790 * @param curr The current action. Must be a read.
791 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
792 * @return True if modification order edges were added; false otherwise
794 template <typename rf_type>
795 bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
797 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
800 ASSERT(curr->is_read());
802 /* Last SC fence in the current thread */
803 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
804 ModelAction *last_sc_write = NULL;
805 if (curr->is_seqcst())
806 last_sc_write = get_last_seq_cst_write(curr);
808 /* Iterate over all threads */
809 for (i = 0;i < thrd_lists->size();i++) {
810 /* Last SC fence in thread i */
811 ModelAction *last_sc_fence_thread_local = NULL;
812 if (int_to_id((int)i) != curr->get_tid())
813 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
815 /* Last SC fence in thread i, before last SC fence in current thread */
816 ModelAction *last_sc_fence_thread_before = NULL;
817 if (last_sc_fence_local)
818 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
820 /* Iterate over actions in thread, starting from most recent */
821 action_list_t *list = &(*thrd_lists)[i];
822 action_list_t::reverse_iterator rit;
823 for (rit = list->rbegin();rit != list->rend();rit++) {
824 ModelAction *act = *rit;
829 /* Don't want to add reflexive edges on 'rf' */
830 if (act->equals(rf)) {
831 if (act->happens_before(curr))
837 if (act->is_write()) {
838 /* C++, Section 29.3 statement 5 */
839 if (curr->is_seqcst() && last_sc_fence_thread_local &&
840 *act < *last_sc_fence_thread_local) {
841 added = mo_graph->addEdge(act, rf) || added;
844 /* C++, Section 29.3 statement 4 */
845 else if (act->is_seqcst() && last_sc_fence_local &&
846 *act < *last_sc_fence_local) {
847 added = mo_graph->addEdge(act, rf) || added;
850 /* C++, Section 29.3 statement 6 */
851 else if (last_sc_fence_thread_before &&
852 *act < *last_sc_fence_thread_before) {
853 added = mo_graph->addEdge(act, rf) || added;
859 * Include at most one act per-thread that "happens
862 if (act->happens_before(curr)) {
863 if (act->is_write()) {
864 added = mo_graph->addEdge(act, rf) || added;
866 const ModelAction *prevrf = act->get_reads_from();
867 if (!prevrf->equals(rf))
868 added = mo_graph->addEdge(prevrf, rf) || added;
879 * Updates the mo_graph with the constraints imposed from the current write.
881 * Basic idea is the following: Go through each other thread and find
882 * the lastest action that happened before our write. Two cases:
884 * (1) The action is a write => that write must occur before
887 * (2) The action is a read => the write that that action read from
888 * must occur before the current write.
890 * This method also handles two other issues:
892 * (I) Sequential Consistency: Making sure that if the current write is
893 * seq_cst, that it occurs after the previous seq_cst write.
895 * (II) Sending the write back to non-synchronizing reads.
897 * @param curr The current action. Must be a write.
898 * @param send_fv A vector for stashing reads to which we may pass our future
899 * value. If NULL, then don't record any future values.
900 * @return True if modification order edges were added; false otherwise
902 bool ModelExecution::w_modification_order(ModelAction *curr)
904 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
907 ASSERT(curr->is_write());
909 if (curr->is_seqcst()) {
910 /* We have to at least see the last sequentially consistent write,
911 so we are initialized. */
912 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
913 if (last_seq_cst != NULL) {
914 added = mo_graph->addEdge(last_seq_cst, curr) || added;
918 /* Last SC fence in the current thread */
919 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
921 /* Iterate over all threads */
922 for (i = 0;i < thrd_lists->size();i++) {
923 /* Last SC fence in thread i, before last SC fence in current thread */
924 ModelAction *last_sc_fence_thread_before = NULL;
925 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
926 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
928 /* Iterate over actions in thread, starting from most recent */
929 action_list_t *list = &(*thrd_lists)[i];
930 action_list_t::reverse_iterator rit;
931 for (rit = list->rbegin();rit != list->rend();rit++) {
932 ModelAction *act = *rit;
935 * 1) If RMW and it actually read from something, then we
936 * already have all relevant edges, so just skip to next
939 * 2) If RMW and it didn't read from anything, we should
940 * whatever edge we can get to speed up convergence.
942 * 3) If normal write, we need to look at earlier actions, so
943 * continue processing list.
945 if (curr->is_rmw()) {
946 if (curr->get_reads_from() != NULL)
954 /* C++, Section 29.3 statement 7 */
955 if (last_sc_fence_thread_before && act->is_write() &&
956 *act < *last_sc_fence_thread_before) {
957 added = mo_graph->addEdge(act, curr) || added;
962 * Include at most one act per-thread that "happens
965 if (act->happens_before(curr)) {
967 * Note: if act is RMW, just add edge:
969 * The following edge should be handled elsewhere:
970 * readfrom(act) --mo--> act
973 added = mo_graph->addEdge(act, curr) || added;
974 else if (act->is_read()) {
975 //if previous read accessed a null, just keep going
976 added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
979 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
980 !act->same_thread(curr)) {
981 /* We have an action that:
982 (1) did not happen before us
983 (2) is a read and we are a write
984 (3) cannot synchronize with us
985 (4) is in a different thread
987 that read could potentially read from our write. Note that
988 these checks are overly conservative at this point, we'll
989 do more checks before actually removing the
1002 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1003 * some constraints. This method checks one the following constraint (others
1004 * require compiler support):
1006 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1007 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1009 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1011 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1013 /* Iterate over all threads */
1014 for (i = 0;i < thrd_lists->size();i++) {
1015 const ModelAction *write_after_read = NULL;
1017 /* Iterate over actions in thread, starting from most recent */
1018 action_list_t *list = &(*thrd_lists)[i];
1019 action_list_t::reverse_iterator rit;
1020 for (rit = list->rbegin();rit != list->rend();rit++) {
1021 ModelAction *act = *rit;
1023 /* Don't disallow due to act == reader */
1024 if (!reader->happens_before(act) || reader == act)
1026 else if (act->is_write())
1027 write_after_read = act;
1028 else if (act->is_read() && act->get_reads_from() != NULL)
1029 write_after_read = act->get_reads_from();
1032 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1039 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1040 * The ModelAction under consideration is expected to be taking part in
1041 * release/acquire synchronization as an object of the "reads from" relation.
1042 * Note that this can only provide release sequence support for RMW chains
1043 * which do not read from the future, as those actions cannot be traced until
1044 * their "promise" is fulfilled. Similarly, we may not even establish the
1045 * presence of a release sequence with certainty, as some modification order
1046 * constraints may be decided further in the future. Thus, this function
1047 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1048 * and a boolean representing certainty.
1050 * @param rf The action that might be part of a release sequence. Must be a
1052 * @param release_heads A pass-by-reference style return parameter. After
1053 * execution of this function, release_heads will contain the heads of all the
1054 * relevant release sequences, if any exists with certainty
1055 * @return true, if the ModelExecution is certain that release_heads is complete;
1058 bool ModelExecution::release_seq_heads(const ModelAction *rf,
1059 rel_heads_list_t *release_heads) const
1061 /* Only check for release sequences if there are no cycles */
1062 if (mo_graph->checkForCycles())
1065 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1066 ASSERT(rf->is_write());
1068 if (rf->is_release())
1069 release_heads->push_back(rf);
1070 else if (rf->get_last_fence_release())
1071 release_heads->push_back(rf->get_last_fence_release());
1073 break;/* End of RMW chain */
1075 /** @todo Need to be smarter here... In the linux lock
1076 * example, this will run to the beginning of the program for
1078 /** @todo The way to be smarter here is to keep going until 1
1079 * thread has a release preceded by an acquire and you've seen
1082 /* acq_rel RMW is a sufficient stopping condition */
1083 if (rf->is_acquire() && rf->is_release())
1084 return true;/* complete */
1086 ASSERT(rf); // Needs to be real write
1088 if (rf->is_release())
1089 return true;/* complete */
1091 /* else relaxed write
1092 * - check for fence-release in the same thread (29.8, stmt. 3)
1093 * - check modification order for contiguous subsequence
1094 * -> rf must be same thread as release */
1096 const ModelAction *fence_release = rf->get_last_fence_release();
1097 /* Synchronize with a fence-release unconditionally; we don't need to
1098 * find any more "contiguous subsequence..." for it */
1100 release_heads->push_back(fence_release);
1102 return true; /* complete */
1106 * An interface for getting the release sequence head(s) with which a
1107 * given ModelAction must synchronize. This function only returns a non-empty
1108 * result when it can locate a release sequence head with certainty. Otherwise,
1109 * it may mark the internal state of the ModelExecution so that it will handle
1110 * the release sequence at a later time, causing @a acquire to update its
1111 * synchronization at some later point in execution.
1113 * @param acquire The 'acquire' action that may synchronize with a release
1115 * @param read The read action that may read from a release sequence; this may
1116 * be the same as acquire, or else an earlier action in the same thread (i.e.,
1117 * when 'acquire' is a fence-acquire)
1118 * @param release_heads A pass-by-reference return parameter. Will be filled
1119 * with the head(s) of the release sequence(s), if they exists with certainty.
1120 * @see ModelExecution::release_seq_heads
1122 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
1123 ModelAction *read, rel_heads_list_t *release_heads)
1125 const ModelAction *rf = read->get_reads_from();
1127 release_seq_heads(rf, release_heads);
1131 * Performs various bookkeeping operations for the current ModelAction. For
1132 * instance, adds action to the per-object, per-thread action vector and to the
1133 * action trace list of all thread actions.
1135 * @param act is the ModelAction to add.
1137 void ModelExecution::add_action_to_lists(ModelAction *act)
1139 int tid = id_to_int(act->get_tid());
1140 ModelAction *uninit = NULL;
1142 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1143 if (list->empty() && act->is_atomic_var()) {
1144 uninit = get_uninitialized_action(act);
1145 uninit_id = id_to_int(uninit->get_tid());
1146 list->push_front(uninit);
1148 list->push_back(act);
1150 action_trace.push_back(act);
1152 action_trace.push_front(uninit);
1154 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1155 if (tid >= (int)vec->size())
1156 vec->resize(priv->next_thread_id);
1157 (*vec)[tid].push_back(act);
1159 (*vec)[uninit_id].push_front(uninit);
1161 if ((int)thrd_last_action.size() <= tid)
1162 thrd_last_action.resize(get_num_threads());
1163 thrd_last_action[tid] = act;
1165 thrd_last_action[uninit_id] = uninit;
1167 if (act->is_fence() && act->is_release()) {
1168 if ((int)thrd_last_fence_release.size() <= tid)
1169 thrd_last_fence_release.resize(get_num_threads());
1170 thrd_last_fence_release[tid] = act;
1173 if (act->is_wait()) {
1174 void *mutex_loc = (void *) act->get_value();
1175 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1177 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1178 if (tid >= (int)vec->size())
1179 vec->resize(priv->next_thread_id);
1180 (*vec)[tid].push_back(act);
1185 * @brief Get the last action performed by a particular Thread
1186 * @param tid The thread ID of the Thread in question
1187 * @return The last action in the thread
1189 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1191 int threadid = id_to_int(tid);
1192 if (threadid < (int)thrd_last_action.size())
1193 return thrd_last_action[id_to_int(tid)];
1199 * @brief Get the last fence release performed by a particular Thread
1200 * @param tid The thread ID of the Thread in question
1201 * @return The last fence release in the thread, if one exists; NULL otherwise
1203 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1205 int threadid = id_to_int(tid);
1206 if (threadid < (int)thrd_last_fence_release.size())
1207 return thrd_last_fence_release[id_to_int(tid)];
1213 * Gets the last memory_order_seq_cst write (in the total global sequence)
1214 * performed on a particular object (i.e., memory location), not including the
1216 * @param curr The current ModelAction; also denotes the object location to
1218 * @return The last seq_cst write
1220 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1222 void *location = curr->get_location();
1223 action_list_t *list = obj_map.get(location);
1224 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1225 action_list_t::reverse_iterator rit;
1226 for (rit = list->rbegin();(*rit) != curr;rit++)
1228 rit++; /* Skip past curr */
1229 for ( ;rit != list->rend();rit++)
1230 if ((*rit)->is_write() && (*rit)->is_seqcst())
1236 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1237 * performed in a particular thread, prior to a particular fence.
1238 * @param tid The ID of the thread to check
1239 * @param before_fence The fence from which to begin the search; if NULL, then
1240 * search for the most recent fence in the thread.
1241 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1243 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1245 /* All fences should have location FENCE_LOCATION */
1246 action_list_t *list = obj_map.get(FENCE_LOCATION);
1251 action_list_t::reverse_iterator rit = list->rbegin();
1254 for (;rit != list->rend();rit++)
1255 if (*rit == before_fence)
1258 ASSERT(*rit == before_fence);
1262 for (;rit != list->rend();rit++)
1263 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1269 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1270 * location). This function identifies the mutex according to the current
1271 * action, which is presumed to perform on the same mutex.
1272 * @param curr The current ModelAction; also denotes the object location to
1274 * @return The last unlock operation
1276 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1278 void *location = curr->get_location();
1280 action_list_t *list = obj_map.get(location);
1281 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1282 action_list_t::reverse_iterator rit;
1283 for (rit = list->rbegin();rit != list->rend();rit++)
1284 if ((*rit)->is_unlock() || (*rit)->is_wait())
1289 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1291 ModelAction *parent = get_last_action(tid);
1293 parent = get_thread(tid)->get_creation();
1298 * Returns the clock vector for a given thread.
1299 * @param tid The thread whose clock vector we want
1300 * @return Desired clock vector
1302 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1304 return get_parent_action(tid)->get_cv();
1307 bool valequals(uint64_t val1, uint64_t val2, int size) {
1310 return ((uint8_t)val1) == ((uint8_t)val2);
1312 return ((uint16_t)val1) == ((uint16_t)val2);
1314 return ((uint32_t)val1) == ((uint32_t)val2);
1324 * Build up an initial set of all past writes that this 'read' action may read
1325 * from, as well as any previously-observed future values that must still be valid.
1327 * @param curr is the current ModelAction that we are exploring; it must be a
1330 ModelVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1332 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1334 ASSERT(curr->is_read());
1336 ModelAction *last_sc_write = NULL;
1338 if (curr->is_seqcst())
1339 last_sc_write = get_last_seq_cst_write(curr);
1341 ModelVector<ModelAction *> * rf_set = new ModelVector<ModelAction *>();
1343 /* Iterate over all threads */
1344 for (i = 0;i < thrd_lists->size();i++) {
1345 /* Iterate over actions in thread, starting from most recent */
1346 action_list_t *list = &(*thrd_lists)[i];
1347 action_list_t::reverse_iterator rit;
1348 for (rit = list->rbegin();rit != list->rend();rit++) {
1349 ModelAction *act = *rit;
1351 /* Only consider 'write' actions */
1352 if (!act->is_write() || act == curr)
1355 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1356 bool allow_read = true;
1358 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1361 /* Need to check whether we will have two RMW reading from the same value */
1362 if (curr->is_rmwr()) {
1363 /* It is okay if we have a failing CAS */
1364 if (!curr->is_rmwrcas() ||
1365 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1366 //Need to make sure we aren't the second RMW
1367 CycleNode * node = mo_graph->getNode_noCreate(act);
1368 if (node != NULL && node->getRMW() != NULL) {
1369 //we are the second RMW
1376 /* Only add feasible reads */
1377 mo_graph->startChanges();
1378 r_modification_order(curr, act);
1379 if (!is_infeasible())
1380 rf_set->push_back(act);
1381 mo_graph->rollbackChanges();
1384 /* Include at most one act per-thread that "happens before" curr */
1385 if (act->happens_before(curr))
1390 if (DBG_ENABLED()) {
1391 model_print("Reached read action:\n");
1393 model_print("End printing read_from_past\n");
1399 * @brief Get an action representing an uninitialized atomic
1401 * This function may create a new one or try to retrieve one from the NodeStack
1403 * @param curr The current action, which prompts the creation of an UNINIT action
1404 * @return A pointer to the UNINIT ModelAction
1406 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1408 Node *node = curr->get_node();
1409 ModelAction *act = node->get_uninit_action();
1411 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1412 node->set_uninit_action(act);
1414 act->create_cv(NULL);
1418 static void print_list(const action_list_t *list)
1420 action_list_t::const_iterator it;
1422 model_print("------------------------------------------------------------------------------------\n");
1423 model_print("# t Action type MO Location Value Rf CV\n");
1424 model_print("------------------------------------------------------------------------------------\n");
1426 unsigned int hash = 0;
1428 for (it = list->begin();it != list->end();it++) {
1429 const ModelAction *act = *it;
1430 if (act->get_seq_number() > 0)
1432 hash = hash^(hash<<3)^((*it)->hash());
1434 model_print("HASH %u\n", hash);
1435 model_print("------------------------------------------------------------------------------------\n");
1438 #if SUPPORT_MOD_ORDER_DUMP
1439 void ModelExecution::dumpGraph(char *filename) const
1442 sprintf(buffer, "%s.dot", filename);
1443 FILE *file = fopen(buffer, "w");
1444 fprintf(file, "digraph %s {\n", filename);
1445 mo_graph->dumpNodes(file);
1446 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1448 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1449 ModelAction *act = *it;
1450 if (act->is_read()) {
1451 mo_graph->dot_print_node(file, act);
1452 mo_graph->dot_print_edge(file,
1453 act->get_reads_from(),
1455 "label=\"rf\", color=red, weight=2");
1457 if (thread_array[act->get_tid()]) {
1458 mo_graph->dot_print_edge(file,
1459 thread_array[id_to_int(act->get_tid())],
1461 "label=\"sb\", color=blue, weight=400");
1464 thread_array[act->get_tid()] = act;
1466 fprintf(file, "}\n");
1467 model_free(thread_array);
1472 /** @brief Prints an execution trace summary. */
1473 void ModelExecution::print_summary() const
1475 #if SUPPORT_MOD_ORDER_DUMP
1476 char buffername[100];
1477 sprintf(buffername, "exec%04u", get_execution_number());
1478 mo_graph->dumpGraphToFile(buffername);
1479 sprintf(buffername, "graph%04u", get_execution_number());
1480 dumpGraph(buffername);
1483 model_print("Execution trace %d:", get_execution_number());
1484 if (isfeasibleprefix()) {
1485 if (scheduler->all_threads_sleeping())
1486 model_print(" SLEEP-SET REDUNDANT");
1487 if (have_bug_reports())
1488 model_print(" DETECTED BUG(S)");
1490 print_infeasibility(" INFEASIBLE");
1493 print_list(&action_trace);
1499 * Add a Thread to the system for the first time. Should only be called once
1501 * @param t The Thread to add
1503 void ModelExecution::add_thread(Thread *t)
1505 unsigned int i = id_to_int(t->get_id());
1506 if (i >= thread_map.size())
1507 thread_map.resize(i + 1);
1509 if (!t->is_model_thread())
1510 scheduler->add_thread(t);
1514 * @brief Get a Thread reference by its ID
1515 * @param tid The Thread's ID
1516 * @return A Thread reference
1518 Thread * ModelExecution::get_thread(thread_id_t tid) const
1520 unsigned int i = id_to_int(tid);
1521 if (i < thread_map.size())
1522 return thread_map[i];
1527 * @brief Get a reference to the Thread in which a ModelAction was executed
1528 * @param act The ModelAction
1529 * @return A Thread reference
1531 Thread * ModelExecution::get_thread(const ModelAction *act) const
1533 return get_thread(act->get_tid());
1537 * @brief Get a Thread reference by its pthread ID
1538 * @param index The pthread's ID
1539 * @return A Thread reference
1541 Thread * ModelExecution::get_pthread(pthread_t pid) {
1547 uint32_t thread_id = x.v;
1548 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1553 * @brief Check if a Thread is currently enabled
1554 * @param t The Thread to check
1555 * @return True if the Thread is currently enabled
1557 bool ModelExecution::is_enabled(Thread *t) const
1559 return scheduler->is_enabled(t);
1563 * @brief Check if a Thread is currently enabled
1564 * @param tid The ID of the Thread to check
1565 * @return True if the Thread is currently enabled
1567 bool ModelExecution::is_enabled(thread_id_t tid) const
1569 return scheduler->is_enabled(tid);
1573 * @brief Select the next thread to execute based on the curren action
1575 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1576 * actions should be followed by the execution of their child thread. In either
1577 * case, the current action should determine the next thread schedule.
1579 * @param curr The current action
1580 * @return The next thread to run, if the current action will determine this
1581 * selection; otherwise NULL
1583 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1585 /* Do not split atomic RMW */
1586 if (curr->is_rmwr())
1587 return get_thread(curr);
1588 if (curr->is_write()) {
1589 std::memory_order order = curr->get_mo();
1591 case std::memory_order_relaxed:
1592 return get_thread(curr);
1593 case std::memory_order_release:
1594 return get_thread(curr);
1600 /* Follow CREATE with the created thread */
1601 /* which is not needed, because model.cc takes care of this */
1602 if (curr->get_type() == THREAD_CREATE)
1603 return curr->get_thread_operand();
1604 if (curr->get_type() == PTHREAD_CREATE) {
1605 return curr->get_thread_operand();
1611 * Takes the next step in the execution, if possible.
1612 * @param curr The current step to take
1613 * @return Returns the next Thread to run, if any; NULL if this execution
1616 Thread * ModelExecution::take_step(ModelAction *curr)
1618 Thread *curr_thrd = get_thread(curr);
1619 ASSERT(curr_thrd->get_state() == THREAD_READY);
1621 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1622 curr = check_current_action(curr);
1625 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1626 scheduler->remove_thread(curr_thrd);
1628 return action_select_next_thread(curr);
1631 Fuzzer * ModelExecution::getFuzzer() {