11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
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 */
49 /** @brief Constructor */
50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
54 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
63 thrd_last_fence_release(),
64 priv(new struct model_snapshot_members ()),
65 mo_graph(new CycleGraph()),
69 /* Initialize a model-checker thread, for special ModelActions */
70 model_thread = new Thread(get_next_id());
71 add_thread(model_thread);
72 fuzzer->register_engine(this);
73 scheduler->register_engine(this);
75 pthread_key_create(&pthreadkey, tlsdestructor);
79 /** @brief Destructor */
80 ModelExecution::~ModelExecution()
82 for (unsigned int i = 0;i < get_num_threads();i++)
83 delete get_thread(int_to_id(i));
89 int ModelExecution::get_execution_number() const
91 return model->get_execution_number();
94 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
96 action_list_t *tmp = hash->get(ptr);
98 tmp = new action_list_t();
104 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
106 SnapVector<action_list_t> *tmp = hash->get(ptr);
108 tmp = new SnapVector<action_list_t>();
114 /** @return a thread ID for a new Thread */
115 thread_id_t ModelExecution::get_next_id()
117 return priv->next_thread_id++;
120 /** @return the number of user threads created during this execution */
121 unsigned int ModelExecution::get_num_threads() const
123 return priv->next_thread_id;
126 /** @return a sequence number for a new ModelAction */
127 modelclock_t ModelExecution::get_next_seq_num()
129 return ++priv->used_sequence_numbers;
132 /** @return a sequence number for a new ModelAction */
133 modelclock_t ModelExecution::get_curr_seq_num()
135 return priv->used_sequence_numbers;
138 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
139 void ModelExecution::restore_last_seq_num()
141 priv->used_sequence_numbers--;
145 * @brief Should the current action wake up a given thread?
147 * @param curr The current action
148 * @param thread The thread that we might wake up
149 * @return True, if we should wake up the sleeping thread; false otherwise
151 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
153 const ModelAction *asleep = thread->get_pending();
154 /* Don't allow partial RMW to wake anyone up */
157 /* Synchronizing actions may have been backtracked */
158 if (asleep->could_synchronize_with(curr))
160 /* All acquire/release fences and fence-acquire/store-release */
161 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
163 /* Fence-release + store can awake load-acquire on the same location */
164 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
165 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
166 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
169 /* The sleep is literally sleeping */
170 if (asleep->is_sleep()) {
171 if (fuzzer->shouldWake(asleep))
178 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
180 for (unsigned int i = 0;i < get_num_threads();i++) {
181 Thread *thr = get_thread(int_to_id(i));
182 if (scheduler->is_sleep_set(thr)) {
183 if (should_wake_up(curr, thr)) {
184 /* Remove this thread from sleep set */
185 scheduler->remove_sleep(thr);
186 if (thr->get_pending()->is_sleep())
187 thr->set_wakeup_state(true);
193 void ModelExecution::assert_bug(const char *msg)
195 priv->bugs.push_back(new bug_message(msg));
199 /** @return True, if any bugs have been reported for this execution */
200 bool ModelExecution::have_bug_reports() const
202 return priv->bugs.size() != 0;
205 SnapVector<bug_message *> * ModelExecution::get_bugs() const
211 * Check whether the current trace has triggered an assertion which should halt
214 * @return True, if the execution should be aborted; false otherwise
216 bool ModelExecution::has_asserted() const
218 return priv->asserted;
222 * Trigger a trace assertion which should cause this execution to be halted.
223 * This can be due to a detected bug or due to an infeasibility that should
226 void ModelExecution::set_assert()
228 priv->asserted = true;
232 * Check if we are in a deadlock. Should only be called at the end of an
233 * execution, although it should not give false positives in the middle of an
234 * execution (there should be some ENABLED thread).
236 * @return True if program is in a deadlock; false otherwise
238 bool ModelExecution::is_deadlocked() const
240 bool blocking_threads = false;
241 for (unsigned int i = 0;i < get_num_threads();i++) {
242 thread_id_t tid = int_to_id(i);
245 Thread *t = get_thread(tid);
246 if (!t->is_model_thread() && t->get_pending())
247 blocking_threads = true;
249 return blocking_threads;
253 * Check if this is a complete execution. That is, have all thread completed
254 * execution (rather than exiting because sleep sets have forced a redundant
257 * @return True if the execution is complete.
259 bool ModelExecution::is_complete_execution() const
261 for (unsigned int i = 0;i < get_num_threads();i++)
262 if (is_enabled(int_to_id(i)))
267 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
268 uint64_t value = *((const uint64_t *) location);
269 modelclock_t storeclock;
270 thread_id_t storethread;
271 getStoreThreadAndClock(location, &storethread, &storeclock);
272 setAtomicStoreFlag(location);
273 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
274 act->set_seq_number(storeclock);
275 add_normal_write_to_lists(act);
276 add_write_to_lists(act);
277 w_modification_order(act);
278 model->get_history()->process_action(act, act->get_tid());
283 * Processes a read model action.
284 * @param curr is the read model action to process.
285 * @param rf_set is the set of model actions we can possibly read from
286 * @return True if the read can be pruned from the thread map list.
288 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
290 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
291 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
292 if (hasnonatomicstore) {
293 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
294 rf_set->push_back(nonatomicstore);
297 // Remove writes that violate read modification order
300 while (i < rf_set->size()) {
301 ModelAction * rf = (*rf_set)[i];
302 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
303 (*rf_set)[i] = rf_set->back();
310 int index = fuzzer->selectWrite(curr, rf_set);
312 ModelAction *rf = (*rf_set)[index];
315 bool canprune = false;
316 if (r_modification_order(curr, rf, priorset, &canprune)) {
317 for(unsigned int i=0;i<priorset->size();i++) {
318 mo_graph->addEdge((*priorset)[i], rf);
321 get_thread(curr)->set_return_value(curr->get_return_value());
323 return canprune && (curr->get_type() == ATOMIC_READ);
326 (*rf_set)[index] = rf_set->back();
332 * Processes a lock, trylock, or unlock model action. @param curr is
333 * the read model action to process.
335 * The try lock operation checks whether the lock is taken. If not,
336 * it falls to the normal lock operation case. If so, it returns
339 * The lock operation has already been checked that it is enabled, so
340 * it just grabs the lock and synchronizes with the previous unlock.
342 * The unlock operation has to re-enable all of the threads that are
343 * waiting on the lock.
345 * @return True if synchronization was updated; false otherwise
347 bool ModelExecution::process_mutex(ModelAction *curr)
349 cdsc::mutex *mutex = curr->get_mutex();
350 struct cdsc::mutex_state *state = NULL;
353 state = mutex->get_state();
355 switch (curr->get_type()) {
356 case ATOMIC_TRYLOCK: {
357 bool success = !state->locked;
358 curr->set_try_lock(success);
360 get_thread(curr)->set_return_value(0);
363 get_thread(curr)->set_return_value(1);
365 //otherwise fall into the lock case
367 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
368 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
369 // assert_bug("Lock access before initialization");
370 state->locked = get_thread(curr);
371 ModelAction *unlock = get_last_unlock(curr);
372 //synchronize with the previous unlock statement
373 if (unlock != NULL) {
374 synchronize(unlock, curr);
380 //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
381 if (fuzzer->shouldWait(curr)) {
382 /* wake up the other threads */
383 for (unsigned int i = 0;i < get_num_threads();i++) {
384 Thread *t = get_thread(int_to_id(i));
385 Thread *curr_thrd = get_thread(curr);
386 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
390 /* unlock the lock - after checking who was waiting on it */
391 state->locked = NULL;
393 /* disable this thread */
394 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
395 scheduler->sleep(get_thread(curr));
400 case ATOMIC_TIMEDWAIT:
401 case ATOMIC_UNLOCK: {
402 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
403 //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
404 //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
405 //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
406 //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
407 //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
408 //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
409 //MUST EVENMTUALLY RELEASE...
411 /* wake up the other threads */
412 for (unsigned int i = 0;i < get_num_threads();i++) {
413 Thread *t = get_thread(int_to_id(i));
414 Thread *curr_thrd = get_thread(curr);
415 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
419 /* unlock the lock - after checking who was waiting on it */
420 state->locked = NULL;
423 case ATOMIC_NOTIFY_ALL: {
424 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
425 //activate all the waiting threads
426 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
427 scheduler->wake(get_thread(rit->getVal()));
432 case ATOMIC_NOTIFY_ONE: {
433 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
434 if (waiters->size() != 0) {
435 Thread * thread = fuzzer->selectNotify(waiters);
436 scheduler->wake(thread);
448 * Process a write ModelAction
449 * @param curr The ModelAction to process
450 * @return True if the mo_graph was updated or promises were resolved
452 void ModelExecution::process_write(ModelAction *curr)
454 w_modification_order(curr);
455 get_thread(curr)->set_return_value(VALUE_NONE);
459 * Process a fence ModelAction
460 * @param curr The ModelAction to process
461 * @return True if synchronization was updated
463 bool ModelExecution::process_fence(ModelAction *curr)
466 * fence-relaxed: no-op
467 * fence-release: only log the occurence (not in this function), for
468 * use in later synchronization
469 * fence-acquire (this function): search for hypothetical release
471 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
473 bool updated = false;
474 if (curr->is_acquire()) {
475 action_list_t *list = &action_trace;
476 sllnode<ModelAction *> * rit;
477 /* Find X : is_read(X) && X --sb-> curr */
478 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
479 ModelAction *act = rit->getVal();
482 if (act->get_tid() != curr->get_tid())
484 /* Stop at the beginning of the thread */
485 if (act->is_thread_start())
487 /* Stop once we reach a prior fence-acquire */
488 if (act->is_fence() && act->is_acquire())
492 /* read-acquire will find its own release sequences */
493 if (act->is_acquire())
496 /* Establish hypothetical release sequences */
497 ClockVector *cv = get_hb_from_write(act->get_reads_from());
498 if (cv != NULL && curr->get_cv()->merge(cv))
506 * @brief Process the current action for thread-related activity
508 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
509 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
510 * synchronization, etc. This function is a no-op for non-THREAD actions
511 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
513 * @param curr The current action
514 * @return True if synchronization was updated or a thread completed
516 void ModelExecution::process_thread_action(ModelAction *curr)
518 switch (curr->get_type()) {
519 case THREAD_CREATE: {
520 thrd_t *thrd = (thrd_t *)curr->get_location();
521 struct thread_params *params = (struct thread_params *)curr->get_value();
522 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
523 curr->set_thread_operand(th);
525 th->set_creation(curr);
528 case PTHREAD_CREATE: {
529 (*(uint32_t *)curr->get_location()) = pthread_counter++;
531 struct pthread_params *params = (struct pthread_params *)curr->get_value();
532 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
533 curr->set_thread_operand(th);
535 th->set_creation(curr);
537 if ( pthread_map.size() < pthread_counter )
538 pthread_map.resize( pthread_counter );
539 pthread_map[ pthread_counter-1 ] = th;
544 Thread *blocking = curr->get_thread_operand();
545 ModelAction *act = get_last_action(blocking->get_id());
546 synchronize(act, curr);
550 Thread *blocking = curr->get_thread_operand();
551 ModelAction *act = get_last_action(blocking->get_id());
552 synchronize(act, curr);
553 break; // WL: to be add (modified)
556 case THREADONLY_FINISH:
557 case THREAD_FINISH: {
558 Thread *th = get_thread(curr);
559 if (curr->get_type() == THREAD_FINISH &&
560 th == model->getInitThread()) {
566 /* Wake up any joining threads */
567 for (unsigned int i = 0;i < get_num_threads();i++) {
568 Thread *waiting = get_thread(int_to_id(i));
569 if (waiting->waiting_on() == th &&
570 waiting->get_pending()->is_thread_join())
571 scheduler->wake(waiting);
580 Thread *th = get_thread(curr);
581 th->set_pending(curr);
582 scheduler->add_sleep(th);
591 * Initialize the current action by performing one or more of the following
592 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
593 * manipulating backtracking sets, allocating and
594 * initializing clock vectors, and computing the promises to fulfill.
596 * @param curr The current action, as passed from the user context; may be
597 * freed/invalidated after the execution of this function, with a different
598 * action "returned" its place (pass-by-reference)
599 * @return True if curr is a newly-explored action; false otherwise
601 bool ModelExecution::initialize_curr_action(ModelAction **curr)
603 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
604 ModelAction *newcurr = process_rmw(*curr);
610 ModelAction *newcurr = *curr;
612 newcurr->set_seq_number(get_next_seq_num());
613 /* Always compute new clock vector */
614 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
616 /* Assign most recent release fence */
617 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
619 return true; /* This was a new ModelAction */
624 * @brief Establish reads-from relation between two actions
626 * Perform basic operations involved with establishing a concrete rf relation,
627 * including setting the ModelAction data and checking for release sequences.
629 * @param act The action that is reading (must be a read)
630 * @param rf The action from which we are reading (must be a write)
632 * @return True if this read established synchronization
635 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
638 ASSERT(rf->is_write());
640 act->set_read_from(rf);
641 if (act->is_acquire()) {
642 ClockVector *cv = get_hb_from_write(rf);
645 act->get_cv()->merge(cv);
650 * @brief Synchronizes two actions
652 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
653 * This function performs the synchronization as well as providing other hooks
654 * for other checks along with synchronization.
656 * @param first The left-hand side of the synchronizes-with relation
657 * @param second The right-hand side of the synchronizes-with relation
658 * @return True if the synchronization was successful (i.e., was consistent
659 * with the execution order); false otherwise
661 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
663 if (*second < *first) {
664 ASSERT(0); //This should not happend
667 return second->synchronize_with(first);
671 * @brief Check whether a model action is enabled.
673 * Checks whether an operation would be successful (i.e., is a lock already
674 * locked, or is the joined thread already complete).
676 * For yield-blocking, yields are never enabled.
678 * @param curr is the ModelAction to check whether it is enabled.
679 * @return a bool that indicates whether the action is enabled.
681 bool ModelExecution::check_action_enabled(ModelAction *curr) {
682 if (curr->is_lock()) {
683 cdsc::mutex *lock = curr->get_mutex();
684 struct cdsc::mutex_state *state = lock->get_state();
687 } else if (curr->is_thread_join()) {
688 Thread *blocking = curr->get_thread_operand();
689 if (!blocking->is_complete()) {
692 } else if (curr->is_sleep()) {
693 if (!fuzzer->shouldSleep(curr))
701 * This is the heart of the model checker routine. It performs model-checking
702 * actions corresponding to a given "current action." Among other processes, it
703 * calculates reads-from relationships, updates synchronization clock vectors,
704 * forms a memory_order constraints graph, and handles replay/backtrack
705 * execution when running permutations of previously-observed executions.
707 * @param curr The current action to process
708 * @return The ModelAction that is actually executed; may be different than
711 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
714 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
715 bool newly_explored = initialize_curr_action(&curr);
719 wake_up_sleeping_actions(curr);
721 SnapVector<ModelAction *> * rf_set = NULL;
722 /* Build may_read_from set for newly-created actions */
723 if (newly_explored && curr->is_read())
724 rf_set = build_may_read_from(curr);
726 bool canprune = false;
728 if (curr->is_read() && !second_part_of_rmw) {
729 canprune = process_read(curr, rf_set);
732 ASSERT(rf_set == NULL);
734 /* Add the action to lists */
735 if (!second_part_of_rmw)
736 add_action_to_lists(curr, canprune);
738 if (curr->is_write())
739 add_write_to_lists(curr);
741 process_thread_action(curr);
743 if (curr->is_write())
746 if (curr->is_fence())
749 if (curr->is_mutex_op())
755 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
756 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
757 ModelAction *lastread = get_last_action(act->get_tid());
758 lastread->process_rmw(act);
760 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
766 * @brief Updates the mo_graph with the constraints imposed from the current
769 * Basic idea is the following: Go through each other thread and find
770 * the last action that happened before our read. Two cases:
772 * -# The action is a write: that write must either occur before
773 * the write we read from or be the write we read from.
774 * -# The action is a read: the write that that action read from
775 * must occur before the write we read from or be the same write.
777 * @param curr The current action. Must be a read.
778 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
779 * @param check_only If true, then only check whether the current action satisfies
780 * read modification order or not, without modifiying priorset and canprune.
782 * @return True if modification order edges were added; false otherwise
785 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
786 SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
788 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
789 ASSERT(curr->is_read());
791 /* Last SC fence in the current thread */
792 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
794 int tid = curr->get_tid();
796 /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
797 if ((int)thrd_lists->size() <= tid) {
798 uint oldsize = thrd_lists->size();
799 thrd_lists->resize(priv->next_thread_id);
800 for(uint i = oldsize;i < priv->next_thread_id;i++)
801 new (&(*thrd_lists)[i]) action_list_t();
804 ModelAction *prev_same_thread = NULL;
805 /* Iterate over all threads */
806 for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
807 /* Last SC fence in thread tid */
808 ModelAction *last_sc_fence_thread_local = NULL;
810 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
812 /* Last SC fence in thread tid, before last SC fence in current thread */
813 ModelAction *last_sc_fence_thread_before = NULL;
814 if (last_sc_fence_local)
815 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
817 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
818 if (prev_same_thread != NULL &&
819 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
820 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
824 /* Iterate over actions in thread, starting from most recent */
825 action_list_t *list = &(*thrd_lists)[tid];
826 sllnode<ModelAction *> * rit;
827 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
828 ModelAction *act = rit->getVal();
833 /* Don't want to add reflexive edges on 'rf' */
834 if (act->equals(rf)) {
835 if (act->happens_before(curr))
841 if (act->is_write()) {
842 /* C++, Section 29.3 statement 5 */
843 if (curr->is_seqcst() && last_sc_fence_thread_local &&
844 *act < *last_sc_fence_thread_local) {
845 if (mo_graph->checkReachable(rf, act))
848 priorset->push_back(act);
851 /* C++, Section 29.3 statement 4 */
852 else if (act->is_seqcst() && last_sc_fence_local &&
853 *act < *last_sc_fence_local) {
854 if (mo_graph->checkReachable(rf, act))
857 priorset->push_back(act);
860 /* C++, Section 29.3 statement 6 */
861 else if (last_sc_fence_thread_before &&
862 *act < *last_sc_fence_thread_before) {
863 if (mo_graph->checkReachable(rf, act))
866 priorset->push_back(act);
872 * Include at most one act per-thread that "happens
875 if (act->happens_before(curr)) {
877 if (last_sc_fence_local == NULL ||
878 (*last_sc_fence_local < *act)) {
879 prev_same_thread = act;
882 if (act->is_write()) {
883 if (mo_graph->checkReachable(rf, act))
886 priorset->push_back(act);
888 ModelAction *prevrf = act->get_reads_from();
889 if (!prevrf->equals(rf)) {
890 if (mo_graph->checkReachable(rf, prevrf))
893 priorset->push_back(prevrf);
895 if (act->get_tid() == curr->get_tid()) {
896 //Can prune curr from obj list
910 * Updates the mo_graph with the constraints imposed from the current write.
912 * Basic idea is the following: Go through each other thread and find
913 * the lastest action that happened before our write. Two cases:
915 * (1) The action is a write => that write must occur before
918 * (2) The action is a read => the write that that action read from
919 * must occur before the current write.
921 * This method also handles two other issues:
923 * (I) Sequential Consistency: Making sure that if the current write is
924 * seq_cst, that it occurs after the previous seq_cst write.
926 * (II) Sending the write back to non-synchronizing reads.
928 * @param curr The current action. Must be a write.
929 * @param send_fv A vector for stashing reads to which we may pass our future
930 * value. If NULL, then don't record any future values.
931 * @return True if modification order edges were added; false otherwise
933 void ModelExecution::w_modification_order(ModelAction *curr)
935 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
937 ASSERT(curr->is_write());
939 SnapList<ModelAction *> edgeset;
941 if (curr->is_seqcst()) {
942 /* We have to at least see the last sequentially consistent write,
943 so we are initialized. */
944 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
945 if (last_seq_cst != NULL) {
946 edgeset.push_back(last_seq_cst);
948 //update map for next query
949 obj_last_sc_map.put(curr->get_location(), curr);
952 /* Last SC fence in the current thread */
953 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
955 /* Iterate over all threads */
956 for (i = 0;i < thrd_lists->size();i++) {
957 /* Last SC fence in thread i, before last SC fence in current thread */
958 ModelAction *last_sc_fence_thread_before = NULL;
959 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
960 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
962 /* Iterate over actions in thread, starting from most recent */
963 action_list_t *list = &(*thrd_lists)[i];
964 sllnode<ModelAction*>* rit;
965 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
966 ModelAction *act = rit->getVal();
969 * 1) If RMW and it actually read from something, then we
970 * already have all relevant edges, so just skip to next
973 * 2) If RMW and it didn't read from anything, we should
974 * whatever edge we can get to speed up convergence.
976 * 3) If normal write, we need to look at earlier actions, so
977 * continue processing list.
979 if (curr->is_rmw()) {
980 if (curr->get_reads_from() != NULL)
988 /* C++, Section 29.3 statement 7 */
989 if (last_sc_fence_thread_before && act->is_write() &&
990 *act < *last_sc_fence_thread_before) {
991 edgeset.push_back(act);
996 * Include at most one act per-thread that "happens
999 if (act->happens_before(curr)) {
1001 * Note: if act is RMW, just add edge:
1003 * The following edge should be handled elsewhere:
1004 * readfrom(act) --mo--> act
1006 if (act->is_write())
1007 edgeset.push_back(act);
1008 else if (act->is_read()) {
1009 //if previous read accessed a null, just keep going
1010 edgeset.push_back(act->get_reads_from());
1016 mo_graph->addEdges(&edgeset, curr);
1021 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1022 * some constraints. This method checks one the following constraint (others
1023 * require compiler support):
1025 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1026 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1028 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1030 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1032 /* Iterate over all threads */
1033 for (i = 0;i < thrd_lists->size();i++) {
1034 const ModelAction *write_after_read = NULL;
1036 /* Iterate over actions in thread, starting from most recent */
1037 action_list_t *list = &(*thrd_lists)[i];
1038 sllnode<ModelAction *>* rit;
1039 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1040 ModelAction *act = rit->getVal();
1042 /* Don't disallow due to act == reader */
1043 if (!reader->happens_before(act) || reader == act)
1045 else if (act->is_write())
1046 write_after_read = act;
1047 else if (act->is_read() && act->get_reads_from() != NULL)
1048 write_after_read = act->get_reads_from();
1051 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1058 * Computes the clock vector that happens before propagates from this write.
1060 * @param rf The action that might be part of a release sequence. Must be a
1062 * @return ClockVector of happens before relation.
1065 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1066 SnapVector<ModelAction *> * processset = NULL;
1067 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1068 ASSERT(rf->is_write());
1069 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1071 if (processset == NULL)
1072 processset = new SnapVector<ModelAction *>();
1073 processset->push_back(rf);
1076 int i = (processset == NULL) ? 0 : processset->size();
1078 ClockVector * vec = NULL;
1080 if (rf->get_rfcv() != NULL) {
1081 vec = rf->get_rfcv();
1082 } else if (rf->is_acquire() && rf->is_release()) {
1084 } else if (rf->is_release() && !rf->is_rmw()) {
1086 } else if (rf->is_release()) {
1087 //have rmw that is release and doesn't have a rfcv
1088 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1091 //operation that isn't release
1092 if (rf->get_last_fence_release()) {
1094 vec = rf->get_last_fence_release()->get_cv();
1096 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1102 rf = (*processset)[i];
1106 if (processset != NULL)
1112 * Performs various bookkeeping operations for the current ModelAction. For
1113 * instance, adds action to the per-object, per-thread action vector and to the
1114 * action trace list of all thread actions.
1116 * @param act is the ModelAction to add.
1118 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1120 int tid = id_to_int(act->get_tid());
1121 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1122 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1123 act->setActionRef(list->add_back(act));
1126 // Update action trace, a total order of all actions
1127 act->setTraceRef(action_trace.add_back(act));
1130 // Update obj_thrd_map, a per location, per thread, order of actions
1131 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1132 if ((int)vec->size() <= tid) {
1133 uint oldsize = vec->size();
1134 vec->resize(priv->next_thread_id);
1135 for(uint i = oldsize;i < priv->next_thread_id;i++)
1136 new (&(*vec)[i]) action_list_t();
1139 act->setThrdMapRef((*vec)[tid].add_back(act));
1141 // Update thrd_last_action, the last action taken by each thread
1142 if ((int)thrd_last_action.size() <= tid)
1143 thrd_last_action.resize(get_num_threads());
1144 thrd_last_action[tid] = act;
1146 // Update thrd_last_fence_release, the last release fence taken by each thread
1147 if (act->is_fence() && act->is_release()) {
1148 if ((int)thrd_last_fence_release.size() <= tid)
1149 thrd_last_fence_release.resize(get_num_threads());
1150 thrd_last_fence_release[tid] = act;
1153 if (act->is_wait()) {
1154 void *mutex_loc = (void *) act->get_value();
1155 act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
1157 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1158 if ((int)vec->size() <= tid) {
1159 uint oldsize = vec->size();
1160 vec->resize(priv->next_thread_id);
1161 for(uint i = oldsize;i < priv->next_thread_id;i++)
1162 new (&(*vec)[i]) action_list_t();
1164 act->setThrdMapRef((*vec)[tid].add_back(act));
1168 sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *act) {
1169 sllnode<ModelAction*> * rit = list->end();
1170 modelclock_t next_seq = act->get_seq_number();
1171 if (rit == NULL || (rit->getVal()->get_seq_number() <= next_seq))
1172 return list->add_back(act);
1174 for(;rit != NULL;rit=rit->getPrev()) {
1175 if (rit->getVal()->get_seq_number() <= next_seq) {
1176 return list->insertAfter(rit, act);
1179 return list->add_front(act);
1183 sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1184 sllnode<ModelAction*> * rit = list->end();
1185 modelclock_t next_seq = act->get_seq_number();
1187 act->create_cv(NULL);
1188 return list->add_back(act);
1189 } else if (rit->getVal()->get_seq_number() <= next_seq) {
1190 act->create_cv(rit->getVal());
1191 return list->add_back(act);
1193 for(;rit != NULL;rit=rit->getPrev()) {
1194 if (rit->getVal()->get_seq_number() <= next_seq) {
1195 act->create_cv(rit->getVal());
1196 return list->insertAfter(rit, act);
1199 return list->add_front(act);
1204 * Performs various bookkeeping operations for a normal write. The
1205 * complication is that we are typically inserting a normal write
1206 * lazily, so we need to insert it into the middle of lists.
1208 * @param act is the ModelAction to add.
1211 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1213 int tid = id_to_int(act->get_tid());
1214 act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
1216 // Update obj_thrd_map, a per location, per thread, order of actions
1217 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1218 if (tid >= (int)vec->size()) {
1219 uint oldsize =vec->size();
1220 vec->resize(priv->next_thread_id);
1221 for(uint i=oldsize;i<priv->next_thread_id;i++)
1222 new (&(*vec)[i]) action_list_t();
1224 act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
1226 ModelAction * lastact = thrd_last_action[tid];
1227 // Update thrd_last_action, the last action taken by each thrad
1228 if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
1229 thrd_last_action[tid] = act;
1233 void ModelExecution::add_write_to_lists(ModelAction *write) {
1234 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1235 int tid = id_to_int(write->get_tid());
1236 if (tid >= (int)vec->size()) {
1237 uint oldsize =vec->size();
1238 vec->resize(priv->next_thread_id);
1239 for(uint i=oldsize;i<priv->next_thread_id;i++)
1240 new (&(*vec)[i]) action_list_t();
1242 write->setActionRef((*vec)[tid].add_back(write));
1246 * @brief Get the last action performed by a particular Thread
1247 * @param tid The thread ID of the Thread in question
1248 * @return The last action in the thread
1250 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1252 int threadid = id_to_int(tid);
1253 if (threadid < (int)thrd_last_action.size())
1254 return thrd_last_action[id_to_int(tid)];
1260 * @brief Get the last fence release performed by a particular Thread
1261 * @param tid The thread ID of the Thread in question
1262 * @return The last fence release in the thread, if one exists; NULL otherwise
1264 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1266 int threadid = id_to_int(tid);
1267 if (threadid < (int)thrd_last_fence_release.size())
1268 return thrd_last_fence_release[id_to_int(tid)];
1274 * Gets the last memory_order_seq_cst write (in the total global sequence)
1275 * performed on a particular object (i.e., memory location), not including the
1277 * @param curr The current ModelAction; also denotes the object location to
1279 * @return The last seq_cst write
1281 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1283 void *location = curr->get_location();
1284 return obj_last_sc_map.get(location);
1288 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1289 * performed in a particular thread, prior to a particular fence.
1290 * @param tid The ID of the thread to check
1291 * @param before_fence The fence from which to begin the search; if NULL, then
1292 * search for the most recent fence in the thread.
1293 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1295 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1297 /* All fences should have location FENCE_LOCATION */
1298 action_list_t *list = obj_map.get(FENCE_LOCATION);
1303 sllnode<ModelAction*>* rit = list->end();
1306 for (;rit != NULL;rit=rit->getPrev())
1307 if (rit->getVal() == before_fence)
1310 ASSERT(rit->getVal() == before_fence);
1314 for (;rit != NULL;rit=rit->getPrev()) {
1315 ModelAction *act = rit->getVal();
1316 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1323 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1324 * location). This function identifies the mutex according to the current
1325 * action, which is presumed to perform on the same mutex.
1326 * @param curr The current ModelAction; also denotes the object location to
1328 * @return The last unlock operation
1330 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1332 void *location = curr->get_location();
1334 action_list_t *list = obj_map.get(location);
1338 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1339 sllnode<ModelAction*>* rit;
1340 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1341 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1342 return rit->getVal();
1346 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1348 ModelAction *parent = get_last_action(tid);
1350 parent = get_thread(tid)->get_creation();
1355 * Returns the clock vector for a given thread.
1356 * @param tid The thread whose clock vector we want
1357 * @return Desired clock vector
1359 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1361 ModelAction *firstaction=get_parent_action(tid);
1362 return firstaction != NULL ? firstaction->get_cv() : NULL;
1365 bool valequals(uint64_t val1, uint64_t val2, int size) {
1368 return ((uint8_t)val1) == ((uint8_t)val2);
1370 return ((uint16_t)val1) == ((uint16_t)val2);
1372 return ((uint32_t)val1) == ((uint32_t)val2);
1382 * Build up an initial set of all past writes that this 'read' action may read
1383 * from, as well as any previously-observed future values that must still be valid.
1385 * @param curr is the current ModelAction that we are exploring; it must be a
1388 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1390 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1392 ASSERT(curr->is_read());
1394 ModelAction *last_sc_write = NULL;
1396 if (curr->is_seqcst())
1397 last_sc_write = get_last_seq_cst_write(curr);
1399 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1401 /* Iterate over all threads */
1402 if (thrd_lists != NULL)
1403 for (i = 0;i < thrd_lists->size();i++) {
1404 /* Iterate over actions in thread, starting from most recent */
1405 action_list_t *list = &(*thrd_lists)[i];
1406 sllnode<ModelAction *> * rit;
1407 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1408 ModelAction *act = rit->getVal();
1413 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1414 bool allow_read = true;
1416 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1419 /* Need to check whether we will have two RMW reading from the same value */
1420 if (curr->is_rmwr()) {
1421 /* It is okay if we have a failing CAS */
1422 if (!curr->is_rmwrcas() ||
1423 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1424 //Need to make sure we aren't the second RMW
1425 CycleNode * node = mo_graph->getNode_noCreate(act);
1426 if (node != NULL && node->getRMW() != NULL) {
1427 //we are the second RMW
1434 /* Only add feasible reads */
1435 rf_set->push_back(act);
1438 /* Include at most one act per-thread that "happens before" curr */
1439 if (act->happens_before(curr))
1444 if (DBG_ENABLED()) {
1445 model_print("Reached read action:\n");
1447 model_print("End printing read_from_past\n");
1452 static void print_list(action_list_t *list)
1454 sllnode<ModelAction*> *it;
1456 model_print("------------------------------------------------------------------------------------\n");
1457 model_print("# t Action type MO Location Value Rf CV\n");
1458 model_print("------------------------------------------------------------------------------------\n");
1460 unsigned int hash = 0;
1462 for (it = list->begin();it != NULL;it=it->getNext()) {
1463 const ModelAction *act = it->getVal();
1464 if (act->get_seq_number() > 0)
1466 hash = hash^(hash<<3)^(it->getVal()->hash());
1468 model_print("HASH %u\n", hash);
1469 model_print("------------------------------------------------------------------------------------\n");
1472 #if SUPPORT_MOD_ORDER_DUMP
1473 void ModelExecution::dumpGraph(char *filename)
1476 sprintf(buffer, "%s.dot", filename);
1477 FILE *file = fopen(buffer, "w");
1478 fprintf(file, "digraph %s {\n", filename);
1479 mo_graph->dumpNodes(file);
1480 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1482 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1483 ModelAction *act = it->getVal();
1484 if (act->is_read()) {
1485 mo_graph->dot_print_node(file, act);
1486 mo_graph->dot_print_edge(file,
1487 act->get_reads_from(),
1489 "label=\"rf\", color=red, weight=2");
1491 if (thread_array[act->get_tid()]) {
1492 mo_graph->dot_print_edge(file,
1493 thread_array[id_to_int(act->get_tid())],
1495 "label=\"sb\", color=blue, weight=400");
1498 thread_array[act->get_tid()] = act;
1500 fprintf(file, "}\n");
1501 model_free(thread_array);
1506 /** @brief Prints an execution trace summary. */
1507 void ModelExecution::print_summary()
1509 #if SUPPORT_MOD_ORDER_DUMP
1510 char buffername[100];
1511 sprintf(buffername, "exec%04u", get_execution_number());
1512 mo_graph->dumpGraphToFile(buffername);
1513 sprintf(buffername, "graph%04u", get_execution_number());
1514 dumpGraph(buffername);
1517 model_print("Execution trace %d:", get_execution_number());
1518 if (scheduler->all_threads_sleeping())
1519 model_print(" SLEEP-SET REDUNDANT");
1520 if (have_bug_reports())
1521 model_print(" DETECTED BUG(S)");
1525 print_list(&action_trace);
1531 * Add a Thread to the system for the first time. Should only be called once
1533 * @param t The Thread to add
1535 void ModelExecution::add_thread(Thread *t)
1537 unsigned int i = id_to_int(t->get_id());
1538 if (i >= thread_map.size())
1539 thread_map.resize(i + 1);
1541 if (!t->is_model_thread())
1542 scheduler->add_thread(t);
1546 * @brief Get a Thread reference by its ID
1547 * @param tid The Thread's ID
1548 * @return A Thread reference
1550 Thread * ModelExecution::get_thread(thread_id_t tid) const
1552 unsigned int i = id_to_int(tid);
1553 if (i < thread_map.size())
1554 return thread_map[i];
1559 * @brief Get a reference to the Thread in which a ModelAction was executed
1560 * @param act The ModelAction
1561 * @return A Thread reference
1563 Thread * ModelExecution::get_thread(const ModelAction *act) const
1565 return get_thread(act->get_tid());
1569 * @brief Get a Thread reference by its pthread ID
1570 * @param index The pthread's ID
1571 * @return A Thread reference
1573 Thread * ModelExecution::get_pthread(pthread_t pid) {
1579 uint32_t thread_id = x.v;
1580 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1585 * @brief Check if a Thread is currently enabled
1586 * @param t The Thread to check
1587 * @return True if the Thread is currently enabled
1589 bool ModelExecution::is_enabled(Thread *t) const
1591 return scheduler->is_enabled(t);
1595 * @brief Check if a Thread is currently enabled
1596 * @param tid The ID of the Thread to check
1597 * @return True if the Thread is currently enabled
1599 bool ModelExecution::is_enabled(thread_id_t tid) const
1601 return scheduler->is_enabled(tid);
1605 * @brief Select the next thread to execute based on the curren action
1607 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1608 * actions should be followed by the execution of their child thread. In either
1609 * case, the current action should determine the next thread schedule.
1611 * @param curr The current action
1612 * @return The next thread to run, if the current action will determine this
1613 * selection; otherwise NULL
1615 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1617 /* Do not split atomic RMW */
1618 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1619 return get_thread(curr);
1620 /* Follow CREATE with the created thread */
1621 /* which is not needed, because model.cc takes care of this */
1622 if (curr->get_type() == THREAD_CREATE)
1623 return curr->get_thread_operand();
1624 if (curr->get_type() == PTHREAD_CREATE) {
1625 return curr->get_thread_operand();
1630 /** @param act A read atomic action */
1631 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1633 ASSERT(act->is_read());
1635 // Actions paused by fuzzer have their sequence number reset to 0
1636 return act->get_seq_number() == 0;
1640 * Takes the next step in the execution, if possible.
1641 * @param curr The current step to take
1642 * @return Returns the next Thread to run, if any; NULL if this execution
1645 Thread * ModelExecution::take_step(ModelAction *curr)
1647 Thread *curr_thrd = get_thread(curr);
1648 ASSERT(curr_thrd->get_state() == THREAD_READY);
1650 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1651 curr = check_current_action(curr);
1654 /* Process this action in ModelHistory for records */
1655 model->get_history()->process_action( curr, curr->get_tid() );
1657 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1658 scheduler->remove_thread(curr_thrd);
1660 return action_select_next_thread(curr);
1663 /** This method removes references to an Action before we delete it. */
1665 void ModelExecution::removeAction(ModelAction *act) {
1667 sllnode<ModelAction *> * listref = act->getTraceRef();
1668 if (listref != NULL) {
1669 action_trace.erase(listref);
1673 sllnode<ModelAction *> * listref = act->getThrdMapRef();
1674 if (listref != NULL) {
1675 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1676 (*vec)[act->get_tid()].erase(listref);
1679 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1680 sllnode<ModelAction *> * listref = act->getActionRef();
1681 if (listref != NULL) {
1682 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1683 list->erase(listref);
1685 } else if (act->is_wait()) {
1686 sllnode<ModelAction *> * listref = act->getActionRef();
1687 if (listref != NULL) {
1688 void *mutex_loc = (void *) act->get_value();
1689 get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
1691 } else if (act->is_free()) {
1692 sllnode<ModelAction *> * listref = act->getActionRef();
1693 if (listref != NULL) {
1694 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1695 (*vec)[act->get_tid()].erase(listref);
1697 //Clear it from last_sc_map
1698 if (obj_last_sc_map.get(act->get_location()) == act) {
1699 obj_last_sc_map.remove(act->get_location());
1702 //Remove from Cyclegraph
1703 mo_graph->freeAction(act);
1707 /** Computes clock vector that all running threads have already synchronized to. */
1709 ClockVector * ModelExecution::computeMinimalCV() {
1710 ClockVector *cvmin = NULL;
1711 //Thread 0 isn't a real thread, so skip it..
1712 for(unsigned int i = 1;i < thread_map.size();i++) {
1713 Thread * t = thread_map[i];
1714 if (t->get_state() == THREAD_COMPLETED)
1716 thread_id_t tid = int_to_id(i);
1717 ClockVector * cv = get_cv(tid);
1719 cvmin = new ClockVector(cv, NULL);
1721 cvmin->minmerge(cv);
1727 /** Sometimes we need to remove an action that is the most recent in the thread. This happens if it is mo before action in other threads. In that case we need to create a replacement latest ModelAction */
1729 void ModelExecution::fixupLastAct(ModelAction *act) {
1730 ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, get_thread(act->get_tid()));
1731 newact->set_seq_number(get_next_seq_num());
1732 newact->create_cv(act);
1733 newact->set_last_fence_release(act->get_last_fence_release());
1734 add_action_to_lists(newact, false);
1737 /** Compute which actions to free. */
1739 void ModelExecution::collectActions() {
1740 //Compute minimal clock vector for all live threads
1741 ClockVector *cvmin = computeMinimalCV();
1742 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1743 modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1745 //Next walk action trace... When we hit an action, see if it is
1746 //invisible (e.g., earlier than the first before the minimum
1747 //clock for the thread... if so erase it and all previous
1748 //actions in cyclegraph
1749 sllnode<ModelAction*> * it;
1750 for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1751 ModelAction *act = it->getVal();
1752 modelclock_t actseq = act->get_seq_number();
1754 //See if we are done
1755 if (actseq > maxtofree)
1758 thread_id_t act_tid = act->get_tid();
1759 modelclock_t tid_clock = cvmin->getClock(act_tid);
1761 //Free if it is invisible or we have set a flag to remove visible actions.
1762 if (actseq <= tid_clock || params->removevisible) {
1763 ModelAction * write;
1764 if (act->is_write()) {
1766 } else if (act->is_read()) {
1767 write = act->get_reads_from();
1771 //Mark everything earlier in MO graph to be freed
1772 CycleNode * cn = mo_graph->getNode_noCreate(write);
1774 queue->push_back(cn);
1775 while(!queue->empty()) {
1776 CycleNode * node = queue->back();
1778 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1779 CycleNode * prevnode = node->getInEdge(i);
1780 ModelAction * prevact = prevnode->getAction();
1781 if (prevact->get_type() != READY_FREE) {
1782 prevact->set_free();
1783 queue->push_back(prevnode);
1791 //We may need to remove read actions in the window we don't delete to preserve correctness.
1793 for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1794 ModelAction *act = it2->getVal();
1795 //Do iteration early in case we delete the act
1797 bool islastact = false;
1798 ModelAction *lastact = get_last_action(act->get_tid());
1799 if (act == lastact) {
1800 Thread * th = get_thread(act);
1801 islastact = !th->is_complete();
1804 if (act->is_read()) {
1805 if (act->get_reads_from()->is_free()) {
1806 if (act->is_rmw()) {
1807 //Weaken a RMW from a freed store to a write
1808 act->set_type(ATOMIC_WRITE);
1819 //If we don't delete the action, we should remove references to release fences
1821 const ModelAction *rel_fence =act->get_last_fence_release();
1822 if (rel_fence != NULL) {
1823 modelclock_t relfenceseq = rel_fence->get_seq_number();
1824 thread_id_t relfence_tid = rel_fence->get_tid();
1825 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1826 //Remove references to irrelevant release fences
1827 if (relfenceseq <= tid_clock)
1828 act->set_last_fence_release(NULL);
1831 //Now we are in the window of old actions that we remove if possible
1832 for (;it != NULL;) {
1833 ModelAction *act = it->getVal();
1834 //Do iteration early since we may delete node...
1836 bool islastact = false;
1837 ModelAction *lastact = get_last_action(act->get_tid());
1838 if (act == lastact) {
1839 Thread * th = get_thread(act);
1840 islastact = !th->is_complete();
1843 if (act->is_read()) {
1844 if (act->get_reads_from()->is_free()) {
1845 if (act->is_rmw()) {
1846 act->set_type(ATOMIC_WRITE);
1856 } else if (act->is_free()) {
1863 } else if (act->is_write()) {
1864 //Do nothing with write that hasn't been marked to be freed
1865 } else if (islastact) {
1866 //Keep the last action for non-read/write actions
1867 } else if (act->is_fence()) {
1868 //Note that acquire fences can always be safely
1869 //removed, but could incur extra overheads in
1870 //traversals. Removing them before the cvmin seems
1871 //like a good compromise.
1873 //Release fences before the cvmin don't do anything
1874 //because everyone has already synchronized.
1876 //Sequentially fences before cvmin are redundant
1877 //because happens-before will enforce same
1880 modelclock_t actseq = act->get_seq_number();
1881 thread_id_t act_tid = act->get_tid();
1882 modelclock_t tid_clock = cvmin->getClock(act_tid);
1883 if (actseq <= tid_clock) {
1889 //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1890 //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1891 //need to keep most recent unlock/wait for each lock
1892 if(act->is_unlock() || act->is_wait()) {
1893 ModelAction * lastlock = get_last_unlock(act);
1894 if (lastlock != act) {
1899 } else if (act->is_create()) {
1900 if (act->get_thread_operand()->is_complete()) {
1911 //If we don't delete the action, we should remove references to release fences
1912 const ModelAction *rel_fence =act->get_last_fence_release();
1913 if (rel_fence != NULL) {
1914 modelclock_t relfenceseq = rel_fence->get_seq_number();
1915 thread_id_t relfence_tid = rel_fence->get_tid();
1916 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1917 //Remove references to irrelevant release fences
1918 if (relfenceseq <= tid_clock)
1919 act->set_last_fence_release(NULL);
1929 Fuzzer * ModelExecution::getFuzzer() {