12 #include "clockvector.h"
13 #include "cyclegraph.h"
15 #include "threads-model.h"
16 #include "bugmessage.h"
19 #include "newfuzzer.h"
21 #define INITIAL_THREAD_ID 0
24 static unsigned int atomic_load_count = 0;
25 static unsigned int atomic_store_count = 0;
26 static unsigned int atomic_rmw_count = 0;
28 static unsigned int atomic_fence_count = 0;
29 static unsigned int atomic_lock_count = 0;
30 static unsigned int atomic_trylock_count = 0;
31 static unsigned int atomic_unlock_count = 0;
32 static unsigned int atomic_notify_count = 0;
33 static unsigned int atomic_wait_count = 0;
34 static unsigned int atomic_timedwait_count = 0;
38 * Structure for holding small ModelChecker members that should be snapshotted
40 struct model_snapshot_members {
41 model_snapshot_members() :
42 /* First thread created will have id INITIAL_THREAD_ID */
43 next_thread_id(INITIAL_THREAD_ID),
44 used_sequence_numbers(0),
49 ~model_snapshot_members() {
50 for (unsigned int i = 0;i < bugs.size();i++)
55 unsigned int next_thread_id;
56 modelclock_t used_sequence_numbers;
57 SnapVector<bug_message *> bugs;
58 /** @brief Incorrectly-ordered synchronization was made */
64 /** @brief Constructor */
65 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
69 thread_map(2), /* We'll always need at least 2 threads */
74 condvar_waiters_map(),
81 thrd_last_fence_release(),
82 priv(new struct model_snapshot_members ()),
83 mo_graph(new CycleGraph()),
85 fuzzer(new NewFuzzer()),
91 /* Initialize a model-checker thread, for special ModelActions */
92 model_thread = new Thread(get_next_id());
93 add_thread(model_thread);
94 fuzzer->register_engine(m, this);
95 scheduler->register_engine(this);
97 pthread_key_create(&pthreadkey, tlsdestructor);
101 /** @brief Destructor */
102 ModelExecution::~ModelExecution()
104 for (unsigned int i = 0;i < get_num_threads();i++)
105 delete get_thread(int_to_id(i));
111 int ModelExecution::get_execution_number() const
113 return model->get_execution_number();
116 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
118 SnapVector<action_list_t> *tmp = hash->get(ptr);
120 tmp = new SnapVector<action_list_t>();
126 static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)
128 simple_action_list_t *tmp = hash->get(ptr);
130 tmp = new simple_action_list_t();
136 static SnapVector<simple_action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<simple_action_list_t> *, uintptr_t, 2> * hash, void * ptr)
138 SnapVector<simple_action_list_t> *tmp = hash->get(ptr);
140 tmp = new SnapVector<simple_action_list_t>();
147 * When vectors of action lists are reallocated due to resize, the root address of
148 * action lists may change. Hence we need to fix the parent pointer of the children
151 static void fixup_action_list(SnapVector<action_list_t> * vec)
153 for (uint i = 0;i < vec->size();i++) {
154 action_list_t * list = &(*vec)[i];
161 static inline void record_atomic_stats(ModelAction * act)
163 switch (act->get_type()) {
165 atomic_store_count++;
174 atomic_fence_count++;
180 atomic_trylock_count++;
183 atomic_unlock_count++;
185 case ATOMIC_NOTIFY_ONE:
186 case ATOMIC_NOTIFY_ALL:
187 atomic_notify_count++;
192 case ATOMIC_TIMEDWAIT:
193 atomic_timedwait_count++;
199 void print_atomic_accesses()
201 model_print("atomic store count: %u\n", atomic_store_count);
202 model_print("atomic load count: %u\n", atomic_load_count);
203 model_print("atomic rmw count: %u\n", atomic_rmw_count);
205 model_print("atomic fence count: %u\n", atomic_fence_count);
206 model_print("atomic lock count: %u\n", atomic_lock_count);
207 model_print("atomic trylock count: %u\n", atomic_trylock_count);
208 model_print("atomic unlock count: %u\n", atomic_unlock_count);
209 model_print("atomic notify count: %u\n", atomic_notify_count);
210 model_print("atomic wait count: %u\n", atomic_wait_count);
211 model_print("atomic timedwait count: %u\n", atomic_timedwait_count);
214 /** @return a thread ID for a new Thread */
215 thread_id_t ModelExecution::get_next_id()
217 return priv->next_thread_id++;
220 /** @return the number of user threads created during this execution */
221 unsigned int ModelExecution::get_num_threads() const
223 return priv->next_thread_id;
226 /** @return a sequence number for a new ModelAction */
227 modelclock_t ModelExecution::get_next_seq_num()
229 return ++priv->used_sequence_numbers;
232 /** @return a sequence number for a new ModelAction */
233 modelclock_t ModelExecution::get_curr_seq_num()
235 return priv->used_sequence_numbers;
238 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
239 void ModelExecution::restore_last_seq_num()
241 priv->used_sequence_numbers--;
245 * @brief Should the current action wake up a given thread?
247 * @param curr The current action
248 * @param thread The thread that we might wake up
249 * @return True, if we should wake up the sleeping thread; false otherwise
251 bool ModelExecution::should_wake_up(const ModelAction * asleep) const
253 /* The sleep is literally sleeping */
254 switch (asleep->get_type()) {
256 if (fuzzer->shouldWake(asleep))
260 case ATOMIC_TIMEDWAIT:
261 if (fuzzer->waitShouldWakeUp(asleep))
271 void ModelExecution::wake_up_sleeping_actions()
273 for (unsigned int i = 0;i < get_num_threads();i++) {
274 thread_id_t tid = int_to_id(i);
275 if (scheduler->is_sleep_set(tid)) {
276 Thread *thr = get_thread(tid);
277 ModelAction * pending = thr->get_pending();
278 if (should_wake_up(pending)) {
279 /* Remove this thread from sleep set */
280 scheduler->remove_sleep(thr);
282 if (pending->is_sleep()) {
283 thr->set_wakeup_state(true);
284 } else if (pending->is_wait()) {
285 thr->set_wakeup_state(true);
286 /* Remove this thread from list of waiters */
287 simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, pending->get_location());
288 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
289 if (rit->getVal()->get_tid() == tid) {
295 /* Set ETIMEDOUT error */
296 if (pending->is_timedwait())
297 thr->set_return_value(ETIMEDOUT);
304 void ModelExecution::assert_bug(const char *msg)
306 priv->bugs.push_back(new bug_message(msg));
310 /** @return True, if any bugs have been reported for this execution */
311 bool ModelExecution::have_bug_reports() const
313 return priv->bugs.size() != 0;
316 SnapVector<bug_message *> * ModelExecution::get_bugs() const
322 * Check whether the current trace has triggered an assertion which should halt
325 * @return True, if the execution should be aborted; false otherwise
327 bool ModelExecution::has_asserted() const
329 return priv->asserted;
333 * Trigger a trace assertion which should cause this execution to be halted.
334 * This can be due to a detected bug or due to an infeasibility that should
337 void ModelExecution::set_assert()
339 priv->asserted = true;
343 * Check if we are in a deadlock. Should only be called at the end of an
344 * execution, although it should not give false positives in the middle of an
345 * execution (there should be some ENABLED thread).
347 * @return True if program is in a deadlock; false otherwise
349 bool ModelExecution::is_deadlocked() const
351 bool blocking_threads = false;
352 for (unsigned int i = 0;i < get_num_threads();i++) {
353 thread_id_t tid = int_to_id(i);
356 Thread *t = get_thread(tid);
357 if (!t->is_model_thread() && t->get_pending())
358 blocking_threads = true;
360 return blocking_threads;
364 * Check if this is a complete execution. That is, have all thread completed
365 * execution (rather than exiting because sleep sets have forced a redundant
368 * @return True if the execution is complete.
370 bool ModelExecution::is_complete_execution() const
372 for (unsigned int i = 0;i < get_num_threads();i++)
373 if (is_enabled(int_to_id(i)))
378 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
379 uint64_t value = *((const uint64_t *) location);
380 modelclock_t storeclock;
381 thread_id_t storethread;
382 getStoreThreadAndClock(location, &storethread, &storeclock);
383 setAtomicStoreFlag(location);
384 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
385 act->set_seq_number(storeclock);
386 add_normal_write_to_lists(act);
387 add_write_to_lists(act);
388 w_modification_order(act);
390 model->get_history()->process_action(act, act->get_tid());
396 * Processes a read model action.
397 * @param curr is the read model action to process.
398 * @param rf_set is the set of model actions we can possibly read from
399 * @return True if the read can be pruned from the thread map list.
401 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
403 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
404 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
405 if (hasnonatomicstore) {
406 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
407 rf_set->push_back(nonatomicstore);
410 // Remove writes that violate read modification order
413 while (i < rf_set->size()) {
414 ModelAction * rf = (*rf_set)[i];
415 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
416 (*rf_set)[i] = rf_set->back();
423 int index = fuzzer->selectWrite(curr, rf_set);
425 ModelAction *rf = (*rf_set)[index];
428 bool canprune = false;
429 if (r_modification_order(curr, rf, priorset, &canprune)) {
430 for(unsigned int i=0;i<priorset->size();i++) {
431 mo_graph->addEdge((*priorset)[i], rf);
434 get_thread(curr)->set_return_value(rf->get_write_value());
436 //Update acquire fence clock vector
437 ClockVector * hbcv = get_hb_from_write(rf);
439 get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
440 return canprune && (curr->get_type() == ATOMIC_READ);
443 (*rf_set)[index] = rf_set->back();
449 * Processes a lock, trylock, or unlock model action. @param curr is
450 * the read model action to process.
452 * The try lock operation checks whether the lock is taken. If not,
453 * it falls to the normal lock operation case. If so, it returns
456 * The lock operation has already been checked that it is enabled, so
457 * it just grabs the lock and synchronizes with the previous unlock.
459 * The unlock operation has to re-enable all of the threads that are
460 * waiting on the lock.
462 * @return True if synchronization was updated; false otherwise
464 bool ModelExecution::process_mutex(ModelAction *curr)
466 cdsc::mutex *mutex = curr->get_mutex();
467 struct cdsc::mutex_state *state = NULL;
470 state = mutex->get_state();
472 switch (curr->get_type()) {
473 case ATOMIC_TRYLOCK: {
474 bool success = !state->locked;
475 curr->set_try_lock(success);
477 get_thread(curr)->set_return_value(0);
480 get_thread(curr)->set_return_value(1);
482 //otherwise fall into the lock case
484 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
485 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
486 // assert_bug("Lock access before initialization");
488 // TODO: lock count for recursive mutexes
489 state->locked = get_thread(curr);
490 ModelAction *unlock = get_last_unlock(curr);
491 //synchronize with the previous unlock statement
492 if (unlock != NULL) {
493 synchronize(unlock, curr);
499 Thread *curr_thrd = get_thread(curr);
500 /* wake up the other threads */
501 for (unsigned int i = 0;i < get_num_threads();i++) {
502 Thread *t = get_thread(int_to_id(i));
503 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
507 /* unlock the lock - after checking who was waiting on it */
508 state->locked = NULL;
510 /* disable this thread */
511 simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
512 waiters->push_back(curr);
513 curr_thrd->set_pending(curr); // Forbid this thread to stash a new action
515 if (fuzzer->waitShouldFail(curr)) // If wait should fail spuriously,
516 scheduler->add_sleep(curr_thrd); // place this thread into THREAD_SLEEP_SET
518 scheduler->sleep(curr_thrd);
522 case ATOMIC_TIMEDWAIT: {
523 Thread *curr_thrd = get_thread(curr);
524 if (!fuzzer->randomizeWaitTime(curr)) {
525 curr_thrd->set_return_value(ETIMEDOUT);
529 /* wake up the other threads */
530 for (unsigned int i = 0;i < get_num_threads();i++) {
531 Thread *t = get_thread(int_to_id(i));
532 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
536 /* unlock the lock - after checking who was waiting on it */
537 state->locked = NULL;
539 /* disable this thread */
540 simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
541 waiters->push_back(curr);
542 curr_thrd->set_pending(curr); // Forbid this thread to stash a new action
543 scheduler->add_sleep(curr_thrd);
546 case ATOMIC_UNLOCK: {
547 // TODO: lock count for recursive mutexes
548 /* wake up the other threads */
549 Thread *curr_thrd = get_thread(curr);
550 for (unsigned int i = 0;i < get_num_threads();i++) {
551 Thread *t = get_thread(int_to_id(i));
552 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
556 /* unlock the lock - after checking who was waiting on it */
557 state->locked = NULL;
560 case ATOMIC_NOTIFY_ALL: {
561 simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
562 //activate all the waiting threads
563 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
564 Thread * thread = get_thread(rit->getVal());
565 if (thread->get_state() != THREAD_COMPLETED)
566 scheduler->wake(thread);
567 thread->set_wakeup_state(true);
572 case ATOMIC_NOTIFY_ONE: {
573 simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
574 if (waiters->size() != 0) {
575 Thread * thread = fuzzer->selectNotify(waiters);
576 if (thread->get_state() != THREAD_COMPLETED)
577 scheduler->wake(thread);
578 thread->set_wakeup_state(true);
590 * Process a write ModelAction
591 * @param curr The ModelAction to process
592 * @return True if the mo_graph was updated or promises were resolved
594 void ModelExecution::process_write(ModelAction *curr)
596 w_modification_order(curr);
597 get_thread(curr)->set_return_value(VALUE_NONE);
601 * Process a fence ModelAction
602 * @param curr The ModelAction to process
603 * @return True if synchronization was updated
605 void ModelExecution::process_fence(ModelAction *curr)
608 * fence-relaxed: no-op
609 * fence-release: only log the occurence (not in this function), for
610 * use in later synchronization
611 * fence-acquire (this function): search for hypothetical release
613 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
615 if (curr->is_acquire()) {
616 curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
621 * @brief Process the current action for thread-related activity
623 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
624 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
625 * synchronization, etc. This function is a no-op for non-THREAD actions
626 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
628 * @param curr The current action
629 * @return True if synchronization was updated or a thread completed
631 void ModelExecution::process_thread_action(ModelAction *curr)
633 switch (curr->get_type()) {
634 case THREAD_CREATE: {
635 thrd_t *thrd = (thrd_t *)curr->get_location();
636 struct thread_params *params = (struct thread_params *)curr->get_value();
637 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
638 curr->set_thread_operand(th);
640 th->set_creation(curr);
643 case PTHREAD_CREATE: {
644 (*(uint32_t *)curr->get_location()) = pthread_counter++;
646 struct pthread_params *params = (struct pthread_params *)curr->get_value();
647 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
648 curr->set_thread_operand(th);
650 th->set_creation(curr);
652 if ( pthread_map.size() < pthread_counter )
653 pthread_map.resize( pthread_counter );
654 pthread_map[ pthread_counter-1 ] = th;
659 Thread *blocking = curr->get_thread_operand();
660 ModelAction *act = get_last_action(blocking->get_id());
661 synchronize(act, curr);
665 Thread *blocking = curr->get_thread_operand();
666 ModelAction *act = get_last_action(blocking->get_id());
667 synchronize(act, curr);
671 case THREADONLY_FINISH:
672 case THREAD_FINISH: {
673 Thread *th = get_thread(curr);
674 if (curr->get_type() == THREAD_FINISH &&
675 th == model->getInitThread()) {
681 /* Wake up any joining threads */
682 for (unsigned int i = 0;i < get_num_threads();i++) {
683 Thread *waiting = get_thread(int_to_id(i));
684 if (waiting->waiting_on() == th &&
685 waiting->get_pending()->is_thread_join())
686 scheduler->wake(waiting);
695 Thread *th = get_thread(curr);
696 th->set_pending(curr);
697 scheduler->add_sleep(th);
706 * Initialize the current action by performing one or more of the following
707 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
708 * manipulating backtracking sets, allocating and
709 * initializing clock vectors, and computing the promises to fulfill.
711 * @param curr The current action, as passed from the user context; may be
712 * freed/invalidated after the execution of this function, with a different
713 * action "returned" its place (pass-by-reference)
714 * @return True if curr is a newly-explored action; false otherwise
716 bool ModelExecution::initialize_curr_action(ModelAction **curr)
718 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
719 ModelAction *newcurr = process_rmw(*curr);
725 ModelAction *newcurr = *curr;
727 newcurr->set_seq_number(get_next_seq_num());
728 /* Always compute new clock vector */
729 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
731 /* Assign most recent release fence */
732 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
734 return true; /* This was a new ModelAction */
739 * @brief Establish reads-from relation between two actions
741 * Perform basic operations involved with establishing a concrete rf relation,
742 * including setting the ModelAction data and checking for release sequences.
744 * @param act The action that is reading (must be a read)
745 * @param rf The action from which we are reading (must be a write)
747 * @return True if this read established synchronization
750 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
753 ASSERT(rf->is_write());
755 act->set_read_from(rf);
756 if (act->is_acquire()) {
757 ClockVector *cv = get_hb_from_write(rf);
760 act->get_cv()->merge(cv);
765 * @brief Synchronizes two actions
767 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
768 * This function performs the synchronization as well as providing other hooks
769 * for other checks along with synchronization.
771 * @param first The left-hand side of the synchronizes-with relation
772 * @param second The right-hand side of the synchronizes-with relation
773 * @return True if the synchronization was successful (i.e., was consistent
774 * with the execution order); false otherwise
776 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
778 if (*second < *first) {
779 ASSERT(0); //This should not happend
782 return second->synchronize_with(first);
786 * @brief Check whether a model action is enabled.
788 * Checks whether an operation would be successful (i.e., is a lock already
789 * locked, or is the joined thread already complete).
791 * For yield-blocking, yields are never enabled.
793 * @param curr is the ModelAction to check whether it is enabled.
794 * @return a bool that indicates whether the action is enabled.
796 bool ModelExecution::check_action_enabled(ModelAction *curr) {
797 switch (curr->get_type()) {
799 cdsc::mutex *lock = curr->get_mutex();
800 struct cdsc::mutex_state *state = lock->get_state();
802 Thread *lock_owner = (Thread *)state->locked;
803 Thread *curr_thread = get_thread(curr);
804 if (lock_owner == curr_thread && state->type == PTHREAD_MUTEX_RECURSIVE) {
814 Thread *blocking = curr->get_thread_operand();
815 if (!blocking->is_complete()) {
821 if (!fuzzer->shouldSleep(curr))
833 * This is the heart of the model checker routine. It performs model-checking
834 * actions corresponding to a given "current action." Among other processes, it
835 * calculates reads-from relationships, updates synchronization clock vectors,
836 * forms a memory_order constraints graph, and handles replay/backtrack
837 * execution when running permutations of previously-observed executions.
839 * @param curr The current action to process
840 * @return The ModelAction that is actually executed; may be different than
843 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
846 bool newly_explored = initialize_curr_action(&curr);
850 wake_up_sleeping_actions();
852 SnapVector<ModelAction *> * rf_set = NULL;
853 bool canprune = false;
854 /* Build may_read_from set for newly-created actions */
855 if (curr->is_read() && newly_explored) {
856 rf_set = build_may_read_from(curr);
857 canprune = process_read(curr, rf_set);
860 ASSERT(rf_set == NULL);
862 /* Add the action to lists if not the second part of a rmw */
863 if (newly_explored) {
865 record_atomic_stats(curr);
867 add_action_to_lists(curr, canprune);
870 if (curr->is_write())
871 add_write_to_lists(curr);
873 process_thread_action(curr);
875 if (curr->is_write())
878 if (curr->is_fence())
881 if (curr->is_mutex_op())
887 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
888 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
889 ModelAction *lastread = get_last_action(act->get_tid());
890 lastread->process_rmw(act);
892 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
898 * @brief Updates the mo_graph with the constraints imposed from the current
901 * Basic idea is the following: Go through each other thread and find
902 * the last action that happened before our read. Two cases:
904 * -# The action is a write: that write must either occur before
905 * the write we read from or be the write we read from.
906 * -# The action is a read: the write that that action read from
907 * must occur before the write we read from or be the same write.
909 * @param curr The current action. Must be a read.
910 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
911 * @param check_only If true, then only check whether the current action satisfies
912 * read modification order or not, without modifiying priorset and canprune.
914 * @return True if modification order edges were added; false otherwise
917 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
918 SnapVector<ModelAction *> * priorset, bool * canprune)
920 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
921 ASSERT(curr->is_read());
923 /* Last SC fence in the current thread */
924 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
926 int tid = curr->get_tid();
928 /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
929 if ((int)thrd_lists->size() <= tid) {
930 uint oldsize = thrd_lists->size();
931 thrd_lists->resize(priv->next_thread_id);
932 for(uint i = oldsize;i < priv->next_thread_id;i++)
933 new (&(*thrd_lists)[i]) action_list_t();
935 fixup_action_list(thrd_lists);
938 ModelAction *prev_same_thread = NULL;
939 /* Iterate over all threads */
940 for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
941 /* Last SC fence in thread tid */
942 ModelAction *last_sc_fence_thread_local = NULL;
944 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
946 /* Last SC fence in thread tid, before last SC fence in current thread */
947 ModelAction *last_sc_fence_thread_before = NULL;
948 if (last_sc_fence_local)
949 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
951 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
952 if (prev_same_thread != NULL &&
953 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
954 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
958 /* Iterate over actions in thread, starting from most recent */
959 action_list_t *list = &(*thrd_lists)[tid];
960 sllnode<ModelAction *> * rit;
961 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
962 ModelAction *act = rit->getVal();
967 /* Don't want to add reflexive edges on 'rf' */
968 if (act->equals(rf)) {
969 if (act->happens_before(curr))
975 if (act->is_write()) {
976 /* C++, Section 29.3 statement 5 */
977 if (curr->is_seqcst() && last_sc_fence_thread_local &&
978 *act < *last_sc_fence_thread_local) {
979 if (mo_graph->checkReachable(rf, act))
981 priorset->push_back(act);
984 /* C++, Section 29.3 statement 4 */
985 else if (act->is_seqcst() && last_sc_fence_local &&
986 *act < *last_sc_fence_local) {
987 if (mo_graph->checkReachable(rf, act))
989 priorset->push_back(act);
992 /* C++, Section 29.3 statement 6 */
993 else if (last_sc_fence_thread_before &&
994 *act < *last_sc_fence_thread_before) {
995 if (mo_graph->checkReachable(rf, act))
997 priorset->push_back(act);
1003 * Include at most one act per-thread that "happens
1006 if (act->happens_before(curr)) {
1008 if (last_sc_fence_local == NULL ||
1009 (*last_sc_fence_local < *act)) {
1010 prev_same_thread = act;
1013 if (act->is_write()) {
1014 if (mo_graph->checkReachable(rf, act))
1016 priorset->push_back(act);
1018 ModelAction *prevrf = act->get_reads_from();
1019 if (!prevrf->equals(rf)) {
1020 if (mo_graph->checkReachable(rf, prevrf))
1022 priorset->push_back(prevrf);
1024 if (act->get_tid() == curr->get_tid()) {
1025 //Can prune curr from obj list
1038 * Updates the mo_graph with the constraints imposed from the current write.
1040 * Basic idea is the following: Go through each other thread and find
1041 * the lastest action that happened before our write. Two cases:
1043 * (1) The action is a write => that write must occur before
1046 * (2) The action is a read => the write that that action read from
1047 * must occur before the current write.
1049 * This method also handles two other issues:
1051 * (I) Sequential Consistency: Making sure that if the current write is
1052 * seq_cst, that it occurs after the previous seq_cst write.
1054 * (II) Sending the write back to non-synchronizing reads.
1056 * @param curr The current action. Must be a write.
1057 * @param send_fv A vector for stashing reads to which we may pass our future
1058 * value. If NULL, then don't record any future values.
1059 * @return True if modification order edges were added; false otherwise
1061 void ModelExecution::w_modification_order(ModelAction *curr)
1063 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1065 ASSERT(curr->is_write());
1067 SnapList<ModelAction *> edgeset;
1069 if (curr->is_seqcst()) {
1070 /* We have to at least see the last sequentially consistent write,
1071 so we are initialized. */
1072 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
1073 if (last_seq_cst != NULL) {
1074 edgeset.push_back(last_seq_cst);
1076 //update map for next query
1077 obj_last_sc_map.put(curr->get_location(), curr);
1080 /* Last SC fence in the current thread */
1081 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1083 /* Iterate over all threads */
1084 for (i = 0;i < thrd_lists->size();i++) {
1085 /* Last SC fence in thread i, before last SC fence in current thread */
1086 ModelAction *last_sc_fence_thread_before = NULL;
1087 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
1088 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1090 /* Iterate over actions in thread, starting from most recent */
1091 action_list_t *list = &(*thrd_lists)[i];
1092 sllnode<ModelAction*>* rit;
1093 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1094 ModelAction *act = rit->getVal();
1097 * 1) If RMW and it actually read from something, then we
1098 * already have all relevant edges, so just skip to next
1101 * 2) If RMW and it didn't read from anything, we should
1102 * whatever edge we can get to speed up convergence.
1104 * 3) If normal write, we need to look at earlier actions, so
1105 * continue processing list.
1107 if (curr->is_rmw()) {
1108 if (curr->get_reads_from() != NULL)
1116 /* C++, Section 29.3 statement 7 */
1117 if (last_sc_fence_thread_before && act->is_write() &&
1118 *act < *last_sc_fence_thread_before) {
1119 edgeset.push_back(act);
1124 * Include at most one act per-thread that "happens
1127 if (act->happens_before(curr)) {
1129 * Note: if act is RMW, just add edge:
1131 * The following edge should be handled elsewhere:
1132 * readfrom(act) --mo--> act
1134 if (act->is_write())
1135 edgeset.push_back(act);
1136 else if (act->is_read()) {
1137 //if previous read accessed a null, just keep going
1138 edgeset.push_back(act->get_reads_from());
1144 mo_graph->addEdges(&edgeset, curr);
1149 * Computes the clock vector that happens before propagates from this write.
1151 * @param rf The action that might be part of a release sequence. Must be a
1153 * @return ClockVector of happens before relation.
1156 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1157 SnapVector<ModelAction *> * processset = NULL;
1158 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1159 ASSERT(rf->is_write());
1160 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1162 if (processset == NULL)
1163 processset = new SnapVector<ModelAction *>();
1164 processset->push_back(rf);
1167 int i = (processset == NULL) ? 0 : processset->size();
1169 ClockVector * vec = NULL;
1171 if (rf->get_rfcv() != NULL) {
1172 vec = rf->get_rfcv();
1173 } else if (rf->is_acquire() && rf->is_release()) {
1175 } else if (rf->is_release() && !rf->is_rmw()) {
1177 } else if (rf->is_release()) {
1178 //have rmw that is release and doesn't have a rfcv
1179 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1182 //operation that isn't release
1183 if (rf->get_last_fence_release()) {
1185 vec = new ClockVector(rf->get_last_fence_release()->get_cv(), NULL);
1187 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1191 vec = new ClockVector(NULL, NULL);
1194 vec = new ClockVector(vec, NULL);
1201 rf = (*processset)[i];
1205 if (processset != NULL)
1211 * Performs various bookkeeping operations for the current ModelAction. For
1212 * instance, adds action to the per-object, per-thread action vector and to the
1213 * action trace list of all thread actions.
1215 * @param act is the ModelAction to add.
1217 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1219 int tid = id_to_int(act->get_tid());
1220 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1221 simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1222 act->setActionRef(list->add_back(act));
1225 // Update action trace, a total order of all actions
1226 action_trace.addAction(act);
1229 // Update obj_thrd_map, a per location, per thread, order of actions
1230 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1231 if ((int)vec->size() <= tid) {
1232 uint oldsize = vec->size();
1233 vec->resize(priv->next_thread_id);
1234 for(uint i = oldsize;i < priv->next_thread_id;i++)
1235 new (&(*vec)[i]) action_list_t();
1237 fixup_action_list(vec);
1239 if (!canprune && (act->is_read() || act->is_write()))
1240 (*vec)[tid].addAction(act);
1242 // Update thrd_last_action, the last action taken by each thread
1243 if ((int)thrd_last_action.size() <= tid)
1244 thrd_last_action.resize(get_num_threads());
1245 thrd_last_action[tid] = act;
1247 // Update thrd_last_fence_release, the last release fence taken by each thread
1248 if (act->is_fence() && act->is_release()) {
1249 if ((int)thrd_last_fence_release.size() <= tid)
1250 thrd_last_fence_release.resize(get_num_threads());
1251 thrd_last_fence_release[tid] = act;
1254 if (act->is_wait()) {
1255 void *mutex_loc = (void *) act->get_value();
1256 act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
1260 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1261 list->addAction(act);
1264 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1265 act->create_cv(NULL);
1266 list->addAction(act);
1270 * Performs various bookkeeping operations for a normal write. The
1271 * complication is that we are typically inserting a normal write
1272 * lazily, so we need to insert it into the middle of lists.
1274 * @param act is the ModelAction to add.
1277 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1279 int tid = id_to_int(act->get_tid());
1280 insertIntoActionListAndSetCV(&action_trace, act);
1282 // Update obj_thrd_map, a per location, per thread, order of actions
1283 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1284 if (tid >= (int)vec->size()) {
1285 uint oldsize =vec->size();
1286 vec->resize(priv->next_thread_id);
1287 for(uint i=oldsize;i<priv->next_thread_id;i++)
1288 new (&(*vec)[i]) action_list_t();
1290 fixup_action_list(vec);
1292 insertIntoActionList(&(*vec)[tid],act);
1294 ModelAction * lastact = thrd_last_action[tid];
1295 // Update thrd_last_action, the last action taken by each thrad
1296 if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
1297 thrd_last_action[tid] = act;
1301 void ModelExecution::add_write_to_lists(ModelAction *write) {
1302 SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1303 int tid = id_to_int(write->get_tid());
1304 if (tid >= (int)vec->size()) {
1305 uint oldsize =vec->size();
1306 vec->resize(priv->next_thread_id);
1307 for(uint i=oldsize;i<priv->next_thread_id;i++)
1308 new (&(*vec)[i]) simple_action_list_t();
1310 write->setActionRef((*vec)[tid].add_back(write));
1314 * @brief Get the last action performed by a particular Thread
1315 * @param tid The thread ID of the Thread in question
1316 * @return The last action in the thread
1318 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1320 int threadid = id_to_int(tid);
1321 if (threadid < (int)thrd_last_action.size())
1322 return thrd_last_action[id_to_int(tid)];
1328 * @brief Get the last fence release performed by a particular Thread
1329 * @param tid The thread ID of the Thread in question
1330 * @return The last fence release in the thread, if one exists; NULL otherwise
1332 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1334 int threadid = id_to_int(tid);
1335 if (threadid < (int)thrd_last_fence_release.size())
1336 return thrd_last_fence_release[id_to_int(tid)];
1342 * Gets the last memory_order_seq_cst write (in the total global sequence)
1343 * performed on a particular object (i.e., memory location), not including the
1345 * @param curr The current ModelAction; also denotes the object location to
1347 * @return The last seq_cst write
1349 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1351 void *location = curr->get_location();
1352 return obj_last_sc_map.get(location);
1356 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1357 * performed in a particular thread, prior to a particular fence.
1358 * @param tid The ID of the thread to check
1359 * @param before_fence The fence from which to begin the search; if NULL, then
1360 * search for the most recent fence in the thread.
1361 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1363 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1365 /* All fences should have location FENCE_LOCATION */
1366 simple_action_list_t *list = obj_map.get(FENCE_LOCATION);
1371 sllnode<ModelAction*>* rit = list->end();
1374 for (;rit != NULL;rit=rit->getPrev())
1375 if (rit->getVal() == before_fence)
1378 ASSERT(rit->getVal() == before_fence);
1382 for (;rit != NULL;rit=rit->getPrev()) {
1383 ModelAction *act = rit->getVal();
1384 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1391 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1392 * location). This function identifies the mutex according to the current
1393 * action, which is presumed to perform on the same mutex.
1394 * @param curr The current ModelAction; also denotes the object location to
1396 * @return The last unlock operation
1398 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1400 void *location = curr->get_location();
1402 simple_action_list_t *list = obj_map.get(location);
1406 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1407 sllnode<ModelAction*>* rit;
1408 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1409 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1410 return rit->getVal();
1414 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1416 ModelAction *parent = get_last_action(tid);
1418 parent = get_thread(tid)->get_creation();
1423 * Returns the clock vector for a given thread.
1424 * @param tid The thread whose clock vector we want
1425 * @return Desired clock vector
1427 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1429 ModelAction *firstaction=get_parent_action(tid);
1430 return firstaction != NULL ? firstaction->get_cv() : NULL;
1433 bool valequals(uint64_t val1, uint64_t val2, int size) {
1436 return ((uint8_t)val1) == ((uint8_t)val2);
1438 return ((uint16_t)val1) == ((uint16_t)val2);
1440 return ((uint32_t)val1) == ((uint32_t)val2);
1450 * Build up an initial set of all past writes that this 'read' action may read
1451 * from, as well as any previously-observed future values that must still be valid.
1453 * @param curr is the current ModelAction that we are exploring; it must be a
1456 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1458 SnapVector<simple_action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1460 ASSERT(curr->is_read());
1462 ModelAction *last_sc_write = NULL;
1464 if (curr->is_seqcst())
1465 last_sc_write = get_last_seq_cst_write(curr);
1467 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1469 /* Iterate over all threads */
1470 if (thrd_lists != NULL)
1471 for (i = 0;i < thrd_lists->size();i++) {
1472 /* Iterate over actions in thread, starting from most recent */
1473 simple_action_list_t *list = &(*thrd_lists)[i];
1474 sllnode<ModelAction *> * rit;
1475 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1476 ModelAction *act = rit->getVal();
1481 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1482 bool allow_read = true;
1484 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1487 /* Need to check whether we will have two RMW reading from the same value */
1488 if (curr->is_rmwr()) {
1489 /* It is okay if we have a failing CAS */
1490 if (!curr->is_rmwrcas() ||
1491 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1492 //Need to make sure we aren't the second RMW
1493 CycleNode * node = mo_graph->getNode_noCreate(act);
1494 if (node != NULL && node->getRMW() != NULL) {
1495 //we are the second RMW
1502 /* Only add feasible reads */
1503 rf_set->push_back(act);
1506 /* Include at most one act per-thread that "happens before" curr */
1507 if (act->happens_before(curr))
1512 if (DBG_ENABLED()) {
1513 model_print("Reached read action:\n");
1515 model_print("End printing read_from_past\n");
1520 static void print_list(action_list_t *list)
1522 sllnode<ModelAction*> *it;
1524 model_print("------------------------------------------------------------------------------------\n");
1525 model_print("# t Action type MO Location Value Rf CV\n");
1526 model_print("------------------------------------------------------------------------------------\n");
1528 unsigned int hash = 0;
1530 for (it = list->begin();it != NULL;it=it->getNext()) {
1531 const ModelAction *act = it->getVal();
1532 if (act->get_seq_number() > 0)
1534 hash = hash^(hash<<3)^(it->getVal()->hash());
1536 model_print("HASH %u\n", hash);
1537 model_print("------------------------------------------------------------------------------------\n");
1540 #if SUPPORT_MOD_ORDER_DUMP
1541 void ModelExecution::dumpGraph(char *filename)
1544 sprintf(buffer, "%s.dot", filename);
1545 FILE *file = fopen(buffer, "w");
1546 fprintf(file, "digraph %s {\n", filename);
1547 mo_graph->dumpNodes(file);
1548 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1550 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1551 ModelAction *act = it->getVal();
1552 if (act->is_read()) {
1553 mo_graph->dot_print_node(file, act);
1554 mo_graph->dot_print_edge(file,
1555 act->get_reads_from(),
1557 "label=\"rf\", color=red, weight=2");
1559 if (thread_array[act->get_tid()]) {
1560 mo_graph->dot_print_edge(file,
1561 thread_array[id_to_int(act->get_tid())],
1563 "label=\"sb\", color=blue, weight=400");
1566 thread_array[act->get_tid()] = act;
1568 fprintf(file, "}\n");
1569 model_free(thread_array);
1574 /** @brief Prints an execution trace summary. */
1575 void ModelExecution::print_summary()
1577 #if SUPPORT_MOD_ORDER_DUMP
1578 char buffername[100];
1579 sprintf(buffername, "exec%04u", get_execution_number());
1580 mo_graph->dumpGraphToFile(buffername);
1581 sprintf(buffername, "graph%04u", get_execution_number());
1582 dumpGraph(buffername);
1585 model_print("Execution trace %d:", get_execution_number());
1586 if (scheduler->all_threads_sleeping())
1587 model_print(" SLEEP-SET REDUNDANT");
1588 if (have_bug_reports())
1589 model_print(" DETECTED BUG(S)");
1593 print_list(&action_trace);
1598 void ModelExecution::print_tail()
1600 model_print("Execution trace %d:\n", get_execution_number());
1602 sllnode<ModelAction*> *it;
1604 model_print("------------------------------------------------------------------------------------\n");
1605 model_print("# t Action type MO Location Value Rf CV\n");
1606 model_print("------------------------------------------------------------------------------------\n");
1608 unsigned int hash = 0;
1612 SnapList<ModelAction *> list;
1613 for (it = action_trace.end();it != NULL;it = it->getPrev()) {
1614 if (counter > length)
1617 ModelAction * act = it->getVal();
1618 list.push_front(act);
1622 for (it = list.begin();it != NULL;it=it->getNext()) {
1623 const ModelAction *act = it->getVal();
1624 if (act->get_seq_number() > 0)
1626 hash = hash^(hash<<3)^(it->getVal()->hash());
1628 model_print("HASH %u\n", hash);
1629 model_print("------------------------------------------------------------------------------------\n");
1633 * Add a Thread to the system for the first time. Should only be called once
1635 * @param t The Thread to add
1637 void ModelExecution::add_thread(Thread *t)
1639 unsigned int i = id_to_int(t->get_id());
1640 if (i >= thread_map.size())
1641 thread_map.resize(i + 1);
1643 if (!t->is_model_thread())
1644 scheduler->add_thread(t);
1648 * @brief Get a Thread reference by its ID
1649 * @param tid The Thread's ID
1650 * @return A Thread reference
1652 Thread * ModelExecution::get_thread(thread_id_t tid) const
1654 unsigned int i = id_to_int(tid);
1655 if (i < thread_map.size())
1656 return thread_map[i];
1661 * @brief Get a reference to the Thread in which a ModelAction was executed
1662 * @param act The ModelAction
1663 * @return A Thread reference
1665 Thread * ModelExecution::get_thread(const ModelAction *act) const
1667 return get_thread(act->get_tid());
1671 * @brief Get a Thread reference by its pthread ID
1672 * @param index The pthread's ID
1673 * @return A Thread reference
1675 Thread * ModelExecution::get_pthread(pthread_t pid) {
1676 // pid 1 is reserved for the main thread, pthread ids should start from 2
1678 return get_thread(pid);
1685 uint32_t thread_id = x.v;
1687 if (thread_id < pthread_counter + 1)
1688 return pthread_map[thread_id];
1694 * @brief Check if a Thread is currently enabled
1695 * @param t The Thread to check
1696 * @return True if the Thread is currently enabled
1698 bool ModelExecution::is_enabled(Thread *t) const
1700 return scheduler->is_enabled(t);
1704 * @brief Check if a Thread is currently enabled
1705 * @param tid The ID of the Thread to check
1706 * @return True if the Thread is currently enabled
1708 bool ModelExecution::is_enabled(thread_id_t tid) const
1710 return scheduler->is_enabled(tid);
1714 * @brief Select the next thread to execute based on the curren action
1716 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1717 * actions should be followed by the execution of their child thread. In either
1718 * case, the current action should determine the next thread schedule.
1720 * @param curr The current action
1721 * @return The next thread to run, if the current action will determine this
1722 * selection; otherwise NULL
1724 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1726 /* Do not split atomic RMW */
1727 if (curr->is_rmwr())
1728 return get_thread(curr);
1729 /* Follow CREATE with the created thread */
1730 /* which is not needed, because model.cc takes care of this */
1731 if (curr->get_type() == THREAD_CREATE)
1732 return curr->get_thread_operand();
1733 if (curr->get_type() == PTHREAD_CREATE) {
1734 return curr->get_thread_operand();
1740 * Takes the next step in the execution, if possible.
1741 * @param curr The current step to take
1742 * @return Returns the next Thread to run, if any; NULL if this execution
1745 Thread * ModelExecution::take_step(ModelAction *curr)
1747 Thread *curr_thrd = get_thread(curr);
1748 ASSERT(curr_thrd->get_state() == THREAD_READY);
1750 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1751 curr = check_current_action(curr);
1754 /* Process this action in ModelHistory for records */
1756 model->get_history()->process_action( curr, curr->get_tid() );
1758 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1759 scheduler->remove_thread(curr_thrd);
1761 return action_select_next_thread(curr);
1764 /** This method removes references to an Action before we delete it. */
1766 void ModelExecution::removeAction(ModelAction *act) {
1768 action_trace.removeAction(act);
1771 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1772 (*vec)[act->get_tid()].removeAction(act);
1774 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1775 sllnode<ModelAction *> * listref = act->getActionRef();
1776 if (listref != NULL) {
1777 simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1778 list->erase(listref);
1780 } else if (act->is_wait()) {
1781 sllnode<ModelAction *> * listref = act->getActionRef();
1782 if (listref != NULL) {
1783 void *mutex_loc = (void *) act->get_value();
1784 get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
1786 } else if (act->is_free()) {
1787 sllnode<ModelAction *> * listref = act->getActionRef();
1788 if (listref != NULL) {
1789 SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1790 (*vec)[act->get_tid()].erase(listref);
1793 //Clear it from last_sc_map
1794 if (obj_last_sc_map.get(act->get_location()) == act) {
1795 obj_last_sc_map.remove(act->get_location());
1798 //Remove from Cyclegraph
1799 mo_graph->freeAction(act);
1803 /** Computes clock vector that all running threads have already synchronized to. */
1805 ClockVector * ModelExecution::computeMinimalCV() {
1806 ClockVector *cvmin = NULL;
1807 //Thread 0 isn't a real thread, so skip it..
1808 for(unsigned int i = 1;i < thread_map.size();i++) {
1809 Thread * t = thread_map[i];
1810 if (t->is_complete())
1812 thread_id_t tid = int_to_id(i);
1813 ClockVector * cv = get_cv(tid);
1815 cvmin = new ClockVector(cv, NULL);
1817 cvmin->minmerge(cv);
1823 /** 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 */
1825 void ModelExecution::fixupLastAct(ModelAction *act) {
1826 ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid()));
1827 newact->set_seq_number(get_next_seq_num());
1828 newact->create_cv(act);
1829 newact->set_last_fence_release(act->get_last_fence_release());
1830 add_action_to_lists(newact, false);
1833 /** Compute which actions to free. */
1835 void ModelExecution::collectActions() {
1836 if (priv->used_sequence_numbers < params->traceminsize)
1839 //Compute minimal clock vector for all live threads
1840 ClockVector *cvmin = computeMinimalCV();
1841 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1842 modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1844 //Next walk action trace... When we hit an action, see if it is
1845 //invisible (e.g., earlier than the first before the minimum
1846 //clock for the thread... if so erase it and all previous
1847 //actions in cyclegraph
1848 sllnode<ModelAction*> * it;
1849 for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1850 ModelAction *act = it->getVal();
1851 modelclock_t actseq = act->get_seq_number();
1853 //See if we are done
1854 if (actseq > maxtofree)
1857 thread_id_t act_tid = act->get_tid();
1858 modelclock_t tid_clock = cvmin->getClock(act_tid);
1860 //Free if it is invisible or we have set a flag to remove visible actions.
1861 if (actseq <= tid_clock || params->removevisible) {
1862 ModelAction * write;
1863 if (act->is_write()) {
1865 } else if (act->is_read()) {
1866 write = act->get_reads_from();
1870 //Mark everything earlier in MO graph to be freed
1871 CycleNode * cn = mo_graph->getNode_noCreate(write);
1873 queue->push_back(cn);
1874 while(!queue->empty()) {
1875 CycleNode * node = queue->back();
1877 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1878 CycleNode * prevnode = node->getInEdge(i);
1879 ModelAction * prevact = prevnode->getAction();
1880 if (prevact->get_type() != READY_FREE) {
1881 prevact->set_free();
1882 queue->push_back(prevnode);
1890 //We may need to remove read actions in the window we don't delete to preserve correctness.
1892 for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1893 ModelAction *act = it2->getVal();
1894 //Do iteration early in case we delete the act
1896 bool islastact = false;
1897 ModelAction *lastact = get_last_action(act->get_tid());
1898 if (act == lastact) {
1899 Thread * th = get_thread(act);
1900 islastact = !th->is_complete();
1903 if (act->is_read()) {
1904 if (act->get_reads_from()->is_free()) {
1905 if (act->is_rmw()) {
1906 //Weaken a RMW from a freed store to a write
1907 act->set_type(ATOMIC_WRITE);
1919 //If we don't delete the action, we should remove references to release fences
1921 const ModelAction *rel_fence =act->get_last_fence_release();
1922 if (rel_fence != NULL) {
1923 modelclock_t relfenceseq = rel_fence->get_seq_number();
1924 thread_id_t relfence_tid = rel_fence->get_tid();
1925 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1926 //Remove references to irrelevant release fences
1927 if (relfenceseq <= tid_clock)
1928 act->set_last_fence_release(NULL);
1931 //Now we are in the window of old actions that we remove if possible
1932 for (;it != NULL;) {
1933 ModelAction *act = it->getVal();
1934 //Do iteration early since we may delete node...
1936 bool islastact = false;
1937 ModelAction *lastact = get_last_action(act->get_tid());
1938 if (act == lastact) {
1939 Thread * th = get_thread(act);
1940 islastact = !th->is_complete();
1943 if (act->is_read()) {
1944 if (act->get_reads_from()->is_free()) {
1945 if (act->is_rmw()) {
1946 act->set_type(ATOMIC_WRITE);
1956 } else if (act->is_free()) {
1963 } else if (act->is_write()) {
1964 //Do nothing with write that hasn't been marked to be freed
1965 } else if (islastact) {
1966 //Keep the last action for non-read/write actions
1967 } else if (act->is_fence()) {
1968 //Note that acquire fences can always be safely
1969 //removed, but could incur extra overheads in
1970 //traversals. Removing them before the cvmin seems
1971 //like a good compromise.
1973 //Release fences before the cvmin don't do anything
1974 //because everyone has already synchronized.
1976 //Sequentially fences before cvmin are redundant
1977 //because happens-before will enforce same
1980 modelclock_t actseq = act->get_seq_number();
1981 thread_id_t act_tid = act->get_tid();
1982 modelclock_t tid_clock = cvmin->getClock(act_tid);
1983 if (actseq <= tid_clock) {
1985 // Remove reference to act from thrd_last_fence_release
1986 int thread_id = id_to_int( act->get_tid() );
1987 if (thrd_last_fence_release[thread_id] == act) {
1988 thrd_last_fence_release[thread_id] = NULL;
1994 //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1995 //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1996 //need to keep most recent unlock/wait for each lock
1997 if(act->is_unlock() || act->is_wait()) {
1998 ModelAction * lastlock = get_last_unlock(act);
1999 if (lastlock != act) {
2004 } else if (act->is_create()) {
2005 if (act->get_thread_operand()->is_complete()) {
2017 //If we don't delete the action, we should remove references to release fences
2018 const ModelAction *rel_fence =act->get_last_fence_release();
2019 if (rel_fence != NULL) {
2020 modelclock_t relfenceseq = rel_fence->get_seq_number();
2021 thread_id_t relfence_tid = rel_fence->get_tid();
2022 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
2023 //Remove references to irrelevant release fences
2024 if (relfenceseq <= tid_clock)
2025 act->set_last_fence_release(NULL);
2033 Fuzzer * ModelExecution::getFuzzer() {