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(),
66 thrd_last_fence_release(),
67 priv(new struct model_snapshot_members ()),
68 mo_graph(new CycleGraph()),
70 fuzzer(new NewFuzzer()),
76 /* Initialize a model-checker thread, for special ModelActions */
77 model_thread = new Thread(get_next_id());
78 add_thread(model_thread);
79 fuzzer->register_engine(m, this);
80 scheduler->register_engine(this);
82 pthread_key_create(&pthreadkey, tlsdestructor);
86 /** @brief Destructor */
87 ModelExecution::~ModelExecution()
89 for (unsigned int i = 0;i < get_num_threads();i++)
90 delete get_thread(int_to_id(i));
96 int ModelExecution::get_execution_number() const
98 return model->get_execution_number();
101 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
103 action_list_t *tmp = hash->get(ptr);
105 tmp = new action_list_t();
111 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
113 SnapVector<action_list_t> *tmp = hash->get(ptr);
115 tmp = new SnapVector<action_list_t>();
121 /** @return a thread ID for a new Thread */
122 thread_id_t ModelExecution::get_next_id()
124 return priv->next_thread_id++;
127 /** @return the number of user threads created during this execution */
128 unsigned int ModelExecution::get_num_threads() const
130 return priv->next_thread_id;
133 /** @return a sequence number for a new ModelAction */
134 modelclock_t ModelExecution::get_next_seq_num()
136 return ++priv->used_sequence_numbers;
139 /** @return a sequence number for a new ModelAction */
140 modelclock_t ModelExecution::get_curr_seq_num()
142 return priv->used_sequence_numbers;
145 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
146 void ModelExecution::restore_last_seq_num()
148 priv->used_sequence_numbers--;
152 * @brief Should the current action wake up a given thread?
154 * @param curr The current action
155 * @param thread The thread that we might wake up
156 * @return True, if we should wake up the sleeping thread; false otherwise
158 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
160 const ModelAction *asleep = thread->get_pending();
161 /* Don't allow partial RMW to wake anyone up */
164 /* Synchronizing actions may have been backtracked */
165 if (asleep->could_synchronize_with(curr))
167 /* All acquire/release fences and fence-acquire/store-release */
168 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
170 /* Fence-release + store can awake load-acquire on the same location */
171 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
172 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
173 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
176 /* The sleep is literally sleeping */
177 if (asleep->is_sleep()) {
178 if (fuzzer->shouldWake(asleep))
185 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
187 for (unsigned int i = 0;i < get_num_threads();i++) {
188 Thread *thr = get_thread(int_to_id(i));
189 if (scheduler->is_sleep_set(thr)) {
190 if (should_wake_up(curr, thr)) {
191 /* Remove this thread from sleep set */
192 scheduler->remove_sleep(thr);
193 if (thr->get_pending()->is_sleep())
194 thr->set_wakeup_state(true);
200 void ModelExecution::assert_bug(const char *msg)
202 priv->bugs.push_back(new bug_message(msg));
206 /** @return True, if any bugs have been reported for this execution */
207 bool ModelExecution::have_bug_reports() const
209 return priv->bugs.size() != 0;
212 SnapVector<bug_message *> * ModelExecution::get_bugs() const
218 * Check whether the current trace has triggered an assertion which should halt
221 * @return True, if the execution should be aborted; false otherwise
223 bool ModelExecution::has_asserted() const
225 return priv->asserted;
229 * Trigger a trace assertion which should cause this execution to be halted.
230 * This can be due to a detected bug or due to an infeasibility that should
233 void ModelExecution::set_assert()
235 priv->asserted = true;
239 * Check if we are in a deadlock. Should only be called at the end of an
240 * execution, although it should not give false positives in the middle of an
241 * execution (there should be some ENABLED thread).
243 * @return True if program is in a deadlock; false otherwise
245 bool ModelExecution::is_deadlocked() const
247 bool blocking_threads = false;
248 for (unsigned int i = 0;i < get_num_threads();i++) {
249 thread_id_t tid = int_to_id(i);
252 Thread *t = get_thread(tid);
253 if (!t->is_model_thread() && t->get_pending())
254 blocking_threads = true;
256 return blocking_threads;
260 * Check if this is a complete execution. That is, have all thread completed
261 * execution (rather than exiting because sleep sets have forced a redundant
264 * @return True if the execution is complete.
266 bool ModelExecution::is_complete_execution() const
268 for (unsigned int i = 0;i < get_num_threads();i++)
269 if (is_enabled(int_to_id(i)))
274 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
275 uint64_t value = *((const uint64_t *) location);
276 modelclock_t storeclock;
277 thread_id_t storethread;
278 getStoreThreadAndClock(location, &storethread, &storeclock);
279 setAtomicStoreFlag(location);
280 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
281 act->set_seq_number(storeclock);
282 add_normal_write_to_lists(act);
283 add_write_to_lists(act);
284 w_modification_order(act);
286 model->get_history()->process_action(act, act->get_tid());
292 * Processes a read model action.
293 * @param curr is the read model action to process.
294 * @param rf_set is the set of model actions we can possibly read from
295 * @return True if the read can be pruned from the thread map list.
297 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
299 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
300 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
301 if (hasnonatomicstore) {
302 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
303 rf_set->push_back(nonatomicstore);
306 // Remove writes that violate read modification order
309 while (i < rf_set->size()) {
310 ModelAction * rf = (*rf_set)[i];
311 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
312 (*rf_set)[i] = rf_set->back();
319 int index = fuzzer->selectWrite(curr, rf_set);
321 ModelAction *rf = (*rf_set)[index];
324 bool canprune = false;
325 if (r_modification_order(curr, rf, priorset, &canprune)) {
326 for(unsigned int i=0;i<priorset->size();i++) {
327 mo_graph->addEdge((*priorset)[i], rf);
330 get_thread(curr)->set_return_value(curr->get_return_value());
332 return canprune && (curr->get_type() == ATOMIC_READ);
335 (*rf_set)[index] = rf_set->back();
341 * Processes a lock, trylock, or unlock model action. @param curr is
342 * the read model action to process.
344 * The try lock operation checks whether the lock is taken. If not,
345 * it falls to the normal lock operation case. If so, it returns
348 * The lock operation has already been checked that it is enabled, so
349 * it just grabs the lock and synchronizes with the previous unlock.
351 * The unlock operation has to re-enable all of the threads that are
352 * waiting on the lock.
354 * @return True if synchronization was updated; false otherwise
356 bool ModelExecution::process_mutex(ModelAction *curr)
358 cdsc::mutex *mutex = curr->get_mutex();
359 struct cdsc::mutex_state *state = NULL;
362 state = mutex->get_state();
364 switch (curr->get_type()) {
365 case ATOMIC_TRYLOCK: {
366 bool success = !state->locked;
367 curr->set_try_lock(success);
369 get_thread(curr)->set_return_value(0);
372 get_thread(curr)->set_return_value(1);
374 //otherwise fall into the lock case
376 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
377 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
378 // assert_bug("Lock access before initialization");
379 state->locked = get_thread(curr);
380 ModelAction *unlock = get_last_unlock(curr);
381 //synchronize with the previous unlock statement
382 if (unlock != NULL) {
383 synchronize(unlock, curr);
389 //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
390 if (fuzzer->shouldWait(curr)) {
391 /* wake up the other threads */
392 for (unsigned int i = 0;i < get_num_threads();i++) {
393 Thread *t = get_thread(int_to_id(i));
394 Thread *curr_thrd = get_thread(curr);
395 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
399 /* unlock the lock - after checking who was waiting on it */
400 state->locked = NULL;
402 /* disable this thread */
403 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
404 scheduler->sleep(get_thread(curr));
409 case ATOMIC_TIMEDWAIT:
410 case ATOMIC_UNLOCK: {
411 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
412 //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
413 //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
414 //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
415 //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
416 //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
417 //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
418 //MUST EVENMTUALLY RELEASE...
420 /* wake up the other threads */
421 for (unsigned int i = 0;i < get_num_threads();i++) {
422 Thread *t = get_thread(int_to_id(i));
423 Thread *curr_thrd = get_thread(curr);
424 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
428 /* unlock the lock - after checking who was waiting on it */
429 state->locked = NULL;
432 case ATOMIC_NOTIFY_ALL: {
433 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
434 //activate all the waiting threads
435 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
436 scheduler->wake(get_thread(rit->getVal()));
441 case ATOMIC_NOTIFY_ONE: {
442 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
443 if (waiters->size() != 0) {
444 Thread * thread = fuzzer->selectNotify(waiters);
445 scheduler->wake(thread);
457 * Process a write ModelAction
458 * @param curr The ModelAction to process
459 * @return True if the mo_graph was updated or promises were resolved
461 void ModelExecution::process_write(ModelAction *curr)
463 w_modification_order(curr);
464 get_thread(curr)->set_return_value(VALUE_NONE);
468 * Process a fence ModelAction
469 * @param curr The ModelAction to process
470 * @return True if synchronization was updated
472 bool ModelExecution::process_fence(ModelAction *curr)
475 * fence-relaxed: no-op
476 * fence-release: only log the occurence (not in this function), for
477 * use in later synchronization
478 * fence-acquire (this function): search for hypothetical release
480 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
482 bool updated = false;
483 if (curr->is_acquire()) {
484 action_list_t *list = &action_trace;
485 sllnode<ModelAction *> * rit;
486 /* Find X : is_read(X) && X --sb-> curr */
487 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
488 ModelAction *act = rit->getVal();
491 if (act->get_tid() != curr->get_tid())
493 /* Stop at the beginning of the thread */
494 if (act->is_thread_start())
496 /* Stop once we reach a prior fence-acquire */
497 if (act->is_fence() && act->is_acquire())
501 /* read-acquire will find its own release sequences */
502 if (act->is_acquire())
505 /* Establish hypothetical release sequences */
506 ClockVector *cv = get_hb_from_write(act->get_reads_from());
507 if (cv != NULL && curr->get_cv()->merge(cv))
515 * @brief Process the current action for thread-related activity
517 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
518 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
519 * synchronization, etc. This function is a no-op for non-THREAD actions
520 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
522 * @param curr The current action
523 * @return True if synchronization was updated or a thread completed
525 void ModelExecution::process_thread_action(ModelAction *curr)
527 switch (curr->get_type()) {
528 case THREAD_CREATE: {
529 thrd_t *thrd = (thrd_t *)curr->get_location();
530 struct thread_params *params = (struct thread_params *)curr->get_value();
531 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
532 curr->set_thread_operand(th);
534 th->set_creation(curr);
537 case PTHREAD_CREATE: {
538 (*(uint32_t *)curr->get_location()) = pthread_counter++;
540 struct pthread_params *params = (struct pthread_params *)curr->get_value();
541 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
542 curr->set_thread_operand(th);
544 th->set_creation(curr);
546 if ( pthread_map.size() < pthread_counter )
547 pthread_map.resize( pthread_counter );
548 pthread_map[ pthread_counter-1 ] = th;
553 Thread *blocking = curr->get_thread_operand();
554 ModelAction *act = get_last_action(blocking->get_id());
555 synchronize(act, curr);
559 Thread *blocking = curr->get_thread_operand();
560 ModelAction *act = get_last_action(blocking->get_id());
561 synchronize(act, curr);
562 break; // WL: to be add (modified)
565 case THREADONLY_FINISH:
566 case THREAD_FINISH: {
567 Thread *th = get_thread(curr);
568 if (curr->get_type() == THREAD_FINISH &&
569 th == model->getInitThread()) {
575 /* Wake up any joining threads */
576 for (unsigned int i = 0;i < get_num_threads();i++) {
577 Thread *waiting = get_thread(int_to_id(i));
578 if (waiting->waiting_on() == th &&
579 waiting->get_pending()->is_thread_join())
580 scheduler->wake(waiting);
589 Thread *th = get_thread(curr);
590 th->set_pending(curr);
591 scheduler->add_sleep(th);
600 * Initialize the current action by performing one or more of the following
601 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
602 * manipulating backtracking sets, allocating and
603 * initializing clock vectors, and computing the promises to fulfill.
605 * @param curr The current action, as passed from the user context; may be
606 * freed/invalidated after the execution of this function, with a different
607 * action "returned" its place (pass-by-reference)
608 * @return True if curr is a newly-explored action; false otherwise
610 bool ModelExecution::initialize_curr_action(ModelAction **curr)
612 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
613 ModelAction *newcurr = process_rmw(*curr);
619 ModelAction *newcurr = *curr;
621 newcurr->set_seq_number(get_next_seq_num());
622 /* Always compute new clock vector */
623 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
625 /* Assign most recent release fence */
626 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
628 return true; /* This was a new ModelAction */
633 * @brief Establish reads-from relation between two actions
635 * Perform basic operations involved with establishing a concrete rf relation,
636 * including setting the ModelAction data and checking for release sequences.
638 * @param act The action that is reading (must be a read)
639 * @param rf The action from which we are reading (must be a write)
641 * @return True if this read established synchronization
644 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
647 ASSERT(rf->is_write());
649 act->set_read_from(rf);
650 if (act->is_acquire()) {
651 ClockVector *cv = get_hb_from_write(rf);
654 act->get_cv()->merge(cv);
659 * @brief Synchronizes two actions
661 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
662 * This function performs the synchronization as well as providing other hooks
663 * for other checks along with synchronization.
665 * @param first The left-hand side of the synchronizes-with relation
666 * @param second The right-hand side of the synchronizes-with relation
667 * @return True if the synchronization was successful (i.e., was consistent
668 * with the execution order); false otherwise
670 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
672 if (*second < *first) {
673 ASSERT(0); //This should not happend
676 return second->synchronize_with(first);
680 * @brief Check whether a model action is enabled.
682 * Checks whether an operation would be successful (i.e., is a lock already
683 * locked, or is the joined thread already complete).
685 * For yield-blocking, yields are never enabled.
687 * @param curr is the ModelAction to check whether it is enabled.
688 * @return a bool that indicates whether the action is enabled.
690 bool ModelExecution::check_action_enabled(ModelAction *curr) {
691 if (curr->is_lock()) {
692 cdsc::mutex *lock = curr->get_mutex();
693 struct cdsc::mutex_state *state = lock->get_state();
696 } else if (curr->is_thread_join()) {
697 Thread *blocking = curr->get_thread_operand();
698 if (!blocking->is_complete()) {
701 } else if (curr->is_sleep()) {
702 if (!fuzzer->shouldSleep(curr))
710 * This is the heart of the model checker routine. It performs model-checking
711 * actions corresponding to a given "current action." Among other processes, it
712 * calculates reads-from relationships, updates synchronization clock vectors,
713 * forms a memory_order constraints graph, and handles replay/backtrack
714 * execution when running permutations of previously-observed executions.
716 * @param curr The current action to process
717 * @return The ModelAction that is actually executed; may be different than
720 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
723 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
724 bool newly_explored = initialize_curr_action(&curr);
728 wake_up_sleeping_actions(curr);
730 SnapVector<ModelAction *> * rf_set = NULL;
731 /* Build may_read_from set for newly-created actions */
732 if (newly_explored && curr->is_read())
733 rf_set = build_may_read_from(curr);
735 bool canprune = false;
737 if (curr->is_read() && !second_part_of_rmw) {
738 canprune = process_read(curr, rf_set);
741 ASSERT(rf_set == NULL);
743 /* Add the action to lists */
744 if (!second_part_of_rmw)
745 add_action_to_lists(curr, canprune);
747 if (curr->is_write())
748 add_write_to_lists(curr);
750 process_thread_action(curr);
752 if (curr->is_write())
755 if (curr->is_fence())
758 if (curr->is_mutex_op())
764 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
765 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
766 ModelAction *lastread = get_last_action(act->get_tid());
767 lastread->process_rmw(act);
769 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
775 * @brief Updates the mo_graph with the constraints imposed from the current
778 * Basic idea is the following: Go through each other thread and find
779 * the last action that happened before our read. Two cases:
781 * -# The action is a write: that write must either occur before
782 * the write we read from or be the write we read from.
783 * -# The action is a read: the write that that action read from
784 * must occur before the write we read from or be the same write.
786 * @param curr The current action. Must be a read.
787 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
788 * @param check_only If true, then only check whether the current action satisfies
789 * read modification order or not, without modifiying priorset and canprune.
791 * @return True if modification order edges were added; false otherwise
794 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
795 SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
797 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
798 ASSERT(curr->is_read());
800 /* Last SC fence in the current thread */
801 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
803 int tid = curr->get_tid();
805 /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
806 if ((int)thrd_lists->size() <= tid) {
807 uint oldsize = thrd_lists->size();
808 thrd_lists->resize(priv->next_thread_id);
809 for(uint i = oldsize;i < priv->next_thread_id;i++)
810 new (&(*thrd_lists)[i]) action_list_t();
813 ModelAction *prev_same_thread = NULL;
814 /* Iterate over all threads */
815 for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
816 /* Last SC fence in thread tid */
817 ModelAction *last_sc_fence_thread_local = NULL;
819 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
821 /* Last SC fence in thread tid, before last SC fence in current thread */
822 ModelAction *last_sc_fence_thread_before = NULL;
823 if (last_sc_fence_local)
824 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
826 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
827 if (prev_same_thread != NULL &&
828 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
829 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
833 /* Iterate over actions in thread, starting from most recent */
834 action_list_t *list = &(*thrd_lists)[tid];
835 sllnode<ModelAction *> * rit;
836 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
837 ModelAction *act = rit->getVal();
842 /* Don't want to add reflexive edges on 'rf' */
843 if (act->equals(rf)) {
844 if (act->happens_before(curr))
850 if (act->is_write()) {
851 /* C++, Section 29.3 statement 5 */
852 if (curr->is_seqcst() && last_sc_fence_thread_local &&
853 *act < *last_sc_fence_thread_local) {
854 if (mo_graph->checkReachable(rf, act))
857 priorset->push_back(act);
860 /* C++, Section 29.3 statement 4 */
861 else if (act->is_seqcst() && last_sc_fence_local &&
862 *act < *last_sc_fence_local) {
863 if (mo_graph->checkReachable(rf, act))
866 priorset->push_back(act);
869 /* C++, Section 29.3 statement 6 */
870 else if (last_sc_fence_thread_before &&
871 *act < *last_sc_fence_thread_before) {
872 if (mo_graph->checkReachable(rf, act))
875 priorset->push_back(act);
881 * Include at most one act per-thread that "happens
884 if (act->happens_before(curr)) {
886 if (last_sc_fence_local == NULL ||
887 (*last_sc_fence_local < *act)) {
888 prev_same_thread = act;
891 if (act->is_write()) {
892 if (mo_graph->checkReachable(rf, act))
895 priorset->push_back(act);
897 ModelAction *prevrf = act->get_reads_from();
898 if (!prevrf->equals(rf)) {
899 if (mo_graph->checkReachable(rf, prevrf))
902 priorset->push_back(prevrf);
904 if (act->get_tid() == curr->get_tid()) {
905 //Can prune curr from obj list
919 * Updates the mo_graph with the constraints imposed from the current write.
921 * Basic idea is the following: Go through each other thread and find
922 * the lastest action that happened before our write. Two cases:
924 * (1) The action is a write => that write must occur before
927 * (2) The action is a read => the write that that action read from
928 * must occur before the current write.
930 * This method also handles two other issues:
932 * (I) Sequential Consistency: Making sure that if the current write is
933 * seq_cst, that it occurs after the previous seq_cst write.
935 * (II) Sending the write back to non-synchronizing reads.
937 * @param curr The current action. Must be a write.
938 * @param send_fv A vector for stashing reads to which we may pass our future
939 * value. If NULL, then don't record any future values.
940 * @return True if modification order edges were added; false otherwise
942 void ModelExecution::w_modification_order(ModelAction *curr)
944 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
946 ASSERT(curr->is_write());
948 SnapList<ModelAction *> edgeset;
950 if (curr->is_seqcst()) {
951 /* We have to at least see the last sequentially consistent write,
952 so we are initialized. */
953 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
954 if (last_seq_cst != NULL) {
955 edgeset.push_back(last_seq_cst);
957 //update map for next query
958 obj_last_sc_map.put(curr->get_location(), curr);
961 /* Last SC fence in the current thread */
962 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
964 /* Iterate over all threads */
965 for (i = 0;i < thrd_lists->size();i++) {
966 /* Last SC fence in thread i, before last SC fence in current thread */
967 ModelAction *last_sc_fence_thread_before = NULL;
968 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
969 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
971 /* Iterate over actions in thread, starting from most recent */
972 action_list_t *list = &(*thrd_lists)[i];
973 sllnode<ModelAction*>* rit;
974 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
975 ModelAction *act = rit->getVal();
978 * 1) If RMW and it actually read from something, then we
979 * already have all relevant edges, so just skip to next
982 * 2) If RMW and it didn't read from anything, we should
983 * whatever edge we can get to speed up convergence.
985 * 3) If normal write, we need to look at earlier actions, so
986 * continue processing list.
988 if (curr->is_rmw()) {
989 if (curr->get_reads_from() != NULL)
997 /* C++, Section 29.3 statement 7 */
998 if (last_sc_fence_thread_before && act->is_write() &&
999 *act < *last_sc_fence_thread_before) {
1000 edgeset.push_back(act);
1005 * Include at most one act per-thread that "happens
1008 if (act->happens_before(curr)) {
1010 * Note: if act is RMW, just add edge:
1012 * The following edge should be handled elsewhere:
1013 * readfrom(act) --mo--> act
1015 if (act->is_write())
1016 edgeset.push_back(act);
1017 else if (act->is_read()) {
1018 //if previous read accessed a null, just keep going
1019 edgeset.push_back(act->get_reads_from());
1025 mo_graph->addEdges(&edgeset, curr);
1030 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1031 * some constraints. This method checks one the following constraint (others
1032 * require compiler support):
1034 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1035 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1037 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1039 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1041 /* Iterate over all threads */
1042 for (i = 0;i < thrd_lists->size();i++) {
1043 const ModelAction *write_after_read = NULL;
1045 /* Iterate over actions in thread, starting from most recent */
1046 action_list_t *list = &(*thrd_lists)[i];
1047 sllnode<ModelAction *>* rit;
1048 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1049 ModelAction *act = rit->getVal();
1051 /* Don't disallow due to act == reader */
1052 if (!reader->happens_before(act) || reader == act)
1054 else if (act->is_write())
1055 write_after_read = act;
1056 else if (act->is_read() && act->get_reads_from() != NULL)
1057 write_after_read = act->get_reads_from();
1060 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1067 * Computes the clock vector that happens before propagates from this write.
1069 * @param rf The action that might be part of a release sequence. Must be a
1071 * @return ClockVector of happens before relation.
1074 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1075 SnapVector<ModelAction *> * processset = NULL;
1076 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1077 ASSERT(rf->is_write());
1078 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1080 if (processset == NULL)
1081 processset = new SnapVector<ModelAction *>();
1082 processset->push_back(rf);
1085 int i = (processset == NULL) ? 0 : processset->size();
1087 ClockVector * vec = NULL;
1089 if (rf->get_rfcv() != NULL) {
1090 vec = rf->get_rfcv();
1091 } else if (rf->is_acquire() && rf->is_release()) {
1093 } else if (rf->is_release() && !rf->is_rmw()) {
1095 } else if (rf->is_release()) {
1096 //have rmw that is release and doesn't have a rfcv
1097 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1100 //operation that isn't release
1101 if (rf->get_last_fence_release()) {
1103 vec = rf->get_last_fence_release()->get_cv();
1105 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1111 rf = (*processset)[i];
1115 if (processset != NULL)
1121 * Performs various bookkeeping operations for the current ModelAction. For
1122 * instance, adds action to the per-object, per-thread action vector and to the
1123 * action trace list of all thread actions.
1125 * @param act is the ModelAction to add.
1127 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1129 int tid = id_to_int(act->get_tid());
1130 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1131 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1132 act->setActionRef(list->add_back(act));
1135 // Update action trace, a total order of all actions
1136 act->setTraceRef(action_trace.add_back(act));
1139 // Update obj_thrd_map, a per location, per thread, order of actions
1140 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1141 if ((int)vec->size() <= tid) {
1142 uint oldsize = vec->size();
1143 vec->resize(priv->next_thread_id);
1144 for(uint i = oldsize;i < priv->next_thread_id;i++)
1145 new (&(*vec)[i]) action_list_t();
1147 if (!canprune && (act->is_read() || act->is_write()))
1148 act->setThrdMapRef((*vec)[tid].add_back(act));
1150 // Update thrd_last_action, the last action taken by each thread
1151 if ((int)thrd_last_action.size() <= tid)
1152 thrd_last_action.resize(get_num_threads());
1153 thrd_last_action[tid] = act;
1155 // Update thrd_last_fence_release, the last release fence taken by each thread
1156 if (act->is_fence() && act->is_release()) {
1157 if ((int)thrd_last_fence_release.size() <= tid)
1158 thrd_last_fence_release.resize(get_num_threads());
1159 thrd_last_fence_release[tid] = act;
1162 if (act->is_wait()) {
1163 void *mutex_loc = (void *) act->get_value();
1164 act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->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())
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();
1631 * Takes the next step in the execution, if possible.
1632 * @param curr The current step to take
1633 * @return Returns the next Thread to run, if any; NULL if this execution
1636 Thread * ModelExecution::take_step(ModelAction *curr)
1638 Thread *curr_thrd = get_thread(curr);
1639 ASSERT(curr_thrd->get_state() == THREAD_READY);
1641 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1642 curr = check_current_action(curr);
1645 /* Process this action in ModelHistory for records */
1647 model->get_history()->process_action( curr, curr->get_tid() );
1649 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1650 scheduler->remove_thread(curr_thrd);
1652 return action_select_next_thread(curr);
1655 /** This method removes references to an Action before we delete it. */
1657 void ModelExecution::removeAction(ModelAction *act) {
1659 sllnode<ModelAction *> * listref = act->getTraceRef();
1660 if (listref != NULL) {
1661 action_trace.erase(listref);
1665 sllnode<ModelAction *> * listref = act->getThrdMapRef();
1666 if (listref != NULL) {
1667 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1668 (*vec)[act->get_tid()].erase(listref);
1671 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1672 sllnode<ModelAction *> * listref = act->getActionRef();
1673 if (listref != NULL) {
1674 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1675 list->erase(listref);
1677 } else if (act->is_wait()) {
1678 sllnode<ModelAction *> * listref = act->getActionRef();
1679 if (listref != NULL) {
1680 void *mutex_loc = (void *) act->get_value();
1681 get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
1683 } else if (act->is_free()) {
1684 sllnode<ModelAction *> * listref = act->getActionRef();
1685 if (listref != NULL) {
1686 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1687 (*vec)[act->get_tid()].erase(listref);
1689 //Clear it from last_sc_map
1690 if (obj_last_sc_map.get(act->get_location()) == act) {
1691 obj_last_sc_map.remove(act->get_location());
1694 //Remove from Cyclegraph
1695 mo_graph->freeAction(act);
1699 /** Computes clock vector that all running threads have already synchronized to. */
1701 ClockVector * ModelExecution::computeMinimalCV() {
1702 ClockVector *cvmin = NULL;
1703 //Thread 0 isn't a real thread, so skip it..
1704 for(unsigned int i = 1;i < thread_map.size();i++) {
1705 Thread * t = thread_map[i];
1706 if (t->get_state() == THREAD_COMPLETED)
1708 thread_id_t tid = int_to_id(i);
1709 ClockVector * cv = get_cv(tid);
1711 cvmin = new ClockVector(cv, NULL);
1713 cvmin->minmerge(cv);
1719 /** 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 */
1721 void ModelExecution::fixupLastAct(ModelAction *act) {
1722 ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid()));
1723 newact->set_seq_number(get_next_seq_num());
1724 newact->create_cv(act);
1725 newact->set_last_fence_release(act->get_last_fence_release());
1726 add_action_to_lists(newact, false);
1729 /** Compute which actions to free. */
1731 void ModelExecution::collectActions() {
1732 if (priv->used_sequence_numbers < params->traceminsize)
1735 //Compute minimal clock vector for all live threads
1736 ClockVector *cvmin = computeMinimalCV();
1737 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1738 modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1740 //Next walk action trace... When we hit an action, see if it is
1741 //invisible (e.g., earlier than the first before the minimum
1742 //clock for the thread... if so erase it and all previous
1743 //actions in cyclegraph
1744 sllnode<ModelAction*> * it;
1745 for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1746 ModelAction *act = it->getVal();
1747 modelclock_t actseq = act->get_seq_number();
1749 //See if we are done
1750 if (actseq > maxtofree)
1753 thread_id_t act_tid = act->get_tid();
1754 modelclock_t tid_clock = cvmin->getClock(act_tid);
1756 //Free if it is invisible or we have set a flag to remove visible actions.
1757 if (actseq <= tid_clock || params->removevisible) {
1758 ModelAction * write;
1759 if (act->is_write()) {
1761 } else if (act->is_read()) {
1762 write = act->get_reads_from();
1766 //Mark everything earlier in MO graph to be freed
1767 CycleNode * cn = mo_graph->getNode_noCreate(write);
1769 queue->push_back(cn);
1770 while(!queue->empty()) {
1771 CycleNode * node = queue->back();
1773 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1774 CycleNode * prevnode = node->getInEdge(i);
1775 ModelAction * prevact = prevnode->getAction();
1776 if (prevact->get_type() != READY_FREE) {
1777 prevact->set_free();
1778 queue->push_back(prevnode);
1786 //We may need to remove read actions in the window we don't delete to preserve correctness.
1788 for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1789 ModelAction *act = it2->getVal();
1790 //Do iteration early in case we delete the act
1792 bool islastact = false;
1793 ModelAction *lastact = get_last_action(act->get_tid());
1794 if (act == lastact) {
1795 Thread * th = get_thread(act);
1796 islastact = !th->is_complete();
1799 if (act->is_read()) {
1800 if (act->get_reads_from()->is_free()) {
1801 if (act->is_rmw()) {
1802 //Weaken a RMW from a freed store to a write
1803 act->set_type(ATOMIC_WRITE);
1815 //If we don't delete the action, we should remove references to release fences
1817 const ModelAction *rel_fence =act->get_last_fence_release();
1818 if (rel_fence != NULL) {
1819 modelclock_t relfenceseq = rel_fence->get_seq_number();
1820 thread_id_t relfence_tid = rel_fence->get_tid();
1821 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1822 //Remove references to irrelevant release fences
1823 if (relfenceseq <= tid_clock)
1824 act->set_last_fence_release(NULL);
1827 //Now we are in the window of old actions that we remove if possible
1828 for (;it != NULL;) {
1829 ModelAction *act = it->getVal();
1830 //Do iteration early since we may delete node...
1832 bool islastact = false;
1833 ModelAction *lastact = get_last_action(act->get_tid());
1834 if (act == lastact) {
1835 Thread * th = get_thread(act);
1836 islastact = !th->is_complete();
1839 if (act->is_read()) {
1840 if (act->get_reads_from()->is_free()) {
1841 if (act->is_rmw()) {
1842 act->set_type(ATOMIC_WRITE);
1852 } else if (act->is_free()) {
1859 } else if (act->is_write()) {
1860 //Do nothing with write that hasn't been marked to be freed
1861 } else if (islastact) {
1862 //Keep the last action for non-read/write actions
1863 } else if (act->is_fence()) {
1864 //Note that acquire fences can always be safely
1865 //removed, but could incur extra overheads in
1866 //traversals. Removing them before the cvmin seems
1867 //like a good compromise.
1869 //Release fences before the cvmin don't do anything
1870 //because everyone has already synchronized.
1872 //Sequentially fences before cvmin are redundant
1873 //because happens-before will enforce same
1876 modelclock_t actseq = act->get_seq_number();
1877 thread_id_t act_tid = act->get_tid();
1878 modelclock_t tid_clock = cvmin->getClock(act_tid);
1879 if (actseq <= tid_clock) {
1881 // Remove reference to act from thrd_last_fence_release
1882 int thread_id = id_to_int( act->get_tid() );
1883 if (thrd_last_fence_release[thread_id] == act) {
1884 thrd_last_fence_release[thread_id] = NULL;
1890 //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1891 //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1892 //need to keep most recent unlock/wait for each lock
1893 if(act->is_unlock() || act->is_wait()) {
1894 ModelAction * lastlock = get_last_unlock(act);
1895 if (lastlock != act) {
1900 } else if (act->is_create()) {
1901 if (act->get_thread_operand()->is_complete()) {
1913 //If we don't delete the action, we should remove references to release fences
1914 const ModelAction *rel_fence =act->get_last_fence_release();
1915 if (rel_fence != NULL) {
1916 modelclock_t relfenceseq = rel_fence->get_seq_number();
1917 thread_id_t relfence_tid = rel_fence->get_tid();
1918 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1919 //Remove references to irrelevant release fences
1920 if (relfenceseq <= tid_clock)
1921 act->set_last_fence_release(NULL);
1929 Fuzzer * ModelExecution::getFuzzer() {