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()),
66 fuzzer(new NewFuzzer()),
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(m->get_history(), 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 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
133 void ModelExecution::restore_last_seq_num()
135 priv->used_sequence_numbers--;
139 * @brief Should the current action wake up a given thread?
141 * @param curr The current action
142 * @param thread The thread that we might wake up
143 * @return True, if we should wake up the sleeping thread; false otherwise
145 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
147 const ModelAction *asleep = thread->get_pending();
148 /* Don't allow partial RMW to wake anyone up */
151 /* Synchronizing actions may have been backtracked */
152 if (asleep->could_synchronize_with(curr))
154 /* All acquire/release fences and fence-acquire/store-release */
155 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
157 /* Fence-release + store can awake load-acquire on the same location */
158 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
159 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
160 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
163 /* The sleep is literally sleeping */
164 if (asleep->is_sleep()) {
165 if (fuzzer->shouldWake(asleep))
172 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
174 for (unsigned int i = 0;i < get_num_threads();i++) {
175 Thread *thr = get_thread(int_to_id(i));
176 if (scheduler->is_sleep_set(thr)) {
177 if (should_wake_up(curr, thr)) {
178 /* Remove this thread from sleep set */
179 scheduler->remove_sleep(thr);
180 if (thr->get_pending()->is_sleep())
181 thr->set_wakeup_state(true);
187 void ModelExecution::assert_bug(const char *msg)
189 priv->bugs.push_back(new bug_message(msg));
193 /** @return True, if any bugs have been reported for this execution */
194 bool ModelExecution::have_bug_reports() const
196 return priv->bugs.size() != 0;
199 SnapVector<bug_message *> * ModelExecution::get_bugs() const
205 * Check whether the current trace has triggered an assertion which should halt
208 * @return True, if the execution should be aborted; false otherwise
210 bool ModelExecution::has_asserted() const
212 return priv->asserted;
216 * Trigger a trace assertion which should cause this execution to be halted.
217 * This can be due to a detected bug or due to an infeasibility that should
220 void ModelExecution::set_assert()
222 priv->asserted = true;
226 * Check if we are in a deadlock. Should only be called at the end of an
227 * execution, although it should not give false positives in the middle of an
228 * execution (there should be some ENABLED thread).
230 * @return True if program is in a deadlock; false otherwise
232 bool ModelExecution::is_deadlocked() const
234 bool blocking_threads = false;
235 for (unsigned int i = 0;i < get_num_threads();i++) {
236 thread_id_t tid = int_to_id(i);
239 Thread *t = get_thread(tid);
240 if (!t->is_model_thread() && t->get_pending())
241 blocking_threads = true;
243 return blocking_threads;
247 * Check if this is a complete execution. That is, have all thread completed
248 * execution (rather than exiting because sleep sets have forced a redundant
251 * @return True if the execution is complete.
253 bool ModelExecution::is_complete_execution() const
255 for (unsigned int i = 0;i < get_num_threads();i++)
256 if (is_enabled(int_to_id(i)))
261 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
262 uint64_t value = *((const uint64_t *) location);
263 modelclock_t storeclock;
264 thread_id_t storethread;
265 getStoreThreadAndClock(location, &storethread, &storeclock);
266 setAtomicStoreFlag(location);
267 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
268 act->set_seq_number(storeclock);
269 add_normal_write_to_lists(act);
270 add_write_to_lists(act);
271 w_modification_order(act);
272 model->get_history()->process_action(act, act->get_tid());
277 * Processes a read model action.
278 * @param curr is the read model action to process.
279 * @param rf_set is the set of model actions we can possibly read from
280 * @return True if processing this read updates the mo_graph.
282 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
284 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
285 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
286 if (hasnonatomicstore) {
287 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
288 rf_set->push_back(nonatomicstore);
291 // Remove writes that violate read modification order
293 while (i < rf_set->size()) {
294 ModelAction * rf = (*rf_set)[i];
295 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
296 (*rf_set)[i] = rf_set->back();
303 int index = fuzzer->selectWrite(curr, rf_set);
305 ModelAction *rf = (*rf_set)[index];
308 bool canprune = false;
309 if (r_modification_order(curr, rf, priorset, &canprune)) {
310 for(unsigned int i=0;i<priorset->size();i++) {
311 mo_graph->addEdge((*priorset)[i], rf);
314 get_thread(curr)->set_return_value(curr->get_return_value());
316 if (canprune && curr->get_type() == ATOMIC_READ) {
317 int tid = id_to_int(curr->get_tid());
318 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
319 curr->setThrdMapRef(NULL);
325 /* TODO: Following code not needed anymore */
327 (*rf_set)[index] = rf_set->back();
333 * Processes a lock, trylock, or unlock model action. @param curr is
334 * the read model action to process.
336 * The try lock operation checks whether the lock is taken. If not,
337 * it falls to the normal lock operation case. If so, it returns
340 * The lock operation has already been checked that it is enabled, so
341 * it just grabs the lock and synchronizes with the previous unlock.
343 * The unlock operation has to re-enable all of the threads that are
344 * waiting on the lock.
346 * @return True if synchronization was updated; false otherwise
348 bool ModelExecution::process_mutex(ModelAction *curr)
350 cdsc::mutex *mutex = curr->get_mutex();
351 struct cdsc::mutex_state *state = NULL;
354 state = mutex->get_state();
356 switch (curr->get_type()) {
357 case ATOMIC_TRYLOCK: {
358 bool success = !state->locked;
359 curr->set_try_lock(success);
361 get_thread(curr)->set_return_value(0);
364 get_thread(curr)->set_return_value(1);
366 //otherwise fall into the lock case
368 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
369 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
370 // assert_bug("Lock access before initialization");
371 state->locked = get_thread(curr);
372 ModelAction *unlock = get_last_unlock(curr);
373 //synchronize with the previous unlock statement
374 if (unlock != NULL) {
375 synchronize(unlock, curr);
381 /* wake up the other threads */
382 for (unsigned int i = 0;i < get_num_threads();i++) {
383 Thread *t = get_thread(int_to_id(i));
384 Thread *curr_thrd = get_thread(curr);
385 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
389 /* unlock the lock - after checking who was waiting on it */
390 state->locked = NULL;
392 if (fuzzer->shouldWait(curr)) {
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 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...
404 /* wake up the other threads */
405 for (unsigned int i = 0;i < get_num_threads();i++) {
406 Thread *t = get_thread(int_to_id(i));
407 Thread *curr_thrd = get_thread(curr);
408 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
412 /* unlock the lock - after checking who was waiting on it */
413 state->locked = NULL;
416 case ATOMIC_NOTIFY_ALL: {
417 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
418 //activate all the waiting threads
419 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
420 scheduler->wake(get_thread(rit->getVal()));
425 case ATOMIC_NOTIFY_ONE: {
426 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
427 if (waiters->size() != 0) {
428 Thread * thread = fuzzer->selectNotify(waiters);
429 scheduler->wake(thread);
441 * Process a write ModelAction
442 * @param curr The ModelAction to process
443 * @return True if the mo_graph was updated or promises were resolved
445 void ModelExecution::process_write(ModelAction *curr)
447 w_modification_order(curr);
448 get_thread(curr)->set_return_value(VALUE_NONE);
452 * Process a fence ModelAction
453 * @param curr The ModelAction to process
454 * @return True if synchronization was updated
456 bool ModelExecution::process_fence(ModelAction *curr)
459 * fence-relaxed: no-op
460 * fence-release: only log the occurence (not in this function), for
461 * use in later synchronization
462 * fence-acquire (this function): search for hypothetical release
464 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
466 bool updated = false;
467 if (curr->is_acquire()) {
468 action_list_t *list = &action_trace;
469 sllnode<ModelAction *> * rit;
470 /* Find X : is_read(X) && X --sb-> curr */
471 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
472 ModelAction *act = rit->getVal();
475 if (act->get_tid() != curr->get_tid())
477 /* Stop at the beginning of the thread */
478 if (act->is_thread_start())
480 /* Stop once we reach a prior fence-acquire */
481 if (act->is_fence() && act->is_acquire())
485 /* read-acquire will find its own release sequences */
486 if (act->is_acquire())
489 /* Establish hypothetical release sequences */
490 ClockVector *cv = get_hb_from_write(act->get_reads_from());
491 if (cv != NULL && curr->get_cv()->merge(cv))
499 * @brief Process the current action for thread-related activity
501 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
502 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
503 * synchronization, etc. This function is a no-op for non-THREAD actions
504 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
506 * @param curr The current action
507 * @return True if synchronization was updated or a thread completed
509 void ModelExecution::process_thread_action(ModelAction *curr)
511 switch (curr->get_type()) {
512 case THREAD_CREATE: {
513 thrd_t *thrd = (thrd_t *)curr->get_location();
514 struct thread_params *params = (struct thread_params *)curr->get_value();
515 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
516 curr->set_thread_operand(th);
518 th->set_creation(curr);
521 case PTHREAD_CREATE: {
522 (*(uint32_t *)curr->get_location()) = pthread_counter++;
524 struct pthread_params *params = (struct pthread_params *)curr->get_value();
525 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
526 curr->set_thread_operand(th);
528 th->set_creation(curr);
530 if ( pthread_map.size() < pthread_counter )
531 pthread_map.resize( pthread_counter );
532 pthread_map[ pthread_counter-1 ] = th;
537 Thread *blocking = curr->get_thread_operand();
538 ModelAction *act = get_last_action(blocking->get_id());
539 synchronize(act, curr);
543 Thread *blocking = curr->get_thread_operand();
544 ModelAction *act = get_last_action(blocking->get_id());
545 synchronize(act, curr);
546 break; // WL: to be add (modified)
549 case THREADONLY_FINISH:
550 case THREAD_FINISH: {
551 Thread *th = get_thread(curr);
552 if (curr->get_type() == THREAD_FINISH &&
553 th == model->getInitThread()) {
559 /* Wake up any joining threads */
560 for (unsigned int i = 0;i < get_num_threads();i++) {
561 Thread *waiting = get_thread(int_to_id(i));
562 if (waiting->waiting_on() == th &&
563 waiting->get_pending()->is_thread_join())
564 scheduler->wake(waiting);
573 Thread *th = get_thread(curr);
574 th->set_pending(curr);
575 scheduler->add_sleep(th);
584 * Initialize the current action by performing one or more of the following
585 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
586 * manipulating backtracking sets, allocating and
587 * initializing clock vectors, and computing the promises to fulfill.
589 * @param curr The current action, as passed from the user context; may be
590 * freed/invalidated after the execution of this function, with a different
591 * action "returned" its place (pass-by-reference)
592 * @return True if curr is a newly-explored action; false otherwise
594 bool ModelExecution::initialize_curr_action(ModelAction **curr)
596 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
597 ModelAction *newcurr = process_rmw(*curr);
603 ModelAction *newcurr = *curr;
605 newcurr->set_seq_number(get_next_seq_num());
606 /* Always compute new clock vector */
607 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
609 /* Assign most recent release fence */
610 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
612 return true; /* This was a new ModelAction */
617 * @brief Establish reads-from relation between two actions
619 * Perform basic operations involved with establishing a concrete rf relation,
620 * including setting the ModelAction data and checking for release sequences.
622 * @param act The action that is reading (must be a read)
623 * @param rf The action from which we are reading (must be a write)
625 * @return True if this read established synchronization
628 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
631 ASSERT(rf->is_write());
633 act->set_read_from(rf);
634 if (act->is_acquire()) {
635 ClockVector *cv = get_hb_from_write(rf);
638 act->get_cv()->merge(cv);
643 * @brief Synchronizes two actions
645 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
646 * This function performs the synchronization as well as providing other hooks
647 * for other checks along with synchronization.
649 * @param first The left-hand side of the synchronizes-with relation
650 * @param second The right-hand side of the synchronizes-with relation
651 * @return True if the synchronization was successful (i.e., was consistent
652 * with the execution order); false otherwise
654 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
656 if (*second < *first) {
657 ASSERT(0); //This should not happend
660 return second->synchronize_with(first);
664 * @brief Check whether a model action is enabled.
666 * Checks whether an operation would be successful (i.e., is a lock already
667 * locked, or is the joined thread already complete).
669 * For yield-blocking, yields are never enabled.
671 * @param curr is the ModelAction to check whether it is enabled.
672 * @return a bool that indicates whether the action is enabled.
674 bool ModelExecution::check_action_enabled(ModelAction *curr) {
675 if (curr->is_lock()) {
676 cdsc::mutex *lock = curr->get_mutex();
677 struct cdsc::mutex_state *state = lock->get_state();
680 } else if (curr->is_thread_join()) {
681 Thread *blocking = curr->get_thread_operand();
682 if (!blocking->is_complete()) {
685 } else if (curr->is_sleep()) {
686 if (!fuzzer->shouldSleep(curr))
694 * This is the heart of the model checker routine. It performs model-checking
695 * actions corresponding to a given "current action." Among other processes, it
696 * calculates reads-from relationships, updates synchronization clock vectors,
697 * forms a memory_order constraints graph, and handles replay/backtrack
698 * execution when running permutations of previously-observed executions.
700 * @param curr The current action to process
701 * @return The ModelAction that is actually executed; may be different than
704 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
707 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
708 bool newly_explored = initialize_curr_action(&curr);
712 wake_up_sleeping_actions(curr);
714 SnapVector<ModelAction *> * rf_set = NULL;
715 /* Build may_read_from set for newly-created actions */
716 if (newly_explored && curr->is_read())
717 rf_set = build_may_read_from(curr);
719 if (curr->is_read() && !second_part_of_rmw) {
720 process_read(curr, rf_set);
723 ASSERT(rf_set == NULL);
725 /* Add the action to lists */
726 if (!second_part_of_rmw)
727 add_action_to_lists(curr);
729 if (curr->is_write())
730 add_write_to_lists(curr);
732 process_thread_action(curr);
734 if (curr->is_write())
737 if (curr->is_fence())
740 if (curr->is_mutex_op())
746 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
747 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
748 ModelAction *lastread = get_last_action(act->get_tid());
749 lastread->process_rmw(act);
751 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
757 * @brief Updates the mo_graph with the constraints imposed from the current
760 * Basic idea is the following: Go through each other thread and find
761 * the last action that happened before our read. Two cases:
763 * -# The action is a write: that write must either occur before
764 * the write we read from or be the write we read from.
765 * -# The action is a read: the write that that action read from
766 * must occur before the write we read from or be the same write.
768 * @param curr The current action. Must be a read.
769 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
770 * @param check_only If true, then only check whether the current action satisfies
771 * read modification order or not, without modifiying priorset and canprune.
773 * @return True if modification order edges were added; false otherwise
776 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
777 SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
779 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
781 ASSERT(curr->is_read());
783 /* Last SC fence in the current thread */
784 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
786 int tid = curr->get_tid();
787 ModelAction *prev_same_thread = NULL;
788 /* Iterate over all threads */
789 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
790 /* Last SC fence in thread tid */
791 ModelAction *last_sc_fence_thread_local = NULL;
793 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
795 /* Last SC fence in thread tid, before last SC fence in current thread */
796 ModelAction *last_sc_fence_thread_before = NULL;
797 if (last_sc_fence_local)
798 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
800 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
801 if (prev_same_thread != NULL &&
802 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
803 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
807 /* Iterate over actions in thread, starting from most recent */
808 action_list_t *list = &(*thrd_lists)[tid];
809 sllnode<ModelAction *> * rit;
810 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
811 ModelAction *act = rit->getVal();
816 /* Don't want to add reflexive edges on 'rf' */
817 if (act->equals(rf)) {
818 if (act->happens_before(curr))
824 if (act->is_write()) {
825 /* C++, Section 29.3 statement 5 */
826 if (curr->is_seqcst() && last_sc_fence_thread_local &&
827 *act < *last_sc_fence_thread_local) {
828 if (mo_graph->checkReachable(rf, act))
831 priorset->push_back(act);
834 /* C++, Section 29.3 statement 4 */
835 else if (act->is_seqcst() && last_sc_fence_local &&
836 *act < *last_sc_fence_local) {
837 if (mo_graph->checkReachable(rf, act))
840 priorset->push_back(act);
843 /* C++, Section 29.3 statement 6 */
844 else if (last_sc_fence_thread_before &&
845 *act < *last_sc_fence_thread_before) {
846 if (mo_graph->checkReachable(rf, act))
849 priorset->push_back(act);
855 * Include at most one act per-thread that "happens
858 if (act->happens_before(curr)) {
860 if (last_sc_fence_local == NULL ||
861 (*last_sc_fence_local < *act)) {
862 prev_same_thread = act;
865 if (act->is_write()) {
866 if (mo_graph->checkReachable(rf, act))
869 priorset->push_back(act);
871 ModelAction *prevrf = act->get_reads_from();
872 if (!prevrf->equals(rf)) {
873 if (mo_graph->checkReachable(rf, prevrf))
876 priorset->push_back(prevrf);
878 if (act->get_tid() == curr->get_tid()) {
879 //Can prune curr from obj list
893 * Updates the mo_graph with the constraints imposed from the current write.
895 * Basic idea is the following: Go through each other thread and find
896 * the lastest action that happened before our write. Two cases:
898 * (1) The action is a write => that write must occur before
901 * (2) The action is a read => the write that that action read from
902 * must occur before the current write.
904 * This method also handles two other issues:
906 * (I) Sequential Consistency: Making sure that if the current write is
907 * seq_cst, that it occurs after the previous seq_cst write.
909 * (II) Sending the write back to non-synchronizing reads.
911 * @param curr The current action. Must be a write.
912 * @param send_fv A vector for stashing reads to which we may pass our future
913 * value. If NULL, then don't record any future values.
914 * @return True if modification order edges were added; false otherwise
916 void ModelExecution::w_modification_order(ModelAction *curr)
918 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
920 ASSERT(curr->is_write());
922 SnapList<ModelAction *> edgeset;
924 if (curr->is_seqcst()) {
925 /* We have to at least see the last sequentially consistent write,
926 so we are initialized. */
927 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
928 if (last_seq_cst != NULL) {
929 edgeset.push_back(last_seq_cst);
931 //update map for next query
932 obj_last_sc_map.put(curr->get_location(), curr);
935 /* Last SC fence in the current thread */
936 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
938 /* Iterate over all threads */
939 for (i = 0;i < thrd_lists->size();i++) {
940 /* Last SC fence in thread i, before last SC fence in current thread */
941 ModelAction *last_sc_fence_thread_before = NULL;
942 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
943 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
945 /* Iterate over actions in thread, starting from most recent */
946 action_list_t *list = &(*thrd_lists)[i];
947 sllnode<ModelAction*>* rit;
948 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
949 ModelAction *act = rit->getVal();
952 * 1) If RMW and it actually read from something, then we
953 * already have all relevant edges, so just skip to next
956 * 2) If RMW and it didn't read from anything, we should
957 * whatever edge we can get to speed up convergence.
959 * 3) If normal write, we need to look at earlier actions, so
960 * continue processing list.
962 if (curr->is_rmw()) {
963 if (curr->get_reads_from() != NULL)
971 /* C++, Section 29.3 statement 7 */
972 if (last_sc_fence_thread_before && act->is_write() &&
973 *act < *last_sc_fence_thread_before) {
974 edgeset.push_back(act);
979 * Include at most one act per-thread that "happens
982 if (act->happens_before(curr)) {
984 * Note: if act is RMW, just add edge:
986 * The following edge should be handled elsewhere:
987 * readfrom(act) --mo--> act
990 edgeset.push_back(act);
991 else if (act->is_read()) {
992 //if previous read accessed a null, just keep going
993 edgeset.push_back(act->get_reads_from());
999 mo_graph->addEdges(&edgeset, curr);
1004 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1005 * some constraints. This method checks one the following constraint (others
1006 * require compiler support):
1008 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1009 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1011 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1013 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1015 /* Iterate over all threads */
1016 for (i = 0;i < thrd_lists->size();i++) {
1017 const ModelAction *write_after_read = NULL;
1019 /* Iterate over actions in thread, starting from most recent */
1020 action_list_t *list = &(*thrd_lists)[i];
1021 sllnode<ModelAction *>* rit;
1022 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1023 ModelAction *act = rit->getVal();
1025 /* Don't disallow due to act == reader */
1026 if (!reader->happens_before(act) || reader == act)
1028 else if (act->is_write())
1029 write_after_read = act;
1030 else if (act->is_read() && act->get_reads_from() != NULL)
1031 write_after_read = act->get_reads_from();
1034 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1041 * Computes the clock vector that happens before propagates from this write.
1043 * @param rf The action that might be part of a release sequence. Must be a
1045 * @return ClockVector of happens before relation.
1048 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1049 SnapVector<ModelAction *> * processset = NULL;
1050 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1051 ASSERT(rf->is_write());
1052 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1054 if (processset == NULL)
1055 processset = new SnapVector<ModelAction *>();
1056 processset->push_back(rf);
1059 int i = (processset == NULL) ? 0 : processset->size();
1061 ClockVector * vec = NULL;
1063 if (rf->get_rfcv() != NULL) {
1064 vec = rf->get_rfcv();
1065 } else if (rf->is_acquire() && rf->is_release()) {
1067 } else if (rf->is_release() && !rf->is_rmw()) {
1069 } else if (rf->is_release()) {
1070 //have rmw that is release and doesn't have a rfcv
1071 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1074 //operation that isn't release
1075 if (rf->get_last_fence_release()) {
1077 vec = rf->get_last_fence_release()->get_cv();
1079 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1085 rf = (*processset)[i];
1089 if (processset != NULL)
1095 * Performs various bookkeeping operations for the current ModelAction. For
1096 * instance, adds action to the per-object, per-thread action vector and to the
1097 * action trace list of all thread actions.
1099 * @param act is the ModelAction to add.
1101 void ModelExecution::add_action_to_lists(ModelAction *act)
1103 int tid = id_to_int(act->get_tid());
1104 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1105 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1106 act->setActionRef(list->add_back(act));
1109 // Update action trace, a total order of all actions
1110 act->setTraceRef(action_trace.add_back(act));
1113 // Update obj_thrd_map, a per location, per thread, order of actions
1114 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1115 if ((int)vec->size() <= tid) {
1116 uint oldsize = vec->size();
1117 vec->resize(priv->next_thread_id);
1118 for(uint i = oldsize;i < priv->next_thread_id;i++)
1119 new (&(*vec)[i]) action_list_t();
1121 act->setThrdMapRef((*vec)[tid].add_back(act));
1123 // Update thrd_last_action, the last action taken by each thread
1124 if ((int)thrd_last_action.size() <= tid)
1125 thrd_last_action.resize(get_num_threads());
1126 thrd_last_action[tid] = act;
1128 // Update thrd_last_fence_release, the last release fence taken by each thread
1129 if (act->is_fence() && act->is_release()) {
1130 if ((int)thrd_last_fence_release.size() <= tid)
1131 thrd_last_fence_release.resize(get_num_threads());
1132 thrd_last_fence_release[tid] = act;
1135 if (act->is_wait()) {
1136 void *mutex_loc = (void *) act->get_value();
1137 act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
1139 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1140 if ((int)vec->size() <= tid) {
1141 uint oldsize = vec->size();
1142 vec->resize(priv->next_thread_id);
1143 for(uint i = oldsize;i < priv->next_thread_id;i++)
1144 new (&(*vec)[i]) action_list_t();
1146 act->setThrdMapRef((*vec)[tid].add_back(act));
1150 sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *act) {
1151 sllnode<ModelAction*> * rit = list->end();
1152 modelclock_t next_seq = act->get_seq_number();
1153 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1154 return list->add_back(act);
1156 for(;rit != NULL;rit=rit->getPrev()) {
1157 if (rit->getVal()->get_seq_number() == next_seq) {
1158 return list->insertAfter(rit, act);
1165 sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1166 sllnode<ModelAction*> * rit = list->end();
1167 modelclock_t next_seq = act->get_seq_number();
1169 act->create_cv(NULL);
1171 } else if (rit->getVal()->get_seq_number() == next_seq) {
1172 act->create_cv(rit->getVal());
1173 return list->add_back(act);
1175 for(;rit != NULL;rit=rit->getPrev()) {
1176 if (rit->getVal()->get_seq_number() == next_seq) {
1177 act->create_cv(rit->getVal());
1178 return list->insertAfter(rit, act);
1186 * Performs various bookkeeping operations for a normal write. The
1187 * complication is that we are typically inserting a normal write
1188 * lazily, so we need to insert it into the middle of lists.
1190 * @param act is the ModelAction to add.
1193 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1195 int tid = id_to_int(act->get_tid());
1196 act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
1198 // Update obj_thrd_map, a per location, per thread, order of actions
1199 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1200 if (tid >= (int)vec->size()) {
1201 uint oldsize =vec->size();
1202 vec->resize(priv->next_thread_id);
1203 for(uint i=oldsize;i<priv->next_thread_id;i++)
1204 new (&(*vec)[i]) action_list_t();
1206 act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
1208 // Update thrd_last_action, the last action taken by each thrad
1209 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1210 thrd_last_action[tid] = act;
1214 void ModelExecution::add_write_to_lists(ModelAction *write) {
1215 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1216 int tid = id_to_int(write->get_tid());
1217 if (tid >= (int)vec->size()) {
1218 uint oldsize =vec->size();
1219 vec->resize(priv->next_thread_id);
1220 for(uint i=oldsize;i<priv->next_thread_id;i++)
1221 new (&(*vec)[i]) action_list_t();
1223 write->setActionRef((*vec)[tid].add_back(write));
1227 * @brief Get the last action performed by a particular Thread
1228 * @param tid The thread ID of the Thread in question
1229 * @return The last action in the thread
1231 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1233 int threadid = id_to_int(tid);
1234 if (threadid < (int)thrd_last_action.size())
1235 return thrd_last_action[id_to_int(tid)];
1241 * @brief Get the last fence release performed by a particular Thread
1242 * @param tid The thread ID of the Thread in question
1243 * @return The last fence release in the thread, if one exists; NULL otherwise
1245 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1247 int threadid = id_to_int(tid);
1248 if (threadid < (int)thrd_last_fence_release.size())
1249 return thrd_last_fence_release[id_to_int(tid)];
1255 * Gets the last memory_order_seq_cst write (in the total global sequence)
1256 * performed on a particular object (i.e., memory location), not including the
1258 * @param curr The current ModelAction; also denotes the object location to
1260 * @return The last seq_cst write
1262 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1264 void *location = curr->get_location();
1265 return obj_last_sc_map.get(location);
1269 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1270 * performed in a particular thread, prior to a particular fence.
1271 * @param tid The ID of the thread to check
1272 * @param before_fence The fence from which to begin the search; if NULL, then
1273 * search for the most recent fence in the thread.
1274 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1276 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1278 /* All fences should have location FENCE_LOCATION */
1279 action_list_t *list = obj_map.get(FENCE_LOCATION);
1284 sllnode<ModelAction*>* rit = list->end();
1287 for (;rit != NULL;rit=rit->getPrev())
1288 if (rit->getVal() == before_fence)
1291 ASSERT(rit->getVal() == before_fence);
1295 for (;rit != NULL;rit=rit->getPrev()) {
1296 ModelAction *act = rit->getVal();
1297 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1304 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1305 * location). This function identifies the mutex according to the current
1306 * action, which is presumed to perform on the same mutex.
1307 * @param curr The current ModelAction; also denotes the object location to
1309 * @return The last unlock operation
1311 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1313 void *location = curr->get_location();
1315 action_list_t *list = obj_map.get(location);
1319 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1320 sllnode<ModelAction*>* rit;
1321 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1322 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1323 return rit->getVal();
1327 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1329 ModelAction *parent = get_last_action(tid);
1331 parent = get_thread(tid)->get_creation();
1336 * Returns the clock vector for a given thread.
1337 * @param tid The thread whose clock vector we want
1338 * @return Desired clock vector
1340 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1342 ModelAction *firstaction=get_parent_action(tid);
1343 return firstaction != NULL ? firstaction->get_cv() : NULL;
1346 bool valequals(uint64_t val1, uint64_t val2, int size) {
1349 return ((uint8_t)val1) == ((uint8_t)val2);
1351 return ((uint16_t)val1) == ((uint16_t)val2);
1353 return ((uint32_t)val1) == ((uint32_t)val2);
1363 * Build up an initial set of all past writes that this 'read' action may read
1364 * from, as well as any previously-observed future values that must still be valid.
1366 * @param curr is the current ModelAction that we are exploring; it must be a
1369 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1371 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1373 ASSERT(curr->is_read());
1375 ModelAction *last_sc_write = NULL;
1377 if (curr->is_seqcst())
1378 last_sc_write = get_last_seq_cst_write(curr);
1380 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1382 /* Iterate over all threads */
1383 for (i = 0;i < thrd_lists->size();i++) {
1384 /* Iterate over actions in thread, starting from most recent */
1385 action_list_t *list = &(*thrd_lists)[i];
1386 sllnode<ModelAction *> * rit;
1387 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1388 ModelAction *act = rit->getVal();
1393 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1394 bool allow_read = true;
1396 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1399 /* Need to check whether we will have two RMW reading from the same value */
1400 if (curr->is_rmwr()) {
1401 /* It is okay if we have a failing CAS */
1402 if (!curr->is_rmwrcas() ||
1403 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1404 //Need to make sure we aren't the second RMW
1405 CycleNode * node = mo_graph->getNode_noCreate(act);
1406 if (node != NULL && node->getRMW() != NULL) {
1407 //we are the second RMW
1414 /* Only add feasible reads */
1415 rf_set->push_back(act);
1418 /* Include at most one act per-thread that "happens before" curr */
1419 if (act->happens_before(curr))
1424 if (DBG_ENABLED()) {
1425 model_print("Reached read action:\n");
1427 model_print("End printing read_from_past\n");
1432 static void print_list(action_list_t *list)
1434 sllnode<ModelAction*> *it;
1436 model_print("------------------------------------------------------------------------------------\n");
1437 model_print("# t Action type MO Location Value Rf CV\n");
1438 model_print("------------------------------------------------------------------------------------\n");
1440 unsigned int hash = 0;
1442 for (it = list->begin();it != NULL;it=it->getNext()) {
1443 const ModelAction *act = it->getVal();
1444 if (act->get_seq_number() > 0)
1446 hash = hash^(hash<<3)^(it->getVal()->hash());
1448 model_print("HASH %u\n", hash);
1449 model_print("------------------------------------------------------------------------------------\n");
1452 #if SUPPORT_MOD_ORDER_DUMP
1453 void ModelExecution::dumpGraph(char *filename)
1456 sprintf(buffer, "%s.dot", filename);
1457 FILE *file = fopen(buffer, "w");
1458 fprintf(file, "digraph %s {\n", filename);
1459 mo_graph->dumpNodes(file);
1460 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1462 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1463 ModelAction *act = it->getVal();
1464 if (act->is_read()) {
1465 mo_graph->dot_print_node(file, act);
1466 mo_graph->dot_print_edge(file,
1467 act->get_reads_from(),
1469 "label=\"rf\", color=red, weight=2");
1471 if (thread_array[act->get_tid()]) {
1472 mo_graph->dot_print_edge(file,
1473 thread_array[id_to_int(act->get_tid())],
1475 "label=\"sb\", color=blue, weight=400");
1478 thread_array[act->get_tid()] = act;
1480 fprintf(file, "}\n");
1481 model_free(thread_array);
1486 /** @brief Prints an execution trace summary. */
1487 void ModelExecution::print_summary()
1489 #if SUPPORT_MOD_ORDER_DUMP
1490 char buffername[100];
1491 sprintf(buffername, "exec%04u", get_execution_number());
1492 mo_graph->dumpGraphToFile(buffername);
1493 sprintf(buffername, "graph%04u", get_execution_number());
1494 dumpGraph(buffername);
1497 model_print("Execution trace %d:", get_execution_number());
1498 if (scheduler->all_threads_sleeping())
1499 model_print(" SLEEP-SET REDUNDANT");
1500 if (have_bug_reports())
1501 model_print(" DETECTED BUG(S)");
1505 print_list(&action_trace);
1511 * Add a Thread to the system for the first time. Should only be called once
1513 * @param t The Thread to add
1515 void ModelExecution::add_thread(Thread *t)
1517 unsigned int i = id_to_int(t->get_id());
1518 if (i >= thread_map.size())
1519 thread_map.resize(i + 1);
1521 if (!t->is_model_thread())
1522 scheduler->add_thread(t);
1526 * @brief Get a Thread reference by its ID
1527 * @param tid The Thread's ID
1528 * @return A Thread reference
1530 Thread * ModelExecution::get_thread(thread_id_t tid) const
1532 unsigned int i = id_to_int(tid);
1533 if (i < thread_map.size())
1534 return thread_map[i];
1539 * @brief Get a reference to the Thread in which a ModelAction was executed
1540 * @param act The ModelAction
1541 * @return A Thread reference
1543 Thread * ModelExecution::get_thread(const ModelAction *act) const
1545 return get_thread(act->get_tid());
1549 * @brief Get a Thread reference by its pthread ID
1550 * @param index The pthread's ID
1551 * @return A Thread reference
1553 Thread * ModelExecution::get_pthread(pthread_t pid) {
1559 uint32_t thread_id = x.v;
1560 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1565 * @brief Check if a Thread is currently enabled
1566 * @param t The Thread to check
1567 * @return True if the Thread is currently enabled
1569 bool ModelExecution::is_enabled(Thread *t) const
1571 return scheduler->is_enabled(t);
1575 * @brief Check if a Thread is currently enabled
1576 * @param tid The ID of the Thread to check
1577 * @return True if the Thread is currently enabled
1579 bool ModelExecution::is_enabled(thread_id_t tid) const
1581 return scheduler->is_enabled(tid);
1585 * @brief Select the next thread to execute based on the curren action
1587 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1588 * actions should be followed by the execution of their child thread. In either
1589 * case, the current action should determine the next thread schedule.
1591 * @param curr The current action
1592 * @return The next thread to run, if the current action will determine this
1593 * selection; otherwise NULL
1595 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1597 /* Do not split atomic RMW */
1598 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1599 return get_thread(curr);
1600 /* Follow CREATE with the created thread */
1601 /* which is not needed, because model.cc takes care of this */
1602 if (curr->get_type() == THREAD_CREATE)
1603 return curr->get_thread_operand();
1604 if (curr->get_type() == PTHREAD_CREATE) {
1605 return curr->get_thread_operand();
1610 /** @param act A read atomic action */
1611 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1613 ASSERT(act->is_read());
1615 // Actions paused by fuzzer have their sequence number reset to 0
1616 return act->get_seq_number() == 0;
1620 * Takes the next step in the execution, if possible.
1621 * @param curr The current step to take
1622 * @return Returns the next Thread to run, if any; NULL if this execution
1625 Thread * ModelExecution::take_step(ModelAction *curr)
1627 Thread *curr_thrd = get_thread(curr);
1628 ASSERT(curr_thrd->get_state() == THREAD_READY);
1630 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1631 curr = check_current_action(curr);
1634 /* Process this action in ModelHistory for records */
1635 model->get_history()->process_action( curr, curr->get_tid() );
1637 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1638 scheduler->remove_thread(curr_thrd);
1640 return action_select_next_thread(curr);
1643 void ModelExecution::removeAction(ModelAction *act) {
1645 sllnode<ModelAction *> * listref = act->getTraceRef();
1646 if (listref != NULL) {
1647 action_trace.erase(listref);
1651 sllnode<ModelAction *> * listref = act->getThrdMapRef();
1652 if (listref != NULL) {
1653 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1654 (*vec)[act->get_tid()].erase(listref);
1657 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1658 sllnode<ModelAction *> * listref = act->getActionRef();
1659 if (listref != NULL) {
1660 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1661 list->erase(listref);
1663 } else if (act->is_wait()) {
1664 sllnode<ModelAction *> * listref = act->getActionRef();
1665 if (listref != NULL) {
1666 void *mutex_loc = (void *) act->get_value();
1667 get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
1669 } else if (act->is_write()) {
1670 sllnode<ModelAction *> * listref = act->getActionRef();
1671 if (listref != NULL) {
1672 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1673 (*vec)[act->get_tid()].erase(listref);
1675 //Remove from Cyclegraph
1676 mo_graph->freeAction(act);
1680 ClockVector * ModelExecution::computeMinimalCV() {
1681 ClockVector *cvmin = NULL;
1682 for(unsigned int i = 0;i < thread_map.size();i++) {
1683 Thread * t = thread_map[i];
1684 if (t->get_state() == THREAD_COMPLETED)
1686 thread_id_t tid = int_to_id(i);
1687 ClockVector * cv = get_cv(tid);
1689 cvmin = new ClockVector(cv, NULL);
1691 cvmin->minmerge(cv);
1696 void ModelExecution::collectActions() {
1697 //Compute minimal clock vector for all live threads
1698 ClockVector *cvmin = computeMinimalCV();
1699 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1700 //walk action trace... When we hit an action ,see if it is
1701 //invisible (e.g., earlier than the first before the minimum
1702 //clock for the thread... if so erase it and all previous
1703 //actions in cyclegraph
1704 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1705 ModelAction *act = it->getVal();
1706 modelclock_t actseq = act->get_seq_number();
1707 thread_id_t act_tid = act->get_tid();
1708 modelclock_t tid_clock = cvmin->getClock(act_tid);
1709 if (actseq <= tid_clock) {
1710 ModelAction * write;
1711 if (act->is_write()) {
1713 } else if (act->is_read()) {
1714 write = act->get_reads_from();
1718 //Mark everything earlier in MO graph to be freed
1719 queue->push_back(mo_graph->getNode_noCreate(write));
1720 while(!queue->empty()) {
1721 CycleNode * node = queue->back();
1723 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1724 CycleNode * prevnode = node->getInEdge(i);
1725 ModelAction * prevact = prevnode->getAction();
1726 if (prevact->get_type() != READY_FREE) {
1727 prevact->set_free();
1728 queue->push_back(prevnode);
1741 Fuzzer * ModelExecution::getFuzzer() {