11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #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),
31 bad_synchronization(false),
35 ~model_snapshot_members() {
36 for (unsigned int i = 0;i < bugs.size();i++)
38 for (unsigned int i = 0;i < dataraces.size(); i++)
44 unsigned int next_thread_id;
45 modelclock_t used_sequence_numbers;
46 SnapVector<bug_message *> bugs;
47 SnapVector<bug_message *> dataraces;
48 /** @brief Incorrectly-ordered synchronization was made */
49 bool bad_synchronization;
55 /** @brief Constructor */
56 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
61 thread_map(2), /* We'll always need at least 2 threads */
65 condvar_waiters_map(),
69 thrd_last_fence_release(),
70 priv(new struct model_snapshot_members ()),
71 mo_graph(new CycleGraph()),
74 thrd_func_inst_lists()
76 /* Initialize a model-checker thread, for special ModelActions */
77 model_thread = new Thread(get_next_id());
78 add_thread(model_thread);
79 scheduler->register_engine(this);
82 /** @brief Destructor */
83 ModelExecution::~ModelExecution()
85 for (unsigned int i = 0;i < get_num_threads();i++)
86 delete get_thread(int_to_id(i));
92 int ModelExecution::get_execution_number() const
94 return model->get_execution_number();
97 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
99 action_list_t *tmp = hash->get(ptr);
101 tmp = new action_list_t();
107 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
109 SnapVector<action_list_t> *tmp = hash->get(ptr);
111 tmp = new SnapVector<action_list_t>();
117 /** @return a thread ID for a new Thread */
118 thread_id_t ModelExecution::get_next_id()
120 return priv->next_thread_id++;
123 /** @return the number of user threads created during this execution */
124 unsigned int ModelExecution::get_num_threads() const
126 return priv->next_thread_id;
129 /** @return a sequence number for a new ModelAction */
130 modelclock_t ModelExecution::get_next_seq_num()
132 return ++priv->used_sequence_numbers;
136 * @brief Should the current action wake up a given thread?
138 * @param curr The current action
139 * @param thread The thread that we might wake up
140 * @return True, if we should wake up the sleeping thread; false otherwise
142 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
144 const ModelAction *asleep = thread->get_pending();
145 /* Don't allow partial RMW to wake anyone up */
148 /* Synchronizing actions may have been backtracked */
149 if (asleep->could_synchronize_with(curr))
151 /* All acquire/release fences and fence-acquire/store-release */
152 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
154 /* Fence-release + store can awake load-acquire on the same location */
155 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
156 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
157 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
163 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
165 for (unsigned int i = 0;i < get_num_threads();i++) {
166 Thread *thr = get_thread(int_to_id(i));
167 if (scheduler->is_sleep_set(thr)) {
168 if (should_wake_up(curr, thr))
169 /* Remove this thread from sleep set */
170 scheduler->remove_sleep(thr);
175 /** @brief Alert the model-checker that an incorrectly-ordered
176 * synchronization was made */
177 void ModelExecution::set_bad_synchronization()
179 priv->bad_synchronization = true;
182 bool ModelExecution::assert_bug(const char *msg)
184 priv->bugs.push_back(new bug_message(msg));
186 if (isfeasibleprefix()) {
193 /* @brief Put data races in a different list from other bugs. The purpose
194 * is to continue the program untill the number of data races exceeds a
197 /* TODO: check whether set_assert should be called */
198 bool ModelExecution::assert_race(const char *msg)
200 priv->dataraces.push_back(new bug_message(msg));
202 if (isfeasibleprefix()) {
209 /** @return True, if any bugs have been reported for this execution */
210 bool ModelExecution::have_bug_reports() const
212 return priv->bugs.size() != 0;
215 /** @return True, if any fatal bugs have been reported for this execution.
216 * Any bug other than a data race is considered a fatal bug. Data races
217 * are not considered fatal unless the number of races is exceeds
218 * a threshold (temporarily set as 15).
220 bool ModelExecution::have_fatal_bug_reports() const
222 return priv->bugs.size() != 0 || priv->dataraces.size() >= 15;
225 SnapVector<bug_message *> * ModelExecution::get_bugs() const
231 * Check whether the current trace has triggered an assertion which should halt
234 * @return True, if the execution should be aborted; false otherwise
236 bool ModelExecution::has_asserted() const
238 return priv->asserted;
242 * Trigger a trace assertion which should cause this execution to be halted.
243 * This can be due to a detected bug or due to an infeasibility that should
246 void ModelExecution::set_assert()
248 priv->asserted = true;
252 * Check if we are in a deadlock. Should only be called at the end of an
253 * execution, although it should not give false positives in the middle of an
254 * execution (there should be some ENABLED thread).
256 * @return True if program is in a deadlock; false otherwise
258 bool ModelExecution::is_deadlocked() const
260 bool blocking_threads = false;
261 for (unsigned int i = 0;i < get_num_threads();i++) {
262 thread_id_t tid = int_to_id(i);
265 Thread *t = get_thread(tid);
266 if (!t->is_model_thread() && t->get_pending())
267 blocking_threads = true;
269 return blocking_threads;
273 * Check if this is a complete execution. That is, have all thread completed
274 * execution (rather than exiting because sleep sets have forced a redundant
277 * @return True if the execution is complete.
279 bool ModelExecution::is_complete_execution() const
281 for (unsigned int i = 0;i < get_num_threads();i++)
282 if (is_enabled(int_to_id(i)))
289 * Processes a read model action.
290 * @param curr is the read model action to process.
291 * @param rf_set is the set of model actions we can possibly read from
292 * @return True if processing this read updates the mo_graph.
294 void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
296 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
299 int index = fuzzer->selectWrite(curr, rf_set);
300 ModelAction *rf = (*rf_set)[index];
304 bool canprune = false;
305 if (r_modification_order(curr, rf, priorset, &canprune)) {
306 for(unsigned int i=0;i<priorset->size();i++) {
307 mo_graph->addEdge((*priorset)[i], rf);
310 get_thread(curr)->set_return_value(curr->get_return_value());
312 if (canprune && curr->get_type() == ATOMIC_READ) {
313 int tid = id_to_int(curr->get_tid());
314 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
319 (*rf_set)[index] = rf_set->back();
325 * Processes a lock, trylock, or unlock model action. @param curr is
326 * the read model action to process.
328 * The try lock operation checks whether the lock is taken. If not,
329 * it falls to the normal lock operation case. If so, it returns
332 * The lock operation has already been checked that it is enabled, so
333 * it just grabs the lock and synchronizes with the previous unlock.
335 * The unlock operation has to re-enable all of the threads that are
336 * waiting on the lock.
338 * @return True if synchronization was updated; false otherwise
340 bool ModelExecution::process_mutex(ModelAction *curr)
342 cdsc::mutex *mutex = curr->get_mutex();
343 struct cdsc::mutex_state *state = NULL;
346 state = mutex->get_state();
348 switch (curr->get_type()) {
349 case ATOMIC_TRYLOCK: {
350 bool success = !state->locked;
351 curr->set_try_lock(success);
353 get_thread(curr)->set_return_value(0);
356 get_thread(curr)->set_return_value(1);
358 //otherwise fall into the lock case
360 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
361 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
362 // assert_bug("Lock access before initialization");
363 state->locked = get_thread(curr);
364 ModelAction *unlock = get_last_unlock(curr);
365 //synchronize with the previous unlock statement
366 if (unlock != NULL) {
367 synchronize(unlock, curr);
373 case ATOMIC_UNLOCK: {
374 //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...
376 /* wake up the other threads */
377 for (unsigned int i = 0;i < get_num_threads();i++) {
378 Thread *t = get_thread(int_to_id(i));
379 Thread *curr_thrd = get_thread(curr);
380 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
384 /* unlock the lock - after checking who was waiting on it */
385 state->locked = NULL;
387 if (!curr->is_wait())
388 break;/* The rest is only for ATOMIC_WAIT */
392 case ATOMIC_NOTIFY_ALL: {
393 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
394 //activate all the waiting threads
395 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
396 scheduler->wake(get_thread(*rit));
401 case ATOMIC_NOTIFY_ONE: {
402 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
403 if (waiters->size() != 0) {
404 Thread * thread = fuzzer->selectNotify(waiters);
405 scheduler->wake(thread);
417 * Process a write ModelAction
418 * @param curr The ModelAction to process
419 * @return True if the mo_graph was updated or promises were resolved
421 void ModelExecution::process_write(ModelAction *curr)
423 w_modification_order(curr);
424 get_thread(curr)->set_return_value(VALUE_NONE);
428 * Process a fence ModelAction
429 * @param curr The ModelAction to process
430 * @return True if synchronization was updated
432 bool ModelExecution::process_fence(ModelAction *curr)
435 * fence-relaxed: no-op
436 * fence-release: only log the occurence (not in this function), for
437 * use in later synchronization
438 * fence-acquire (this function): search for hypothetical release
440 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
442 bool updated = false;
443 if (curr->is_acquire()) {
444 action_list_t *list = &action_trace;
445 action_list_t::reverse_iterator rit;
446 /* Find X : is_read(X) && X --sb-> curr */
447 for (rit = list->rbegin();rit != list->rend();rit++) {
448 ModelAction *act = *rit;
451 if (act->get_tid() != curr->get_tid())
453 /* Stop at the beginning of the thread */
454 if (act->is_thread_start())
456 /* Stop once we reach a prior fence-acquire */
457 if (act->is_fence() && act->is_acquire())
461 /* read-acquire will find its own release sequences */
462 if (act->is_acquire())
465 /* Establish hypothetical release sequences */
466 ClockVector *cv = get_hb_from_write(act);
467 if (curr->get_cv()->merge(cv))
475 * @brief Process the current action for thread-related activity
477 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
478 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
479 * synchronization, etc. This function is a no-op for non-THREAD actions
480 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
482 * @param curr The current action
483 * @return True if synchronization was updated or a thread completed
485 bool ModelExecution::process_thread_action(ModelAction *curr)
487 bool updated = false;
489 switch (curr->get_type()) {
490 case THREAD_CREATE: {
491 thrd_t *thrd = (thrd_t *)curr->get_location();
492 struct thread_params *params = (struct thread_params *)curr->get_value();
493 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
494 curr->set_thread_operand(th);
496 th->set_creation(curr);
499 case PTHREAD_CREATE: {
500 (*(uint32_t *)curr->get_location()) = pthread_counter++;
502 struct pthread_params *params = (struct pthread_params *)curr->get_value();
503 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
504 curr->set_thread_operand(th);
506 th->set_creation(curr);
508 if ( pthread_map.size() < pthread_counter )
509 pthread_map.resize( pthread_counter );
510 pthread_map[ pthread_counter-1 ] = th;
515 Thread *blocking = curr->get_thread_operand();
516 ModelAction *act = get_last_action(blocking->get_id());
517 synchronize(act, curr);
518 updated = true; /* trigger rel-seq checks */
522 Thread *blocking = curr->get_thread_operand();
523 ModelAction *act = get_last_action(blocking->get_id());
524 synchronize(act, curr);
525 updated = true; /* trigger rel-seq checks */
526 break; // WL: to be add (modified)
529 case THREAD_FINISH: {
530 Thread *th = get_thread(curr);
531 /* Wake up any joining threads */
532 for (unsigned int i = 0;i < get_num_threads();i++) {
533 Thread *waiting = get_thread(int_to_id(i));
534 if (waiting->waiting_on() == th &&
535 waiting->get_pending()->is_thread_join())
536 scheduler->wake(waiting);
539 updated = true; /* trigger rel-seq checks */
553 * Initialize the current action by performing one or more of the following
554 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
555 * manipulating backtracking sets, allocating and
556 * initializing clock vectors, and computing the promises to fulfill.
558 * @param curr The current action, as passed from the user context; may be
559 * freed/invalidated after the execution of this function, with a different
560 * action "returned" its place (pass-by-reference)
561 * @return True if curr is a newly-explored action; false otherwise
563 bool ModelExecution::initialize_curr_action(ModelAction **curr)
565 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
566 ModelAction *newcurr = process_rmw(*curr);
572 ModelAction *newcurr = *curr;
574 newcurr->set_seq_number(get_next_seq_num());
575 /* Always compute new clock vector */
576 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
578 /* Assign most recent release fence */
579 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
581 return true; /* This was a new ModelAction */
586 * @brief Establish reads-from relation between two actions
588 * Perform basic operations involved with establishing a concrete rf relation,
589 * including setting the ModelAction data and checking for release sequences.
591 * @param act The action that is reading (must be a read)
592 * @param rf The action from which we are reading (must be a write)
594 * @return True if this read established synchronization
597 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
600 ASSERT(rf->is_write());
602 act->set_read_from(rf);
603 if (act->is_acquire()) {
604 ClockVector *cv = get_hb_from_write(rf);
607 act->get_cv()->merge(cv);
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 if (curr->is_write())
685 add_write_to_lists(curr);
687 SnapVector<ModelAction *> * rf_set = NULL;
688 /* Build may_read_from set for newly-created actions */
689 if (newly_explored && curr->is_read())
690 rf_set = build_may_read_from(curr);
692 process_thread_action(curr);
694 if (curr->is_read() && !second_part_of_rmw) {
695 process_read(curr, rf_set);
698 ASSERT(rf_set == NULL);
701 if (curr->is_write())
704 if (curr->is_fence())
707 if (curr->is_mutex_op())
714 * This is the strongest feasibility check available.
715 * @return whether the current trace (partial or complete) must be a prefix of
718 bool ModelExecution::isfeasibleprefix() const
720 return !is_infeasible();
724 * Print disagnostic information about an infeasible execution
725 * @param prefix A string to prefix the output with; if NULL, then a default
726 * message prefix will be provided
728 void ModelExecution::print_infeasibility(const char *prefix) const
732 if (priv->bad_synchronization)
733 ptr += sprintf(ptr, "[bad sw ordering]");
735 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
739 * Check if the current partial trace is infeasible. Does not check any
740 * end-of-execution flags, which might rule out the execution. Thus, this is
741 * useful only for ruling an execution as infeasible.
742 * @return whether the current partial trace is infeasible.
744 bool ModelExecution::is_infeasible() const
746 return priv->bad_synchronization;
749 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
750 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
751 ModelAction *lastread = get_last_action(act->get_tid());
752 lastread->process_rmw(act);
754 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
760 * @brief Updates the mo_graph with the constraints imposed from the current
763 * Basic idea is the following: Go through each other thread and find
764 * the last action that happened before our read. Two cases:
766 * -# The action is a write: that write must either occur before
767 * the write we read from or be the write we read from.
768 * -# The action is a read: the write that that action read from
769 * must occur before the write we read from or be the same write.
771 * @param curr The current action. Must be a read.
772 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
773 * @return True if modification order edges were added; false otherwise
776 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
778 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
780 ASSERT(curr->is_read());
782 /* Last SC fence in the current thread */
783 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
785 int tid = curr->get_tid();
786 ModelAction *prev_same_thread = NULL;
787 /* Iterate over all threads */
788 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
789 /* Last SC fence in thread tid */
790 ModelAction *last_sc_fence_thread_local = NULL;
792 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
794 /* Last SC fence in thread tid, before last SC fence in current thread */
795 ModelAction *last_sc_fence_thread_before = NULL;
796 if (last_sc_fence_local)
797 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
799 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
800 if (prev_same_thread != NULL &&
801 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
802 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
806 /* Iterate over actions in thread, starting from most recent */
807 action_list_t *list = &(*thrd_lists)[tid];
808 action_list_t::reverse_iterator rit;
809 for (rit = list->rbegin();rit != list->rend();rit++) {
810 ModelAction *act = *rit;
815 /* Don't want to add reflexive edges on 'rf' */
816 if (act->equals(rf)) {
817 if (act->happens_before(curr))
823 if (act->is_write()) {
824 /* C++, Section 29.3 statement 5 */
825 if (curr->is_seqcst() && last_sc_fence_thread_local &&
826 *act < *last_sc_fence_thread_local) {
827 if (mo_graph->checkReachable(rf, act))
829 priorset->push_back(act);
832 /* C++, Section 29.3 statement 4 */
833 else if (act->is_seqcst() && last_sc_fence_local &&
834 *act < *last_sc_fence_local) {
835 if (mo_graph->checkReachable(rf, act))
837 priorset->push_back(act);
840 /* C++, Section 29.3 statement 6 */
841 else if (last_sc_fence_thread_before &&
842 *act < *last_sc_fence_thread_before) {
843 if (mo_graph->checkReachable(rf, act))
845 priorset->push_back(act);
851 * Include at most one act per-thread that "happens
854 if (act->happens_before(curr)) {
856 if (last_sc_fence_local == NULL ||
857 (*last_sc_fence_local < *prev_same_thread)) {
858 prev_same_thread = act;
861 if (act->is_write()) {
862 if (mo_graph->checkReachable(rf, act))
864 priorset->push_back(act);
866 const ModelAction *prevrf = act->get_reads_from();
867 if (!prevrf->equals(rf)) {
868 if (mo_graph->checkReachable(rf, prevrf))
870 priorset->push_back(prevrf);
872 if (act->get_tid() == curr->get_tid()) {
873 //Can prune curr from obj list
886 * Updates the mo_graph with the constraints imposed from the current write.
888 * Basic idea is the following: Go through each other thread and find
889 * the lastest action that happened before our write. Two cases:
891 * (1) The action is a write => that write must occur before
894 * (2) The action is a read => the write that that action read from
895 * must occur before the current write.
897 * This method also handles two other issues:
899 * (I) Sequential Consistency: Making sure that if the current write is
900 * seq_cst, that it occurs after the previous seq_cst write.
902 * (II) Sending the write back to non-synchronizing reads.
904 * @param curr The current action. Must be a write.
905 * @param send_fv A vector for stashing reads to which we may pass our future
906 * value. If NULL, then don't record any future values.
907 * @return True if modification order edges were added; false otherwise
909 void ModelExecution::w_modification_order(ModelAction *curr)
911 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
913 ASSERT(curr->is_write());
915 if (curr->is_seqcst()) {
916 /* We have to at least see the last sequentially consistent write,
917 so we are initialized. */
918 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
919 if (last_seq_cst != NULL) {
920 mo_graph->addEdge(last_seq_cst, curr);
924 /* Last SC fence in the current thread */
925 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
927 /* Iterate over all threads */
928 for (i = 0;i < thrd_lists->size();i++) {
929 /* Last SC fence in thread i, before last SC fence in current thread */
930 ModelAction *last_sc_fence_thread_before = NULL;
931 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
932 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
934 /* Iterate over actions in thread, starting from most recent */
935 action_list_t *list = &(*thrd_lists)[i];
936 action_list_t::reverse_iterator rit;
937 bool force_edge = false;
938 for (rit = list->rbegin();rit != list->rend();rit++) {
939 ModelAction *act = *rit;
942 * 1) If RMW and it actually read from something, then we
943 * already have all relevant edges, so just skip to next
946 * 2) If RMW and it didn't read from anything, we should
947 * whatever edge we can get to speed up convergence.
949 * 3) If normal write, we need to look at earlier actions, so
950 * continue processing list.
953 if (curr->is_rmw()) {
954 if (curr->get_reads_from() != NULL)
962 /* C++, Section 29.3 statement 7 */
963 if (last_sc_fence_thread_before && act->is_write() &&
964 *act < *last_sc_fence_thread_before) {
965 mo_graph->addEdge(act, curr, force_edge);
970 * Include at most one act per-thread that "happens
973 if (act->happens_before(curr)) {
975 * Note: if act is RMW, just add edge:
977 * The following edge should be handled elsewhere:
978 * readfrom(act) --mo--> act
981 mo_graph->addEdge(act, curr, force_edge);
982 else if (act->is_read()) {
983 //if previous read accessed a null, just keep going
984 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
993 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
994 * some constraints. This method checks one the following constraint (others
995 * require compiler support):
997 * If X --hb-> Y --mo-> Z, then X should not read from Z.
998 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1000 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1002 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1004 /* Iterate over all threads */
1005 for (i = 0;i < thrd_lists->size();i++) {
1006 const ModelAction *write_after_read = NULL;
1008 /* Iterate over actions in thread, starting from most recent */
1009 action_list_t *list = &(*thrd_lists)[i];
1010 action_list_t::reverse_iterator rit;
1011 for (rit = list->rbegin();rit != list->rend();rit++) {
1012 ModelAction *act = *rit;
1014 /* Don't disallow due to act == reader */
1015 if (!reader->happens_before(act) || reader == act)
1017 else if (act->is_write())
1018 write_after_read = act;
1019 else if (act->is_read() && act->get_reads_from() != NULL)
1020 write_after_read = act->get_reads_from();
1023 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1030 * Computes the clock vector that happens before propagates from this write.
1032 * @param rf The action that might be part of a release sequence. Must be a
1034 * @return ClockVector of happens before relation.
1037 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1038 SnapVector<ModelAction *> * processset = NULL;
1039 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1040 ASSERT(rf->is_write());
1041 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1043 if (processset == NULL)
1044 processset = new SnapVector<ModelAction *>();
1045 processset->push_back(rf);
1048 int i = (processset == NULL) ? 0 : processset->size();
1050 ClockVector * vec = NULL;
1052 if (rf->get_rfcv() != NULL) {
1053 vec = rf->get_rfcv();
1054 } else if (rf->is_acquire() && rf->is_release()) {
1056 } else if (rf->is_release() && !rf->is_rmw()) {
1058 } else if (rf->is_release()) {
1059 //have rmw that is release and doesn't have a rfcv
1060 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1063 //operation that isn't release
1064 if (rf->get_last_fence_release()) {
1066 vec = rf->get_last_fence_release()->get_cv();
1068 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1074 rf = (*processset)[i];
1078 if (processset != NULL)
1084 * Performs various bookkeeping operations for the current ModelAction. For
1085 * instance, adds action to the per-object, per-thread action vector and to the
1086 * action trace list of all thread actions.
1088 * @param act is the ModelAction to add.
1090 void ModelExecution::add_action_to_lists(ModelAction *act)
1092 int tid = id_to_int(act->get_tid());
1093 ModelAction *uninit = NULL;
1095 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1096 if (list->empty() && act->is_atomic_var()) {
1097 uninit = get_uninitialized_action(act);
1098 uninit_id = id_to_int(uninit->get_tid());
1099 list->push_front(uninit);
1100 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1101 if (uninit_id >= (int)vec->size())
1102 vec->resize(uninit_id + 1);
1103 (*vec)[uninit_id].push_front(uninit);
1105 list->push_back(act);
1107 // Update action trace, a total order of all actions
1108 action_trace.push_back(act);
1110 action_trace.push_front(uninit);
1112 // Update obj_thrd_map, a per location, per thread, order of actions
1113 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1114 if (tid >= (int)vec->size())
1115 vec->resize(priv->next_thread_id);
1116 (*vec)[tid].push_back(act);
1118 (*vec)[uninit_id].push_front(uninit);
1120 // Update thrd_last_action, the last action taken by each thrad
1121 if ((int)thrd_last_action.size() <= tid)
1122 thrd_last_action.resize(get_num_threads());
1123 thrd_last_action[tid] = act;
1125 thrd_last_action[uninit_id] = uninit;
1127 // Update thrd_last_fence_release, the last release fence taken by each thread
1128 if (act->is_fence() && act->is_release()) {
1129 if ((int)thrd_last_fence_release.size() <= tid)
1130 thrd_last_fence_release.resize(get_num_threads());
1131 thrd_last_fence_release[tid] = act;
1134 if (act->is_wait()) {
1135 void *mutex_loc = (void *) act->get_value();
1136 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1138 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1139 if (tid >= (int)vec->size())
1140 vec->resize(priv->next_thread_id);
1141 (*vec)[tid].push_back(act);
1145 void ModelExecution::add_write_to_lists(ModelAction *write) {
1146 // Update seq_cst map
1147 if (write->is_seqcst())
1148 obj_last_sc_map.put(write->get_location(), write);
1150 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1151 int tid = id_to_int(write->get_tid());
1152 if (tid >= (int)vec->size())
1153 vec->resize(priv->next_thread_id);
1154 (*vec)[tid].push_back(write);
1158 * @brief Get the last action performed by a particular Thread
1159 * @param tid The thread ID of the Thread in question
1160 * @return The last action in the thread
1162 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1164 int threadid = id_to_int(tid);
1165 if (threadid < (int)thrd_last_action.size())
1166 return thrd_last_action[id_to_int(tid)];
1172 * @brief Get the last fence release performed by a particular Thread
1173 * @param tid The thread ID of the Thread in question
1174 * @return The last fence release in the thread, if one exists; NULL otherwise
1176 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1178 int threadid = id_to_int(tid);
1179 if (threadid < (int)thrd_last_fence_release.size())
1180 return thrd_last_fence_release[id_to_int(tid)];
1186 * Gets the last memory_order_seq_cst write (in the total global sequence)
1187 * performed on a particular object (i.e., memory location), not including the
1189 * @param curr The current ModelAction; also denotes the object location to
1191 * @return The last seq_cst write
1193 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1195 void *location = curr->get_location();
1196 return obj_last_sc_map.get(location);
1200 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1201 * performed in a particular thread, prior to a particular fence.
1202 * @param tid The ID of the thread to check
1203 * @param before_fence The fence from which to begin the search; if NULL, then
1204 * search for the most recent fence in the thread.
1205 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1207 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1209 /* All fences should have location FENCE_LOCATION */
1210 action_list_t *list = obj_map.get(FENCE_LOCATION);
1215 action_list_t::reverse_iterator rit = list->rbegin();
1218 for (;rit != list->rend();rit++)
1219 if (*rit == before_fence)
1222 ASSERT(*rit == before_fence);
1226 for (;rit != list->rend();rit++)
1227 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1233 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1234 * location). This function identifies the mutex according to the current
1235 * action, which is presumed to perform on the same mutex.
1236 * @param curr The current ModelAction; also denotes the object location to
1238 * @return The last unlock operation
1240 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1242 void *location = curr->get_location();
1244 action_list_t *list = obj_map.get(location);
1245 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1246 action_list_t::reverse_iterator rit;
1247 for (rit = list->rbegin();rit != list->rend();rit++)
1248 if ((*rit)->is_unlock() || (*rit)->is_wait())
1253 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1255 ModelAction *parent = get_last_action(tid);
1257 parent = get_thread(tid)->get_creation();
1262 * Returns the clock vector for a given thread.
1263 * @param tid The thread whose clock vector we want
1264 * @return Desired clock vector
1266 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1268 ModelAction *firstaction=get_parent_action(tid);
1269 return firstaction != NULL ? firstaction->get_cv() : NULL;
1272 bool valequals(uint64_t val1, uint64_t val2, int size) {
1275 return ((uint8_t)val1) == ((uint8_t)val2);
1277 return ((uint16_t)val1) == ((uint16_t)val2);
1279 return ((uint32_t)val1) == ((uint32_t)val2);
1289 * Build up an initial set of all past writes that this 'read' action may read
1290 * from, as well as any previously-observed future values that must still be valid.
1292 * @param curr is the current ModelAction that we are exploring; it must be a
1295 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1297 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1299 ASSERT(curr->is_read());
1301 ModelAction *last_sc_write = NULL;
1303 if (curr->is_seqcst())
1304 last_sc_write = get_last_seq_cst_write(curr);
1306 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1308 /* Iterate over all threads */
1309 for (i = 0;i < thrd_lists->size();i++) {
1310 /* Iterate over actions in thread, starting from most recent */
1311 action_list_t *list = &(*thrd_lists)[i];
1312 action_list_t::reverse_iterator rit;
1313 for (rit = list->rbegin();rit != list->rend();rit++) {
1314 ModelAction *act = *rit;
1319 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1320 bool allow_read = true;
1322 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1325 /* Need to check whether we will have two RMW reading from the same value */
1326 if (curr->is_rmwr()) {
1327 /* It is okay if we have a failing CAS */
1328 if (!curr->is_rmwrcas() ||
1329 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1330 //Need to make sure we aren't the second RMW
1331 CycleNode * node = mo_graph->getNode_noCreate(act);
1332 if (node != NULL && node->getRMW() != NULL) {
1333 //we are the second RMW
1340 /* Only add feasible reads */
1341 rf_set->push_back(act);
1344 /* Include at most one act per-thread that "happens before" curr */
1345 if (act->happens_before(curr))
1350 if (DBG_ENABLED()) {
1351 model_print("Reached read action:\n");
1353 model_print("End printing read_from_past\n");
1359 * @brief Get an action representing an uninitialized atomic
1361 * This function may create a new one.
1363 * @param curr The current action, which prompts the creation of an UNINIT action
1364 * @return A pointer to the UNINIT ModelAction
1366 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1368 ModelAction *act = curr->get_uninit_action();
1370 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1371 curr->set_uninit_action(act);
1373 act->create_cv(NULL);
1377 static void print_list(const action_list_t *list)
1379 action_list_t::const_iterator it;
1381 model_print("------------------------------------------------------------------------------------\n");
1382 model_print("# t Action type MO Location Value Rf CV\n");
1383 model_print("------------------------------------------------------------------------------------\n");
1385 unsigned int hash = 0;
1387 for (it = list->begin();it != list->end();it++) {
1388 const ModelAction *act = *it;
1389 if (act->get_seq_number() > 0)
1391 hash = hash^(hash<<3)^((*it)->hash());
1393 model_print("HASH %u\n", hash);
1394 model_print("------------------------------------------------------------------------------------\n");
1397 #if SUPPORT_MOD_ORDER_DUMP
1398 void ModelExecution::dumpGraph(char *filename) const
1401 sprintf(buffer, "%s.dot", filename);
1402 FILE *file = fopen(buffer, "w");
1403 fprintf(file, "digraph %s {\n", filename);
1404 mo_graph->dumpNodes(file);
1405 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1407 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1408 ModelAction *act = *it;
1409 if (act->is_read()) {
1410 mo_graph->dot_print_node(file, act);
1411 mo_graph->dot_print_edge(file,
1412 act->get_reads_from(),
1414 "label=\"rf\", color=red, weight=2");
1416 if (thread_array[act->get_tid()]) {
1417 mo_graph->dot_print_edge(file,
1418 thread_array[id_to_int(act->get_tid())],
1420 "label=\"sb\", color=blue, weight=400");
1423 thread_array[act->get_tid()] = act;
1425 fprintf(file, "}\n");
1426 model_free(thread_array);
1431 /** @brief Prints an execution trace summary. */
1432 void ModelExecution::print_summary() const
1434 #if SUPPORT_MOD_ORDER_DUMP
1435 char buffername[100];
1436 sprintf(buffername, "exec%04u", get_execution_number());
1437 mo_graph->dumpGraphToFile(buffername);
1438 sprintf(buffername, "graph%04u", get_execution_number());
1439 dumpGraph(buffername);
1442 model_print("Execution trace %d:", get_execution_number());
1443 if (isfeasibleprefix()) {
1444 if (scheduler->all_threads_sleeping())
1445 model_print(" SLEEP-SET REDUNDANT");
1446 if (have_bug_reports())
1447 model_print(" DETECTED BUG(S)");
1449 print_infeasibility(" INFEASIBLE");
1452 print_list(&action_trace);
1458 * Add a Thread to the system for the first time. Should only be called once
1460 * @param t The Thread to add
1462 void ModelExecution::add_thread(Thread *t)
1464 unsigned int i = id_to_int(t->get_id());
1465 if (i >= thread_map.size())
1466 thread_map.resize(i + 1);
1468 if (!t->is_model_thread())
1469 scheduler->add_thread(t);
1473 * @brief Get a Thread reference by its ID
1474 * @param tid The Thread's ID
1475 * @return A Thread reference
1477 Thread * ModelExecution::get_thread(thread_id_t tid) const
1479 unsigned int i = id_to_int(tid);
1480 if (i < thread_map.size())
1481 return thread_map[i];
1486 * @brief Get a reference to the Thread in which a ModelAction was executed
1487 * @param act The ModelAction
1488 * @return A Thread reference
1490 Thread * ModelExecution::get_thread(const ModelAction *act) const
1492 return get_thread(act->get_tid());
1496 * @brief Get a Thread reference by its pthread ID
1497 * @param index The pthread's ID
1498 * @return A Thread reference
1500 Thread * ModelExecution::get_pthread(pthread_t pid) {
1506 uint32_t thread_id = x.v;
1507 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1512 * @brief Check if a Thread is currently enabled
1513 * @param t The Thread to check
1514 * @return True if the Thread is currently enabled
1516 bool ModelExecution::is_enabled(Thread *t) const
1518 return scheduler->is_enabled(t);
1522 * @brief Check if a Thread is currently enabled
1523 * @param tid The ID of the Thread to check
1524 * @return True if the Thread is currently enabled
1526 bool ModelExecution::is_enabled(thread_id_t tid) const
1528 return scheduler->is_enabled(tid);
1532 * @brief Select the next thread to execute based on the curren action
1534 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1535 * actions should be followed by the execution of their child thread. In either
1536 * case, the current action should determine the next thread schedule.
1538 * @param curr The current action
1539 * @return The next thread to run, if the current action will determine this
1540 * selection; otherwise NULL
1542 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1544 /* Do not split atomic RMW */
1545 if (curr->is_rmwr())
1546 return get_thread(curr);
1547 /* Follow CREATE with the created thread */
1548 /* which is not needed, because model.cc takes care of this */
1549 if (curr->get_type() == THREAD_CREATE)
1550 return curr->get_thread_operand();
1551 if (curr->get_type() == PTHREAD_CREATE) {
1552 return curr->get_thread_operand();
1558 * Takes the next step in the execution, if possible.
1559 * @param curr The current step to take
1560 * @return Returns the next Thread to run, if any; NULL if this execution
1563 Thread * ModelExecution::take_step(ModelAction *curr)
1565 Thread *curr_thrd = get_thread(curr);
1566 ASSERT(curr_thrd->get_state() == THREAD_READY);
1568 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1569 curr = check_current_action(curr);
1572 /* Process this action in ModelHistory for records*/
1573 model->get_history()->process_action( curr, curr_thrd->get_id() );
1575 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1576 scheduler->remove_thread(curr_thrd);
1578 return action_select_next_thread(curr);
1581 Fuzzer * ModelExecution::getFuzzer() {