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)))
256 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
257 uint64_t value = *((const uint64_t *) location);
258 modelclock_t storeclock;
259 thread_id_t storethread;
260 getStoreThreadAndClock(location, &storethread, &storeclock);
261 setAtomicStoreFlag(location);
262 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
263 add_normal_write_to_lists(act);
264 add_write_to_lists(act);
265 w_modification_order(act);
271 * Processes a read model action.
272 * @param curr is the read model action to process.
273 * @param rf_set is the set of model actions we can possibly read from
274 * @return True if processing this read updates the mo_graph.
276 void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
278 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
280 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
281 if (hasnonatomicstore) {
282 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
283 rf_set->push_back(nonatomicstore);
286 int index = fuzzer->selectWrite(curr, rf_set);
287 ModelAction *rf = (*rf_set)[index];
291 bool canprune = false;
292 if (r_modification_order(curr, rf, priorset, &canprune)) {
293 for(unsigned int i=0;i<priorset->size();i++) {
294 mo_graph->addEdge((*priorset)[i], rf);
297 get_thread(curr)->set_return_value(curr->get_return_value());
299 if (canprune && curr->get_type() == ATOMIC_READ) {
300 int tid = id_to_int(curr->get_tid());
301 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
306 (*rf_set)[index] = rf_set->back();
312 * Processes a lock, trylock, or unlock model action. @param curr is
313 * the read model action to process.
315 * The try lock operation checks whether the lock is taken. If not,
316 * it falls to the normal lock operation case. If so, it returns
319 * The lock operation has already been checked that it is enabled, so
320 * it just grabs the lock and synchronizes with the previous unlock.
322 * The unlock operation has to re-enable all of the threads that are
323 * waiting on the lock.
325 * @return True if synchronization was updated; false otherwise
327 bool ModelExecution::process_mutex(ModelAction *curr)
329 cdsc::mutex *mutex = curr->get_mutex();
330 struct cdsc::mutex_state *state = NULL;
333 state = mutex->get_state();
335 switch (curr->get_type()) {
336 case ATOMIC_TRYLOCK: {
337 bool success = !state->locked;
338 curr->set_try_lock(success);
340 get_thread(curr)->set_return_value(0);
343 get_thread(curr)->set_return_value(1);
345 //otherwise fall into the lock case
347 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
348 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
349 // assert_bug("Lock access before initialization");
350 state->locked = get_thread(curr);
351 ModelAction *unlock = get_last_unlock(curr);
352 //synchronize with the previous unlock statement
353 if (unlock != NULL) {
354 synchronize(unlock, curr);
360 case ATOMIC_UNLOCK: {
361 //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...
363 /* wake up the other threads */
364 for (unsigned int i = 0;i < get_num_threads();i++) {
365 Thread *t = get_thread(int_to_id(i));
366 Thread *curr_thrd = get_thread(curr);
367 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
371 /* unlock the lock - after checking who was waiting on it */
372 state->locked = NULL;
374 if (!curr->is_wait())
375 break;/* The rest is only for ATOMIC_WAIT */
379 case ATOMIC_NOTIFY_ALL: {
380 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
381 //activate all the waiting threads
382 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
383 scheduler->wake(get_thread(*rit));
388 case ATOMIC_NOTIFY_ONE: {
389 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
390 if (waiters->size() != 0) {
391 Thread * thread = fuzzer->selectNotify(waiters);
392 scheduler->wake(thread);
404 * Process a write ModelAction
405 * @param curr The ModelAction to process
406 * @return True if the mo_graph was updated or promises were resolved
408 void ModelExecution::process_write(ModelAction *curr)
410 w_modification_order(curr);
411 get_thread(curr)->set_return_value(VALUE_NONE);
415 * Process a fence ModelAction
416 * @param curr The ModelAction to process
417 * @return True if synchronization was updated
419 bool ModelExecution::process_fence(ModelAction *curr)
422 * fence-relaxed: no-op
423 * fence-release: only log the occurence (not in this function), for
424 * use in later synchronization
425 * fence-acquire (this function): search for hypothetical release
427 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
429 bool updated = false;
430 if (curr->is_acquire()) {
431 action_list_t *list = &action_trace;
432 action_list_t::reverse_iterator rit;
433 /* Find X : is_read(X) && X --sb-> curr */
434 for (rit = list->rbegin();rit != list->rend();rit++) {
435 ModelAction *act = *rit;
438 if (act->get_tid() != curr->get_tid())
440 /* Stop at the beginning of the thread */
441 if (act->is_thread_start())
443 /* Stop once we reach a prior fence-acquire */
444 if (act->is_fence() && act->is_acquire())
448 /* read-acquire will find its own release sequences */
449 if (act->is_acquire())
452 /* Establish hypothetical release sequences */
453 ClockVector *cv = get_hb_from_write(act);
454 if (curr->get_cv()->merge(cv))
462 * @brief Process the current action for thread-related activity
464 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
465 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
466 * synchronization, etc. This function is a no-op for non-THREAD actions
467 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
469 * @param curr The current action
470 * @return True if synchronization was updated or a thread completed
472 bool ModelExecution::process_thread_action(ModelAction *curr)
474 bool updated = false;
476 switch (curr->get_type()) {
477 case THREAD_CREATE: {
478 thrd_t *thrd = (thrd_t *)curr->get_location();
479 struct thread_params *params = (struct thread_params *)curr->get_value();
480 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
481 curr->set_thread_operand(th);
483 th->set_creation(curr);
486 case PTHREAD_CREATE: {
487 (*(uint32_t *)curr->get_location()) = pthread_counter++;
489 struct pthread_params *params = (struct pthread_params *)curr->get_value();
490 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
491 curr->set_thread_operand(th);
493 th->set_creation(curr);
495 if ( pthread_map.size() < pthread_counter )
496 pthread_map.resize( pthread_counter );
497 pthread_map[ pthread_counter-1 ] = th;
502 Thread *blocking = curr->get_thread_operand();
503 ModelAction *act = get_last_action(blocking->get_id());
504 synchronize(act, curr);
505 updated = true; /* trigger rel-seq checks */
509 Thread *blocking = curr->get_thread_operand();
510 ModelAction *act = get_last_action(blocking->get_id());
511 synchronize(act, curr);
512 updated = true; /* trigger rel-seq checks */
513 break; // WL: to be add (modified)
516 case THREAD_FINISH: {
517 Thread *th = get_thread(curr);
518 /* Wake up any joining threads */
519 for (unsigned int i = 0;i < get_num_threads();i++) {
520 Thread *waiting = get_thread(int_to_id(i));
521 if (waiting->waiting_on() == th &&
522 waiting->get_pending()->is_thread_join())
523 scheduler->wake(waiting);
526 updated = true; /* trigger rel-seq checks */
540 * Initialize the current action by performing one or more of the following
541 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
542 * manipulating backtracking sets, allocating and
543 * initializing clock vectors, and computing the promises to fulfill.
545 * @param curr The current action, as passed from the user context; may be
546 * freed/invalidated after the execution of this function, with a different
547 * action "returned" its place (pass-by-reference)
548 * @return True if curr is a newly-explored action; false otherwise
550 bool ModelExecution::initialize_curr_action(ModelAction **curr)
552 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
553 ModelAction *newcurr = process_rmw(*curr);
559 ModelAction *newcurr = *curr;
561 newcurr->set_seq_number(get_next_seq_num());
562 /* Always compute new clock vector */
563 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
565 /* Assign most recent release fence */
566 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
568 return true; /* This was a new ModelAction */
573 * @brief Establish reads-from relation between two actions
575 * Perform basic operations involved with establishing a concrete rf relation,
576 * including setting the ModelAction data and checking for release sequences.
578 * @param act The action that is reading (must be a read)
579 * @param rf The action from which we are reading (must be a write)
581 * @return True if this read established synchronization
584 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
587 ASSERT(rf->is_write());
589 act->set_read_from(rf);
590 if (act->is_acquire()) {
591 ClockVector *cv = get_hb_from_write(rf);
594 act->get_cv()->merge(cv);
599 * @brief Synchronizes two actions
601 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
602 * This function performs the synchronization as well as providing other hooks
603 * for other checks along with synchronization.
605 * @param first The left-hand side of the synchronizes-with relation
606 * @param second The right-hand side of the synchronizes-with relation
607 * @return True if the synchronization was successful (i.e., was consistent
608 * with the execution order); false otherwise
610 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
612 if (*second < *first) {
613 set_bad_synchronization();
616 return second->synchronize_with(first);
620 * @brief Check whether a model action is enabled.
622 * Checks whether an operation would be successful (i.e., is a lock already
623 * locked, or is the joined thread already complete).
625 * For yield-blocking, yields are never enabled.
627 * @param curr is the ModelAction to check whether it is enabled.
628 * @return a bool that indicates whether the action is enabled.
630 bool ModelExecution::check_action_enabled(ModelAction *curr) {
631 if (curr->is_lock()) {
632 cdsc::mutex *lock = curr->get_mutex();
633 struct cdsc::mutex_state *state = lock->get_state();
636 } else if (curr->is_thread_join()) {
637 Thread *blocking = curr->get_thread_operand();
638 if (!blocking->is_complete()) {
647 * This is the heart of the model checker routine. It performs model-checking
648 * actions corresponding to a given "current action." Among other processes, it
649 * calculates reads-from relationships, updates synchronization clock vectors,
650 * forms a memory_order constraints graph, and handles replay/backtrack
651 * execution when running permutations of previously-observed executions.
653 * @param curr The current action to process
654 * @return The ModelAction that is actually executed; may be different than
657 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
660 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
661 bool newly_explored = initialize_curr_action(&curr);
665 wake_up_sleeping_actions(curr);
667 /* Add the action to lists before any other model-checking tasks */
668 if (!second_part_of_rmw && curr->get_type() != NOOP)
669 add_action_to_lists(curr);
671 if (curr->is_write())
672 add_write_to_lists(curr);
674 SnapVector<ModelAction *> * rf_set = NULL;
675 /* Build may_read_from set for newly-created actions */
676 if (newly_explored && curr->is_read())
677 rf_set = build_may_read_from(curr);
679 process_thread_action(curr);
681 if (curr->is_read() && !second_part_of_rmw) {
682 process_read(curr, rf_set);
685 ASSERT(rf_set == NULL);
688 if (curr->is_write())
691 if (curr->is_fence())
694 if (curr->is_mutex_op())
701 * This is the strongest feasibility check available.
702 * @return whether the current trace (partial or complete) must be a prefix of
705 bool ModelExecution::isfeasibleprefix() const
707 return !is_infeasible();
711 * Print disagnostic information about an infeasible execution
712 * @param prefix A string to prefix the output with; if NULL, then a default
713 * message prefix will be provided
715 void ModelExecution::print_infeasibility(const char *prefix) const
719 if (priv->bad_synchronization)
720 ptr += sprintf(ptr, "[bad sw ordering]");
722 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
726 * Check if the current partial trace is infeasible. Does not check any
727 * end-of-execution flags, which might rule out the execution. Thus, this is
728 * useful only for ruling an execution as infeasible.
729 * @return whether the current partial trace is infeasible.
731 bool ModelExecution::is_infeasible() const
733 return priv->bad_synchronization;
736 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
737 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
738 ModelAction *lastread = get_last_action(act->get_tid());
739 lastread->process_rmw(act);
741 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
747 * @brief Updates the mo_graph with the constraints imposed from the current
750 * Basic idea is the following: Go through each other thread and find
751 * the last action that happened before our read. Two cases:
753 * -# The action is a write: that write must either occur before
754 * the write we read from or be the write we read from.
755 * -# The action is a read: the write that that action read from
756 * must occur before the write we read from or be the same write.
758 * @param curr The current action. Must be a read.
759 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
760 * @return True if modification order edges were added; false otherwise
763 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
765 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
767 ASSERT(curr->is_read());
769 /* Last SC fence in the current thread */
770 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
772 int tid = curr->get_tid();
773 ModelAction *prev_same_thread = NULL;
774 /* Iterate over all threads */
775 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
776 /* Last SC fence in thread tid */
777 ModelAction *last_sc_fence_thread_local = NULL;
779 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
781 /* Last SC fence in thread tid, before last SC fence in current thread */
782 ModelAction *last_sc_fence_thread_before = NULL;
783 if (last_sc_fence_local)
784 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
786 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
787 if (prev_same_thread != NULL &&
788 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
789 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
793 /* Iterate over actions in thread, starting from most recent */
794 action_list_t *list = &(*thrd_lists)[tid];
795 action_list_t::reverse_iterator rit;
796 for (rit = list->rbegin();rit != list->rend();rit++) {
797 ModelAction *act = *rit;
802 /* Don't want to add reflexive edges on 'rf' */
803 if (act->equals(rf)) {
804 if (act->happens_before(curr))
810 if (act->is_write()) {
811 /* C++, Section 29.3 statement 5 */
812 if (curr->is_seqcst() && last_sc_fence_thread_local &&
813 *act < *last_sc_fence_thread_local) {
814 if (mo_graph->checkReachable(rf, act))
816 priorset->push_back(act);
819 /* C++, Section 29.3 statement 4 */
820 else if (act->is_seqcst() && last_sc_fence_local &&
821 *act < *last_sc_fence_local) {
822 if (mo_graph->checkReachable(rf, act))
824 priorset->push_back(act);
827 /* C++, Section 29.3 statement 6 */
828 else if (last_sc_fence_thread_before &&
829 *act < *last_sc_fence_thread_before) {
830 if (mo_graph->checkReachable(rf, act))
832 priorset->push_back(act);
838 * Include at most one act per-thread that "happens
841 if (act->happens_before(curr)) {
843 if (last_sc_fence_local == NULL ||
844 (*last_sc_fence_local < *prev_same_thread)) {
845 prev_same_thread = act;
848 if (act->is_write()) {
849 if (mo_graph->checkReachable(rf, act))
851 priorset->push_back(act);
853 const ModelAction *prevrf = act->get_reads_from();
854 if (!prevrf->equals(rf)) {
855 if (mo_graph->checkReachable(rf, prevrf))
857 priorset->push_back(prevrf);
859 if (act->get_tid() == curr->get_tid()) {
860 //Can prune curr from obj list
873 * Updates the mo_graph with the constraints imposed from the current write.
875 * Basic idea is the following: Go through each other thread and find
876 * the lastest action that happened before our write. Two cases:
878 * (1) The action is a write => that write must occur before
881 * (2) The action is a read => the write that that action read from
882 * must occur before the current write.
884 * This method also handles two other issues:
886 * (I) Sequential Consistency: Making sure that if the current write is
887 * seq_cst, that it occurs after the previous seq_cst write.
889 * (II) Sending the write back to non-synchronizing reads.
891 * @param curr The current action. Must be a write.
892 * @param send_fv A vector for stashing reads to which we may pass our future
893 * value. If NULL, then don't record any future values.
894 * @return True if modification order edges were added; false otherwise
896 void ModelExecution::w_modification_order(ModelAction *curr)
898 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
900 ASSERT(curr->is_write());
902 if (curr->is_seqcst()) {
903 /* We have to at least see the last sequentially consistent write,
904 so we are initialized. */
905 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
906 if (last_seq_cst != NULL) {
907 mo_graph->addEdge(last_seq_cst, curr);
911 /* Last SC fence in the current thread */
912 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
914 /* Iterate over all threads */
915 for (i = 0;i < thrd_lists->size();i++) {
916 /* Last SC fence in thread i, before last SC fence in current thread */
917 ModelAction *last_sc_fence_thread_before = NULL;
918 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
919 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
921 /* Iterate over actions in thread, starting from most recent */
922 action_list_t *list = &(*thrd_lists)[i];
923 action_list_t::reverse_iterator rit;
924 bool force_edge = false;
925 for (rit = list->rbegin();rit != list->rend();rit++) {
926 ModelAction *act = *rit;
929 * 1) If RMW and it actually read from something, then we
930 * already have all relevant edges, so just skip to next
933 * 2) If RMW and it didn't read from anything, we should
934 * whatever edge we can get to speed up convergence.
936 * 3) If normal write, we need to look at earlier actions, so
937 * continue processing list.
940 if (curr->is_rmw()) {
941 if (curr->get_reads_from() != NULL)
949 /* C++, Section 29.3 statement 7 */
950 if (last_sc_fence_thread_before && act->is_write() &&
951 *act < *last_sc_fence_thread_before) {
952 mo_graph->addEdge(act, curr, force_edge);
957 * Include at most one act per-thread that "happens
960 if (act->happens_before(curr)) {
962 * Note: if act is RMW, just add edge:
964 * The following edge should be handled elsewhere:
965 * readfrom(act) --mo--> act
968 mo_graph->addEdge(act, curr, force_edge);
969 else if (act->is_read()) {
970 //if previous read accessed a null, just keep going
971 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
980 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
981 * some constraints. This method checks one the following constraint (others
982 * require compiler support):
984 * If X --hb-> Y --mo-> Z, then X should not read from Z.
985 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
987 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
989 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
991 /* Iterate over all threads */
992 for (i = 0;i < thrd_lists->size();i++) {
993 const ModelAction *write_after_read = NULL;
995 /* Iterate over actions in thread, starting from most recent */
996 action_list_t *list = &(*thrd_lists)[i];
997 action_list_t::reverse_iterator rit;
998 for (rit = list->rbegin();rit != list->rend();rit++) {
999 ModelAction *act = *rit;
1001 /* Don't disallow due to act == reader */
1002 if (!reader->happens_before(act) || reader == act)
1004 else if (act->is_write())
1005 write_after_read = act;
1006 else if (act->is_read() && act->get_reads_from() != NULL)
1007 write_after_read = act->get_reads_from();
1010 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1017 * Computes the clock vector that happens before propagates from this write.
1019 * @param rf The action that might be part of a release sequence. Must be a
1021 * @return ClockVector of happens before relation.
1024 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1025 SnapVector<ModelAction *> * processset = NULL;
1026 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1027 ASSERT(rf->is_write());
1028 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1030 if (processset == NULL)
1031 processset = new SnapVector<ModelAction *>();
1032 processset->push_back(rf);
1035 int i = (processset == NULL) ? 0 : processset->size();
1037 ClockVector * vec = NULL;
1039 if (rf->get_rfcv() != NULL) {
1040 vec = rf->get_rfcv();
1041 } else if (rf->is_acquire() && rf->is_release()) {
1043 } else if (rf->is_release() && !rf->is_rmw()) {
1045 } else if (rf->is_release()) {
1046 //have rmw that is release and doesn't have a rfcv
1047 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1050 //operation that isn't release
1051 if (rf->get_last_fence_release()) {
1053 vec = rf->get_last_fence_release()->get_cv();
1055 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1061 rf = (*processset)[i];
1065 if (processset != NULL)
1071 * Performs various bookkeeping operations for the current ModelAction. For
1072 * instance, adds action to the per-object, per-thread action vector and to the
1073 * action trace list of all thread actions.
1075 * @param act is the ModelAction to add.
1077 void ModelExecution::add_action_to_lists(ModelAction *act)
1079 int tid = id_to_int(act->get_tid());
1080 ModelAction *uninit = NULL;
1082 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1083 if (list->empty() && act->is_atomic_var()) {
1084 uninit = get_uninitialized_action(act);
1085 uninit_id = id_to_int(uninit->get_tid());
1086 list->push_front(uninit);
1087 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1088 if (uninit_id >= (int)vec->size())
1089 vec->resize(uninit_id + 1);
1090 (*vec)[uninit_id].push_front(uninit);
1092 list->push_back(act);
1094 // Update action trace, a total order of all actions
1095 action_trace.push_back(act);
1097 action_trace.push_front(uninit);
1099 // Update obj_thrd_map, a per location, per thread, order of actions
1100 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1101 if (tid >= (int)vec->size())
1102 vec->resize(priv->next_thread_id);
1103 (*vec)[tid].push_back(act);
1105 (*vec)[uninit_id].push_front(uninit);
1107 // Update thrd_last_action, the last action taken by each thrad
1108 if ((int)thrd_last_action.size() <= tid)
1109 thrd_last_action.resize(get_num_threads());
1110 thrd_last_action[tid] = act;
1112 thrd_last_action[uninit_id] = uninit;
1114 // Update thrd_last_fence_release, the last release fence taken by each thread
1115 if (act->is_fence() && act->is_release()) {
1116 if ((int)thrd_last_fence_release.size() <= tid)
1117 thrd_last_fence_release.resize(get_num_threads());
1118 thrd_last_fence_release[tid] = act;
1121 if (act->is_wait()) {
1122 void *mutex_loc = (void *) act->get_value();
1123 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1125 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1126 if (tid >= (int)vec->size())
1127 vec->resize(priv->next_thread_id);
1128 (*vec)[tid].push_back(act);
1132 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1133 action_list_t::reverse_iterator rit = list->rbegin();
1134 modelclock_t next_seq = act->get_seq_number();
1135 if (rit == list->rend() || (*rit)->get_seq_number() == next_seq)
1136 list->push_back(act);
1138 for(;rit != list->rend();rit++) {
1139 if ((*rit)->get_seq_number() == next_seq) {
1140 action_list_t::iterator it = rit.base();
1141 it++; //get to right sequence number
1142 it++; //get to item after it
1143 list->insert(it, act);
1150 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1151 action_list_t::reverse_iterator rit = list->rbegin();
1152 modelclock_t next_seq = act->get_seq_number();
1153 if (rit == list->rend()) {
1154 act->create_cv(NULL);
1155 } else if ((*rit)->get_seq_number() == next_seq) {
1156 act->create_cv((*rit));
1157 list->push_back(act);
1159 for(;rit != list->rend();rit++) {
1160 if ((*rit)->get_seq_number() == next_seq) {
1161 act->create_cv((*rit));
1162 action_list_t::iterator it = rit.base();
1163 it++; //get to right sequence number
1164 it++; //get to item after it
1165 list->insert(it, act);
1173 * Performs various bookkeeping operations for a normal write. The
1174 * complication is that we are typically inserting a normal write
1175 * lazily, so we need to insert it into the middle of lists.
1177 * @param act is the ModelAction to add.
1180 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1182 int tid = id_to_int(act->get_tid());
1183 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1184 insertIntoActionList(list, act);
1185 insertIntoActionListAndSetCV(&action_trace, act);
1187 // Update obj_thrd_map, a per location, per thread, order of actions
1188 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1189 if (tid >= (int)vec->size())
1190 vec->resize(priv->next_thread_id);
1191 insertIntoActionList(&(*vec)[tid],act);
1193 // Update thrd_last_action, the last action taken by each thrad
1194 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1195 thrd_last_action[tid] = act;
1199 void ModelExecution::add_write_to_lists(ModelAction *write) {
1200 // Update seq_cst map
1201 if (write->is_seqcst())
1202 obj_last_sc_map.put(write->get_location(), write);
1204 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1205 int tid = id_to_int(write->get_tid());
1206 if (tid >= (int)vec->size())
1207 vec->resize(priv->next_thread_id);
1208 (*vec)[tid].push_back(write);
1212 * @brief Get the last action performed by a particular Thread
1213 * @param tid The thread ID of the Thread in question
1214 * @return The last action in the thread
1216 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1218 int threadid = id_to_int(tid);
1219 if (threadid < (int)thrd_last_action.size())
1220 return thrd_last_action[id_to_int(tid)];
1226 * @brief Get the last fence release performed by a particular Thread
1227 * @param tid The thread ID of the Thread in question
1228 * @return The last fence release in the thread, if one exists; NULL otherwise
1230 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1232 int threadid = id_to_int(tid);
1233 if (threadid < (int)thrd_last_fence_release.size())
1234 return thrd_last_fence_release[id_to_int(tid)];
1240 * Gets the last memory_order_seq_cst write (in the total global sequence)
1241 * performed on a particular object (i.e., memory location), not including the
1243 * @param curr The current ModelAction; also denotes the object location to
1245 * @return The last seq_cst write
1247 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1249 void *location = curr->get_location();
1250 return obj_last_sc_map.get(location);
1254 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1255 * performed in a particular thread, prior to a particular fence.
1256 * @param tid The ID of the thread to check
1257 * @param before_fence The fence from which to begin the search; if NULL, then
1258 * search for the most recent fence in the thread.
1259 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1261 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1263 /* All fences should have location FENCE_LOCATION */
1264 action_list_t *list = obj_map.get(FENCE_LOCATION);
1269 action_list_t::reverse_iterator rit = list->rbegin();
1272 for (;rit != list->rend();rit++)
1273 if (*rit == before_fence)
1276 ASSERT(*rit == before_fence);
1280 for (;rit != list->rend();rit++)
1281 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1287 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1288 * location). This function identifies the mutex according to the current
1289 * action, which is presumed to perform on the same mutex.
1290 * @param curr The current ModelAction; also denotes the object location to
1292 * @return The last unlock operation
1294 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1296 void *location = curr->get_location();
1298 action_list_t *list = obj_map.get(location);
1299 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1300 action_list_t::reverse_iterator rit;
1301 for (rit = list->rbegin();rit != list->rend();rit++)
1302 if ((*rit)->is_unlock() || (*rit)->is_wait())
1307 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1309 ModelAction *parent = get_last_action(tid);
1311 parent = get_thread(tid)->get_creation();
1316 * Returns the clock vector for a given thread.
1317 * @param tid The thread whose clock vector we want
1318 * @return Desired clock vector
1320 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1322 ModelAction *firstaction=get_parent_action(tid);
1323 return firstaction != NULL ? firstaction->get_cv() : NULL;
1326 bool valequals(uint64_t val1, uint64_t val2, int size) {
1329 return ((uint8_t)val1) == ((uint8_t)val2);
1331 return ((uint16_t)val1) == ((uint16_t)val2);
1333 return ((uint32_t)val1) == ((uint32_t)val2);
1343 * Build up an initial set of all past writes that this 'read' action may read
1344 * from, as well as any previously-observed future values that must still be valid.
1346 * @param curr is the current ModelAction that we are exploring; it must be a
1349 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1351 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1353 ASSERT(curr->is_read());
1355 ModelAction *last_sc_write = NULL;
1357 if (curr->is_seqcst())
1358 last_sc_write = get_last_seq_cst_write(curr);
1360 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1362 /* Iterate over all threads */
1363 for (i = 0;i < thrd_lists->size();i++) {
1364 /* Iterate over actions in thread, starting from most recent */
1365 action_list_t *list = &(*thrd_lists)[i];
1366 action_list_t::reverse_iterator rit;
1367 for (rit = list->rbegin();rit != list->rend();rit++) {
1368 ModelAction *act = *rit;
1373 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1374 bool allow_read = true;
1376 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1379 /* Need to check whether we will have two RMW reading from the same value */
1380 if (curr->is_rmwr()) {
1381 /* It is okay if we have a failing CAS */
1382 if (!curr->is_rmwrcas() ||
1383 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1384 //Need to make sure we aren't the second RMW
1385 CycleNode * node = mo_graph->getNode_noCreate(act);
1386 if (node != NULL && node->getRMW() != NULL) {
1387 //we are the second RMW
1394 /* Only add feasible reads */
1395 rf_set->push_back(act);
1398 /* Include at most one act per-thread that "happens before" curr */
1399 if (act->happens_before(curr))
1404 if (DBG_ENABLED()) {
1405 model_print("Reached read action:\n");
1407 model_print("End printing read_from_past\n");
1413 * @brief Get an action representing an uninitialized atomic
1415 * This function may create a new one.
1417 * @param curr The current action, which prompts the creation of an UNINIT action
1418 * @return A pointer to the UNINIT ModelAction
1420 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1422 ModelAction *act = curr->get_uninit_action();
1424 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1425 curr->set_uninit_action(act);
1427 act->create_cv(NULL);
1431 static void print_list(const action_list_t *list)
1433 action_list_t::const_iterator it;
1435 model_print("------------------------------------------------------------------------------------\n");
1436 model_print("# t Action type MO Location Value Rf CV\n");
1437 model_print("------------------------------------------------------------------------------------\n");
1439 unsigned int hash = 0;
1441 for (it = list->begin();it != list->end();it++) {
1442 const ModelAction *act = *it;
1443 if (act->get_seq_number() > 0)
1445 hash = hash^(hash<<3)^((*it)->hash());
1447 model_print("HASH %u\n", hash);
1448 model_print("------------------------------------------------------------------------------------\n");
1451 #if SUPPORT_MOD_ORDER_DUMP
1452 void ModelExecution::dumpGraph(char *filename) const
1455 sprintf(buffer, "%s.dot", filename);
1456 FILE *file = fopen(buffer, "w");
1457 fprintf(file, "digraph %s {\n", filename);
1458 mo_graph->dumpNodes(file);
1459 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1461 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1462 ModelAction *act = *it;
1463 if (act->is_read()) {
1464 mo_graph->dot_print_node(file, act);
1465 mo_graph->dot_print_edge(file,
1466 act->get_reads_from(),
1468 "label=\"rf\", color=red, weight=2");
1470 if (thread_array[act->get_tid()]) {
1471 mo_graph->dot_print_edge(file,
1472 thread_array[id_to_int(act->get_tid())],
1474 "label=\"sb\", color=blue, weight=400");
1477 thread_array[act->get_tid()] = act;
1479 fprintf(file, "}\n");
1480 model_free(thread_array);
1485 /** @brief Prints an execution trace summary. */
1486 void ModelExecution::print_summary() const
1488 #if SUPPORT_MOD_ORDER_DUMP
1489 char buffername[100];
1490 sprintf(buffername, "exec%04u", get_execution_number());
1491 mo_graph->dumpGraphToFile(buffername);
1492 sprintf(buffername, "graph%04u", get_execution_number());
1493 dumpGraph(buffername);
1496 model_print("Execution trace %d:", get_execution_number());
1497 if (isfeasibleprefix()) {
1498 if (scheduler->all_threads_sleeping())
1499 model_print(" SLEEP-SET REDUNDANT");
1500 if (have_bug_reports())
1501 model_print(" DETECTED BUG(S)");
1503 print_infeasibility(" INFEASIBLE");
1506 print_list(&action_trace);
1512 * Add a Thread to the system for the first time. Should only be called once
1514 * @param t The Thread to add
1516 void ModelExecution::add_thread(Thread *t)
1518 unsigned int i = id_to_int(t->get_id());
1519 if (i >= thread_map.size())
1520 thread_map.resize(i + 1);
1522 if (!t->is_model_thread())
1523 scheduler->add_thread(t);
1527 * @brief Get a Thread reference by its ID
1528 * @param tid The Thread's ID
1529 * @return A Thread reference
1531 Thread * ModelExecution::get_thread(thread_id_t tid) const
1533 unsigned int i = id_to_int(tid);
1534 if (i < thread_map.size())
1535 return thread_map[i];
1540 * @brief Get a reference to the Thread in which a ModelAction was executed
1541 * @param act The ModelAction
1542 * @return A Thread reference
1544 Thread * ModelExecution::get_thread(const ModelAction *act) const
1546 return get_thread(act->get_tid());
1550 * @brief Get a Thread reference by its pthread ID
1551 * @param index The pthread's ID
1552 * @return A Thread reference
1554 Thread * ModelExecution::get_pthread(pthread_t pid) {
1560 uint32_t thread_id = x.v;
1561 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1566 * @brief Check if a Thread is currently enabled
1567 * @param t The Thread to check
1568 * @return True if the Thread is currently enabled
1570 bool ModelExecution::is_enabled(Thread *t) const
1572 return scheduler->is_enabled(t);
1576 * @brief Check if a Thread is currently enabled
1577 * @param tid The ID of the Thread to check
1578 * @return True if the Thread is currently enabled
1580 bool ModelExecution::is_enabled(thread_id_t tid) const
1582 return scheduler->is_enabled(tid);
1586 * @brief Select the next thread to execute based on the curren action
1588 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1589 * actions should be followed by the execution of their child thread. In either
1590 * case, the current action should determine the next thread schedule.
1592 * @param curr The current action
1593 * @return The next thread to run, if the current action will determine this
1594 * selection; otherwise NULL
1596 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1598 /* Do not split atomic RMW */
1599 if (curr->is_rmwr())
1600 return get_thread(curr);
1601 /* Follow CREATE with the created thread */
1602 /* which is not needed, because model.cc takes care of this */
1603 if (curr->get_type() == THREAD_CREATE)
1604 return curr->get_thread_operand();
1605 if (curr->get_type() == PTHREAD_CREATE) {
1606 return curr->get_thread_operand();
1612 * Takes the next step in the execution, if possible.
1613 * @param curr The current step to take
1614 * @return Returns the next Thread to run, if any; NULL if this execution
1617 Thread * ModelExecution::take_step(ModelAction *curr)
1619 Thread *curr_thrd = get_thread(curr);
1620 ASSERT(curr_thrd->get_state() == THREAD_READY);
1622 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1623 curr = check_current_action(curr);
1626 // 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() );
1627 model->get_history()->add_func_atomic( curr, curr_thrd->get_id() );
1629 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1630 scheduler->remove_thread(curr_thrd);
1632 return action_select_next_thread(curr);
1635 Fuzzer * ModelExecution::getFuzzer() {