11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #define INITIAL_THREAD_ID 0
21 * Structure for holding small ModelChecker members that should be snapshotted
23 struct model_snapshot_members {
24 model_snapshot_members() :
25 /* First thread created will have id INITIAL_THREAD_ID */
26 next_thread_id(INITIAL_THREAD_ID),
27 used_sequence_numbers(0),
29 bad_synchronization(false),
33 ~model_snapshot_members() {
34 for (unsigned int i = 0;i < bugs.size();i++)
39 unsigned int next_thread_id;
40 modelclock_t used_sequence_numbers;
41 SnapVector<bug_message *> bugs;
42 /** @brief Incorrectly-ordered synchronization was made */
43 bool bad_synchronization;
49 /** @brief Constructor */
50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
55 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
63 thrd_last_fence_release(),
64 priv(new struct model_snapshot_members ()),
65 mo_graph(new CycleGraph()),
68 /* Initialize a model-checker thread, for special ModelActions */
69 model_thread = new Thread(get_next_id());
70 add_thread(model_thread);
71 scheduler->register_engine(this);
74 /** @brief Destructor */
75 ModelExecution::~ModelExecution()
77 for (unsigned int i = 0;i < get_num_threads();i++)
78 delete get_thread(int_to_id(i));
84 int ModelExecution::get_execution_number() const
86 return model->get_execution_number();
89 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
91 action_list_t *tmp = hash->get(ptr);
93 tmp = new action_list_t();
99 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
101 SnapVector<action_list_t> *tmp = hash->get(ptr);
103 tmp = new SnapVector<action_list_t>();
109 /** @return a thread ID for a new Thread */
110 thread_id_t ModelExecution::get_next_id()
112 return priv->next_thread_id++;
115 /** @return the number of user threads created during this execution */
116 unsigned int ModelExecution::get_num_threads() const
118 return priv->next_thread_id;
121 /** @return a sequence number for a new ModelAction */
122 modelclock_t ModelExecution::get_next_seq_num()
124 return ++priv->used_sequence_numbers;
128 * @brief Should the current action wake up a given thread?
130 * @param curr The current action
131 * @param thread The thread that we might wake up
132 * @return True, if we should wake up the sleeping thread; false otherwise
134 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
136 const ModelAction *asleep = thread->get_pending();
137 /* Don't allow partial RMW to wake anyone up */
140 /* Synchronizing actions may have been backtracked */
141 if (asleep->could_synchronize_with(curr))
143 /* All acquire/release fences and fence-acquire/store-release */
144 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
146 /* Fence-release + store can awake load-acquire on the same location */
147 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
148 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
149 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
155 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
157 for (unsigned int i = 0;i < get_num_threads();i++) {
158 Thread *thr = get_thread(int_to_id(i));
159 if (scheduler->is_sleep_set(thr)) {
160 if (should_wake_up(curr, thr))
161 /* Remove this thread from sleep set */
162 scheduler->remove_sleep(thr);
167 /** @brief Alert the model-checker that an incorrectly-ordered
168 * synchronization was made */
169 void ModelExecution::set_bad_synchronization()
171 priv->bad_synchronization = true;
174 bool ModelExecution::assert_bug(const char *msg)
176 priv->bugs.push_back(new bug_message(msg));
178 if (isfeasibleprefix()) {
185 /** @return True, if any bugs have been reported for this execution */
186 bool ModelExecution::have_bug_reports() const
188 return priv->bugs.size() != 0;
191 SnapVector<bug_message *> * ModelExecution::get_bugs() const
197 * Check whether the current trace has triggered an assertion which should halt
200 * @return True, if the execution should be aborted; false otherwise
202 bool ModelExecution::has_asserted() const
204 return priv->asserted;
208 * Trigger a trace assertion which should cause this execution to be halted.
209 * This can be due to a detected bug or due to an infeasibility that should
212 void ModelExecution::set_assert()
214 priv->asserted = true;
218 * Check if we are in a deadlock. Should only be called at the end of an
219 * execution, although it should not give false positives in the middle of an
220 * execution (there should be some ENABLED thread).
222 * @return True if program is in a deadlock; false otherwise
224 bool ModelExecution::is_deadlocked() const
226 bool blocking_threads = false;
227 for (unsigned int i = 0;i < get_num_threads();i++) {
228 thread_id_t tid = int_to_id(i);
231 Thread *t = get_thread(tid);
232 if (!t->is_model_thread() && t->get_pending())
233 blocking_threads = true;
235 return blocking_threads;
239 * Check if this is a complete execution. That is, have all thread completed
240 * execution (rather than exiting because sleep sets have forced a redundant
243 * @return True if the execution is complete.
245 bool ModelExecution::is_complete_execution() const
247 for (unsigned int i = 0;i < get_num_threads();i++)
248 if (is_enabled(int_to_id(i)))
255 * Processes a read model action.
256 * @param curr is the read model action to process.
257 * @param rf_set is the set of model actions we can possibly read from
258 * @return True if processing this read updates the mo_graph.
260 void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
262 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
265 int index = fuzzer->selectWrite(curr, rf_set);
266 ModelAction *rf = (*rf_set)[index];
270 bool canprune = false;
271 if (r_modification_order(curr, rf, priorset, &canprune)) {
272 for(unsigned int i=0;i<priorset->size();i++) {
273 mo_graph->addEdge((*priorset)[i], rf);
276 get_thread(curr)->set_return_value(curr->get_return_value());
278 if (canprune && curr->get_type() == ATOMIC_READ) {
279 int tid = id_to_int(curr->get_tid());
280 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
285 (*rf_set)[index] = rf_set->back();
291 * Processes a lock, trylock, or unlock model action. @param curr is
292 * the read model action to process.
294 * The try lock operation checks whether the lock is taken. If not,
295 * it falls to the normal lock operation case. If so, it returns
298 * The lock operation has already been checked that it is enabled, so
299 * it just grabs the lock and synchronizes with the previous unlock.
301 * The unlock operation has to re-enable all of the threads that are
302 * waiting on the lock.
304 * @return True if synchronization was updated; false otherwise
306 bool ModelExecution::process_mutex(ModelAction *curr)
308 cdsc::mutex *mutex = curr->get_mutex();
309 struct cdsc::mutex_state *state = NULL;
312 state = mutex->get_state();
314 switch (curr->get_type()) {
315 case ATOMIC_TRYLOCK: {
316 bool success = !state->locked;
317 curr->set_try_lock(success);
319 get_thread(curr)->set_return_value(0);
322 get_thread(curr)->set_return_value(1);
324 //otherwise fall into the lock case
326 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
327 assert_bug("Lock access before initialization");
328 state->locked = get_thread(curr);
329 ModelAction *unlock = get_last_unlock(curr);
330 //synchronize with the previous unlock statement
331 if (unlock != NULL) {
332 synchronize(unlock, curr);
338 case ATOMIC_UNLOCK: {
339 //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...
341 /* wake up the other threads */
342 for (unsigned int i = 0;i < get_num_threads();i++) {
343 Thread *t = get_thread(int_to_id(i));
344 Thread *curr_thrd = get_thread(curr);
345 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
349 /* unlock the lock - after checking who was waiting on it */
350 state->locked = NULL;
352 if (!curr->is_wait())
353 break;/* The rest is only for ATOMIC_WAIT */
357 case ATOMIC_NOTIFY_ALL: {
358 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
359 //activate all the waiting threads
360 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
361 scheduler->wake(get_thread(*rit));
366 case ATOMIC_NOTIFY_ONE: {
367 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
368 if (waiters->size() != 0) {
369 Thread * thread = fuzzer->selectNotify(waiters);
370 scheduler->wake(thread);
382 * Process a write ModelAction
383 * @param curr The ModelAction to process
384 * @return True if the mo_graph was updated or promises were resolved
386 void ModelExecution::process_write(ModelAction *curr)
389 w_modification_order(curr);
392 get_thread(curr)->set_return_value(VALUE_NONE);
396 * Process a fence ModelAction
397 * @param curr The ModelAction to process
398 * @return True if synchronization was updated
400 bool ModelExecution::process_fence(ModelAction *curr)
403 * fence-relaxed: no-op
404 * fence-release: only log the occurence (not in this function), for
405 * use in later synchronization
406 * fence-acquire (this function): search for hypothetical release
408 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
410 bool updated = false;
411 if (curr->is_acquire()) {
412 action_list_t *list = &action_trace;
413 action_list_t::reverse_iterator rit;
414 /* Find X : is_read(X) && X --sb-> curr */
415 for (rit = list->rbegin();rit != list->rend();rit++) {
416 ModelAction *act = *rit;
419 if (act->get_tid() != curr->get_tid())
421 /* Stop at the beginning of the thread */
422 if (act->is_thread_start())
424 /* Stop once we reach a prior fence-acquire */
425 if (act->is_fence() && act->is_acquire())
429 /* read-acquire will find its own release sequences */
430 if (act->is_acquire())
433 /* Establish hypothetical release sequences */
434 ClockVector *cv = get_hb_from_write(act);
435 if (curr->get_cv()->merge(cv))
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,
523 * 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 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
534 ModelAction *newcurr = process_rmw(*curr);
540 ModelAction *newcurr = *curr;
542 newcurr->set_seq_number(get_next_seq_num());
543 /* Always compute new clock vector */
544 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
546 /* Assign most recent release fence */
547 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
549 return true; /* This was a new ModelAction */
554 * @brief Establish reads-from relation between two actions
556 * Perform basic operations involved with establishing a concrete rf relation,
557 * including setting the ModelAction data and checking for release sequences.
559 * @param act The action that is reading (must be a read)
560 * @param rf The action from which we are reading (must be a write)
562 * @return True if this read established synchronization
565 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
568 ASSERT(rf->is_write());
570 act->set_read_from(rf);
571 if (act->is_acquire()) {
572 ClockVector *cv = get_hb_from_write(rf);
575 act->get_cv()->merge(cv);
580 * @brief Synchronizes two actions
582 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
583 * This function performs the synchronization as well as providing other hooks
584 * for other checks along with synchronization.
586 * @param first The left-hand side of the synchronizes-with relation
587 * @param second The right-hand side of the synchronizes-with relation
588 * @return True if the synchronization was successful (i.e., was consistent
589 * with the execution order); false otherwise
591 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
593 if (*second < *first) {
594 set_bad_synchronization();
597 return second->synchronize_with(first);
601 * @brief Check whether a model action is enabled.
603 * Checks whether an operation would be successful (i.e., is a lock already
604 * locked, or is the joined thread already complete).
606 * For yield-blocking, yields are never enabled.
608 * @param curr is the ModelAction to check whether it is enabled.
609 * @return a bool that indicates whether the action is enabled.
611 bool ModelExecution::check_action_enabled(ModelAction *curr) {
612 if (curr->is_lock()) {
613 cdsc::mutex *lock = curr->get_mutex();
614 struct cdsc::mutex_state *state = lock->get_state();
617 } else if (curr->is_thread_join()) {
618 Thread *blocking = curr->get_thread_operand();
619 if (!blocking->is_complete()) {
628 * This is the heart of the model checker routine. It performs model-checking
629 * actions corresponding to a given "current action." Among other processes, it
630 * calculates reads-from relationships, updates synchronization clock vectors,
631 * forms a memory_order constraints graph, and handles replay/backtrack
632 * execution when running permutations of previously-observed executions.
634 * @param curr The current action to process
635 * @return The ModelAction that is actually executed; may be different than
638 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
641 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
642 bool newly_explored = initialize_curr_action(&curr);
646 wake_up_sleeping_actions(curr);
648 /* Add the action to lists before any other model-checking tasks */
649 if (!second_part_of_rmw && curr->get_type() != NOOP)
650 add_action_to_lists(curr);
652 if (curr->is_write())
653 add_write_to_lists(curr);
655 SnapVector<ModelAction *> * rf_set = NULL;
656 /* Build may_read_from set for newly-created actions */
657 if (newly_explored && curr->is_read())
658 rf_set = build_may_read_from(curr);
660 process_thread_action(curr);
662 if (curr->is_read() && !second_part_of_rmw) {
663 process_read(curr, rf_set);
666 ASSERT(rf_set == NULL);
669 if (curr->is_write())
672 if (curr->is_fence())
675 if (curr->is_mutex_op())
682 * This is the strongest feasibility check available.
683 * @return whether the current trace (partial or complete) must be a prefix of
686 bool ModelExecution::isfeasibleprefix() const
688 return !is_infeasible();
692 * Print disagnostic information about an infeasible execution
693 * @param prefix A string to prefix the output with; if NULL, then a default
694 * message prefix will be provided
696 void ModelExecution::print_infeasibility(const char *prefix) const
700 if (priv->bad_synchronization)
701 ptr += sprintf(ptr, "[bad sw ordering]");
703 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
707 * Check if the current partial trace is infeasible. Does not check any
708 * end-of-execution flags, which might rule out the execution. Thus, this is
709 * useful only for ruling an execution as infeasible.
710 * @return whether the current partial trace is infeasible.
712 bool ModelExecution::is_infeasible() const
714 return priv->bad_synchronization;
717 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
718 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
719 ModelAction *lastread = get_last_action(act->get_tid());
720 lastread->process_rmw(act);
722 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
728 * @brief Updates the mo_graph with the constraints imposed from the current
731 * Basic idea is the following: Go through each other thread and find
732 * the last action that happened before our read. Two cases:
734 * -# The action is a write: that write must either occur before
735 * the write we read from or be the write we read from.
736 * -# The action is a read: the write that that action read from
737 * must occur before the write we read from or be the same write.
739 * @param curr The current action. Must be a read.
740 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
741 * @return True if modification order edges were added; false otherwise
744 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
746 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
748 ASSERT(curr->is_read());
750 /* Last SC fence in the current thread */
751 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
753 int tid = curr->get_tid();
754 ModelAction *prev_same_thread = NULL;
755 /* Iterate over all threads */
756 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
757 /* Last SC fence in thread tid */
758 ModelAction *last_sc_fence_thread_local = NULL;
760 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
762 /* Last SC fence in thread tid, before last SC fence in current thread */
763 ModelAction *last_sc_fence_thread_before = NULL;
764 if (last_sc_fence_local)
765 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
767 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
768 if (prev_same_thread != NULL &&
769 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
770 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
774 /* Iterate over actions in thread, starting from most recent */
775 action_list_t *list = &(*thrd_lists)[tid];
776 action_list_t::reverse_iterator rit;
777 for (rit = list->rbegin();rit != list->rend();rit++) {
778 ModelAction *act = *rit;
783 /* Don't want to add reflexive edges on 'rf' */
784 if (act->equals(rf)) {
785 if (act->happens_before(curr))
791 if (act->is_write()) {
792 /* C++, Section 29.3 statement 5 */
793 if (curr->is_seqcst() && last_sc_fence_thread_local &&
794 *act < *last_sc_fence_thread_local) {
795 if (mo_graph->checkReachable(rf, act))
797 priorset->push_back(act);
800 /* C++, Section 29.3 statement 4 */
801 else if (act->is_seqcst() && last_sc_fence_local &&
802 *act < *last_sc_fence_local) {
803 if (mo_graph->checkReachable(rf, act))
805 priorset->push_back(act);
808 /* C++, Section 29.3 statement 6 */
809 else if (last_sc_fence_thread_before &&
810 *act < *last_sc_fence_thread_before) {
811 if (mo_graph->checkReachable(rf, act))
813 priorset->push_back(act);
819 * Include at most one act per-thread that "happens
822 if (act->happens_before(curr)) {
824 if (last_sc_fence_local == NULL ||
825 (*last_sc_fence_local < *prev_same_thread)) {
826 prev_same_thread = act;
829 if (act->is_write()) {
830 if (mo_graph->checkReachable(rf, act))
832 priorset->push_back(act);
834 const ModelAction *prevrf = act->get_reads_from();
835 if (!prevrf->equals(rf)) {
836 if (mo_graph->checkReachable(rf, prevrf))
838 priorset->push_back(prevrf);
840 if (act->get_tid() == curr->get_tid()) {
841 //Can prune curr from obj list
854 * Updates the mo_graph with the constraints imposed from the current write.
856 * Basic idea is the following: Go through each other thread and find
857 * the lastest action that happened before our write. Two cases:
859 * (1) The action is a write => that write must occur before
862 * (2) The action is a read => the write that that action read from
863 * must occur before the current write.
865 * This method also handles two other issues:
867 * (I) Sequential Consistency: Making sure that if the current write is
868 * seq_cst, that it occurs after the previous seq_cst write.
870 * (II) Sending the write back to non-synchronizing reads.
872 * @param curr The current action. Must be a write.
873 * @param send_fv A vector for stashing reads to which we may pass our future
874 * value. If NULL, then don't record any future values.
875 * @return True if modification order edges were added; false otherwise
877 void ModelExecution::w_modification_order(ModelAction *curr)
879 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
881 ASSERT(curr->is_write());
883 if (curr->is_seqcst()) {
884 /* We have to at least see the last sequentially consistent write,
885 so we are initialized. */
886 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
887 if (last_seq_cst != NULL) {
888 mo_graph->addEdge(last_seq_cst, curr);
892 /* Last SC fence in the current thread */
893 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
895 /* Iterate over all threads */
896 for (i = 0;i < thrd_lists->size();i++) {
897 /* Last SC fence in thread i, before last SC fence in current thread */
898 ModelAction *last_sc_fence_thread_before = NULL;
899 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
900 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
902 /* Iterate over actions in thread, starting from most recent */
903 action_list_t *list = &(*thrd_lists)[i];
904 action_list_t::reverse_iterator rit;
905 bool force_edge = false;
906 for (rit = list->rbegin();rit != list->rend();rit++) {
907 ModelAction *act = *rit;
910 * 1) If RMW and it actually read from something, then we
911 * already have all relevant edges, so just skip to next
914 * 2) If RMW and it didn't read from anything, we should
915 * whatever edge we can get to speed up convergence.
917 * 3) If normal write, we need to look at earlier actions, so
918 * continue processing list.
921 if (curr->is_rmw()) {
922 if (curr->get_reads_from() != NULL)
930 /* C++, Section 29.3 statement 7 */
931 if (last_sc_fence_thread_before && act->is_write() &&
932 *act < *last_sc_fence_thread_before) {
933 mo_graph->addEdge(act, curr, force_edge);
938 * Include at most one act per-thread that "happens
941 if (act->happens_before(curr)) {
943 * Note: if act is RMW, just add edge:
945 * The following edge should be handled elsewhere:
946 * readfrom(act) --mo--> act
949 mo_graph->addEdge(act, curr, force_edge);
950 else if (act->is_read()) {
951 //if previous read accessed a null, just keep going
952 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
961 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
962 * some constraints. This method checks one the following constraint (others
963 * require compiler support):
965 * If X --hb-> Y --mo-> Z, then X should not read from Z.
966 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
968 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
970 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
972 /* Iterate over all threads */
973 for (i = 0;i < thrd_lists->size();i++) {
974 const ModelAction *write_after_read = NULL;
976 /* Iterate over actions in thread, starting from most recent */
977 action_list_t *list = &(*thrd_lists)[i];
978 action_list_t::reverse_iterator rit;
979 for (rit = list->rbegin();rit != list->rend();rit++) {
980 ModelAction *act = *rit;
982 /* Don't disallow due to act == reader */
983 if (!reader->happens_before(act) || reader == act)
985 else if (act->is_write())
986 write_after_read = act;
987 else if (act->is_read() && act->get_reads_from() != NULL)
988 write_after_read = act->get_reads_from();
991 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
998 * Computes the clock vector that happens before propagates from this write.
1000 * @param rf The action that might be part of a release sequence. Must be a
1002 * @return ClockVector of happens before relation.
1005 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1006 SnapVector<ModelAction *> * processset = NULL;
1007 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1008 ASSERT(rf->is_write());
1009 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1011 if (processset == NULL)
1012 processset = new SnapVector<ModelAction *>();
1013 processset->push_back(rf);
1016 int i = (processset == NULL) ? 0 : processset->size();
1018 ClockVector * vec = NULL;
1020 if (rf->get_rfcv() != NULL) {
1021 vec = rf->get_rfcv();
1022 } else if (rf->is_acquire() && rf->is_release()) {
1024 } else if (rf->is_release() && !rf->is_rmw()) {
1026 } else if (rf->is_release()) {
1027 //have rmw that is release and doesn't have a rfcv
1028 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1031 //operation that isn't release
1032 if (rf->get_last_fence_release()) {
1034 vec = rf->get_last_fence_release()->get_cv();
1036 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1042 rf = (*processset)[i];
1046 if (processset != NULL)
1052 * Performs various bookkeeping operations for the current ModelAction. For
1053 * instance, adds action to the per-object, per-thread action vector and to the
1054 * action trace list of all thread actions.
1056 * @param act is the ModelAction to add.
1058 void ModelExecution::add_action_to_lists(ModelAction *act)
1060 int tid = id_to_int(act->get_tid());
1061 ModelAction *uninit = NULL;
1063 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1064 if (list->empty() && act->is_atomic_var()) {
1065 uninit = get_uninitialized_action(act);
1066 uninit_id = id_to_int(uninit->get_tid());
1067 list->push_front(uninit);
1068 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1069 if (uninit_id >= (int)vec->size())
1070 vec->resize(uninit_id + 1);
1071 (*vec)[uninit_id].push_front(uninit);
1073 list->push_back(act);
1075 // Update action trace, a total order of all actions
1076 action_trace.push_back(act);
1078 action_trace.push_front(uninit);
1080 // Update obj_thrd_map, a per location, per thread, order of actions
1081 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1082 if (tid >= (int)vec->size())
1083 vec->resize(priv->next_thread_id);
1084 (*vec)[tid].push_back(act);
1086 (*vec)[uninit_id].push_front(uninit);
1088 // Update thrd_last_action, the last action taken by each thrad
1089 if ((int)thrd_last_action.size() <= tid)
1090 thrd_last_action.resize(get_num_threads());
1091 thrd_last_action[tid] = act;
1093 thrd_last_action[uninit_id] = uninit;
1095 // Update thrd_last_fence_release, the last release fence taken by each thread
1096 if (act->is_fence() && act->is_release()) {
1097 if ((int)thrd_last_fence_release.size() <= tid)
1098 thrd_last_fence_release.resize(get_num_threads());
1099 thrd_last_fence_release[tid] = act;
1102 if (act->is_wait()) {
1103 void *mutex_loc = (void *) act->get_value();
1104 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1106 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1107 if (tid >= (int)vec->size())
1108 vec->resize(priv->next_thread_id);
1109 (*vec)[tid].push_back(act);
1113 void ModelExecution::add_write_to_lists(ModelAction *write) {
1114 // Update seq_cst map
1115 if (write->is_seqcst())
1116 obj_last_sc_map.put(write->get_location(), write);
1118 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1119 int tid = id_to_int(write->get_tid());
1120 if (tid >= (int)vec->size())
1121 vec->resize(priv->next_thread_id);
1122 (*vec)[tid].push_back(write);
1126 * @brief Get the last action performed by a particular Thread
1127 * @param tid The thread ID of the Thread in question
1128 * @return The last action in the thread
1130 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1132 int threadid = id_to_int(tid);
1133 if (threadid < (int)thrd_last_action.size())
1134 return thrd_last_action[id_to_int(tid)];
1140 * @brief Get the last fence release performed by a particular Thread
1141 * @param tid The thread ID of the Thread in question
1142 * @return The last fence release in the thread, if one exists; NULL otherwise
1144 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1146 int threadid = id_to_int(tid);
1147 if (threadid < (int)thrd_last_fence_release.size())
1148 return thrd_last_fence_release[id_to_int(tid)];
1154 * Gets the last memory_order_seq_cst write (in the total global sequence)
1155 * performed on a particular object (i.e., memory location), not including the
1157 * @param curr The current ModelAction; also denotes the object location to
1159 * @return The last seq_cst write
1161 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1163 void *location = curr->get_location();
1164 return obj_last_sc_map.get(location);
1168 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1169 * performed in a particular thread, prior to a particular fence.
1170 * @param tid The ID of the thread to check
1171 * @param before_fence The fence from which to begin the search; if NULL, then
1172 * search for the most recent fence in the thread.
1173 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1175 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1177 /* All fences should have location FENCE_LOCATION */
1178 action_list_t *list = obj_map.get(FENCE_LOCATION);
1183 action_list_t::reverse_iterator rit = list->rbegin();
1186 for (;rit != list->rend();rit++)
1187 if (*rit == before_fence)
1190 ASSERT(*rit == before_fence);
1194 for (;rit != list->rend();rit++)
1195 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1201 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1202 * location). This function identifies the mutex according to the current
1203 * action, which is presumed to perform on the same mutex.
1204 * @param curr The current ModelAction; also denotes the object location to
1206 * @return The last unlock operation
1208 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1210 void *location = curr->get_location();
1212 action_list_t *list = obj_map.get(location);
1213 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1214 action_list_t::reverse_iterator rit;
1215 for (rit = list->rbegin();rit != list->rend();rit++)
1216 if ((*rit)->is_unlock() || (*rit)->is_wait())
1221 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1223 ModelAction *parent = get_last_action(tid);
1225 parent = get_thread(tid)->get_creation();
1230 * Returns the clock vector for a given thread.
1231 * @param tid The thread whose clock vector we want
1232 * @return Desired clock vector
1234 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1236 ModelAction *firstaction=get_parent_action(tid);
1237 return firstaction != NULL ? firstaction->get_cv() : NULL;
1240 bool valequals(uint64_t val1, uint64_t val2, int size) {
1243 return ((uint8_t)val1) == ((uint8_t)val2);
1245 return ((uint16_t)val1) == ((uint16_t)val2);
1247 return ((uint32_t)val1) == ((uint32_t)val2);
1257 * Build up an initial set of all past writes that this 'read' action may read
1258 * from, as well as any previously-observed future values that must still be valid.
1260 * @param curr is the current ModelAction that we are exploring; it must be a
1263 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1265 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1267 ASSERT(curr->is_read());
1269 ModelAction *last_sc_write = NULL;
1271 if (curr->is_seqcst())
1272 last_sc_write = get_last_seq_cst_write(curr);
1274 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1276 /* Iterate over all threads */
1277 for (i = 0;i < thrd_lists->size();i++) {
1278 /* Iterate over actions in thread, starting from most recent */
1279 action_list_t *list = &(*thrd_lists)[i];
1280 action_list_t::reverse_iterator rit;
1281 for (rit = list->rbegin();rit != list->rend();rit++) {
1282 ModelAction *act = *rit;
1287 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1288 bool allow_read = true;
1290 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1293 /* Need to check whether we will have two RMW reading from the same value */
1294 if (curr->is_rmwr()) {
1295 /* It is okay if we have a failing CAS */
1296 if (!curr->is_rmwrcas() ||
1297 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1298 //Need to make sure we aren't the second RMW
1299 CycleNode * node = mo_graph->getNode_noCreate(act);
1300 if (node != NULL && node->getRMW() != NULL) {
1301 //we are the second RMW
1308 /* Only add feasible reads */
1309 rf_set->push_back(act);
1312 /* Include at most one act per-thread that "happens before" curr */
1313 if (act->happens_before(curr))
1318 if (DBG_ENABLED()) {
1319 model_print("Reached read action:\n");
1321 model_print("End printing read_from_past\n");
1327 * @brief Get an action representing an uninitialized atomic
1329 * This function may create a new one.
1331 * @param curr The current action, which prompts the creation of an UNINIT action
1332 * @return A pointer to the UNINIT ModelAction
1334 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1336 ModelAction *act = curr->get_uninit_action();
1338 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1339 curr->set_uninit_action(act);
1341 act->create_cv(NULL);
1345 static void print_list(const action_list_t *list)
1347 action_list_t::const_iterator it;
1349 model_print("------------------------------------------------------------------------------------\n");
1350 model_print("# t Action type MO Location Value Rf CV\n");
1351 model_print("------------------------------------------------------------------------------------\n");
1353 unsigned int hash = 0;
1355 for (it = list->begin();it != list->end();it++) {
1356 const ModelAction *act = *it;
1357 if (act->get_seq_number() > 0)
1359 hash = hash^(hash<<3)^((*it)->hash());
1361 model_print("HASH %u\n", hash);
1362 model_print("------------------------------------------------------------------------------------\n");
1365 #if SUPPORT_MOD_ORDER_DUMP
1366 void ModelExecution::dumpGraph(char *filename) const
1369 sprintf(buffer, "%s.dot", filename);
1370 FILE *file = fopen(buffer, "w");
1371 fprintf(file, "digraph %s {\n", filename);
1372 mo_graph->dumpNodes(file);
1373 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1375 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1376 ModelAction *act = *it;
1377 if (act->is_read()) {
1378 mo_graph->dot_print_node(file, act);
1379 mo_graph->dot_print_edge(file,
1380 act->get_reads_from(),
1382 "label=\"rf\", color=red, weight=2");
1384 if (thread_array[act->get_tid()]) {
1385 mo_graph->dot_print_edge(file,
1386 thread_array[id_to_int(act->get_tid())],
1388 "label=\"sb\", color=blue, weight=400");
1391 thread_array[act->get_tid()] = act;
1393 fprintf(file, "}\n");
1394 model_free(thread_array);
1399 /** @brief Prints an execution trace summary. */
1400 void ModelExecution::print_summary() const
1402 #if SUPPORT_MOD_ORDER_DUMP
1403 char buffername[100];
1404 sprintf(buffername, "exec%04u", get_execution_number());
1405 mo_graph->dumpGraphToFile(buffername);
1406 sprintf(buffername, "graph%04u", get_execution_number());
1407 dumpGraph(buffername);
1410 model_print("Execution trace %d:", get_execution_number());
1411 if (isfeasibleprefix()) {
1412 if (scheduler->all_threads_sleeping())
1413 model_print(" SLEEP-SET REDUNDANT");
1414 if (have_bug_reports())
1415 model_print(" DETECTED BUG(S)");
1417 print_infeasibility(" INFEASIBLE");
1420 print_list(&action_trace);
1426 * Add a Thread to the system for the first time. Should only be called once
1428 * @param t The Thread to add
1430 void ModelExecution::add_thread(Thread *t)
1432 unsigned int i = id_to_int(t->get_id());
1433 if (i >= thread_map.size())
1434 thread_map.resize(i + 1);
1436 if (!t->is_model_thread())
1437 scheduler->add_thread(t);
1441 * @brief Get a Thread reference by its ID
1442 * @param tid The Thread's ID
1443 * @return A Thread reference
1445 Thread * ModelExecution::get_thread(thread_id_t tid) const
1447 unsigned int i = id_to_int(tid);
1448 if (i < thread_map.size())
1449 return thread_map[i];
1454 * @brief Get a reference to the Thread in which a ModelAction was executed
1455 * @param act The ModelAction
1456 * @return A Thread reference
1458 Thread * ModelExecution::get_thread(const ModelAction *act) const
1460 return get_thread(act->get_tid());
1464 * @brief Get a Thread reference by its pthread ID
1465 * @param index The pthread's ID
1466 * @return A Thread reference
1468 Thread * ModelExecution::get_pthread(pthread_t pid) {
1474 uint32_t thread_id = x.v;
1475 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1480 * @brief Check if a Thread is currently enabled
1481 * @param t The Thread to check
1482 * @return True if the Thread is currently enabled
1484 bool ModelExecution::is_enabled(Thread *t) const
1486 return scheduler->is_enabled(t);
1490 * @brief Check if a Thread is currently enabled
1491 * @param tid The ID of the Thread to check
1492 * @return True if the Thread is currently enabled
1494 bool ModelExecution::is_enabled(thread_id_t tid) const
1496 return scheduler->is_enabled(tid);
1500 * @brief Select the next thread to execute based on the curren action
1502 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1503 * actions should be followed by the execution of their child thread. In either
1504 * case, the current action should determine the next thread schedule.
1506 * @param curr The current action
1507 * @return The next thread to run, if the current action will determine this
1508 * selection; otherwise NULL
1510 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1512 /* Do not split atomic RMW */
1513 if (curr->is_rmwr())
1514 return get_thread(curr);
1515 /* Follow CREATE with the created thread */
1516 /* which is not needed, because model.cc takes care of this */
1517 if (curr->get_type() == THREAD_CREATE)
1518 return curr->get_thread_operand();
1519 if (curr->get_type() == PTHREAD_CREATE) {
1520 return curr->get_thread_operand();
1526 * Takes the next step in the execution, if possible.
1527 * @param curr The current step to take
1528 * @return Returns the next Thread to run, if any; NULL if this execution
1531 Thread * ModelExecution::take_step(ModelAction *curr)
1533 Thread *curr_thrd = get_thread(curr);
1534 ASSERT(curr_thrd->get_state() == THREAD_READY);
1536 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1537 curr = check_current_action(curr);
1540 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1541 scheduler->remove_thread(curr_thrd);
1543 return action_select_next_thread(curr);
1546 Fuzzer * ModelExecution::getFuzzer() {