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),
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) :
56 thread_map(2), /* We'll always need at least 2 threads */
60 condvar_waiters_map(),
64 thrd_last_fence_release(),
65 priv(new struct model_snapshot_members ()),
66 mo_graph(new CycleGraph()),
69 thrd_func_inst_lists()
71 /* Initialize a model-checker thread, for special ModelActions */
72 model_thread = new Thread(get_next_id());
73 add_thread(model_thread);
74 scheduler->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<const 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<ModelAction *> * rf_set)
265 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
268 int index = fuzzer->selectWrite(curr, rf_set);
269 ModelAction *rf = (*rf_set)[index];
273 bool canprune = false;
274 if (r_modification_order(curr, rf, priorset, &canprune)) {
275 for(unsigned int i=0;i<priorset->size();i++) {
276 mo_graph->addEdge((*priorset)[i], rf);
279 get_thread(curr)->set_return_value(curr->get_return_value());
281 if (canprune && curr->get_type() == ATOMIC_READ) {
282 int tid = id_to_int(curr->get_tid());
283 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
288 (*rf_set)[index] = rf_set->back();
294 * Processes a lock, trylock, or unlock model action. @param curr is
295 * the read model action to process.
297 * The try lock operation checks whether the lock is taken. If not,
298 * it falls to the normal lock operation case. If so, it returns
301 * The lock operation has already been checked that it is enabled, so
302 * it just grabs the lock and synchronizes with the previous unlock.
304 * The unlock operation has to re-enable all of the threads that are
305 * waiting on the lock.
307 * @return True if synchronization was updated; false otherwise
309 bool ModelExecution::process_mutex(ModelAction *curr)
311 cdsc::mutex *mutex = curr->get_mutex();
312 struct cdsc::mutex_state *state = NULL;
315 state = mutex->get_state();
317 switch (curr->get_type()) {
318 case ATOMIC_TRYLOCK: {
319 bool success = !state->locked;
320 curr->set_try_lock(success);
322 get_thread(curr)->set_return_value(0);
325 get_thread(curr)->set_return_value(1);
327 //otherwise fall into the lock case
329 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
330 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
331 // assert_bug("Lock access before initialization");
332 state->locked = get_thread(curr);
333 ModelAction *unlock = get_last_unlock(curr);
334 //synchronize with the previous unlock statement
335 if (unlock != NULL) {
336 synchronize(unlock, curr);
342 case ATOMIC_UNLOCK: {
343 //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...
345 /* wake up the other threads */
346 for (unsigned int i = 0;i < get_num_threads();i++) {
347 Thread *t = get_thread(int_to_id(i));
348 Thread *curr_thrd = get_thread(curr);
349 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
353 /* unlock the lock - after checking who was waiting on it */
354 state->locked = NULL;
356 if (!curr->is_wait())
357 break;/* The rest is only for ATOMIC_WAIT */
361 case ATOMIC_NOTIFY_ALL: {
362 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
363 //activate all the waiting threads
364 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
365 scheduler->wake(get_thread(*rit));
370 case ATOMIC_NOTIFY_ONE: {
371 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
372 if (waiters->size() != 0) {
373 Thread * thread = fuzzer->selectNotify(waiters);
374 scheduler->wake(thread);
386 * Process a write ModelAction
387 * @param curr The ModelAction to process
388 * @return True if the mo_graph was updated or promises were resolved
390 void ModelExecution::process_write(ModelAction *curr)
392 w_modification_order(curr);
393 get_thread(curr)->set_return_value(VALUE_NONE);
397 * Process a fence ModelAction
398 * @param curr The ModelAction to process
399 * @return True if synchronization was updated
401 bool ModelExecution::process_fence(ModelAction *curr)
404 * fence-relaxed: no-op
405 * fence-release: only log the occurence (not in this function), for
406 * use in later synchronization
407 * fence-acquire (this function): search for hypothetical release
409 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
411 bool updated = false;
412 if (curr->is_acquire()) {
413 action_list_t *list = &action_trace;
414 action_list_t::reverse_iterator rit;
415 /* Find X : is_read(X) && X --sb-> curr */
416 for (rit = list->rbegin();rit != list->rend();rit++) {
417 ModelAction *act = *rit;
420 if (act->get_tid() != curr->get_tid())
422 /* Stop at the beginning of the thread */
423 if (act->is_thread_start())
425 /* Stop once we reach a prior fence-acquire */
426 if (act->is_fence() && act->is_acquire())
430 /* read-acquire will find its own release sequences */
431 if (act->is_acquire())
434 /* Establish hypothetical release sequences */
435 ClockVector *cv = get_hb_from_write(act);
436 if (curr->get_cv()->merge(cv))
444 * @brief Process the current action for thread-related activity
446 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
447 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
448 * synchronization, etc. This function is a no-op for non-THREAD actions
449 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
451 * @param curr The current action
452 * @return True if synchronization was updated or a thread completed
454 bool ModelExecution::process_thread_action(ModelAction *curr)
456 bool updated = false;
458 switch (curr->get_type()) {
459 case THREAD_CREATE: {
460 thrd_t *thrd = (thrd_t *)curr->get_location();
461 struct thread_params *params = (struct thread_params *)curr->get_value();
462 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
463 curr->set_thread_operand(th);
465 th->set_creation(curr);
468 case PTHREAD_CREATE: {
469 (*(uint32_t *)curr->get_location()) = pthread_counter++;
471 struct pthread_params *params = (struct pthread_params *)curr->get_value();
472 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
473 curr->set_thread_operand(th);
475 th->set_creation(curr);
477 if ( pthread_map.size() < pthread_counter )
478 pthread_map.resize( pthread_counter );
479 pthread_map[ pthread_counter-1 ] = th;
484 Thread *blocking = curr->get_thread_operand();
485 ModelAction *act = get_last_action(blocking->get_id());
486 synchronize(act, curr);
487 updated = true; /* trigger rel-seq checks */
491 Thread *blocking = curr->get_thread_operand();
492 ModelAction *act = get_last_action(blocking->get_id());
493 synchronize(act, curr);
494 updated = true; /* trigger rel-seq checks */
495 break; // WL: to be add (modified)
498 case THREAD_FINISH: {
499 Thread *th = get_thread(curr);
500 /* Wake up any joining threads */
501 for (unsigned int i = 0;i < get_num_threads();i++) {
502 Thread *waiting = get_thread(int_to_id(i));
503 if (waiting->waiting_on() == th &&
504 waiting->get_pending()->is_thread_join())
505 scheduler->wake(waiting);
508 updated = true; /* trigger rel-seq checks */
522 * Initialize the current action by performing one or more of the following
523 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
524 * manipulating backtracking sets, allocating and
525 * initializing clock vectors, and computing the promises to fulfill.
527 * @param curr The current action, as passed from the user context; may be
528 * freed/invalidated after the execution of this function, with a different
529 * action "returned" its place (pass-by-reference)
530 * @return True if curr is a newly-explored action; false otherwise
532 bool ModelExecution::initialize_curr_action(ModelAction **curr)
534 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
535 ModelAction *newcurr = process_rmw(*curr);
541 ModelAction *newcurr = *curr;
543 newcurr->set_seq_number(get_next_seq_num());
544 /* Always compute new clock vector */
545 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
547 /* Assign most recent release fence */
548 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
550 return true; /* This was a new ModelAction */
555 * @brief Establish reads-from relation between two actions
557 * Perform basic operations involved with establishing a concrete rf relation,
558 * including setting the ModelAction data and checking for release sequences.
560 * @param act The action that is reading (must be a read)
561 * @param rf The action from which we are reading (must be a write)
563 * @return True if this read established synchronization
566 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
569 ASSERT(rf->is_write());
571 act->set_read_from(rf);
572 if (act->is_acquire()) {
573 ClockVector *cv = get_hb_from_write(rf);
576 act->get_cv()->merge(cv);
581 * @brief Synchronizes two actions
583 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
584 * This function performs the synchronization as well as providing other hooks
585 * for other checks along with synchronization.
587 * @param first The left-hand side of the synchronizes-with relation
588 * @param second The right-hand side of the synchronizes-with relation
589 * @return True if the synchronization was successful (i.e., was consistent
590 * with the execution order); false otherwise
592 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
594 if (*second < *first) {
595 set_bad_synchronization();
598 return second->synchronize_with(first);
602 * @brief Check whether a model action is enabled.
604 * Checks whether an operation would be successful (i.e., is a lock already
605 * locked, or is the joined thread already complete).
607 * For yield-blocking, yields are never enabled.
609 * @param curr is the ModelAction to check whether it is enabled.
610 * @return a bool that indicates whether the action is enabled.
612 bool ModelExecution::check_action_enabled(ModelAction *curr) {
613 if (curr->is_lock()) {
614 cdsc::mutex *lock = curr->get_mutex();
615 struct cdsc::mutex_state *state = lock->get_state();
618 } else if (curr->is_thread_join()) {
619 Thread *blocking = curr->get_thread_operand();
620 if (!blocking->is_complete()) {
629 * This is the heart of the model checker routine. It performs model-checking
630 * actions corresponding to a given "current action." Among other processes, it
631 * calculates reads-from relationships, updates synchronization clock vectors,
632 * forms a memory_order constraints graph, and handles replay/backtrack
633 * execution when running permutations of previously-observed executions.
635 * @param curr The current action to process
636 * @return The ModelAction that is actually executed; may be different than
639 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
642 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
643 bool newly_explored = initialize_curr_action(&curr);
647 wake_up_sleeping_actions(curr);
649 /* Add the action to lists before any other model-checking tasks */
650 if (!second_part_of_rmw && curr->get_type() != NOOP)
651 add_action_to_lists(curr);
653 if (curr->is_write())
654 add_write_to_lists(curr);
656 SnapVector<ModelAction *> * rf_set = NULL;
657 /* Build may_read_from set for newly-created actions */
658 if (newly_explored && curr->is_read())
659 rf_set = build_may_read_from(curr);
661 process_thread_action(curr);
663 if (curr->is_read() && !second_part_of_rmw) {
664 process_read(curr, rf_set);
667 ASSERT(rf_set == NULL);
670 if (curr->is_write())
673 if (curr->is_fence())
676 if (curr->is_mutex_op())
683 * This is the strongest feasibility check available.
684 * @return whether the current trace (partial or complete) must be a prefix of
687 bool ModelExecution::isfeasibleprefix() const
689 return !is_infeasible();
693 * Print disagnostic information about an infeasible execution
694 * @param prefix A string to prefix the output with; if NULL, then a default
695 * message prefix will be provided
697 void ModelExecution::print_infeasibility(const char *prefix) const
701 if (priv->bad_synchronization)
702 ptr += sprintf(ptr, "[bad sw ordering]");
704 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
708 * Check if the current partial trace is infeasible. Does not check any
709 * end-of-execution flags, which might rule out the execution. Thus, this is
710 * useful only for ruling an execution as infeasible.
711 * @return whether the current partial trace is infeasible.
713 bool ModelExecution::is_infeasible() const
715 return priv->bad_synchronization;
718 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
719 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
720 ModelAction *lastread = get_last_action(act->get_tid());
721 lastread->process_rmw(act);
723 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
729 * @brief Updates the mo_graph with the constraints imposed from the current
732 * Basic idea is the following: Go through each other thread and find
733 * the last action that happened before our read. Two cases:
735 * -# The action is a write: that write must either occur before
736 * the write we read from or be the write we read from.
737 * -# The action is a read: the write that that action read from
738 * must occur before the write we read from or be the same write.
740 * @param curr The current action. Must be a read.
741 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
742 * @return True if modification order edges were added; false otherwise
745 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
747 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
749 ASSERT(curr->is_read());
751 /* Last SC fence in the current thread */
752 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
754 int tid = curr->get_tid();
755 ModelAction *prev_same_thread = NULL;
756 /* Iterate over all threads */
757 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
758 /* Last SC fence in thread tid */
759 ModelAction *last_sc_fence_thread_local = NULL;
761 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
763 /* Last SC fence in thread tid, before last SC fence in current thread */
764 ModelAction *last_sc_fence_thread_before = NULL;
765 if (last_sc_fence_local)
766 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
768 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
769 if (prev_same_thread != NULL &&
770 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
771 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
775 /* Iterate over actions in thread, starting from most recent */
776 action_list_t *list = &(*thrd_lists)[tid];
777 action_list_t::reverse_iterator rit;
778 for (rit = list->rbegin();rit != list->rend();rit++) {
779 ModelAction *act = *rit;
784 /* Don't want to add reflexive edges on 'rf' */
785 if (act->equals(rf)) {
786 if (act->happens_before(curr))
792 if (act->is_write()) {
793 /* C++, Section 29.3 statement 5 */
794 if (curr->is_seqcst() && last_sc_fence_thread_local &&
795 *act < *last_sc_fence_thread_local) {
796 if (mo_graph->checkReachable(rf, act))
798 priorset->push_back(act);
801 /* C++, Section 29.3 statement 4 */
802 else if (act->is_seqcst() && last_sc_fence_local &&
803 *act < *last_sc_fence_local) {
804 if (mo_graph->checkReachable(rf, act))
806 priorset->push_back(act);
809 /* C++, Section 29.3 statement 6 */
810 else if (last_sc_fence_thread_before &&
811 *act < *last_sc_fence_thread_before) {
812 if (mo_graph->checkReachable(rf, act))
814 priorset->push_back(act);
820 * Include at most one act per-thread that "happens
823 if (act->happens_before(curr)) {
825 if (last_sc_fence_local == NULL ||
826 (*last_sc_fence_local < *prev_same_thread)) {
827 prev_same_thread = act;
830 if (act->is_write()) {
831 if (mo_graph->checkReachable(rf, act))
833 priorset->push_back(act);
835 const ModelAction *prevrf = act->get_reads_from();
836 if (!prevrf->equals(rf)) {
837 if (mo_graph->checkReachable(rf, prevrf))
839 priorset->push_back(prevrf);
841 if (act->get_tid() == curr->get_tid()) {
842 //Can prune curr from obj list
855 * Updates the mo_graph with the constraints imposed from the current write.
857 * Basic idea is the following: Go through each other thread and find
858 * the lastest action that happened before our write. Two cases:
860 * (1) The action is a write => that write must occur before
863 * (2) The action is a read => the write that that action read from
864 * must occur before the current write.
866 * This method also handles two other issues:
868 * (I) Sequential Consistency: Making sure that if the current write is
869 * seq_cst, that it occurs after the previous seq_cst write.
871 * (II) Sending the write back to non-synchronizing reads.
873 * @param curr The current action. Must be a write.
874 * @param send_fv A vector for stashing reads to which we may pass our future
875 * value. If NULL, then don't record any future values.
876 * @return True if modification order edges were added; false otherwise
878 void ModelExecution::w_modification_order(ModelAction *curr)
880 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
882 ASSERT(curr->is_write());
884 if (curr->is_seqcst()) {
885 /* We have to at least see the last sequentially consistent write,
886 so we are initialized. */
887 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
888 if (last_seq_cst != NULL) {
889 mo_graph->addEdge(last_seq_cst, curr);
893 /* Last SC fence in the current thread */
894 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
896 /* Iterate over all threads */
897 for (i = 0;i < thrd_lists->size();i++) {
898 /* Last SC fence in thread i, before last SC fence in current thread */
899 ModelAction *last_sc_fence_thread_before = NULL;
900 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
901 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
903 /* Iterate over actions in thread, starting from most recent */
904 action_list_t *list = &(*thrd_lists)[i];
905 action_list_t::reverse_iterator rit;
906 bool force_edge = false;
907 for (rit = list->rbegin();rit != list->rend();rit++) {
908 ModelAction *act = *rit;
911 * 1) If RMW and it actually read from something, then we
912 * already have all relevant edges, so just skip to next
915 * 2) If RMW and it didn't read from anything, we should
916 * whatever edge we can get to speed up convergence.
918 * 3) If normal write, we need to look at earlier actions, so
919 * continue processing list.
922 if (curr->is_rmw()) {
923 if (curr->get_reads_from() != NULL)
931 /* C++, Section 29.3 statement 7 */
932 if (last_sc_fence_thread_before && act->is_write() &&
933 *act < *last_sc_fence_thread_before) {
934 mo_graph->addEdge(act, curr, force_edge);
939 * Include at most one act per-thread that "happens
942 if (act->happens_before(curr)) {
944 * Note: if act is RMW, just add edge:
946 * The following edge should be handled elsewhere:
947 * readfrom(act) --mo--> act
950 mo_graph->addEdge(act, curr, force_edge);
951 else if (act->is_read()) {
952 //if previous read accessed a null, just keep going
953 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
962 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
963 * some constraints. This method checks one the following constraint (others
964 * require compiler support):
966 * If X --hb-> Y --mo-> Z, then X should not read from Z.
967 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
969 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
971 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
973 /* Iterate over all threads */
974 for (i = 0;i < thrd_lists->size();i++) {
975 const ModelAction *write_after_read = NULL;
977 /* Iterate over actions in thread, starting from most recent */
978 action_list_t *list = &(*thrd_lists)[i];
979 action_list_t::reverse_iterator rit;
980 for (rit = list->rbegin();rit != list->rend();rit++) {
981 ModelAction *act = *rit;
983 /* Don't disallow due to act == reader */
984 if (!reader->happens_before(act) || reader == act)
986 else if (act->is_write())
987 write_after_read = act;
988 else if (act->is_read() && act->get_reads_from() != NULL)
989 write_after_read = act->get_reads_from();
992 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
999 * Computes the clock vector that happens before propagates from this write.
1001 * @param rf The action that might be part of a release sequence. Must be a
1003 * @return ClockVector of happens before relation.
1006 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1007 SnapVector<ModelAction *> * processset = NULL;
1008 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1009 ASSERT(rf->is_write());
1010 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1012 if (processset == NULL)
1013 processset = new SnapVector<ModelAction *>();
1014 processset->push_back(rf);
1017 int i = (processset == NULL) ? 0 : processset->size();
1019 ClockVector * vec = NULL;
1021 if (rf->get_rfcv() != NULL) {
1022 vec = rf->get_rfcv();
1023 } else if (rf->is_acquire() && rf->is_release()) {
1025 } else if (rf->is_release() && !rf->is_rmw()) {
1027 } else if (rf->is_release()) {
1028 //have rmw that is release and doesn't have a rfcv
1029 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1032 //operation that isn't release
1033 if (rf->get_last_fence_release()) {
1035 vec = rf->get_last_fence_release()->get_cv();
1037 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1043 rf = (*processset)[i];
1047 if (processset != NULL)
1053 * Performs various bookkeeping operations for the current ModelAction. For
1054 * instance, adds action to the per-object, per-thread action vector and to the
1055 * action trace list of all thread actions.
1057 * @param act is the ModelAction to add.
1059 void ModelExecution::add_action_to_lists(ModelAction *act)
1061 int tid = id_to_int(act->get_tid());
1062 ModelAction *uninit = NULL;
1064 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1065 if (list->empty() && act->is_atomic_var()) {
1066 uninit = get_uninitialized_action(act);
1067 uninit_id = id_to_int(uninit->get_tid());
1068 list->push_front(uninit);
1069 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1070 if (uninit_id >= (int)vec->size())
1071 vec->resize(uninit_id + 1);
1072 (*vec)[uninit_id].push_front(uninit);
1074 list->push_back(act);
1076 // Update action trace, a total order of all actions
1077 action_trace.push_back(act);
1079 action_trace.push_front(uninit);
1081 // Update obj_thrd_map, a per location, per thread, order of actions
1082 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1083 if (tid >= (int)vec->size())
1084 vec->resize(priv->next_thread_id);
1085 (*vec)[tid].push_back(act);
1087 (*vec)[uninit_id].push_front(uninit);
1089 // Update thrd_last_action, the last action taken by each thrad
1090 if ((int)thrd_last_action.size() <= tid)
1091 thrd_last_action.resize(get_num_threads());
1092 thrd_last_action[tid] = act;
1094 thrd_last_action[uninit_id] = uninit;
1096 // Update thrd_last_fence_release, the last release fence taken by each thread
1097 if (act->is_fence() && act->is_release()) {
1098 if ((int)thrd_last_fence_release.size() <= tid)
1099 thrd_last_fence_release.resize(get_num_threads());
1100 thrd_last_fence_release[tid] = act;
1103 if (act->is_wait()) {
1104 void *mutex_loc = (void *) act->get_value();
1105 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1107 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1108 if (tid >= (int)vec->size())
1109 vec->resize(priv->next_thread_id);
1110 (*vec)[tid].push_back(act);
1114 void ModelExecution::add_write_to_lists(ModelAction *write) {
1115 // Update seq_cst map
1116 if (write->is_seqcst())
1117 obj_last_sc_map.put(write->get_location(), write);
1119 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1120 int tid = id_to_int(write->get_tid());
1121 if (tid >= (int)vec->size())
1122 vec->resize(priv->next_thread_id);
1123 (*vec)[tid].push_back(write);
1127 * @brief Get the last action performed by a particular Thread
1128 * @param tid The thread ID of the Thread in question
1129 * @return The last action in the thread
1131 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1133 int threadid = id_to_int(tid);
1134 if (threadid < (int)thrd_last_action.size())
1135 return thrd_last_action[id_to_int(tid)];
1141 * @brief Get the last fence release performed by a particular Thread
1142 * @param tid The thread ID of the Thread in question
1143 * @return The last fence release in the thread, if one exists; NULL otherwise
1145 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1147 int threadid = id_to_int(tid);
1148 if (threadid < (int)thrd_last_fence_release.size())
1149 return thrd_last_fence_release[id_to_int(tid)];
1155 * Gets the last memory_order_seq_cst write (in the total global sequence)
1156 * performed on a particular object (i.e., memory location), not including the
1158 * @param curr The current ModelAction; also denotes the object location to
1160 * @return The last seq_cst write
1162 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1164 void *location = curr->get_location();
1165 return obj_last_sc_map.get(location);
1169 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1170 * performed in a particular thread, prior to a particular fence.
1171 * @param tid The ID of the thread to check
1172 * @param before_fence The fence from which to begin the search; if NULL, then
1173 * search for the most recent fence in the thread.
1174 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1176 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1178 /* All fences should have location FENCE_LOCATION */
1179 action_list_t *list = obj_map.get(FENCE_LOCATION);
1184 action_list_t::reverse_iterator rit = list->rbegin();
1187 for (;rit != list->rend();rit++)
1188 if (*rit == before_fence)
1191 ASSERT(*rit == before_fence);
1195 for (;rit != list->rend();rit++)
1196 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1202 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1203 * location). This function identifies the mutex according to the current
1204 * action, which is presumed to perform on the same mutex.
1205 * @param curr The current ModelAction; also denotes the object location to
1207 * @return The last unlock operation
1209 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1211 void *location = curr->get_location();
1213 action_list_t *list = obj_map.get(location);
1214 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1215 action_list_t::reverse_iterator rit;
1216 for (rit = list->rbegin();rit != list->rend();rit++)
1217 if ((*rit)->is_unlock() || (*rit)->is_wait())
1222 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1224 ModelAction *parent = get_last_action(tid);
1226 parent = get_thread(tid)->get_creation();
1231 * Returns the clock vector for a given thread.
1232 * @param tid The thread whose clock vector we want
1233 * @return Desired clock vector
1235 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1237 ModelAction *firstaction=get_parent_action(tid);
1238 return firstaction != NULL ? firstaction->get_cv() : NULL;
1241 bool valequals(uint64_t val1, uint64_t val2, int size) {
1244 return ((uint8_t)val1) == ((uint8_t)val2);
1246 return ((uint16_t)val1) == ((uint16_t)val2);
1248 return ((uint32_t)val1) == ((uint32_t)val2);
1258 * Build up an initial set of all past writes that this 'read' action may read
1259 * from, as well as any previously-observed future values that must still be valid.
1261 * @param curr is the current ModelAction that we are exploring; it must be a
1264 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1266 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1268 ASSERT(curr->is_read());
1270 ModelAction *last_sc_write = NULL;
1272 if (curr->is_seqcst())
1273 last_sc_write = get_last_seq_cst_write(curr);
1275 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1277 /* Iterate over all threads */
1278 for (i = 0;i < thrd_lists->size();i++) {
1279 /* Iterate over actions in thread, starting from most recent */
1280 action_list_t *list = &(*thrd_lists)[i];
1281 action_list_t::reverse_iterator rit;
1282 for (rit = list->rbegin();rit != list->rend();rit++) {
1283 ModelAction *act = *rit;
1288 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1289 bool allow_read = true;
1291 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1294 /* Need to check whether we will have two RMW reading from the same value */
1295 if (curr->is_rmwr()) {
1296 /* It is okay if we have a failing CAS */
1297 if (!curr->is_rmwrcas() ||
1298 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1299 //Need to make sure we aren't the second RMW
1300 CycleNode * node = mo_graph->getNode_noCreate(act);
1301 if (node != NULL && node->getRMW() != NULL) {
1302 //we are the second RMW
1309 /* Only add feasible reads */
1310 rf_set->push_back(act);
1313 /* Include at most one act per-thread that "happens before" curr */
1314 if (act->happens_before(curr))
1319 if (DBG_ENABLED()) {
1320 model_print("Reached read action:\n");
1322 model_print("End printing read_from_past\n");
1328 * @brief Get an action representing an uninitialized atomic
1330 * This function may create a new one.
1332 * @param curr The current action, which prompts the creation of an UNINIT action
1333 * @return A pointer to the UNINIT ModelAction
1335 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1337 ModelAction *act = curr->get_uninit_action();
1339 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1340 curr->set_uninit_action(act);
1342 act->create_cv(NULL);
1346 static void print_list(const action_list_t *list)
1348 action_list_t::const_iterator it;
1350 model_print("------------------------------------------------------------------------------------\n");
1351 model_print("# t Action type MO Location Value Rf CV\n");
1352 model_print("------------------------------------------------------------------------------------\n");
1354 unsigned int hash = 0;
1356 for (it = list->begin();it != list->end();it++) {
1357 const ModelAction *act = *it;
1358 if (act->get_seq_number() > 0)
1360 hash = hash^(hash<<3)^((*it)->hash());
1362 model_print("HASH %u\n", hash);
1363 model_print("------------------------------------------------------------------------------------\n");
1366 #if SUPPORT_MOD_ORDER_DUMP
1367 void ModelExecution::dumpGraph(char *filename) const
1370 sprintf(buffer, "%s.dot", filename);
1371 FILE *file = fopen(buffer, "w");
1372 fprintf(file, "digraph %s {\n", filename);
1373 mo_graph->dumpNodes(file);
1374 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1376 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1377 ModelAction *act = *it;
1378 if (act->is_read()) {
1379 mo_graph->dot_print_node(file, act);
1380 mo_graph->dot_print_edge(file,
1381 act->get_reads_from(),
1383 "label=\"rf\", color=red, weight=2");
1385 if (thread_array[act->get_tid()]) {
1386 mo_graph->dot_print_edge(file,
1387 thread_array[id_to_int(act->get_tid())],
1389 "label=\"sb\", color=blue, weight=400");
1392 thread_array[act->get_tid()] = act;
1394 fprintf(file, "}\n");
1395 model_free(thread_array);
1400 /** @brief Prints an execution trace summary. */
1401 void ModelExecution::print_summary() const
1403 #if SUPPORT_MOD_ORDER_DUMP
1404 char buffername[100];
1405 sprintf(buffername, "exec%04u", get_execution_number());
1406 mo_graph->dumpGraphToFile(buffername);
1407 sprintf(buffername, "graph%04u", get_execution_number());
1408 dumpGraph(buffername);
1411 model_print("Execution trace %d:", get_execution_number());
1412 if (isfeasibleprefix()) {
1413 if (scheduler->all_threads_sleeping())
1414 model_print(" SLEEP-SET REDUNDANT");
1415 if (have_bug_reports())
1416 model_print(" DETECTED BUG(S)");
1418 print_infeasibility(" INFEASIBLE");
1421 print_list(&action_trace);
1427 * Add a Thread to the system for the first time. Should only be called once
1429 * @param t The Thread to add
1431 void ModelExecution::add_thread(Thread *t)
1433 unsigned int i = id_to_int(t->get_id());
1434 if (i >= thread_map.size())
1435 thread_map.resize(i + 1);
1437 if (!t->is_model_thread())
1438 scheduler->add_thread(t);
1442 * @brief Get a Thread reference by its ID
1443 * @param tid The Thread's ID
1444 * @return A Thread reference
1446 Thread * ModelExecution::get_thread(thread_id_t tid) const
1448 unsigned int i = id_to_int(tid);
1449 if (i < thread_map.size())
1450 return thread_map[i];
1455 * @brief Get a reference to the Thread in which a ModelAction was executed
1456 * @param act The ModelAction
1457 * @return A Thread reference
1459 Thread * ModelExecution::get_thread(const ModelAction *act) const
1461 return get_thread(act->get_tid());
1465 * @brief Get a Thread reference by its pthread ID
1466 * @param index The pthread's ID
1467 * @return A Thread reference
1469 Thread * ModelExecution::get_pthread(pthread_t pid) {
1475 uint32_t thread_id = x.v;
1476 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1481 * @brief Check if a Thread is currently enabled
1482 * @param t The Thread to check
1483 * @return True if the Thread is currently enabled
1485 bool ModelExecution::is_enabled(Thread *t) const
1487 return scheduler->is_enabled(t);
1491 * @brief Check if a Thread is currently enabled
1492 * @param tid The ID of the Thread to check
1493 * @return True if the Thread is currently enabled
1495 bool ModelExecution::is_enabled(thread_id_t tid) const
1497 return scheduler->is_enabled(tid);
1501 * @brief Select the next thread to execute based on the curren action
1503 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1504 * actions should be followed by the execution of their child thread. In either
1505 * case, the current action should determine the next thread schedule.
1507 * @param curr The current action
1508 * @return The next thread to run, if the current action will determine this
1509 * selection; otherwise NULL
1511 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1513 /* Do not split atomic RMW */
1514 if (curr->is_rmwr())
1515 return get_thread(curr);
1516 /* Follow CREATE with the created thread */
1517 /* which is not needed, because model.cc takes care of this */
1518 if (curr->get_type() == THREAD_CREATE)
1519 return curr->get_thread_operand();
1520 if (curr->get_type() == PTHREAD_CREATE) {
1521 return curr->get_thread_operand();
1527 * Takes the next step in the execution, if possible.
1528 * @param curr The current step to take
1529 * @return Returns the next Thread to run, if any; NULL if this execution
1532 Thread * ModelExecution::take_step(ModelAction *curr)
1534 Thread *curr_thrd = get_thread(curr);
1535 ASSERT(curr_thrd->get_state() == THREAD_READY);
1537 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1538 curr = check_current_action(curr);
1541 // model_print("poitner loc: %p, thread: %d, type: %d, order: %d, position: %s\n", curr, curr->get_tid(), curr->get_type(), curr->get_mo(), curr->get_position() );
1542 model->get_history()->add_func_atomic( curr, curr_thrd->get_id() );
1544 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1545 scheduler->remove_thread(curr_thrd);
1547 return action_select_next_thread(curr);
1550 Fuzzer * ModelExecution::getFuzzer() {