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];
274 if (r_modification_order(curr, rf, priorset)) {
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());
284 (*rf_set)[index] = rf_set->back();
290 * Processes a lock, trylock, or unlock model action. @param curr is
291 * the read model action to process.
293 * The try lock operation checks whether the lock is taken. If not,
294 * it falls to the normal lock operation case. If so, it returns
297 * The lock operation has already been checked that it is enabled, so
298 * it just grabs the lock and synchronizes with the previous unlock.
300 * The unlock operation has to re-enable all of the threads that are
301 * waiting on the lock.
303 * @return True if synchronization was updated; false otherwise
305 bool ModelExecution::process_mutex(ModelAction *curr)
307 cdsc::mutex *mutex = curr->get_mutex();
308 struct cdsc::mutex_state *state = NULL;
311 state = mutex->get_state();
313 switch (curr->get_type()) {
314 case ATOMIC_TRYLOCK: {
315 bool success = !state->locked;
316 curr->set_try_lock(success);
318 get_thread(curr)->set_return_value(0);
321 get_thread(curr)->set_return_value(1);
323 //otherwise fall into the lock case
325 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
326 assert_bug("Lock access before initialization");
327 state->locked = get_thread(curr);
328 ModelAction *unlock = get_last_unlock(curr);
329 //synchronize with the previous unlock statement
330 if (unlock != NULL) {
331 synchronize(unlock, curr);
337 case ATOMIC_UNLOCK: {
338 /* wake up the other threads */
339 for (unsigned int i = 0;i < get_num_threads();i++) {
340 Thread *t = get_thread(int_to_id(i));
341 Thread *curr_thrd = get_thread(curr);
342 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
346 /* unlock the lock - after checking who was waiting on it */
347 state->locked = NULL;
349 if (!curr->is_wait())
350 break;/* The rest is only for ATOMIC_WAIT */
354 case ATOMIC_NOTIFY_ALL: {
355 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
356 //activate all the waiting threads
357 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
358 scheduler->wake(get_thread(*rit));
363 case ATOMIC_NOTIFY_ONE: {
364 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
365 if (waiters->size() != 0) {
366 Thread * thread = fuzzer->selectNotify(waiters);
367 scheduler->wake(thread);
379 * Process a write ModelAction
380 * @param curr The ModelAction to process
381 * @return True if the mo_graph was updated or promises were resolved
383 void ModelExecution::process_write(ModelAction *curr)
386 w_modification_order(curr);
389 get_thread(curr)->set_return_value(VALUE_NONE);
393 * Process a fence ModelAction
394 * @param curr The ModelAction to process
395 * @return True if synchronization was updated
397 bool ModelExecution::process_fence(ModelAction *curr)
400 * fence-relaxed: no-op
401 * fence-release: only log the occurence (not in this function), for
402 * use in later synchronization
403 * fence-acquire (this function): search for hypothetical release
405 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
407 bool updated = false;
408 if (curr->is_acquire()) {
409 action_list_t *list = &action_trace;
410 action_list_t::reverse_iterator rit;
411 /* Find X : is_read(X) && X --sb-> curr */
412 for (rit = list->rbegin();rit != list->rend();rit++) {
413 ModelAction *act = *rit;
416 if (act->get_tid() != curr->get_tid())
418 /* Stop at the beginning of the thread */
419 if (act->is_thread_start())
421 /* Stop once we reach a prior fence-acquire */
422 if (act->is_fence() && act->is_acquire())
426 /* read-acquire will find its own release sequences */
427 if (act->is_acquire())
430 /* Establish hypothetical release sequences */
431 rel_heads_list_t release_heads;
432 get_release_seq_heads(curr, act, &release_heads);
433 for (unsigned int i = 0;i < release_heads.size();i++)
434 synchronize(release_heads[i], curr);
435 if (release_heads.size() != 0)
443 * @brief Process the current action for thread-related activity
445 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
446 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
447 * synchronization, etc. This function is a no-op for non-THREAD actions
448 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
450 * @param curr The current action
451 * @return True if synchronization was updated or a thread completed
453 bool ModelExecution::process_thread_action(ModelAction *curr)
455 bool updated = false;
457 switch (curr->get_type()) {
458 case THREAD_CREATE: {
459 thrd_t *thrd = (thrd_t *)curr->get_location();
460 struct thread_params *params = (struct thread_params *)curr->get_value();
461 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
462 curr->set_thread_operand(th);
464 th->set_creation(curr);
467 case PTHREAD_CREATE: {
468 (*(uint32_t *)curr->get_location()) = pthread_counter++;
470 struct pthread_params *params = (struct pthread_params *)curr->get_value();
471 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
472 curr->set_thread_operand(th);
474 th->set_creation(curr);
476 if ( pthread_map.size() < pthread_counter )
477 pthread_map.resize( pthread_counter );
478 pthread_map[ pthread_counter-1 ] = th;
483 Thread *blocking = curr->get_thread_operand();
484 ModelAction *act = get_last_action(blocking->get_id());
485 synchronize(act, curr);
486 updated = true; /* trigger rel-seq checks */
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 */
494 break; // WL: to be add (modified)
497 case THREAD_FINISH: {
498 Thread *th = get_thread(curr);
499 /* Wake up any joining threads */
500 for (unsigned int i = 0;i < get_num_threads();i++) {
501 Thread *waiting = get_thread(int_to_id(i));
502 if (waiting->waiting_on() == th &&
503 waiting->get_pending()->is_thread_join())
504 scheduler->wake(waiting);
507 updated = true; /* trigger rel-seq checks */
521 * Initialize the current action by performing one or more of the following
522 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
523 * in the NodeStack, manipulating backtracking sets, allocating and
524 * initializing clock vectors, and computing the promises to fulfill.
526 * @param curr The current action, as passed from the user context; may be
527 * freed/invalidated after the execution of this function, with a different
528 * action "returned" its place (pass-by-reference)
529 * @return True if curr is a newly-explored action; false otherwise
531 bool ModelExecution::initialize_curr_action(ModelAction **curr)
533 ModelAction *newcurr;
535 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
536 newcurr = process_rmw(*curr);
543 (*curr)->set_seq_number(get_next_seq_num());
545 newcurr = node_stack->explore_action(*curr);
547 /* First restore type and order in case of RMW operation */
548 if ((*curr)->is_rmwr())
549 newcurr->copy_typeandorder(*curr);
551 ASSERT((*curr)->get_location() == newcurr->get_location());
552 newcurr->copy_from_new(*curr);
554 /* Discard duplicate ModelAction; use action from NodeStack */
557 /* Always compute new clock vector */
558 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
561 return false; /* Action was explored previously */
565 /* Always compute new clock vector */
566 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
568 /* Assign most recent release fence */
569 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
571 return true; /* This was a new ModelAction */
576 * @brief Establish reads-from relation between two actions
578 * Perform basic operations involved with establishing a concrete rf relation,
579 * including setting the ModelAction data and checking for release sequences.
581 * @param act The action that is reading (must be a read)
582 * @param rf The action from which we are reading (must be a write)
584 * @return True if this read established synchronization
587 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
590 ASSERT(rf->is_write());
592 act->set_read_from(rf);
593 if (act->is_acquire()) {
594 rel_heads_list_t release_heads;
595 get_release_seq_heads(act, act, &release_heads);
596 int num_heads = release_heads.size();
597 for (unsigned int i = 0;i < release_heads.size();i++)
598 if (!synchronize(release_heads[i], act))
600 return num_heads > 0;
606 * @brief Synchronizes two actions
608 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
609 * This function performs the synchronization as well as providing other hooks
610 * for other checks along with synchronization.
612 * @param first The left-hand side of the synchronizes-with relation
613 * @param second The right-hand side of the synchronizes-with relation
614 * @return True if the synchronization was successful (i.e., was consistent
615 * with the execution order); false otherwise
617 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
619 if (*second < *first) {
620 set_bad_synchronization();
623 return second->synchronize_with(first);
627 * @brief Check whether a model action is enabled.
629 * Checks whether an operation would be successful (i.e., is a lock already
630 * locked, or is the joined thread already complete).
632 * For yield-blocking, yields are never enabled.
634 * @param curr is the ModelAction to check whether it is enabled.
635 * @return a bool that indicates whether the action is enabled.
637 bool ModelExecution::check_action_enabled(ModelAction *curr) {
638 if (curr->is_lock()) {
639 cdsc::mutex *lock = curr->get_mutex();
640 struct cdsc::mutex_state *state = lock->get_state();
643 } else if (curr->is_thread_join()) {
644 Thread *blocking = curr->get_thread_operand();
645 if (!blocking->is_complete()) {
654 * This is the heart of the model checker routine. It performs model-checking
655 * actions corresponding to a given "current action." Among other processes, it
656 * calculates reads-from relationships, updates synchronization clock vectors,
657 * forms a memory_order constraints graph, and handles replay/backtrack
658 * execution when running permutations of previously-observed executions.
660 * @param curr The current action to process
661 * @return The ModelAction that is actually executed; may be different than
664 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
667 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
668 bool newly_explored = initialize_curr_action(&curr);
672 wake_up_sleeping_actions(curr);
674 /* Add the action to lists before any other model-checking tasks */
675 if (!second_part_of_rmw && curr->get_type() != NOOP)
676 add_action_to_lists(curr);
678 SnapVector<const ModelAction *> * rf_set = NULL;
679 /* Build may_read_from set for newly-created actions */
680 if (newly_explored && curr->is_read())
681 rf_set = build_may_read_from(curr);
683 process_thread_action(curr);
685 if (curr->is_read() && !second_part_of_rmw) {
686 process_read(curr, rf_set);
689 ASSERT(rf_set == NULL);
692 if (curr->is_write())
695 if (curr->is_fence())
698 if (curr->is_mutex_op())
705 * This is the strongest feasibility check available.
706 * @return whether the current trace (partial or complete) must be a prefix of
709 bool ModelExecution::isfeasibleprefix() const
711 return !is_infeasible();
715 * Print disagnostic information about an infeasible execution
716 * @param prefix A string to prefix the output with; if NULL, then a default
717 * message prefix will be provided
719 void ModelExecution::print_infeasibility(const char *prefix) const
723 if (priv->bad_synchronization)
724 ptr += sprintf(ptr, "[bad sw ordering]");
726 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
730 * Check if the current partial trace is infeasible. Does not check any
731 * end-of-execution flags, which might rule out the execution. Thus, this is
732 * useful only for ruling an execution as infeasible.
733 * @return whether the current partial trace is infeasible.
735 bool ModelExecution::is_infeasible() const
737 return priv->bad_synchronization;
740 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
741 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
742 ModelAction *lastread = get_last_action(act->get_tid());
743 lastread->process_rmw(act);
745 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
751 * @brief Updates the mo_graph with the constraints imposed from the current
754 * Basic idea is the following: Go through each other thread and find
755 * the last action that happened before our read. Two cases:
757 * -# The action is a write: that write must either occur before
758 * the write we read from or be the write we read from.
759 * -# The action is a read: the write that that action read from
760 * must occur before the write we read from or be the same write.
762 * @param curr The current action. Must be a read.
763 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
764 * @return True if modification order edges were added; false otherwise
767 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset)
769 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
771 ASSERT(curr->is_read());
773 /* Last SC fence in the current thread */
774 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
775 ModelAction *last_sc_write = NULL;
776 if (curr->is_seqcst())
777 last_sc_write = get_last_seq_cst_write(curr);
779 int tid = curr->get_tid();
780 ModelAction *prev_same_thread = NULL;
781 /* Iterate over all threads */
782 for (i = 0;i < thrd_lists->size();i++, tid = ((tid+1) == thrd_lists->size()) ? 0: tid + 1) {
783 /* Last SC fence in thread tid */
784 ModelAction *last_sc_fence_thread_local = NULL;
786 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
788 /* Last SC fence in thread tid, before last SC fence in current thread */
789 ModelAction *last_sc_fence_thread_before = NULL;
790 if (last_sc_fence_local)
791 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
793 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
794 if (prev_same_thread != NULL &&
795 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
796 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
800 /* Iterate over actions in thread, starting from most recent */
801 action_list_t *list = &(*thrd_lists)[tid];
802 action_list_t::reverse_iterator rit;
803 for (rit = list->rbegin();rit != list->rend();rit++) {
804 ModelAction *act = *rit;
809 /* Don't want to add reflexive edges on 'rf' */
810 if (act->equals(rf)) {
811 if (act->happens_before(curr))
817 if (act->is_write()) {
818 /* C++, Section 29.3 statement 5 */
819 if (curr->is_seqcst() && last_sc_fence_thread_local &&
820 *act < *last_sc_fence_thread_local) {
821 if (mo_graph->checkReachable(rf, act))
823 priorset->push_back(act);
826 /* C++, Section 29.3 statement 4 */
827 else if (act->is_seqcst() && last_sc_fence_local &&
828 *act < *last_sc_fence_local) {
829 if (mo_graph->checkReachable(rf, act))
831 priorset->push_back(act);
834 /* C++, Section 29.3 statement 6 */
835 else if (last_sc_fence_thread_before &&
836 *act < *last_sc_fence_thread_before) {
837 if (mo_graph->checkReachable(rf, act))
839 priorset->push_back(act);
845 * Include at most one act per-thread that "happens
848 if (act->happens_before(curr)) {
850 if (last_sc_fence_local == NULL ||
851 (*last_sc_fence_local < *prev_same_thread)) {
852 prev_same_thread = act;
855 if (act->is_write()) {
856 if (mo_graph->checkReachable(rf, act))
858 priorset->push_back(act);
860 const ModelAction *prevrf = act->get_reads_from();
861 if (!prevrf->equals(rf)) {
862 if (mo_graph->checkReachable(rf, prevrf))
864 priorset->push_back(prevrf);
875 * Updates the mo_graph with the constraints imposed from the current write.
877 * Basic idea is the following: Go through each other thread and find
878 * the lastest action that happened before our write. Two cases:
880 * (1) The action is a write => that write must occur before
883 * (2) The action is a read => the write that that action read from
884 * must occur before the current write.
886 * This method also handles two other issues:
888 * (I) Sequential Consistency: Making sure that if the current write is
889 * seq_cst, that it occurs after the previous seq_cst write.
891 * (II) Sending the write back to non-synchronizing reads.
893 * @param curr The current action. Must be a write.
894 * @param send_fv A vector for stashing reads to which we may pass our future
895 * value. If NULL, then don't record any future values.
896 * @return True if modification order edges were added; false otherwise
898 void ModelExecution::w_modification_order(ModelAction *curr)
900 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
902 ASSERT(curr->is_write());
904 if (curr->is_seqcst()) {
905 /* We have to at least see the last sequentially consistent write,
906 so we are initialized. */
907 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
908 if (last_seq_cst != NULL) {
909 mo_graph->addEdge(last_seq_cst, curr);
913 /* Last SC fence in the current thread */
914 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
916 /* Iterate over all threads */
917 for (i = 0;i < thrd_lists->size();i++) {
918 /* Last SC fence in thread i, before last SC fence in current thread */
919 ModelAction *last_sc_fence_thread_before = NULL;
920 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
921 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
923 /* Iterate over actions in thread, starting from most recent */
924 action_list_t *list = &(*thrd_lists)[i];
925 action_list_t::reverse_iterator rit;
926 bool force_edge = false;
927 for (rit = list->rbegin();rit != list->rend();rit++) {
928 ModelAction *act = *rit;
931 * 1) If RMW and it actually read from something, then we
932 * already have all relevant edges, so just skip to next
935 * 2) If RMW and it didn't read from anything, we should
936 * whatever edge we can get to speed up convergence.
938 * 3) If normal write, we need to look at earlier actions, so
939 * continue processing list.
942 if (curr->is_rmw()) {
943 if (curr->get_reads_from() != NULL)
951 /* C++, Section 29.3 statement 7 */
952 if (last_sc_fence_thread_before && act->is_write() &&
953 *act < *last_sc_fence_thread_before) {
954 mo_graph->addEdge(act, curr, force_edge);
959 * Include at most one act per-thread that "happens
962 if (act->happens_before(curr)) {
964 * Note: if act is RMW, just add edge:
966 * The following edge should be handled elsewhere:
967 * readfrom(act) --mo--> act
970 mo_graph->addEdge(act, curr, force_edge);
971 else if (act->is_read()) {
972 //if previous read accessed a null, just keep going
973 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
976 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
977 !act->same_thread(curr)) {
978 /* We have an action that:
979 (1) did not happen before us
980 (2) is a read and we are a write
981 (3) cannot synchronize with us
982 (4) is in a different thread
984 that read could potentially read from our write. Note that
985 these checks are overly conservative at this point, we'll
986 do more checks before actually removing the
997 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
998 * some constraints. This method checks one the following constraint (others
999 * require compiler support):
1001 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1002 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1004 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1006 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1008 /* Iterate over all threads */
1009 for (i = 0;i < thrd_lists->size();i++) {
1010 const ModelAction *write_after_read = NULL;
1012 /* Iterate over actions in thread, starting from most recent */
1013 action_list_t *list = &(*thrd_lists)[i];
1014 action_list_t::reverse_iterator rit;
1015 for (rit = list->rbegin();rit != list->rend();rit++) {
1016 ModelAction *act = *rit;
1018 /* Don't disallow due to act == reader */
1019 if (!reader->happens_before(act) || reader == act)
1021 else if (act->is_write())
1022 write_after_read = act;
1023 else if (act->is_read() && act->get_reads_from() != NULL)
1024 write_after_read = act->get_reads_from();
1027 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1034 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1035 * The ModelAction under consideration is expected to be taking part in
1036 * release/acquire synchronization as an object of the "reads from" relation.
1037 * Note that this can only provide release sequence support for RMW chains
1038 * which do not read from the future, as those actions cannot be traced until
1039 * their "promise" is fulfilled. Similarly, we may not even establish the
1040 * presence of a release sequence with certainty, as some modification order
1041 * constraints may be decided further in the future. Thus, this function
1042 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1043 * and a boolean representing certainty.
1045 * @param rf The action that might be part of a release sequence. Must be a
1047 * @param release_heads A pass-by-reference style return parameter. After
1048 * execution of this function, release_heads will contain the heads of all the
1049 * relevant release sequences, if any exists with certainty
1050 * @return true, if the ModelExecution is certain that release_heads is complete;
1053 bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
1056 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1057 ASSERT(rf->is_write());
1059 if (rf->is_release())
1060 release_heads->push_back(rf);
1061 else if (rf->get_last_fence_release())
1062 release_heads->push_back(rf->get_last_fence_release());
1064 break;/* End of RMW chain */
1066 /** @todo Need to be smarter here... In the linux lock
1067 * example, this will run to the beginning of the program for
1069 /** @todo The way to be smarter here is to keep going until 1
1070 * thread has a release preceded by an acquire and you've seen
1073 /* acq_rel RMW is a sufficient stopping condition */
1074 if (rf->is_acquire() && rf->is_release())
1075 return true;/* complete */
1077 ASSERT(rf); // Needs to be real write
1079 if (rf->is_release())
1080 return true;/* complete */
1082 /* else relaxed write
1083 * - check for fence-release in the same thread (29.8, stmt. 3)
1084 * - check modification order for contiguous subsequence
1085 * -> rf must be same thread as release */
1087 const ModelAction *fence_release = rf->get_last_fence_release();
1088 /* Synchronize with a fence-release unconditionally; we don't need to
1089 * find any more "contiguous subsequence..." for it */
1091 release_heads->push_back(fence_release);
1093 return true; /* complete */
1097 * An interface for getting the release sequence head(s) with which a
1098 * given ModelAction must synchronize. This function only returns a non-empty
1099 * result when it can locate a release sequence head with certainty. Otherwise,
1100 * it may mark the internal state of the ModelExecution so that it will handle
1101 * the release sequence at a later time, causing @a acquire to update its
1102 * synchronization at some later point in execution.
1104 * @param acquire The 'acquire' action that may synchronize with a release
1106 * @param read The read action that may read from a release sequence; this may
1107 * be the same as acquire, or else an earlier action in the same thread (i.e.,
1108 * when 'acquire' is a fence-acquire)
1109 * @param release_heads A pass-by-reference return parameter. Will be filled
1110 * with the head(s) of the release sequence(s), if they exists with certainty.
1111 * @see ModelExecution::release_seq_heads
1113 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
1114 ModelAction *read, rel_heads_list_t *release_heads)
1116 const ModelAction *rf = read->get_reads_from();
1118 release_seq_heads(rf, release_heads);
1122 * Performs various bookkeeping operations for the current ModelAction. For
1123 * instance, adds action to the per-object, per-thread action vector and to the
1124 * action trace list of all thread actions.
1126 * @param act is the ModelAction to add.
1128 void ModelExecution::add_action_to_lists(ModelAction *act)
1130 int tid = id_to_int(act->get_tid());
1131 ModelAction *uninit = NULL;
1133 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1134 if (list->empty() && act->is_atomic_var()) {
1135 uninit = get_uninitialized_action(act);
1136 uninit_id = id_to_int(uninit->get_tid());
1137 list->push_front(uninit);
1139 list->push_back(act);
1141 action_trace.push_back(act);
1143 action_trace.push_front(uninit);
1145 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1146 if (tid >= (int)vec->size())
1147 vec->resize(priv->next_thread_id);
1148 (*vec)[tid].push_back(act);
1150 (*vec)[uninit_id].push_front(uninit);
1152 if ((int)thrd_last_action.size() <= tid)
1153 thrd_last_action.resize(get_num_threads());
1154 thrd_last_action[tid] = act;
1156 thrd_last_action[uninit_id] = uninit;
1158 if (act->is_fence() && act->is_release()) {
1159 if ((int)thrd_last_fence_release.size() <= tid)
1160 thrd_last_fence_release.resize(get_num_threads());
1161 thrd_last_fence_release[tid] = act;
1164 if (act->is_wait()) {
1165 void *mutex_loc = (void *) act->get_value();
1166 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1168 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1169 if (tid >= (int)vec->size())
1170 vec->resize(priv->next_thread_id);
1171 (*vec)[tid].push_back(act);
1176 * @brief Get the last action performed by a particular Thread
1177 * @param tid The thread ID of the Thread in question
1178 * @return The last action in the thread
1180 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1182 int threadid = id_to_int(tid);
1183 if (threadid < (int)thrd_last_action.size())
1184 return thrd_last_action[id_to_int(tid)];
1190 * @brief Get the last fence release performed by a particular Thread
1191 * @param tid The thread ID of the Thread in question
1192 * @return The last fence release in the thread, if one exists; NULL otherwise
1194 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1196 int threadid = id_to_int(tid);
1197 if (threadid < (int)thrd_last_fence_release.size())
1198 return thrd_last_fence_release[id_to_int(tid)];
1204 * Gets the last memory_order_seq_cst write (in the total global sequence)
1205 * performed on a particular object (i.e., memory location), not including the
1207 * @param curr The current ModelAction; also denotes the object location to
1209 * @return The last seq_cst write
1211 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1213 void *location = curr->get_location();
1214 action_list_t *list = obj_map.get(location);
1215 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1216 action_list_t::reverse_iterator rit;
1217 for (rit = list->rbegin();(*rit) != curr;rit++)
1219 rit++; /* Skip past curr */
1220 for ( ;rit != list->rend();rit++)
1221 if ((*rit)->is_write() && (*rit)->is_seqcst())
1227 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1228 * performed in a particular thread, prior to a particular fence.
1229 * @param tid The ID of the thread to check
1230 * @param before_fence The fence from which to begin the search; if NULL, then
1231 * search for the most recent fence in the thread.
1232 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1234 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1236 /* All fences should have location FENCE_LOCATION */
1237 action_list_t *list = obj_map.get(FENCE_LOCATION);
1242 action_list_t::reverse_iterator rit = list->rbegin();
1245 for (;rit != list->rend();rit++)
1246 if (*rit == before_fence)
1249 ASSERT(*rit == before_fence);
1253 for (;rit != list->rend();rit++)
1254 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1260 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1261 * location). This function identifies the mutex according to the current
1262 * action, which is presumed to perform on the same mutex.
1263 * @param curr The current ModelAction; also denotes the object location to
1265 * @return The last unlock operation
1267 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1269 void *location = curr->get_location();
1271 action_list_t *list = obj_map.get(location);
1272 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1273 action_list_t::reverse_iterator rit;
1274 for (rit = list->rbegin();rit != list->rend();rit++)
1275 if ((*rit)->is_unlock() || (*rit)->is_wait())
1280 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1282 ModelAction *parent = get_last_action(tid);
1284 parent = get_thread(tid)->get_creation();
1289 * Returns the clock vector for a given thread.
1290 * @param tid The thread whose clock vector we want
1291 * @return Desired clock vector
1293 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1295 return get_parent_action(tid)->get_cv();
1298 bool valequals(uint64_t val1, uint64_t val2, int size) {
1301 return ((uint8_t)val1) == ((uint8_t)val2);
1303 return ((uint16_t)val1) == ((uint16_t)val2);
1305 return ((uint32_t)val1) == ((uint32_t)val2);
1315 * Build up an initial set of all past writes that this 'read' action may read
1316 * from, as well as any previously-observed future values that must still be valid.
1318 * @param curr is the current ModelAction that we are exploring; it must be a
1321 SnapVector<const ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1323 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1325 ASSERT(curr->is_read());
1327 ModelAction *last_sc_write = NULL;
1329 if (curr->is_seqcst())
1330 last_sc_write = get_last_seq_cst_write(curr);
1332 SnapVector<const ModelAction *> * rf_set = new SnapVector<const ModelAction *>();
1334 /* Iterate over all threads */
1335 for (i = 0;i < thrd_lists->size();i++) {
1336 /* Iterate over actions in thread, starting from most recent */
1337 action_list_t *list = &(*thrd_lists)[i];
1338 action_list_t::reverse_iterator rit;
1339 for (rit = list->rbegin();rit != list->rend();rit++) {
1340 const ModelAction *act = *rit;
1342 /* Only consider 'write' actions */
1343 if (!act->is_write()) {
1344 if (act != curr && act->is_read() && act->happens_before(curr)) {
1345 const ModelAction *tmp = act->get_reads_from();
1346 if (((unsigned int) id_to_int(tmp->get_tid()))==i)
1357 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1358 bool allow_read = true;
1360 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1363 /* Need to check whether we will have two RMW reading from the same value */
1364 if (curr->is_rmwr()) {
1365 /* It is okay if we have a failing CAS */
1366 if (!curr->is_rmwrcas() ||
1367 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1368 //Need to make sure we aren't the second RMW
1369 CycleNode * node = mo_graph->getNode_noCreate(act);
1370 if (node != NULL && node->getRMW() != NULL) {
1371 //we are the second RMW
1378 /* Only add feasible reads */
1379 rf_set->push_back(act);
1382 /* Include at most one act per-thread that "happens before" curr */
1383 if (act->happens_before(curr))
1388 if (DBG_ENABLED()) {
1389 model_print("Reached read action:\n");
1391 model_print("End printing read_from_past\n");
1397 * @brief Get an action representing an uninitialized atomic
1399 * This function may create a new one or try to retrieve one from the NodeStack
1401 * @param curr The current action, which prompts the creation of an UNINIT action
1402 * @return A pointer to the UNINIT ModelAction
1404 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1406 Node *node = curr->get_node();
1407 ModelAction *act = node->get_uninit_action();
1409 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1410 node->set_uninit_action(act);
1412 act->create_cv(NULL);
1416 static void print_list(const action_list_t *list)
1418 action_list_t::const_iterator it;
1420 model_print("------------------------------------------------------------------------------------\n");
1421 model_print("# t Action type MO Location Value Rf CV\n");
1422 model_print("------------------------------------------------------------------------------------\n");
1424 unsigned int hash = 0;
1426 for (it = list->begin();it != list->end();it++) {
1427 const ModelAction *act = *it;
1428 if (act->get_seq_number() > 0)
1430 hash = hash^(hash<<3)^((*it)->hash());
1432 model_print("HASH %u\n", hash);
1433 model_print("------------------------------------------------------------------------------------\n");
1436 #if SUPPORT_MOD_ORDER_DUMP
1437 void ModelExecution::dumpGraph(char *filename) const
1440 sprintf(buffer, "%s.dot", filename);
1441 FILE *file = fopen(buffer, "w");
1442 fprintf(file, "digraph %s {\n", filename);
1443 mo_graph->dumpNodes(file);
1444 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1446 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1447 ModelAction *act = *it;
1448 if (act->is_read()) {
1449 mo_graph->dot_print_node(file, act);
1450 mo_graph->dot_print_edge(file,
1451 act->get_reads_from(),
1453 "label=\"rf\", color=red, weight=2");
1455 if (thread_array[act->get_tid()]) {
1456 mo_graph->dot_print_edge(file,
1457 thread_array[id_to_int(act->get_tid())],
1459 "label=\"sb\", color=blue, weight=400");
1462 thread_array[act->get_tid()] = act;
1464 fprintf(file, "}\n");
1465 model_free(thread_array);
1470 /** @brief Prints an execution trace summary. */
1471 void ModelExecution::print_summary() const
1473 #if SUPPORT_MOD_ORDER_DUMP
1474 char buffername[100];
1475 sprintf(buffername, "exec%04u", get_execution_number());
1476 mo_graph->dumpGraphToFile(buffername);
1477 sprintf(buffername, "graph%04u", get_execution_number());
1478 dumpGraph(buffername);
1481 model_print("Execution trace %d:", get_execution_number());
1482 if (isfeasibleprefix()) {
1483 if (scheduler->all_threads_sleeping())
1484 model_print(" SLEEP-SET REDUNDANT");
1485 if (have_bug_reports())
1486 model_print(" DETECTED BUG(S)");
1488 print_infeasibility(" INFEASIBLE");
1491 print_list(&action_trace);
1497 * Add a Thread to the system for the first time. Should only be called once
1499 * @param t The Thread to add
1501 void ModelExecution::add_thread(Thread *t)
1503 unsigned int i = id_to_int(t->get_id());
1504 if (i >= thread_map.size())
1505 thread_map.resize(i + 1);
1507 if (!t->is_model_thread())
1508 scheduler->add_thread(t);
1512 * @brief Get a Thread reference by its ID
1513 * @param tid The Thread's ID
1514 * @return A Thread reference
1516 Thread * ModelExecution::get_thread(thread_id_t tid) const
1518 unsigned int i = id_to_int(tid);
1519 if (i < thread_map.size())
1520 return thread_map[i];
1525 * @brief Get a reference to the Thread in which a ModelAction was executed
1526 * @param act The ModelAction
1527 * @return A Thread reference
1529 Thread * ModelExecution::get_thread(const ModelAction *act) const
1531 return get_thread(act->get_tid());
1535 * @brief Get a Thread reference by its pthread ID
1536 * @param index The pthread's ID
1537 * @return A Thread reference
1539 Thread * ModelExecution::get_pthread(pthread_t pid) {
1545 uint32_t thread_id = x.v;
1546 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1551 * @brief Check if a Thread is currently enabled
1552 * @param t The Thread to check
1553 * @return True if the Thread is currently enabled
1555 bool ModelExecution::is_enabled(Thread *t) const
1557 return scheduler->is_enabled(t);
1561 * @brief Check if a Thread is currently enabled
1562 * @param tid The ID of the Thread to check
1563 * @return True if the Thread is currently enabled
1565 bool ModelExecution::is_enabled(thread_id_t tid) const
1567 return scheduler->is_enabled(tid);
1571 * @brief Select the next thread to execute based on the curren action
1573 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1574 * actions should be followed by the execution of their child thread. In either
1575 * case, the current action should determine the next thread schedule.
1577 * @param curr The current action
1578 * @return The next thread to run, if the current action will determine this
1579 * selection; otherwise NULL
1581 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1583 /* Do not split atomic RMW */
1584 if (curr->is_rmwr())
1585 return get_thread(curr);
1586 if (curr->is_write()) {
1587 std::memory_order order = curr->get_mo();
1589 case std::memory_order_relaxed:
1590 return get_thread(curr);
1591 case std::memory_order_release:
1592 return get_thread(curr);
1598 /* Follow CREATE with the created thread */
1599 /* which is not needed, because model.cc takes care of this */
1600 if (curr->get_type() == THREAD_CREATE)
1601 return curr->get_thread_operand();
1602 if (curr->get_type() == PTHREAD_CREATE) {
1603 return curr->get_thread_operand();
1609 * Takes the next step in the execution, if possible.
1610 * @param curr The current step to take
1611 * @return Returns the next Thread to run, if any; NULL if this execution
1614 Thread * ModelExecution::take_step(ModelAction *curr)
1616 Thread *curr_thrd = get_thread(curr);
1617 ASSERT(curr_thrd->get_state() == THREAD_READY);
1619 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1620 curr = check_current_action(curr);
1623 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1624 scheduler->remove_thread(curr_thrd);
1626 return action_select_next_thread(curr);
1629 Fuzzer * ModelExecution::getFuzzer() {