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),
34 ~model_snapshot_members() {
35 for (unsigned int i = 0;i < bugs.size();i++)
40 unsigned int next_thread_id;
41 modelclock_t used_sequence_numbers;
42 SnapVector<bug_message *> bugs;
43 /** @brief Incorrectly-ordered synchronization was made */
44 bool bad_synchronization;
50 /** @brief Constructor */
51 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) :
56 thread_map(2), /* We'll always need at least 2 threads */
60 condvar_waiters_map(),
64 thrd_last_fence_release(),
65 node_stack(node_stack),
66 priv(new struct model_snapshot_members ()),
67 mo_graph(new CycleGraph()),
70 /* Initialize a model-checker thread, for special ModelActions */
71 model_thread = new Thread(get_next_id());
72 add_thread(model_thread);
73 scheduler->register_engine(this);
74 node_stack->register_engine(this);
77 /** @brief Destructor */
78 ModelExecution::~ModelExecution()
80 for (unsigned int i = 0;i < get_num_threads();i++)
81 delete get_thread(int_to_id(i));
87 int ModelExecution::get_execution_number() const
89 return model->get_execution_number();
92 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
94 action_list_t *tmp = hash->get(ptr);
96 tmp = new action_list_t();
102 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
104 SnapVector<action_list_t> *tmp = hash->get(ptr);
106 tmp = new SnapVector<action_list_t>();
112 /** @return a thread ID for a new Thread */
113 thread_id_t ModelExecution::get_next_id()
115 return priv->next_thread_id++;
118 /** @return the number of user threads created during this execution */
119 unsigned int ModelExecution::get_num_threads() const
121 return priv->next_thread_id;
124 /** @return a sequence number for a new ModelAction */
125 modelclock_t ModelExecution::get_next_seq_num()
127 return ++priv->used_sequence_numbers;
131 * @brief Should the current action wake up a given thread?
133 * @param curr The current action
134 * @param thread The thread that we might wake up
135 * @return True, if we should wake up the sleeping thread; false otherwise
137 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
139 const ModelAction *asleep = thread->get_pending();
140 /* Don't allow partial RMW to wake anyone up */
143 /* Synchronizing actions may have been backtracked */
144 if (asleep->could_synchronize_with(curr))
146 /* All acquire/release fences and fence-acquire/store-release */
147 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
149 /* Fence-release + store can awake load-acquire on the same location */
150 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
151 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
152 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
158 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
160 for (unsigned int i = 0;i < get_num_threads();i++) {
161 Thread *thr = get_thread(int_to_id(i));
162 if (scheduler->is_sleep_set(thr)) {
163 if (should_wake_up(curr, thr))
164 /* Remove this thread from sleep set */
165 scheduler->remove_sleep(thr);
170 /** @brief Alert the model-checker that an incorrectly-ordered
171 * synchronization was made */
172 void ModelExecution::set_bad_synchronization()
174 priv->bad_synchronization = true;
177 bool ModelExecution::assert_bug(const char *msg)
179 priv->bugs.push_back(new bug_message(msg));
181 if (isfeasibleprefix()) {
188 /** @return True, if any bugs have been reported for this execution */
189 bool ModelExecution::have_bug_reports() const
191 return priv->bugs.size() != 0;
194 SnapVector<bug_message *> * ModelExecution::get_bugs() const
200 * Check whether the current trace has triggered an assertion which should halt
203 * @return True, if the execution should be aborted; false otherwise
205 bool ModelExecution::has_asserted() const
207 return priv->asserted;
211 * Trigger a trace assertion which should cause this execution to be halted.
212 * This can be due to a detected bug or due to an infeasibility that should
215 void ModelExecution::set_assert()
217 priv->asserted = true;
221 * Check if we are in a deadlock. Should only be called at the end of an
222 * execution, although it should not give false positives in the middle of an
223 * execution (there should be some ENABLED thread).
225 * @return True if program is in a deadlock; false otherwise
227 bool ModelExecution::is_deadlocked() const
229 bool blocking_threads = false;
230 for (unsigned int i = 0;i < get_num_threads();i++) {
231 thread_id_t tid = int_to_id(i);
234 Thread *t = get_thread(tid);
235 if (!t->is_model_thread() && t->get_pending())
236 blocking_threads = true;
238 return blocking_threads;
242 * Check if this is a complete execution. That is, have all thread completed
243 * execution (rather than exiting because sleep sets have forced a redundant
246 * @return True if the execution is complete.
248 bool ModelExecution::is_complete_execution() const
250 for (unsigned int i = 0;i < get_num_threads();i++)
251 if (is_enabled(int_to_id(i)))
258 * Processes a read model action.
259 * @param curr is the read model action to process.
260 * @param rf_set is the set of model actions we can possibly read from
261 * @return True if processing this read updates the mo_graph.
263 void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set)
265 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
268 int index = fuzzer->selectWrite(curr, rf_set);
269 const ModelAction *rf = (*rf_set)[index];
273 bool canprune = false;
274 if (r_modification_order(curr, rf, priorset, &canprune)) {
275 for(unsigned int i=0;i<priorset->size();i++) {
276 mo_graph->addEdge((*priorset)[i], rf);
279 get_thread(curr)->set_return_value(curr->get_return_value());
281 if (canprune && curr->get_type() == ATOMIC_READ) {
282 int tid = id_to_int(curr->get_tid());
283 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
288 (*rf_set)[index] = rf_set->back();
294 * Processes a lock, trylock, or unlock model action. @param curr is
295 * the read model action to process.
297 * The try lock operation checks whether the lock is taken. If not,
298 * it falls to the normal lock operation case. If so, it returns
301 * The lock operation has already been checked that it is enabled, so
302 * it just grabs the lock and synchronizes with the previous unlock.
304 * The unlock operation has to re-enable all of the threads that are
305 * waiting on the lock.
307 * @return True if synchronization was updated; false otherwise
309 bool ModelExecution::process_mutex(ModelAction *curr)
311 cdsc::mutex *mutex = curr->get_mutex();
312 struct cdsc::mutex_state *state = NULL;
315 state = mutex->get_state();
317 switch (curr->get_type()) {
318 case ATOMIC_TRYLOCK: {
319 bool success = !state->locked;
320 curr->set_try_lock(success);
322 get_thread(curr)->set_return_value(0);
325 get_thread(curr)->set_return_value(1);
327 //otherwise fall into the lock case
329 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
330 assert_bug("Lock access before initialization");
331 state->locked = get_thread(curr);
332 ModelAction *unlock = get_last_unlock(curr);
333 //synchronize with the previous unlock statement
334 if (unlock != NULL) {
335 synchronize(unlock, curr);
341 case ATOMIC_UNLOCK: {
342 //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...
344 /* wake up the other threads */
345 for (unsigned int i = 0;i < get_num_threads();i++) {
346 Thread *t = get_thread(int_to_id(i));
347 Thread *curr_thrd = get_thread(curr);
348 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
352 /* unlock the lock - after checking who was waiting on it */
353 state->locked = NULL;
355 if (!curr->is_wait())
356 break;/* The rest is only for ATOMIC_WAIT */
360 case ATOMIC_NOTIFY_ALL: {
361 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
362 //activate all the waiting threads
363 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
364 scheduler->wake(get_thread(*rit));
369 case ATOMIC_NOTIFY_ONE: {
370 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
371 if (waiters->size() != 0) {
372 Thread * thread = fuzzer->selectNotify(waiters);
373 scheduler->wake(thread);
385 * Process a write ModelAction
386 * @param curr The ModelAction to process
387 * @return True if the mo_graph was updated or promises were resolved
389 void ModelExecution::process_write(ModelAction *curr)
392 w_modification_order(curr);
395 get_thread(curr)->set_return_value(VALUE_NONE);
399 * Process a fence ModelAction
400 * @param curr The ModelAction to process
401 * @return True if synchronization was updated
403 bool ModelExecution::process_fence(ModelAction *curr)
406 * fence-relaxed: no-op
407 * fence-release: only log the occurence (not in this function), for
408 * use in later synchronization
409 * fence-acquire (this function): search for hypothetical release
411 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
413 bool updated = false;
414 if (curr->is_acquire()) {
415 action_list_t *list = &action_trace;
416 action_list_t::reverse_iterator rit;
417 /* Find X : is_read(X) && X --sb-> curr */
418 for (rit = list->rbegin();rit != list->rend();rit++) {
419 ModelAction *act = *rit;
422 if (act->get_tid() != curr->get_tid())
424 /* Stop at the beginning of the thread */
425 if (act->is_thread_start())
427 /* Stop once we reach a prior fence-acquire */
428 if (act->is_fence() && act->is_acquire())
432 /* read-acquire will find its own release sequences */
433 if (act->is_acquire())
436 /* Establish hypothetical release sequences */
437 rel_heads_list_t release_heads;
438 get_release_seq_heads(curr, act, &release_heads);
439 for (unsigned int i = 0;i < release_heads.size();i++)
440 synchronize(release_heads[i], curr);
441 if (release_heads.size() != 0)
449 * @brief Process the current action for thread-related activity
451 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
452 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
453 * synchronization, etc. This function is a no-op for non-THREAD actions
454 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
456 * @param curr The current action
457 * @return True if synchronization was updated or a thread completed
459 bool ModelExecution::process_thread_action(ModelAction *curr)
461 bool updated = false;
463 switch (curr->get_type()) {
464 case THREAD_CREATE: {
465 thrd_t *thrd = (thrd_t *)curr->get_location();
466 struct thread_params *params = (struct thread_params *)curr->get_value();
467 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
468 curr->set_thread_operand(th);
470 th->set_creation(curr);
473 case PTHREAD_CREATE: {
474 (*(uint32_t *)curr->get_location()) = pthread_counter++;
476 struct pthread_params *params = (struct pthread_params *)curr->get_value();
477 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
478 curr->set_thread_operand(th);
480 th->set_creation(curr);
482 if ( pthread_map.size() < pthread_counter )
483 pthread_map.resize( pthread_counter );
484 pthread_map[ pthread_counter-1 ] = th;
489 Thread *blocking = curr->get_thread_operand();
490 ModelAction *act = get_last_action(blocking->get_id());
491 synchronize(act, curr);
492 updated = true; /* trigger rel-seq checks */
496 Thread *blocking = curr->get_thread_operand();
497 ModelAction *act = get_last_action(blocking->get_id());
498 synchronize(act, curr);
499 updated = true; /* trigger rel-seq checks */
500 break; // WL: to be add (modified)
503 case THREAD_FINISH: {
504 Thread *th = get_thread(curr);
505 /* Wake up any joining threads */
506 for (unsigned int i = 0;i < get_num_threads();i++) {
507 Thread *waiting = get_thread(int_to_id(i));
508 if (waiting->waiting_on() == th &&
509 waiting->get_pending()->is_thread_join())
510 scheduler->wake(waiting);
513 updated = true; /* trigger rel-seq checks */
527 * Initialize the current action by performing one or more of the following
528 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
529 * in the NodeStack, manipulating backtracking sets, allocating and
530 * initializing clock vectors, and computing the promises to fulfill.
532 * @param curr The current action, as passed from the user context; may be
533 * freed/invalidated after the execution of this function, with a different
534 * action "returned" its place (pass-by-reference)
535 * @return True if curr is a newly-explored action; false otherwise
537 bool ModelExecution::initialize_curr_action(ModelAction **curr)
539 ModelAction *newcurr;
541 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
542 newcurr = process_rmw(*curr);
549 (*curr)->set_seq_number(get_next_seq_num());
551 newcurr = node_stack->explore_action(*curr);
553 /* First restore type and order in case of RMW operation */
554 if ((*curr)->is_rmwr())
555 newcurr->copy_typeandorder(*curr);
557 ASSERT((*curr)->get_location() == newcurr->get_location());
558 newcurr->copy_from_new(*curr);
560 /* Discard duplicate ModelAction; use action from NodeStack */
563 /* Always compute new clock vector */
564 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
567 return false; /* Action was explored previously */
571 /* Always compute new clock vector */
572 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
574 /* Assign most recent release fence */
575 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
577 return true; /* This was a new ModelAction */
582 * @brief Establish reads-from relation between two actions
584 * Perform basic operations involved with establishing a concrete rf relation,
585 * including setting the ModelAction data and checking for release sequences.
587 * @param act The action that is reading (must be a read)
588 * @param rf The action from which we are reading (must be a write)
590 * @return True if this read established synchronization
593 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
596 ASSERT(rf->is_write());
598 act->set_read_from(rf);
599 if (act->is_acquire()) {
600 rel_heads_list_t release_heads;
601 get_release_seq_heads(act, act, &release_heads);
602 int num_heads = release_heads.size();
603 for (unsigned int i = 0;i < release_heads.size();i++)
604 if (!synchronize(release_heads[i], act))
606 return num_heads > 0;
612 * @brief Synchronizes two actions
614 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
615 * This function performs the synchronization as well as providing other hooks
616 * for other checks along with synchronization.
618 * @param first The left-hand side of the synchronizes-with relation
619 * @param second The right-hand side of the synchronizes-with relation
620 * @return True if the synchronization was successful (i.e., was consistent
621 * with the execution order); false otherwise
623 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
625 if (*second < *first) {
626 set_bad_synchronization();
629 return second->synchronize_with(first);
633 * @brief Check whether a model action is enabled.
635 * Checks whether an operation would be successful (i.e., is a lock already
636 * locked, or is the joined thread already complete).
638 * For yield-blocking, yields are never enabled.
640 * @param curr is the ModelAction to check whether it is enabled.
641 * @return a bool that indicates whether the action is enabled.
643 bool ModelExecution::check_action_enabled(ModelAction *curr) {
644 if (curr->is_lock()) {
645 cdsc::mutex *lock = curr->get_mutex();
646 struct cdsc::mutex_state *state = lock->get_state();
649 } else if (curr->is_thread_join()) {
650 Thread *blocking = curr->get_thread_operand();
651 if (!blocking->is_complete()) {
660 * This is the heart of the model checker routine. It performs model-checking
661 * actions corresponding to a given "current action." Among other processes, it
662 * calculates reads-from relationships, updates synchronization clock vectors,
663 * forms a memory_order constraints graph, and handles replay/backtrack
664 * execution when running permutations of previously-observed executions.
666 * @param curr The current action to process
667 * @return The ModelAction that is actually executed; may be different than
670 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
673 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
674 bool newly_explored = initialize_curr_action(&curr);
678 wake_up_sleeping_actions(curr);
680 /* Add the action to lists before any other model-checking tasks */
681 if (!second_part_of_rmw && curr->get_type() != NOOP)
682 add_action_to_lists(curr);
684 SnapVector<const ModelAction *> * rf_set = NULL;
685 /* Build may_read_from set for newly-created actions */
686 if (newly_explored && curr->is_read())
687 rf_set = build_may_read_from(curr);
689 process_thread_action(curr);
691 if (curr->is_read() && !second_part_of_rmw) {
692 process_read(curr, rf_set);
695 ASSERT(rf_set == NULL);
698 if (curr->is_write())
701 if (curr->is_fence())
704 if (curr->is_mutex_op())
711 * This is the strongest feasibility check available.
712 * @return whether the current trace (partial or complete) must be a prefix of
715 bool ModelExecution::isfeasibleprefix() const
717 return !is_infeasible();
721 * Print disagnostic information about an infeasible execution
722 * @param prefix A string to prefix the output with; if NULL, then a default
723 * message prefix will be provided
725 void ModelExecution::print_infeasibility(const char *prefix) const
729 if (priv->bad_synchronization)
730 ptr += sprintf(ptr, "[bad sw ordering]");
732 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
736 * Check if the current partial trace is infeasible. Does not check any
737 * end-of-execution flags, which might rule out the execution. Thus, this is
738 * useful only for ruling an execution as infeasible.
739 * @return whether the current partial trace is infeasible.
741 bool ModelExecution::is_infeasible() const
743 return priv->bad_synchronization;
746 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
747 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
748 ModelAction *lastread = get_last_action(act->get_tid());
749 lastread->process_rmw(act);
751 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
757 * @brief Updates the mo_graph with the constraints imposed from the current
760 * Basic idea is the following: Go through each other thread and find
761 * the last action that happened before our read. Two cases:
763 * -# The action is a write: that write must either occur before
764 * the write we read from or be the write we read from.
765 * -# The action is a read: the write that that action read from
766 * must occur before the write we read from or be the same write.
768 * @param curr The current action. Must be a read.
769 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
770 * @return True if modification order edges were added; false otherwise
773 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
775 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
777 ASSERT(curr->is_read());
779 /* Last SC fence in the current thread */
780 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
782 int tid = curr->get_tid();
783 ModelAction *prev_same_thread = NULL;
784 /* Iterate over all threads */
785 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
786 /* Last SC fence in thread tid */
787 ModelAction *last_sc_fence_thread_local = NULL;
789 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
791 /* Last SC fence in thread tid, before last SC fence in current thread */
792 ModelAction *last_sc_fence_thread_before = NULL;
793 if (last_sc_fence_local)
794 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
796 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
797 if (prev_same_thread != NULL &&
798 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
799 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
803 /* Iterate over actions in thread, starting from most recent */
804 action_list_t *list = &(*thrd_lists)[tid];
805 action_list_t::reverse_iterator rit;
806 for (rit = list->rbegin();rit != list->rend();rit++) {
807 ModelAction *act = *rit;
812 /* Don't want to add reflexive edges on 'rf' */
813 if (act->equals(rf)) {
814 if (act->happens_before(curr))
820 if (act->is_write()) {
821 /* C++, Section 29.3 statement 5 */
822 if (curr->is_seqcst() && last_sc_fence_thread_local &&
823 *act < *last_sc_fence_thread_local) {
824 if (mo_graph->checkReachable(rf, act))
826 priorset->push_back(act);
829 /* C++, Section 29.3 statement 4 */
830 else if (act->is_seqcst() && last_sc_fence_local &&
831 *act < *last_sc_fence_local) {
832 if (mo_graph->checkReachable(rf, act))
834 priorset->push_back(act);
837 /* C++, Section 29.3 statement 6 */
838 else if (last_sc_fence_thread_before &&
839 *act < *last_sc_fence_thread_before) {
840 if (mo_graph->checkReachable(rf, act))
842 priorset->push_back(act);
848 * Include at most one act per-thread that "happens
851 if (act->happens_before(curr)) {
853 if (last_sc_fence_local == NULL ||
854 (*last_sc_fence_local < *prev_same_thread)) {
855 prev_same_thread = act;
858 if (act->is_write()) {
859 if (mo_graph->checkReachable(rf, act))
861 priorset->push_back(act);
863 const ModelAction *prevrf = act->get_reads_from();
864 if (!prevrf->equals(rf)) {
865 if (mo_graph->checkReachable(rf, prevrf))
867 priorset->push_back(prevrf);
869 if (act->get_tid() == curr->get_tid()) {
870 //Can prune curr from obj list
883 * Updates the mo_graph with the constraints imposed from the current write.
885 * Basic idea is the following: Go through each other thread and find
886 * the lastest action that happened before our write. Two cases:
888 * (1) The action is a write => that write must occur before
891 * (2) The action is a read => the write that that action read from
892 * must occur before the current write.
894 * This method also handles two other issues:
896 * (I) Sequential Consistency: Making sure that if the current write is
897 * seq_cst, that it occurs after the previous seq_cst write.
899 * (II) Sending the write back to non-synchronizing reads.
901 * @param curr The current action. Must be a write.
902 * @param send_fv A vector for stashing reads to which we may pass our future
903 * value. If NULL, then don't record any future values.
904 * @return True if modification order edges were added; false otherwise
906 void ModelExecution::w_modification_order(ModelAction *curr)
908 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
910 ASSERT(curr->is_write());
912 if (curr->is_seqcst()) {
913 /* We have to at least see the last sequentially consistent write,
914 so we are initialized. */
915 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
916 if (last_seq_cst != NULL) {
917 mo_graph->addEdge(last_seq_cst, curr);
921 /* Last SC fence in the current thread */
922 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
924 /* Iterate over all threads */
925 for (i = 0;i < thrd_lists->size();i++) {
926 /* Last SC fence in thread i, before last SC fence in current thread */
927 ModelAction *last_sc_fence_thread_before = NULL;
928 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
929 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
931 /* Iterate over actions in thread, starting from most recent */
932 action_list_t *list = &(*thrd_lists)[i];
933 action_list_t::reverse_iterator rit;
934 bool force_edge = false;
935 for (rit = list->rbegin();rit != list->rend();rit++) {
936 ModelAction *act = *rit;
939 * 1) If RMW and it actually read from something, then we
940 * already have all relevant edges, so just skip to next
943 * 2) If RMW and it didn't read from anything, we should
944 * whatever edge we can get to speed up convergence.
946 * 3) If normal write, we need to look at earlier actions, so
947 * continue processing list.
950 if (curr->is_rmw()) {
951 if (curr->get_reads_from() != NULL)
959 /* C++, Section 29.3 statement 7 */
960 if (last_sc_fence_thread_before && act->is_write() &&
961 *act < *last_sc_fence_thread_before) {
962 mo_graph->addEdge(act, curr, force_edge);
967 * Include at most one act per-thread that "happens
970 if (act->happens_before(curr)) {
972 * Note: if act is RMW, just add edge:
974 * The following edge should be handled elsewhere:
975 * readfrom(act) --mo--> act
978 mo_graph->addEdge(act, curr, force_edge);
979 else if (act->is_read()) {
980 //if previous read accessed a null, just keep going
981 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
984 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
985 !act->same_thread(curr)) {
986 /* We have an action that:
987 (1) did not happen before us
988 (2) is a read and we are a write
989 (3) cannot synchronize with us
990 (4) is in a different thread
992 that read could potentially read from our write. Note that
993 these checks are overly conservative at this point, we'll
994 do more checks before actually removing the
1005 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1006 * some constraints. This method checks one the following constraint (others
1007 * require compiler support):
1009 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1010 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1012 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1014 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1016 /* Iterate over all threads */
1017 for (i = 0;i < thrd_lists->size();i++) {
1018 const ModelAction *write_after_read = NULL;
1020 /* Iterate over actions in thread, starting from most recent */
1021 action_list_t *list = &(*thrd_lists)[i];
1022 action_list_t::reverse_iterator rit;
1023 for (rit = list->rbegin();rit != list->rend();rit++) {
1024 ModelAction *act = *rit;
1026 /* Don't disallow due to act == reader */
1027 if (!reader->happens_before(act) || reader == act)
1029 else if (act->is_write())
1030 write_after_read = act;
1031 else if (act->is_read() && act->get_reads_from() != NULL)
1032 write_after_read = act->get_reads_from();
1035 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1042 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1043 * The ModelAction under consideration is expected to be taking part in
1044 * release/acquire synchronization as an object of the "reads from" relation.
1045 * Note that this can only provide release sequence support for RMW chains
1046 * which do not read from the future, as those actions cannot be traced until
1047 * their "promise" is fulfilled. Similarly, we may not even establish the
1048 * presence of a release sequence with certainty, as some modification order
1049 * constraints may be decided further in the future. Thus, this function
1050 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1051 * and a boolean representing certainty.
1053 * @param rf The action that might be part of a release sequence. Must be a
1055 * @param release_heads A pass-by-reference style return parameter. After
1056 * execution of this function, release_heads will contain the heads of all the
1057 * relevant release sequences, if any exists with certainty
1058 * @return true, if the ModelExecution is certain that release_heads is complete;
1061 bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
1064 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1065 ASSERT(rf->is_write());
1067 if (rf->is_release())
1068 release_heads->push_back(rf);
1069 else if (rf->get_last_fence_release())
1070 release_heads->push_back(rf->get_last_fence_release());
1072 break;/* End of RMW chain */
1074 /** @todo Need to be smarter here... In the linux lock
1075 * example, this will run to the beginning of the program for
1077 /** @todo The way to be smarter here is to keep going until 1
1078 * thread has a release preceded by an acquire and you've seen
1081 /* acq_rel RMW is a sufficient stopping condition */
1082 if (rf->is_acquire() && rf->is_release())
1083 return true;/* complete */
1085 ASSERT(rf); // Needs to be real write
1087 if (rf->is_release())
1088 return true;/* complete */
1090 /* else relaxed write
1091 * - check for fence-release in the same thread (29.8, stmt. 3)
1092 * - check modification order for contiguous subsequence
1093 * -> rf must be same thread as release */
1095 const ModelAction *fence_release = rf->get_last_fence_release();
1096 /* Synchronize with a fence-release unconditionally; we don't need to
1097 * find any more "contiguous subsequence..." for it */
1099 release_heads->push_back(fence_release);
1101 return true; /* complete */
1105 * An interface for getting the release sequence head(s) with which a
1106 * given ModelAction must synchronize. This function only returns a non-empty
1107 * result when it can locate a release sequence head with certainty. Otherwise,
1108 * it may mark the internal state of the ModelExecution so that it will handle
1109 * the release sequence at a later time, causing @a acquire to update its
1110 * synchronization at some later point in execution.
1112 * @param acquire The 'acquire' action that may synchronize with a release
1114 * @param read The read action that may read from a release sequence; this may
1115 * be the same as acquire, or else an earlier action in the same thread (i.e.,
1116 * when 'acquire' is a fence-acquire)
1117 * @param release_heads A pass-by-reference return parameter. Will be filled
1118 * with the head(s) of the release sequence(s), if they exists with certainty.
1119 * @see ModelExecution::release_seq_heads
1121 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
1122 ModelAction *read, rel_heads_list_t *release_heads)
1124 const ModelAction *rf = read->get_reads_from();
1126 release_seq_heads(rf, release_heads);
1130 * Performs various bookkeeping operations for the current ModelAction. For
1131 * instance, adds action to the per-object, per-thread action vector and to the
1132 * action trace list of all thread actions.
1134 * @param act is the ModelAction to add.
1136 void ModelExecution::add_action_to_lists(ModelAction *act)
1138 int tid = id_to_int(act->get_tid());
1139 ModelAction *uninit = NULL;
1141 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1142 if (list->empty() && act->is_atomic_var()) {
1143 uninit = get_uninitialized_action(act);
1144 uninit_id = id_to_int(uninit->get_tid());
1145 list->push_front(uninit);
1147 list->push_back(act);
1149 action_trace.push_back(act);
1151 action_trace.push_front(uninit);
1153 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1154 if (tid >= (int)vec->size())
1155 vec->resize(priv->next_thread_id);
1156 (*vec)[tid].push_back(act);
1158 (*vec)[uninit_id].push_front(uninit);
1160 if ((int)thrd_last_action.size() <= tid)
1161 thrd_last_action.resize(get_num_threads());
1162 thrd_last_action[tid] = act;
1164 thrd_last_action[uninit_id] = uninit;
1166 if (act->is_fence() && act->is_release()) {
1167 if ((int)thrd_last_fence_release.size() <= tid)
1168 thrd_last_fence_release.resize(get_num_threads());
1169 thrd_last_fence_release[tid] = act;
1172 if (act->is_wait()) {
1173 void *mutex_loc = (void *) act->get_value();
1174 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1176 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1177 if (tid >= (int)vec->size())
1178 vec->resize(priv->next_thread_id);
1179 (*vec)[tid].push_back(act);
1184 * @brief Get the last action performed by a particular Thread
1185 * @param tid The thread ID of the Thread in question
1186 * @return The last action in the thread
1188 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1190 int threadid = id_to_int(tid);
1191 if (threadid < (int)thrd_last_action.size())
1192 return thrd_last_action[id_to_int(tid)];
1198 * @brief Get the last fence release performed by a particular Thread
1199 * @param tid The thread ID of the Thread in question
1200 * @return The last fence release in the thread, if one exists; NULL otherwise
1202 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1204 int threadid = id_to_int(tid);
1205 if (threadid < (int)thrd_last_fence_release.size())
1206 return thrd_last_fence_release[id_to_int(tid)];
1212 * Gets the last memory_order_seq_cst write (in the total global sequence)
1213 * performed on a particular object (i.e., memory location), not including the
1215 * @param curr The current ModelAction; also denotes the object location to
1217 * @return The last seq_cst write
1219 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1221 void *location = curr->get_location();
1222 action_list_t *list = obj_map.get(location);
1223 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1224 action_list_t::reverse_iterator rit;
1225 for (rit = list->rbegin();(*rit) != curr;rit++)
1227 rit++; /* Skip past curr */
1228 for ( ;rit != list->rend();rit++)
1229 if ((*rit)->is_write() && (*rit)->is_seqcst())
1235 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1236 * performed in a particular thread, prior to a particular fence.
1237 * @param tid The ID of the thread to check
1238 * @param before_fence The fence from which to begin the search; if NULL, then
1239 * search for the most recent fence in the thread.
1240 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1242 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1244 /* All fences should have location FENCE_LOCATION */
1245 action_list_t *list = obj_map.get(FENCE_LOCATION);
1250 action_list_t::reverse_iterator rit = list->rbegin();
1253 for (;rit != list->rend();rit++)
1254 if (*rit == before_fence)
1257 ASSERT(*rit == before_fence);
1261 for (;rit != list->rend();rit++)
1262 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1268 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1269 * location). This function identifies the mutex according to the current
1270 * action, which is presumed to perform on the same mutex.
1271 * @param curr The current ModelAction; also denotes the object location to
1273 * @return The last unlock operation
1275 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1277 void *location = curr->get_location();
1279 action_list_t *list = obj_map.get(location);
1280 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1281 action_list_t::reverse_iterator rit;
1282 for (rit = list->rbegin();rit != list->rend();rit++)
1283 if ((*rit)->is_unlock() || (*rit)->is_wait())
1288 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1290 ModelAction *parent = get_last_action(tid);
1292 parent = get_thread(tid)->get_creation();
1297 * Returns the clock vector for a given thread.
1298 * @param tid The thread whose clock vector we want
1299 * @return Desired clock vector
1301 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1303 ModelAction *firstaction=get_parent_action(tid);
1304 return firstaction != NULL ? firstaction->get_cv() : NULL;
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 SnapVector<const 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 SnapVector<const ModelAction *> * rf_set = new SnapVector<const 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 const ModelAction *act = *rit;
1351 /* Only consider 'write' actions */
1352 if (!act->is_write()) {
1353 if (act != curr && act->is_read() && act->happens_before(curr)) {
1354 const ModelAction *tmp = act->get_reads_from();
1355 if (((unsigned int) id_to_int(tmp->get_tid()))==i)
1366 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1367 bool allow_read = true;
1369 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1372 /* Need to check whether we will have two RMW reading from the same value */
1373 if (curr->is_rmwr()) {
1374 /* It is okay if we have a failing CAS */
1375 if (!curr->is_rmwrcas() ||
1376 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1377 //Need to make sure we aren't the second RMW
1378 CycleNode * node = mo_graph->getNode_noCreate(act);
1379 if (node != NULL && node->getRMW() != NULL) {
1380 //we are the second RMW
1387 /* Only add feasible reads */
1388 rf_set->push_back(act);
1391 /* Include at most one act per-thread that "happens before" curr */
1392 if (act->happens_before(curr))
1397 if (DBG_ENABLED()) {
1398 model_print("Reached read action:\n");
1400 model_print("End printing read_from_past\n");
1406 * @brief Get an action representing an uninitialized atomic
1408 * This function may create a new one or try to retrieve one from the NodeStack
1410 * @param curr The current action, which prompts the creation of an UNINIT action
1411 * @return A pointer to the UNINIT ModelAction
1413 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1415 Node *node = curr->get_node();
1416 ModelAction *act = node->get_uninit_action();
1418 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1419 node->set_uninit_action(act);
1421 act->create_cv(NULL);
1425 static void print_list(const action_list_t *list)
1427 action_list_t::const_iterator it;
1429 model_print("------------------------------------------------------------------------------------\n");
1430 model_print("# t Action type MO Location Value Rf CV\n");
1431 model_print("------------------------------------------------------------------------------------\n");
1433 unsigned int hash = 0;
1435 for (it = list->begin();it != list->end();it++) {
1436 const ModelAction *act = *it;
1437 if (act->get_seq_number() > 0)
1439 hash = hash^(hash<<3)^((*it)->hash());
1441 model_print("HASH %u\n", hash);
1442 model_print("------------------------------------------------------------------------------------\n");
1445 #if SUPPORT_MOD_ORDER_DUMP
1446 void ModelExecution::dumpGraph(char *filename) const
1449 sprintf(buffer, "%s.dot", filename);
1450 FILE *file = fopen(buffer, "w");
1451 fprintf(file, "digraph %s {\n", filename);
1452 mo_graph->dumpNodes(file);
1453 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1455 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1456 ModelAction *act = *it;
1457 if (act->is_read()) {
1458 mo_graph->dot_print_node(file, act);
1459 mo_graph->dot_print_edge(file,
1460 act->get_reads_from(),
1462 "label=\"rf\", color=red, weight=2");
1464 if (thread_array[act->get_tid()]) {
1465 mo_graph->dot_print_edge(file,
1466 thread_array[id_to_int(act->get_tid())],
1468 "label=\"sb\", color=blue, weight=400");
1471 thread_array[act->get_tid()] = act;
1473 fprintf(file, "}\n");
1474 model_free(thread_array);
1479 /** @brief Prints an execution trace summary. */
1480 void ModelExecution::print_summary() const
1482 #if SUPPORT_MOD_ORDER_DUMP
1483 char buffername[100];
1484 sprintf(buffername, "exec%04u", get_execution_number());
1485 mo_graph->dumpGraphToFile(buffername);
1486 sprintf(buffername, "graph%04u", get_execution_number());
1487 dumpGraph(buffername);
1490 model_print("Execution trace %d:", get_execution_number());
1491 if (isfeasibleprefix()) {
1492 if (scheduler->all_threads_sleeping())
1493 model_print(" SLEEP-SET REDUNDANT");
1494 if (have_bug_reports())
1495 model_print(" DETECTED BUG(S)");
1497 print_infeasibility(" INFEASIBLE");
1500 print_list(&action_trace);
1506 * Add a Thread to the system for the first time. Should only be called once
1508 * @param t The Thread to add
1510 void ModelExecution::add_thread(Thread *t)
1512 unsigned int i = id_to_int(t->get_id());
1513 if (i >= thread_map.size())
1514 thread_map.resize(i + 1);
1516 if (!t->is_model_thread())
1517 scheduler->add_thread(t);
1521 * @brief Get a Thread reference by its ID
1522 * @param tid The Thread's ID
1523 * @return A Thread reference
1525 Thread * ModelExecution::get_thread(thread_id_t tid) const
1527 unsigned int i = id_to_int(tid);
1528 if (i < thread_map.size())
1529 return thread_map[i];
1534 * @brief Get a reference to the Thread in which a ModelAction was executed
1535 * @param act The ModelAction
1536 * @return A Thread reference
1538 Thread * ModelExecution::get_thread(const ModelAction *act) const
1540 return get_thread(act->get_tid());
1544 * @brief Get a Thread reference by its pthread ID
1545 * @param index The pthread's ID
1546 * @return A Thread reference
1548 Thread * ModelExecution::get_pthread(pthread_t pid) {
1554 uint32_t thread_id = x.v;
1555 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1560 * @brief Check if a Thread is currently enabled
1561 * @param t The Thread to check
1562 * @return True if the Thread is currently enabled
1564 bool ModelExecution::is_enabled(Thread *t) const
1566 return scheduler->is_enabled(t);
1570 * @brief Check if a Thread is currently enabled
1571 * @param tid The ID of the Thread to check
1572 * @return True if the Thread is currently enabled
1574 bool ModelExecution::is_enabled(thread_id_t tid) const
1576 return scheduler->is_enabled(tid);
1580 * @brief Select the next thread to execute based on the curren action
1582 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1583 * actions should be followed by the execution of their child thread. In either
1584 * case, the current action should determine the next thread schedule.
1586 * @param curr The current action
1587 * @return The next thread to run, if the current action will determine this
1588 * selection; otherwise NULL
1590 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1592 /* Do not split atomic RMW */
1593 if (curr->is_rmwr())
1594 return get_thread(curr);
1595 /* Follow CREATE with the created thread */
1596 /* which is not needed, because model.cc takes care of this */
1597 if (curr->get_type() == THREAD_CREATE)
1598 return curr->get_thread_operand();
1599 if (curr->get_type() == PTHREAD_CREATE) {
1600 return curr->get_thread_operand();
1606 * Takes the next step in the execution, if possible.
1607 * @param curr The current step to take
1608 * @return Returns the next Thread to run, if any; NULL if this execution
1611 Thread * ModelExecution::take_step(ModelAction *curr)
1613 Thread *curr_thrd = get_thread(curr);
1614 ASSERT(curr_thrd->get_state() == THREAD_READY);
1616 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1617 curr = check_current_action(curr);
1620 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1621 scheduler->remove_thread(curr_thrd);
1623 return action_select_next_thread(curr);
1626 Fuzzer * ModelExecution::getFuzzer() {