12 #include "clockvector.h"
13 #include "cyclegraph.h"
15 #include "threads-model.h"
16 #include "bugmessage.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
31 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;
51 /** @brief Constructor */
52 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) :
57 thread_map(2), /* We'll always need at least 2 threads */
61 condvar_waiters_map(),
65 thrd_last_fence_release(),
66 node_stack(node_stack),
67 priv(new struct model_snapshot_members ()),
68 mo_graph(new CycleGraph()),
71 thrd_func_inst_lists()
73 /* Initialize a model-checker thread, for special ModelActions */
74 model_thread = new Thread(get_next_id());
75 add_thread(model_thread);
76 scheduler->register_engine(this);
77 node_stack->register_engine(this);
80 /** @brief Destructor */
81 ModelExecution::~ModelExecution()
83 for (unsigned int i = 0;i < get_num_threads();i++)
84 delete get_thread(int_to_id(i));
90 int ModelExecution::get_execution_number() const
92 return model->get_execution_number();
95 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
97 action_list_t *tmp = hash->get(ptr);
99 tmp = new action_list_t();
105 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
107 SnapVector<action_list_t> *tmp = hash->get(ptr);
109 tmp = new SnapVector<action_list_t>();
115 /** @return a thread ID for a new Thread */
116 thread_id_t ModelExecution::get_next_id()
118 return priv->next_thread_id++;
121 /** @return the number of user threads created during this execution */
122 unsigned int ModelExecution::get_num_threads() const
124 return priv->next_thread_id;
127 /** @return a sequence number for a new ModelAction */
128 modelclock_t ModelExecution::get_next_seq_num()
130 return ++priv->used_sequence_numbers;
134 * @brief Should the current action wake up a given thread?
136 * @param curr The current action
137 * @param thread The thread that we might wake up
138 * @return True, if we should wake up the sleeping thread; false otherwise
140 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
142 const ModelAction *asleep = thread->get_pending();
143 /* Don't allow partial RMW to wake anyone up */
146 /* Synchronizing actions may have been backtracked */
147 if (asleep->could_synchronize_with(curr))
149 /* All acquire/release fences and fence-acquire/store-release */
150 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
152 /* Fence-release + store can awake load-acquire on the same location */
153 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
154 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
155 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
161 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
163 for (unsigned int i = 0;i < get_num_threads();i++) {
164 Thread *thr = get_thread(int_to_id(i));
165 if (scheduler->is_sleep_set(thr)) {
166 if (should_wake_up(curr, thr))
167 /* Remove this thread from sleep set */
168 scheduler->remove_sleep(thr);
173 /** @brief Alert the model-checker that an incorrectly-ordered
174 * synchronization was made */
175 void ModelExecution::set_bad_synchronization()
177 priv->bad_synchronization = true;
180 bool ModelExecution::assert_bug(const char *msg)
182 priv->bugs.push_back(new bug_message(msg));
184 if (isfeasibleprefix()) {
191 /** @return True, if any bugs have been reported for this execution */
192 bool ModelExecution::have_bug_reports() const
194 return priv->bugs.size() != 0;
197 SnapVector<bug_message *> * ModelExecution::get_bugs() const
203 * Check whether the current trace has triggered an assertion which should halt
206 * @return True, if the execution should be aborted; false otherwise
208 bool ModelExecution::has_asserted() const
210 return priv->asserted;
214 * Trigger a trace assertion which should cause this execution to be halted.
215 * This can be due to a detected bug or due to an infeasibility that should
218 void ModelExecution::set_assert()
220 priv->asserted = true;
224 * Check if we are in a deadlock. Should only be called at the end of an
225 * execution, although it should not give false positives in the middle of an
226 * execution (there should be some ENABLED thread).
228 * @return True if program is in a deadlock; false otherwise
230 bool ModelExecution::is_deadlocked() const
232 bool blocking_threads = false;
233 for (unsigned int i = 0;i < get_num_threads();i++) {
234 thread_id_t tid = int_to_id(i);
237 Thread *t = get_thread(tid);
238 if (!t->is_model_thread() && t->get_pending())
239 blocking_threads = true;
241 return blocking_threads;
245 * Check if this is a complete execution. That is, have all thread completed
246 * execution (rather than exiting because sleep sets have forced a redundant
249 * @return True if the execution is complete.
251 bool ModelExecution::is_complete_execution() const
253 for (unsigned int i = 0;i < get_num_threads();i++)
254 if (is_enabled(int_to_id(i)))
261 * Processes a read model action.
262 * @param curr is the read model action to process.
263 * @param rf_set is the set of model actions we can possibly read from
264 * @return True if processing this read updates the mo_graph.
266 void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set)
268 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
271 int index = fuzzer->selectWrite(curr, rf_set);
272 const ModelAction *rf = (*rf_set)[index];
276 bool canprune = false;
277 if (r_modification_order(curr, rf, priorset, &canprune)) {
278 for(unsigned int i=0;i<priorset->size();i++) {
279 mo_graph->addEdge((*priorset)[i], rf);
282 get_thread(curr)->set_return_value(curr->get_return_value());
284 if (canprune && curr->get_type() == ATOMIC_READ) {
285 int tid = id_to_int(curr->get_tid());
286 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
291 (*rf_set)[index] = rf_set->back();
297 * Processes a lock, trylock, or unlock model action. @param curr is
298 * the read model action to process.
300 * The try lock operation checks whether the lock is taken. If not,
301 * it falls to the normal lock operation case. If so, it returns
304 * The lock operation has already been checked that it is enabled, so
305 * it just grabs the lock and synchronizes with the previous unlock.
307 * The unlock operation has to re-enable all of the threads that are
308 * waiting on the lock.
310 * @return True if synchronization was updated; false otherwise
312 bool ModelExecution::process_mutex(ModelAction *curr)
314 cdsc::mutex *mutex = curr->get_mutex();
315 struct cdsc::mutex_state *state = NULL;
318 state = mutex->get_state();
320 switch (curr->get_type()) {
321 case ATOMIC_TRYLOCK: {
322 bool success = !state->locked;
323 curr->set_try_lock(success);
325 get_thread(curr)->set_return_value(0);
328 get_thread(curr)->set_return_value(1);
330 //otherwise fall into the lock case
332 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
333 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
334 // assert_bug("Lock access before initialization");
335 state->locked = get_thread(curr);
336 ModelAction *unlock = get_last_unlock(curr);
337 //synchronize with the previous unlock statement
338 if (unlock != NULL) {
339 synchronize(unlock, curr);
345 case ATOMIC_UNLOCK: {
346 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
348 /* wake up the other threads */
349 for (unsigned int i = 0;i < get_num_threads();i++) {
350 Thread *t = get_thread(int_to_id(i));
351 Thread *curr_thrd = get_thread(curr);
352 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
356 /* unlock the lock - after checking who was waiting on it */
357 state->locked = NULL;
359 if (!curr->is_wait())
360 break;/* The rest is only for ATOMIC_WAIT */
364 case ATOMIC_NOTIFY_ALL: {
365 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
366 //activate all the waiting threads
367 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
368 scheduler->wake(get_thread(*rit));
373 case ATOMIC_NOTIFY_ONE: {
374 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
375 if (waiters->size() != 0) {
376 Thread * thread = fuzzer->selectNotify(waiters);
377 scheduler->wake(thread);
389 * Process a write ModelAction
390 * @param curr The ModelAction to process
391 * @return True if the mo_graph was updated or promises were resolved
393 void ModelExecution::process_write(ModelAction *curr)
395 w_modification_order(curr);
396 get_thread(curr)->set_return_value(VALUE_NONE);
400 * Process a fence ModelAction
401 * @param curr The ModelAction to process
402 * @return True if synchronization was updated
404 bool ModelExecution::process_fence(ModelAction *curr)
407 * fence-relaxed: no-op
408 * fence-release: only log the occurence (not in this function), for
409 * use in later synchronization
410 * fence-acquire (this function): search for hypothetical release
412 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
414 bool updated = false;
415 if (curr->is_acquire()) {
416 action_list_t *list = &action_trace;
417 action_list_t::reverse_iterator rit;
418 /* Find X : is_read(X) && X --sb-> curr */
419 for (rit = list->rbegin();rit != list->rend();rit++) {
420 ModelAction *act = *rit;
423 if (act->get_tid() != curr->get_tid())
425 /* Stop at the beginning of the thread */
426 if (act->is_thread_start())
428 /* Stop once we reach a prior fence-acquire */
429 if (act->is_fence() && act->is_acquire())
433 /* read-acquire will find its own release sequences */
434 if (act->is_acquire())
437 /* Establish hypothetical release sequences */
438 rel_heads_list_t release_heads;
439 get_release_seq_heads(curr, act, &release_heads);
440 for (unsigned int i = 0;i < release_heads.size();i++)
441 synchronize(release_heads[i], curr);
442 if (release_heads.size() != 0)
450 * @brief Process the current action for thread-related activity
452 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
453 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
454 * synchronization, etc. This function is a no-op for non-THREAD actions
455 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
457 * @param curr The current action
458 * @return True if synchronization was updated or a thread completed
460 bool ModelExecution::process_thread_action(ModelAction *curr)
462 bool updated = false;
464 switch (curr->get_type()) {
465 case THREAD_CREATE: {
466 thrd_t *thrd = (thrd_t *)curr->get_location();
467 struct thread_params *params = (struct thread_params *)curr->get_value();
468 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
469 curr->set_thread_operand(th);
471 th->set_creation(curr);
474 case PTHREAD_CREATE: {
475 (*(uint32_t *)curr->get_location()) = pthread_counter++;
477 struct pthread_params *params = (struct pthread_params *)curr->get_value();
478 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
479 curr->set_thread_operand(th);
481 th->set_creation(curr);
483 if ( pthread_map.size() < pthread_counter )
484 pthread_map.resize( pthread_counter );
485 pthread_map[ pthread_counter-1 ] = th;
490 Thread *blocking = curr->get_thread_operand();
491 ModelAction *act = get_last_action(blocking->get_id());
492 synchronize(act, curr);
493 updated = true; /* trigger rel-seq checks */
497 Thread *blocking = curr->get_thread_operand();
498 ModelAction *act = get_last_action(blocking->get_id());
499 synchronize(act, curr);
500 updated = true; /* trigger rel-seq checks */
501 break; // WL: to be add (modified)
504 case THREAD_FINISH: {
505 Thread *th = get_thread(curr);
506 /* Wake up any joining threads */
507 for (unsigned int i = 0;i < get_num_threads();i++) {
508 Thread *waiting = get_thread(int_to_id(i));
509 if (waiting->waiting_on() == th &&
510 waiting->get_pending()->is_thread_join())
511 scheduler->wake(waiting);
514 updated = true; /* trigger rel-seq checks */
528 * Initialize the current action by performing one or more of the following
529 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
530 * in the NodeStack, manipulating backtracking sets, allocating and
531 * initializing clock vectors, and computing the promises to fulfill.
533 * @param curr The current action, as passed from the user context; may be
534 * freed/invalidated after the execution of this function, with a different
535 * action "returned" its place (pass-by-reference)
536 * @return True if curr is a newly-explored action; false otherwise
538 bool ModelExecution::initialize_curr_action(ModelAction **curr)
540 ModelAction *newcurr;
542 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
543 newcurr = process_rmw(*curr);
550 (*curr)->set_seq_number(get_next_seq_num());
552 newcurr = node_stack->explore_action(*curr);
554 /* First restore type and order in case of RMW operation */
555 if ((*curr)->is_rmwr())
556 newcurr->copy_typeandorder(*curr);
558 ASSERT((*curr)->get_location() == newcurr->get_location());
559 newcurr->copy_from_new(*curr);
561 /* Discard duplicate ModelAction; use action from NodeStack */
564 /* Always compute new clock vector */
565 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
568 return false; /* Action was explored previously */
572 /* Always compute new clock vector */
573 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
575 /* Assign most recent release fence */
576 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
578 return true; /* This was a new ModelAction */
583 * @brief Establish reads-from relation between two actions
585 * Perform basic operations involved with establishing a concrete rf relation,
586 * including setting the ModelAction data and checking for release sequences.
588 * @param act The action that is reading (must be a read)
589 * @param rf The action from which we are reading (must be a write)
591 * @return True if this read established synchronization
594 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
597 ASSERT(rf->is_write());
599 act->set_read_from(rf);
600 if (act->is_acquire()) {
601 rel_heads_list_t release_heads;
602 get_release_seq_heads(act, act, &release_heads);
603 int num_heads = release_heads.size();
604 for (unsigned int i = 0;i < release_heads.size();i++)
605 if (!synchronize(release_heads[i], act))
607 return num_heads > 0;
613 * @brief Synchronizes two actions
615 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
616 * This function performs the synchronization as well as providing other hooks
617 * for other checks along with synchronization.
619 * @param first The left-hand side of the synchronizes-with relation
620 * @param second The right-hand side of the synchronizes-with relation
621 * @return True if the synchronization was successful (i.e., was consistent
622 * with the execution order); false otherwise
624 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
626 if (*second < *first) {
627 set_bad_synchronization();
630 return second->synchronize_with(first);
634 * @brief Check whether a model action is enabled.
636 * Checks whether an operation would be successful (i.e., is a lock already
637 * locked, or is the joined thread already complete).
639 * For yield-blocking, yields are never enabled.
641 * @param curr is the ModelAction to check whether it is enabled.
642 * @return a bool that indicates whether the action is enabled.
644 bool ModelExecution::check_action_enabled(ModelAction *curr) {
645 if (curr->is_lock()) {
646 cdsc::mutex *lock = curr->get_mutex();
647 struct cdsc::mutex_state *state = lock->get_state();
650 } else if (curr->is_thread_join()) {
651 Thread *blocking = curr->get_thread_operand();
652 if (!blocking->is_complete()) {
661 * This is the heart of the model checker routine. It performs model-checking
662 * actions corresponding to a given "current action." Among other processes, it
663 * calculates reads-from relationships, updates synchronization clock vectors,
664 * forms a memory_order constraints graph, and handles replay/backtrack
665 * execution when running permutations of previously-observed executions.
667 * @param curr The current action to process
668 * @return The ModelAction that is actually executed; may be different than
671 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
674 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
675 bool newly_explored = initialize_curr_action(&curr);
679 wake_up_sleeping_actions(curr);
681 /* Add the action to lists before any other model-checking tasks */
682 if (!second_part_of_rmw && curr->get_type() != NOOP)
683 add_action_to_lists(curr);
685 SnapVector<const ModelAction *> * rf_set = NULL;
686 /* Build may_read_from set for newly-created actions */
687 if (newly_explored && curr->is_read())
688 rf_set = build_may_read_from(curr);
690 process_thread_action(curr);
692 if (curr->is_read() && !second_part_of_rmw) {
693 process_read(curr, rf_set);
696 ASSERT(rf_set == NULL);
699 if (curr->is_write())
702 if (curr->is_fence())
705 if (curr->is_mutex_op())
712 * This is the strongest feasibility check available.
713 * @return whether the current trace (partial or complete) must be a prefix of
716 bool ModelExecution::isfeasibleprefix() const
718 return !is_infeasible();
722 * Print disagnostic information about an infeasible execution
723 * @param prefix A string to prefix the output with; if NULL, then a default
724 * message prefix will be provided
726 void ModelExecution::print_infeasibility(const char *prefix) const
730 if (priv->bad_synchronization)
731 ptr += sprintf(ptr, "[bad sw ordering]");
733 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
737 * Check if the current partial trace is infeasible. Does not check any
738 * end-of-execution flags, which might rule out the execution. Thus, this is
739 * useful only for ruling an execution as infeasible.
740 * @return whether the current partial trace is infeasible.
742 bool ModelExecution::is_infeasible() const
744 return priv->bad_synchronization;
747 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
748 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
749 ModelAction *lastread = get_last_action(act->get_tid());
750 lastread->process_rmw(act);
752 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
758 * @brief Updates the mo_graph with the constraints imposed from the current
761 * Basic idea is the following: Go through each other thread and find
762 * the last action that happened before our read. Two cases:
764 * -# The action is a write: that write must either occur before
765 * the write we read from or be the write we read from.
766 * -# The action is a read: the write that that action read from
767 * must occur before the write we read from or be the same write.
769 * @param curr The current action. Must be a read.
770 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
771 * @return True if modification order edges were added; false otherwise
774 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
776 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
778 ASSERT(curr->is_read());
780 /* Last SC fence in the current thread */
781 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
783 int tid = curr->get_tid();
784 ModelAction *prev_same_thread = NULL;
785 /* Iterate over all threads */
786 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
787 /* Last SC fence in thread tid */
788 ModelAction *last_sc_fence_thread_local = NULL;
790 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
792 /* Last SC fence in thread tid, before last SC fence in current thread */
793 ModelAction *last_sc_fence_thread_before = NULL;
794 if (last_sc_fence_local)
795 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
797 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
798 if (prev_same_thread != NULL &&
799 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
800 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
804 /* Iterate over actions in thread, starting from most recent */
805 action_list_t *list = &(*thrd_lists)[tid];
806 action_list_t::reverse_iterator rit;
807 for (rit = list->rbegin();rit != list->rend();rit++) {
808 ModelAction *act = *rit;
813 /* Don't want to add reflexive edges on 'rf' */
814 if (act->equals(rf)) {
815 if (act->happens_before(curr))
821 if (act->is_write()) {
822 /* C++, Section 29.3 statement 5 */
823 if (curr->is_seqcst() && last_sc_fence_thread_local &&
824 *act < *last_sc_fence_thread_local) {
825 if (mo_graph->checkReachable(rf, act))
827 priorset->push_back(act);
830 /* C++, Section 29.3 statement 4 */
831 else if (act->is_seqcst() && last_sc_fence_local &&
832 *act < *last_sc_fence_local) {
833 if (mo_graph->checkReachable(rf, act))
835 priorset->push_back(act);
838 /* C++, Section 29.3 statement 6 */
839 else if (last_sc_fence_thread_before &&
840 *act < *last_sc_fence_thread_before) {
841 if (mo_graph->checkReachable(rf, act))
843 priorset->push_back(act);
849 * Include at most one act per-thread that "happens
852 if (act->happens_before(curr)) {
854 if (last_sc_fence_local == NULL ||
855 (*last_sc_fence_local < *prev_same_thread)) {
856 prev_same_thread = act;
859 if (act->is_write()) {
860 if (mo_graph->checkReachable(rf, act))
862 priorset->push_back(act);
864 const ModelAction *prevrf = act->get_reads_from();
865 if (!prevrf->equals(rf)) {
866 if (mo_graph->checkReachable(rf, prevrf))
868 priorset->push_back(prevrf);
870 if (act->get_tid() == curr->get_tid()) {
871 //Can prune curr from obj list
884 * Updates the mo_graph with the constraints imposed from the current write.
886 * Basic idea is the following: Go through each other thread and find
887 * the lastest action that happened before our write. Two cases:
889 * (1) The action is a write => that write must occur before
892 * (2) The action is a read => the write that that action read from
893 * must occur before the current write.
895 * This method also handles two other issues:
897 * (I) Sequential Consistency: Making sure that if the current write is
898 * seq_cst, that it occurs after the previous seq_cst write.
900 * (II) Sending the write back to non-synchronizing reads.
902 * @param curr The current action. Must be a write.
903 * @param send_fv A vector for stashing reads to which we may pass our future
904 * value. If NULL, then don't record any future values.
905 * @return True if modification order edges were added; false otherwise
907 void ModelExecution::w_modification_order(ModelAction *curr)
909 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
911 ASSERT(curr->is_write());
913 if (curr->is_seqcst()) {
914 /* We have to at least see the last sequentially consistent write,
915 so we are initialized. */
916 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
917 if (last_seq_cst != NULL) {
918 mo_graph->addEdge(last_seq_cst, curr);
922 /* Last SC fence in the current thread */
923 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
925 /* Iterate over all threads */
926 for (i = 0;i < thrd_lists->size();i++) {
927 /* Last SC fence in thread i, before last SC fence in current thread */
928 ModelAction *last_sc_fence_thread_before = NULL;
929 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
930 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
932 /* Iterate over actions in thread, starting from most recent */
933 action_list_t *list = &(*thrd_lists)[i];
934 action_list_t::reverse_iterator rit;
935 bool force_edge = false;
936 for (rit = list->rbegin();rit != list->rend();rit++) {
937 ModelAction *act = *rit;
940 * 1) If RMW and it actually read from something, then we
941 * already have all relevant edges, so just skip to next
944 * 2) If RMW and it didn't read from anything, we should
945 * whatever edge we can get to speed up convergence.
947 * 3) If normal write, we need to look at earlier actions, so
948 * continue processing list.
951 if (curr->is_rmw()) {
952 if (curr->get_reads_from() != NULL)
960 /* C++, Section 29.3 statement 7 */
961 if (last_sc_fence_thread_before && act->is_write() &&
962 *act < *last_sc_fence_thread_before) {
963 mo_graph->addEdge(act, curr, force_edge);
968 * Include at most one act per-thread that "happens
971 if (act->happens_before(curr)) {
973 * Note: if act is RMW, just add edge:
975 * The following edge should be handled elsewhere:
976 * readfrom(act) --mo--> act
979 mo_graph->addEdge(act, curr, force_edge);
980 else if (act->is_read()) {
981 //if previous read accessed a null, just keep going
982 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
985 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
986 !act->same_thread(curr)) {
987 /* We have an action that:
988 (1) did not happen before us
989 (2) is a read and we are a write
990 (3) cannot synchronize with us
991 (4) is in a different thread
993 that read could potentially read from our write. Note that
994 these checks are overly conservative at this point, we'll
995 do more checks before actually removing the
1006 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1007 * some constraints. This method checks one the following constraint (others
1008 * require compiler support):
1010 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1011 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1013 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1015 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1017 /* Iterate over all threads */
1018 for (i = 0;i < thrd_lists->size();i++) {
1019 const ModelAction *write_after_read = NULL;
1021 /* Iterate over actions in thread, starting from most recent */
1022 action_list_t *list = &(*thrd_lists)[i];
1023 action_list_t::reverse_iterator rit;
1024 for (rit = list->rbegin();rit != list->rend();rit++) {
1025 ModelAction *act = *rit;
1027 /* Don't disallow due to act == reader */
1028 if (!reader->happens_before(act) || reader == act)
1030 else if (act->is_write())
1031 write_after_read = act;
1032 else if (act->is_read() && act->get_reads_from() != NULL)
1033 write_after_read = act->get_reads_from();
1036 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1043 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1044 * The ModelAction under consideration is expected to be taking part in
1045 * release/acquire synchronization as an object of the "reads from" relation.
1046 * Note that this can only provide release sequence support for RMW chains
1047 * which do not read from the future, as those actions cannot be traced until
1048 * their "promise" is fulfilled. Similarly, we may not even establish the
1049 * presence of a release sequence with certainty, as some modification order
1050 * constraints may be decided further in the future. Thus, this function
1051 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1052 * and a boolean representing certainty.
1054 * @param rf The action that might be part of a release sequence. Must be a
1056 * @param release_heads A pass-by-reference style return parameter. After
1057 * execution of this function, release_heads will contain the heads of all the
1058 * relevant release sequences, if any exists with certainty
1059 * @return true, if the ModelExecution is certain that release_heads is complete;
1062 bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
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 ModelAction *firstaction=get_parent_action(tid);
1305 return firstaction != NULL ? firstaction->get_cv() : NULL;
1308 bool valequals(uint64_t val1, uint64_t val2, int size) {
1311 return ((uint8_t)val1) == ((uint8_t)val2);
1313 return ((uint16_t)val1) == ((uint16_t)val2);
1315 return ((uint32_t)val1) == ((uint32_t)val2);
1325 * Build up an initial set of all past writes that this 'read' action may read
1326 * from, as well as any previously-observed future values that must still be valid.
1328 * @param curr is the current ModelAction that we are exploring; it must be a
1331 SnapVector<const ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1333 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1335 ASSERT(curr->is_read());
1337 ModelAction *last_sc_write = NULL;
1339 if (curr->is_seqcst())
1340 last_sc_write = get_last_seq_cst_write(curr);
1342 SnapVector<const ModelAction *> * rf_set = new SnapVector<const ModelAction *>();
1344 /* Iterate over all threads */
1345 for (i = 0;i < thrd_lists->size();i++) {
1346 /* Iterate over actions in thread, starting from most recent */
1347 action_list_t *list = &(*thrd_lists)[i];
1348 action_list_t::reverse_iterator rit;
1349 for (rit = list->rbegin();rit != list->rend();rit++) {
1350 const ModelAction *act = *rit;
1352 /* Only consider 'write' actions */
1353 if (!act->is_write()) {
1354 if (act != curr && act->is_read() && act->happens_before(curr)) {
1355 const ModelAction *tmp = act->get_reads_from();
1356 if (((unsigned int) id_to_int(tmp->get_tid()))==i)
1367 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1368 bool allow_read = true;
1370 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1373 /* Need to check whether we will have two RMW reading from the same value */
1374 if (curr->is_rmwr()) {
1375 /* It is okay if we have a failing CAS */
1376 if (!curr->is_rmwrcas() ||
1377 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1378 //Need to make sure we aren't the second RMW
1379 CycleNode * node = mo_graph->getNode_noCreate(act);
1380 if (node != NULL && node->getRMW() != NULL) {
1381 //we are the second RMW
1388 /* Only add feasible reads */
1389 rf_set->push_back(act);
1392 /* Include at most one act per-thread that "happens before" curr */
1393 if (act->happens_before(curr))
1398 if (DBG_ENABLED()) {
1399 model_print("Reached read action:\n");
1401 model_print("End printing read_from_past\n");
1407 * @brief Get an action representing an uninitialized atomic
1409 * This function may create a new one or try to retrieve one from the NodeStack
1411 * @param curr The current action, which prompts the creation of an UNINIT action
1412 * @return A pointer to the UNINIT ModelAction
1414 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1416 Node *node = curr->get_node();
1417 ModelAction *act = node->get_uninit_action();
1419 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1420 node->set_uninit_action(act);
1422 act->create_cv(NULL);
1426 static void print_list(const action_list_t *list)
1428 action_list_t::const_iterator it;
1430 model_print("------------------------------------------------------------------------------------\n");
1431 model_print("# t Action type MO Location Value Rf CV\n");
1432 model_print("------------------------------------------------------------------------------------\n");
1434 unsigned int hash = 0;
1436 for (it = list->begin();it != list->end();it++) {
1437 const ModelAction *act = *it;
1438 if (act->get_seq_number() > 0)
1440 hash = hash^(hash<<3)^((*it)->hash());
1442 model_print("HASH %u\n", hash);
1443 model_print("------------------------------------------------------------------------------------\n");
1446 #if SUPPORT_MOD_ORDER_DUMP
1447 void ModelExecution::dumpGraph(char *filename) const
1450 sprintf(buffer, "%s.dot", filename);
1451 FILE *file = fopen(buffer, "w");
1452 fprintf(file, "digraph %s {\n", filename);
1453 mo_graph->dumpNodes(file);
1454 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1456 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1457 ModelAction *act = *it;
1458 if (act->is_read()) {
1459 mo_graph->dot_print_node(file, act);
1460 mo_graph->dot_print_edge(file,
1461 act->get_reads_from(),
1463 "label=\"rf\", color=red, weight=2");
1465 if (thread_array[act->get_tid()]) {
1466 mo_graph->dot_print_edge(file,
1467 thread_array[id_to_int(act->get_tid())],
1469 "label=\"sb\", color=blue, weight=400");
1472 thread_array[act->get_tid()] = act;
1474 fprintf(file, "}\n");
1475 model_free(thread_array);
1480 /** @brief Prints an execution trace summary. */
1481 void ModelExecution::print_summary() const
1483 #if SUPPORT_MOD_ORDER_DUMP
1484 char buffername[100];
1485 sprintf(buffername, "exec%04u", get_execution_number());
1486 mo_graph->dumpGraphToFile(buffername);
1487 sprintf(buffername, "graph%04u", get_execution_number());
1488 dumpGraph(buffername);
1491 model_print("Execution trace %d:", get_execution_number());
1492 if (isfeasibleprefix()) {
1493 if (scheduler->all_threads_sleeping())
1494 model_print(" SLEEP-SET REDUNDANT");
1495 if (have_bug_reports())
1496 model_print(" DETECTED BUG(S)");
1498 print_infeasibility(" INFEASIBLE");
1501 print_list(&action_trace);
1507 * Add a Thread to the system for the first time. Should only be called once
1509 * @param t The Thread to add
1511 void ModelExecution::add_thread(Thread *t)
1513 unsigned int i = id_to_int(t->get_id());
1514 if (i >= thread_map.size())
1515 thread_map.resize(i + 1);
1517 if (!t->is_model_thread())
1518 scheduler->add_thread(t);
1522 * @brief Get a Thread reference by its ID
1523 * @param tid The Thread's ID
1524 * @return A Thread reference
1526 Thread * ModelExecution::get_thread(thread_id_t tid) const
1528 unsigned int i = id_to_int(tid);
1529 if (i < thread_map.size())
1530 return thread_map[i];
1535 * @brief Get a reference to the Thread in which a ModelAction was executed
1536 * @param act The ModelAction
1537 * @return A Thread reference
1539 Thread * ModelExecution::get_thread(const ModelAction *act) const
1541 return get_thread(act->get_tid());
1545 * @brief Get a Thread reference by its pthread ID
1546 * @param index The pthread's ID
1547 * @return A Thread reference
1549 Thread * ModelExecution::get_pthread(pthread_t pid) {
1555 uint32_t thread_id = x.v;
1556 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1561 * @brief Check if a Thread is currently enabled
1562 * @param t The Thread to check
1563 * @return True if the Thread is currently enabled
1565 bool ModelExecution::is_enabled(Thread *t) const
1567 return scheduler->is_enabled(t);
1571 * @brief Check if a Thread is currently enabled
1572 * @param tid The ID of the Thread to check
1573 * @return True if the Thread is currently enabled
1575 bool ModelExecution::is_enabled(thread_id_t tid) const
1577 return scheduler->is_enabled(tid);
1581 * @brief Select the next thread to execute based on the curren action
1583 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1584 * actions should be followed by the execution of their child thread. In either
1585 * case, the current action should determine the next thread schedule.
1587 * @param curr The current action
1588 * @return The next thread to run, if the current action will determine this
1589 * selection; otherwise NULL
1591 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1593 /* Do not split atomic RMW */
1594 if (curr->is_rmwr())
1595 return get_thread(curr);
1596 /* Follow CREATE with the created thread */
1597 /* which is not needed, because model.cc takes care of this */
1598 if (curr->get_type() == THREAD_CREATE)
1599 return curr->get_thread_operand();
1600 if (curr->get_type() == PTHREAD_CREATE) {
1601 return curr->get_thread_operand();
1607 * Takes the next step in the execution, if possible.
1608 * @param curr The current step to take
1609 * @return Returns the next Thread to run, if any; NULL if this execution
1612 Thread * ModelExecution::take_step(ModelAction *curr)
1614 Thread *curr_thrd = get_thread(curr);
1615 ASSERT(curr_thrd->get_state() == THREAD_READY);
1617 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1618 curr = check_current_action(curr);
1621 // model_print("poitner loc: %p, thread: %d, type: %d, order: %d, position: %s\n", curr, curr->get_tid(), curr->get_type(), curr->get_mo(), curr->get_position() );
1622 model->get_history()->add_func_atomic( curr, curr_thrd->get_id() );
1624 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1625 scheduler->remove_thread(curr_thrd);
1627 return action_select_next_thread(curr);
1630 Fuzzer * ModelExecution::getFuzzer() {