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 static unsigned int atomic_load_count = 0;
24 static unsigned int atomic_store_count = 0;
25 static unsigned int atomic_rmw_count = 0;
27 static unsigned int atomic_fence_count = 0;
28 static unsigned int atomic_lock_count = 0;
29 static unsigned int atomic_trylock_count = 0;
30 static unsigned int atomic_unlock_count = 0;
31 static unsigned int atomic_notify_count = 0;
32 static unsigned int atomic_wait_count = 0;
33 static unsigned int atomic_timedwait_count = 0;
37 * Structure for holding small ModelChecker members that should be snapshotted
39 struct model_snapshot_members {
40 model_snapshot_members() :
41 /* First thread created will have id INITIAL_THREAD_ID */
42 next_thread_id(INITIAL_THREAD_ID),
43 used_sequence_numbers(0),
48 ~model_snapshot_members() {
49 for (unsigned int i = 0;i < bugs.size();i++)
54 unsigned int next_thread_id;
55 modelclock_t used_sequence_numbers;
56 SnapVector<bug_message *> bugs;
57 /** @brief Incorrectly-ordered synchronization was made */
63 /** @brief Constructor */
64 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
68 thread_map(2), /* We'll always need at least 2 threads */
73 condvar_waiters_map(),
80 thrd_last_fence_release(),
81 priv(new struct model_snapshot_members ()),
82 mo_graph(new CycleGraph()),
84 fuzzer(new NewFuzzer()),
90 /* Initialize a model-checker thread, for special ModelActions */
91 model_thread = new Thread(get_next_id());
92 add_thread(model_thread);
93 fuzzer->register_engine(m, this);
94 scheduler->register_engine(this);
96 pthread_key_create(&pthreadkey, tlsdestructor);
100 /** @brief Destructor */
101 ModelExecution::~ModelExecution()
103 for (unsigned int i = 0;i < get_num_threads();i++)
104 delete get_thread(int_to_id(i));
110 int ModelExecution::get_execution_number() const
112 return model->get_execution_number();
115 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
117 SnapVector<action_list_t> *tmp = hash->get(ptr);
119 tmp = new SnapVector<action_list_t>();
125 static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)
127 simple_action_list_t *tmp = hash->get(ptr);
129 tmp = new simple_action_list_t();
135 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)
137 SnapVector<simple_action_list_t> *tmp = hash->get(ptr);
139 tmp = new SnapVector<simple_action_list_t>();
146 * When vectors of action lists are reallocated due to resize, the root address of
147 * action lists may change. Hence we need to fix the parent pointer of the children
150 static void fixup_action_list(SnapVector<action_list_t> * vec)
152 for (uint i = 0;i < vec->size();i++) {
153 action_list_t * list = &(*vec)[i];
160 static inline void record_atomic_stats(ModelAction * act)
162 switch (act->get_type()) {
164 atomic_store_count++;
173 atomic_fence_count++;
179 atomic_trylock_count++;
182 atomic_unlock_count++;
184 case ATOMIC_NOTIFY_ONE:
185 case ATOMIC_NOTIFY_ALL:
186 atomic_notify_count++;
191 case ATOMIC_TIMEDWAIT:
192 atomic_timedwait_count++;
198 void print_atomic_accesses()
200 model_print("atomic store count: %u\n", atomic_store_count);
201 model_print("atomic load count: %u\n", atomic_load_count);
202 model_print("atomic rmw count: %u\n", atomic_rmw_count);
204 model_print("atomic fence count: %u\n", atomic_fence_count);
205 model_print("atomic lock count: %u\n", atomic_lock_count);
206 model_print("atomic trylock count: %u\n", atomic_trylock_count);
207 model_print("atomic unlock count: %u\n", atomic_unlock_count);
208 model_print("atomic notify count: %u\n", atomic_notify_count);
209 model_print("atomic wait count: %u\n", atomic_wait_count);
210 model_print("atomic timedwait count: %u\n", atomic_timedwait_count);
213 /** @return a thread ID for a new Thread */
214 thread_id_t ModelExecution::get_next_id()
216 return priv->next_thread_id++;
219 /** @return the number of user threads created during this execution */
220 unsigned int ModelExecution::get_num_threads() const
222 return priv->next_thread_id;
225 /** @return a sequence number for a new ModelAction */
226 modelclock_t ModelExecution::get_next_seq_num()
228 return ++priv->used_sequence_numbers;
231 /** @return a sequence number for a new ModelAction */
232 modelclock_t ModelExecution::get_curr_seq_num()
234 return priv->used_sequence_numbers;
237 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
238 void ModelExecution::restore_last_seq_num()
240 priv->used_sequence_numbers--;
244 * @brief Should the current action wake up a given thread?
246 * @param curr The current action
247 * @param thread The thread that we might wake up
248 * @return True, if we should wake up the sleeping thread; false otherwise
250 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
252 const ModelAction *asleep = thread->get_pending();
254 /* The sleep is literally sleeping */
255 if (asleep->is_sleep()) {
256 if (fuzzer->shouldWake(asleep))
263 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
265 for (unsigned int i = 0;i < get_num_threads();i++) {
266 thread_id_t tid = int_to_id(i);
267 if (scheduler->is_sleep_set(tid)) {
268 Thread *thr = get_thread(tid);
269 if (should_wake_up(curr, thr)) {
270 /* Remove this thread from sleep set */
271 scheduler->remove_sleep(thr);
272 if (thr->get_pending()->is_sleep())
273 thr->set_wakeup_state(true);
279 void ModelExecution::assert_bug(const char *msg)
281 priv->bugs.push_back(new bug_message(msg));
285 /** @return True, if any bugs have been reported for this execution */
286 bool ModelExecution::have_bug_reports() const
288 return priv->bugs.size() != 0;
291 SnapVector<bug_message *> * ModelExecution::get_bugs() const
297 * Check whether the current trace has triggered an assertion which should halt
300 * @return True, if the execution should be aborted; false otherwise
302 bool ModelExecution::has_asserted() const
304 return priv->asserted;
308 * Trigger a trace assertion which should cause this execution to be halted.
309 * This can be due to a detected bug or due to an infeasibility that should
312 void ModelExecution::set_assert()
314 priv->asserted = true;
318 * Check if we are in a deadlock. Should only be called at the end of an
319 * execution, although it should not give false positives in the middle of an
320 * execution (there should be some ENABLED thread).
322 * @return True if program is in a deadlock; false otherwise
324 bool ModelExecution::is_deadlocked() const
326 bool blocking_threads = false;
327 for (unsigned int i = 0;i < get_num_threads();i++) {
328 thread_id_t tid = int_to_id(i);
331 Thread *t = get_thread(tid);
332 if (!t->is_model_thread() && t->get_pending())
333 blocking_threads = true;
335 return blocking_threads;
339 * Check if this is a complete execution. That is, have all thread completed
340 * execution (rather than exiting because sleep sets have forced a redundant
343 * @return True if the execution is complete.
345 bool ModelExecution::is_complete_execution() const
347 for (unsigned int i = 0;i < get_num_threads();i++)
348 if (is_enabled(int_to_id(i)))
353 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
354 uint64_t value = *((const uint64_t *) location);
355 modelclock_t storeclock;
356 thread_id_t storethread;
357 getStoreThreadAndClock(location, &storethread, &storeclock);
358 setAtomicStoreFlag(location);
359 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
360 act->set_seq_number(storeclock);
361 add_normal_write_to_lists(act);
362 add_write_to_lists(act);
363 w_modification_order(act);
365 model->get_history()->process_action(act, act->get_tid());
371 * Processes a read model action.
372 * @param curr is the read model action to process.
373 * @param rf_set is the set of model actions we can possibly read from
374 * @return True if the read can be pruned from the thread map list.
376 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
378 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
379 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
380 if (hasnonatomicstore) {
381 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
382 rf_set->push_back(nonatomicstore);
385 // Remove writes that violate read modification order
388 while (i < rf_set->size()) {
389 ModelAction * rf = (*rf_set)[i];
390 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
391 (*rf_set)[i] = rf_set->back();
398 int index = fuzzer->selectWrite(curr, rf_set);
400 ModelAction *rf = (*rf_set)[index];
403 bool canprune = false;
404 if (r_modification_order(curr, rf, priorset, &canprune)) {
405 for(unsigned int i=0;i<priorset->size();i++) {
406 mo_graph->addEdge((*priorset)[i], rf);
409 get_thread(curr)->set_return_value(rf->get_write_value());
411 //Update acquire fence clock vector
412 ClockVector * hbcv = get_hb_from_write(rf);
414 get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
415 return canprune && (curr->get_type() == ATOMIC_READ);
418 (*rf_set)[index] = rf_set->back();
424 * Processes a lock, trylock, or unlock model action. @param curr is
425 * the read model action to process.
427 * The try lock operation checks whether the lock is taken. If not,
428 * it falls to the normal lock operation case. If so, it returns
431 * The lock operation has already been checked that it is enabled, so
432 * it just grabs the lock and synchronizes with the previous unlock.
434 * The unlock operation has to re-enable all of the threads that are
435 * waiting on the lock.
437 * @return True if synchronization was updated; false otherwise
439 bool ModelExecution::process_mutex(ModelAction *curr)
441 cdsc::mutex *mutex = curr->get_mutex();
442 struct cdsc::mutex_state *state = NULL;
445 state = mutex->get_state();
447 switch (curr->get_type()) {
448 case ATOMIC_TRYLOCK: {
449 bool success = !state->locked;
450 curr->set_try_lock(success);
452 get_thread(curr)->set_return_value(0);
455 get_thread(curr)->set_return_value(1);
457 //otherwise fall into the lock case
459 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
460 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
461 // assert_bug("Lock access before initialization");
463 // TODO: lock count for recursive mutexes
464 state->locked = get_thread(curr);
465 ModelAction *unlock = get_last_unlock(curr);
466 //synchronize with the previous unlock statement
467 if (unlock != NULL) {
468 synchronize(unlock, curr);
474 //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
475 if (fuzzer->shouldWait(curr)) {
476 Thread *curr_thrd = get_thread(curr);
477 /* wake up the other threads */
478 for (unsigned int i = 0;i < get_num_threads();i++) {
479 Thread *t = get_thread(int_to_id(i));
480 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
484 /* unlock the lock - after checking who was waiting on it */
485 state->locked = NULL;
487 /* remove old wait action and disable this thread */
488 simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
489 for (sllnode<ModelAction *> * it = waiters->begin();it != NULL;it = it->getNext()) {
490 ModelAction * wait = it->getVal();
491 if (wait->get_tid() == curr->get_tid()) {
497 waiters->push_back(curr);
498 scheduler->sleep(curr_thrd);
503 case ATOMIC_TIMEDWAIT:
504 case ATOMIC_UNLOCK: {
505 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
506 //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
507 //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
508 //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
509 //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
510 //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
511 //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
512 //MUST EVENMTUALLY RELEASE...
514 // TODO: lock count for recursive mutexes
515 /* wake up the other threads */
516 Thread *curr_thrd = get_thread(curr);
517 for (unsigned int i = 0;i < get_num_threads();i++) {
518 Thread *t = get_thread(int_to_id(i));
519 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
523 /* unlock the lock - after checking who was waiting on it */
524 state->locked = NULL;
527 case ATOMIC_NOTIFY_ALL: {
528 simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
529 //activate all the waiting threads
530 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
531 scheduler->wake(get_thread(rit->getVal()));
536 case ATOMIC_NOTIFY_ONE: {
537 simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
538 if (waiters->size() != 0) {
539 Thread * thread = fuzzer->selectNotify(waiters);
540 scheduler->wake(thread);
552 * Process a write ModelAction
553 * @param curr The ModelAction to process
554 * @return True if the mo_graph was updated or promises were resolved
556 void ModelExecution::process_write(ModelAction *curr)
558 w_modification_order(curr);
559 get_thread(curr)->set_return_value(VALUE_NONE);
563 * Process a fence ModelAction
564 * @param curr The ModelAction to process
565 * @return True if synchronization was updated
567 void ModelExecution::process_fence(ModelAction *curr)
570 * fence-relaxed: no-op
571 * fence-release: only log the occurence (not in this function), for
572 * use in later synchronization
573 * fence-acquire (this function): search for hypothetical release
575 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
577 if (curr->is_acquire()) {
578 curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
583 * @brief Process the current action for thread-related activity
585 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
586 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
587 * synchronization, etc. This function is a no-op for non-THREAD actions
588 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
590 * @param curr The current action
591 * @return True if synchronization was updated or a thread completed
593 void ModelExecution::process_thread_action(ModelAction *curr)
595 switch (curr->get_type()) {
596 case THREAD_CREATE: {
597 thrd_t *thrd = (thrd_t *)curr->get_location();
598 struct thread_params *params = (struct thread_params *)curr->get_value();
599 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
600 curr->set_thread_operand(th);
602 th->set_creation(curr);
605 case PTHREAD_CREATE: {
606 (*(uint32_t *)curr->get_location()) = pthread_counter++;
608 struct pthread_params *params = (struct pthread_params *)curr->get_value();
609 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
610 curr->set_thread_operand(th);
612 th->set_creation(curr);
614 if ( pthread_map.size() < pthread_counter )
615 pthread_map.resize( pthread_counter );
616 pthread_map[ pthread_counter-1 ] = th;
621 Thread *blocking = curr->get_thread_operand();
622 ModelAction *act = get_last_action(blocking->get_id());
623 synchronize(act, curr);
627 Thread *blocking = curr->get_thread_operand();
628 ModelAction *act = get_last_action(blocking->get_id());
629 synchronize(act, curr);
633 case THREADONLY_FINISH:
634 case THREAD_FINISH: {
635 Thread *th = get_thread(curr);
636 if (curr->get_type() == THREAD_FINISH &&
637 th == model->getInitThread()) {
643 /* Wake up any joining threads */
644 for (unsigned int i = 0;i < get_num_threads();i++) {
645 Thread *waiting = get_thread(int_to_id(i));
646 if (waiting->waiting_on() == th &&
647 waiting->get_pending()->is_thread_join())
648 scheduler->wake(waiting);
657 Thread *th = get_thread(curr);
658 th->set_pending(curr);
659 scheduler->add_sleep(th);
668 * Initialize the current action by performing one or more of the following
669 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
670 * manipulating backtracking sets, allocating and
671 * initializing clock vectors, and computing the promises to fulfill.
673 * @param curr The current action, as passed from the user context; may be
674 * freed/invalidated after the execution of this function, with a different
675 * action "returned" its place (pass-by-reference)
676 * @return True if curr is a newly-explored action; false otherwise
678 bool ModelExecution::initialize_curr_action(ModelAction **curr)
680 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
681 ModelAction *newcurr = process_rmw(*curr);
687 ModelAction *newcurr = *curr;
689 newcurr->set_seq_number(get_next_seq_num());
690 /* Always compute new clock vector */
691 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
693 /* Assign most recent release fence */
694 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
696 return true; /* This was a new ModelAction */
701 * @brief Establish reads-from relation between two actions
703 * Perform basic operations involved with establishing a concrete rf relation,
704 * including setting the ModelAction data and checking for release sequences.
706 * @param act The action that is reading (must be a read)
707 * @param rf The action from which we are reading (must be a write)
709 * @return True if this read established synchronization
712 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
715 ASSERT(rf->is_write());
717 act->set_read_from(rf);
718 if (act->is_acquire()) {
719 ClockVector *cv = get_hb_from_write(rf);
722 act->get_cv()->merge(cv);
727 * @brief Synchronizes two actions
729 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
730 * This function performs the synchronization as well as providing other hooks
731 * for other checks along with synchronization.
733 * @param first The left-hand side of the synchronizes-with relation
734 * @param second The right-hand side of the synchronizes-with relation
735 * @return True if the synchronization was successful (i.e., was consistent
736 * with the execution order); false otherwise
738 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
740 if (*second < *first) {
741 ASSERT(0); //This should not happend
744 return second->synchronize_with(first);
748 * @brief Check whether a model action is enabled.
750 * Checks whether an operation would be successful (i.e., is a lock already
751 * locked, or is the joined thread already complete).
753 * For yield-blocking, yields are never enabled.
755 * @param curr is the ModelAction to check whether it is enabled.
756 * @return a bool that indicates whether the action is enabled.
758 bool ModelExecution::check_action_enabled(ModelAction *curr) {
759 switch (curr->get_type()) {
761 cdsc::mutex *lock = curr->get_mutex();
762 struct cdsc::mutex_state *state = lock->get_state();
764 Thread *lock_owner = (Thread *)state->locked;
765 Thread *curr_thread = get_thread(curr);
766 if (lock_owner == curr_thread && state->type == PTHREAD_MUTEX_RECURSIVE) {
776 Thread *blocking = curr->get_thread_operand();
777 if (!blocking->is_complete()) {
783 if (!fuzzer->shouldSleep(curr))
795 * This is the heart of the model checker routine. It performs model-checking
796 * actions corresponding to a given "current action." Among other processes, it
797 * calculates reads-from relationships, updates synchronization clock vectors,
798 * forms a memory_order constraints graph, and handles replay/backtrack
799 * execution when running permutations of previously-observed executions.
801 * @param curr The current action to process
802 * @return The ModelAction that is actually executed; may be different than
805 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
808 bool newly_explored = initialize_curr_action(&curr);
812 wake_up_sleeping_actions(curr);
814 SnapVector<ModelAction *> * rf_set = NULL;
815 bool canprune = false;
816 /* Build may_read_from set for newly-created actions */
817 if (curr->is_read() && newly_explored) {
818 rf_set = build_may_read_from(curr);
819 canprune = process_read(curr, rf_set);
822 ASSERT(rf_set == NULL);
824 /* Add the action to lists if not the second part of a rmw */
825 if (newly_explored) {
827 record_atomic_stats(curr);
829 add_action_to_lists(curr, canprune);
832 if (curr->is_write())
833 add_write_to_lists(curr);
835 process_thread_action(curr);
837 if (curr->is_write())
840 if (curr->is_fence())
843 if (curr->is_mutex_op())
849 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
850 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
851 ModelAction *lastread = get_last_action(act->get_tid());
852 lastread->process_rmw(act);
854 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
860 * @brief Updates the mo_graph with the constraints imposed from the current
863 * Basic idea is the following: Go through each other thread and find
864 * the last action that happened before our read. Two cases:
866 * -# The action is a write: that write must either occur before
867 * the write we read from or be the write we read from.
868 * -# The action is a read: the write that that action read from
869 * must occur before the write we read from or be the same write.
871 * @param curr The current action. Must be a read.
872 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
873 * @param check_only If true, then only check whether the current action satisfies
874 * read modification order or not, without modifiying priorset and canprune.
876 * @return True if modification order edges were added; false otherwise
879 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
880 SnapVector<ModelAction *> * priorset, bool * canprune)
882 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
883 ASSERT(curr->is_read());
885 /* Last SC fence in the current thread */
886 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
888 int tid = curr->get_tid();
890 /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
891 if ((int)thrd_lists->size() <= tid) {
892 uint oldsize = thrd_lists->size();
893 thrd_lists->resize(priv->next_thread_id);
894 for(uint i = oldsize;i < priv->next_thread_id;i++)
895 new (&(*thrd_lists)[i]) action_list_t();
897 fixup_action_list(thrd_lists);
900 ModelAction *prev_same_thread = NULL;
901 /* Iterate over all threads */
902 for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
903 /* Last SC fence in thread tid */
904 ModelAction *last_sc_fence_thread_local = NULL;
906 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
908 /* Last SC fence in thread tid, before last SC fence in current thread */
909 ModelAction *last_sc_fence_thread_before = NULL;
910 if (last_sc_fence_local)
911 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
913 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
914 if (prev_same_thread != NULL &&
915 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
916 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
920 /* Iterate over actions in thread, starting from most recent */
921 action_list_t *list = &(*thrd_lists)[tid];
922 sllnode<ModelAction *> * rit;
923 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
924 ModelAction *act = rit->getVal();
929 /* Don't want to add reflexive edges on 'rf' */
930 if (act->equals(rf)) {
931 if (act->happens_before(curr))
937 if (act->is_write()) {
938 /* C++, Section 29.3 statement 5 */
939 if (curr->is_seqcst() && last_sc_fence_thread_local &&
940 *act < *last_sc_fence_thread_local) {
941 if (mo_graph->checkReachable(rf, act))
943 priorset->push_back(act);
946 /* C++, Section 29.3 statement 4 */
947 else if (act->is_seqcst() && last_sc_fence_local &&
948 *act < *last_sc_fence_local) {
949 if (mo_graph->checkReachable(rf, act))
951 priorset->push_back(act);
954 /* C++, Section 29.3 statement 6 */
955 else if (last_sc_fence_thread_before &&
956 *act < *last_sc_fence_thread_before) {
957 if (mo_graph->checkReachable(rf, act))
959 priorset->push_back(act);
965 * Include at most one act per-thread that "happens
968 if (act->happens_before(curr)) {
970 if (last_sc_fence_local == NULL ||
971 (*last_sc_fence_local < *act)) {
972 prev_same_thread = act;
975 if (act->is_write()) {
976 if (mo_graph->checkReachable(rf, act))
978 priorset->push_back(act);
980 ModelAction *prevrf = act->get_reads_from();
981 if (!prevrf->equals(rf)) {
982 if (mo_graph->checkReachable(rf, prevrf))
984 priorset->push_back(prevrf);
986 if (act->get_tid() == curr->get_tid()) {
987 //Can prune curr from obj list
1000 * Updates the mo_graph with the constraints imposed from the current write.
1002 * Basic idea is the following: Go through each other thread and find
1003 * the lastest action that happened before our write. Two cases:
1005 * (1) The action is a write => that write must occur before
1008 * (2) The action is a read => the write that that action read from
1009 * must occur before the current write.
1011 * This method also handles two other issues:
1013 * (I) Sequential Consistency: Making sure that if the current write is
1014 * seq_cst, that it occurs after the previous seq_cst write.
1016 * (II) Sending the write back to non-synchronizing reads.
1018 * @param curr The current action. Must be a write.
1019 * @param send_fv A vector for stashing reads to which we may pass our future
1020 * value. If NULL, then don't record any future values.
1021 * @return True if modification order edges were added; false otherwise
1023 void ModelExecution::w_modification_order(ModelAction *curr)
1025 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1027 ASSERT(curr->is_write());
1029 SnapList<ModelAction *> edgeset;
1031 if (curr->is_seqcst()) {
1032 /* We have to at least see the last sequentially consistent write,
1033 so we are initialized. */
1034 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
1035 if (last_seq_cst != NULL) {
1036 edgeset.push_back(last_seq_cst);
1038 //update map for next query
1039 obj_last_sc_map.put(curr->get_location(), curr);
1042 /* Last SC fence in the current thread */
1043 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1045 /* Iterate over all threads */
1046 for (i = 0;i < thrd_lists->size();i++) {
1047 /* Last SC fence in thread i, before last SC fence in current thread */
1048 ModelAction *last_sc_fence_thread_before = NULL;
1049 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
1050 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1052 /* Iterate over actions in thread, starting from most recent */
1053 action_list_t *list = &(*thrd_lists)[i];
1054 sllnode<ModelAction*>* rit;
1055 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1056 ModelAction *act = rit->getVal();
1059 * 1) If RMW and it actually read from something, then we
1060 * already have all relevant edges, so just skip to next
1063 * 2) If RMW and it didn't read from anything, we should
1064 * whatever edge we can get to speed up convergence.
1066 * 3) If normal write, we need to look at earlier actions, so
1067 * continue processing list.
1069 if (curr->is_rmw()) {
1070 if (curr->get_reads_from() != NULL)
1078 /* C++, Section 29.3 statement 7 */
1079 if (last_sc_fence_thread_before && act->is_write() &&
1080 *act < *last_sc_fence_thread_before) {
1081 edgeset.push_back(act);
1086 * Include at most one act per-thread that "happens
1089 if (act->happens_before(curr)) {
1091 * Note: if act is RMW, just add edge:
1093 * The following edge should be handled elsewhere:
1094 * readfrom(act) --mo--> act
1096 if (act->is_write())
1097 edgeset.push_back(act);
1098 else if (act->is_read()) {
1099 //if previous read accessed a null, just keep going
1100 edgeset.push_back(act->get_reads_from());
1106 mo_graph->addEdges(&edgeset, curr);
1111 * Computes the clock vector that happens before propagates from this write.
1113 * @param rf The action that might be part of a release sequence. Must be a
1115 * @return ClockVector of happens before relation.
1118 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1119 SnapVector<ModelAction *> * processset = NULL;
1120 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1121 ASSERT(rf->is_write());
1122 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1124 if (processset == NULL)
1125 processset = new SnapVector<ModelAction *>();
1126 processset->push_back(rf);
1129 int i = (processset == NULL) ? 0 : processset->size();
1131 ClockVector * vec = NULL;
1133 if (rf->get_rfcv() != NULL) {
1134 vec = rf->get_rfcv();
1135 } else if (rf->is_acquire() && rf->is_release()) {
1137 } else if (rf->is_release() && !rf->is_rmw()) {
1139 } else if (rf->is_release()) {
1140 //have rmw that is release and doesn't have a rfcv
1141 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1144 //operation that isn't release
1145 if (rf->get_last_fence_release()) {
1147 vec = new ClockVector(rf->get_last_fence_release()->get_cv(), NULL);
1149 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1153 vec = new ClockVector(NULL, NULL);
1156 vec = new ClockVector(vec, NULL);
1163 rf = (*processset)[i];
1167 if (processset != NULL)
1173 * Performs various bookkeeping operations for the current ModelAction. For
1174 * instance, adds action to the per-object, per-thread action vector and to the
1175 * action trace list of all thread actions.
1177 * @param act is the ModelAction to add.
1179 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1181 int tid = id_to_int(act->get_tid());
1182 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1183 simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1184 act->setActionRef(list->add_back(act));
1187 // Update action trace, a total order of all actions
1188 action_trace.addAction(act);
1191 // Update obj_thrd_map, a per location, per thread, order of actions
1192 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1193 if ((int)vec->size() <= tid) {
1194 uint oldsize = vec->size();
1195 vec->resize(priv->next_thread_id);
1196 for(uint i = oldsize;i < priv->next_thread_id;i++)
1197 new (&(*vec)[i]) action_list_t();
1199 fixup_action_list(vec);
1201 if (!canprune && (act->is_read() || act->is_write()))
1202 (*vec)[tid].addAction(act);
1204 // Update thrd_last_action, the last action taken by each thread
1205 if ((int)thrd_last_action.size() <= tid)
1206 thrd_last_action.resize(get_num_threads());
1207 thrd_last_action[tid] = act;
1209 // Update thrd_last_fence_release, the last release fence taken by each thread
1210 if (act->is_fence() && act->is_release()) {
1211 if ((int)thrd_last_fence_release.size() <= tid)
1212 thrd_last_fence_release.resize(get_num_threads());
1213 thrd_last_fence_release[tid] = act;
1216 if (act->is_wait()) {
1217 void *mutex_loc = (void *) act->get_value();
1218 act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
1222 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1223 list->addAction(act);
1226 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1227 act->create_cv(NULL);
1228 list->addAction(act);
1232 * Performs various bookkeeping operations for a normal write. The
1233 * complication is that we are typically inserting a normal write
1234 * lazily, so we need to insert it into the middle of lists.
1236 * @param act is the ModelAction to add.
1239 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1241 int tid = id_to_int(act->get_tid());
1242 insertIntoActionListAndSetCV(&action_trace, act);
1244 // Update obj_thrd_map, a per location, per thread, order of actions
1245 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1246 if (tid >= (int)vec->size()) {
1247 uint oldsize =vec->size();
1248 vec->resize(priv->next_thread_id);
1249 for(uint i=oldsize;i<priv->next_thread_id;i++)
1250 new (&(*vec)[i]) action_list_t();
1252 fixup_action_list(vec);
1254 insertIntoActionList(&(*vec)[tid],act);
1256 ModelAction * lastact = thrd_last_action[tid];
1257 // Update thrd_last_action, the last action taken by each thrad
1258 if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
1259 thrd_last_action[tid] = act;
1263 void ModelExecution::add_write_to_lists(ModelAction *write) {
1264 SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1265 int tid = id_to_int(write->get_tid());
1266 if (tid >= (int)vec->size()) {
1267 uint oldsize =vec->size();
1268 vec->resize(priv->next_thread_id);
1269 for(uint i=oldsize;i<priv->next_thread_id;i++)
1270 new (&(*vec)[i]) simple_action_list_t();
1272 write->setActionRef((*vec)[tid].add_back(write));
1276 * @brief Get the last action performed by a particular Thread
1277 * @param tid The thread ID of the Thread in question
1278 * @return The last action in the thread
1280 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1282 int threadid = id_to_int(tid);
1283 if (threadid < (int)thrd_last_action.size())
1284 return thrd_last_action[id_to_int(tid)];
1290 * @brief Get the last fence release performed by a particular Thread
1291 * @param tid The thread ID of the Thread in question
1292 * @return The last fence release in the thread, if one exists; NULL otherwise
1294 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1296 int threadid = id_to_int(tid);
1297 if (threadid < (int)thrd_last_fence_release.size())
1298 return thrd_last_fence_release[id_to_int(tid)];
1304 * Gets the last memory_order_seq_cst write (in the total global sequence)
1305 * performed on a particular object (i.e., memory location), not including the
1307 * @param curr The current ModelAction; also denotes the object location to
1309 * @return The last seq_cst write
1311 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1313 void *location = curr->get_location();
1314 return obj_last_sc_map.get(location);
1318 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1319 * performed in a particular thread, prior to a particular fence.
1320 * @param tid The ID of the thread to check
1321 * @param before_fence The fence from which to begin the search; if NULL, then
1322 * search for the most recent fence in the thread.
1323 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1325 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1327 /* All fences should have location FENCE_LOCATION */
1328 simple_action_list_t *list = obj_map.get(FENCE_LOCATION);
1333 sllnode<ModelAction*>* rit = list->end();
1336 for (;rit != NULL;rit=rit->getPrev())
1337 if (rit->getVal() == before_fence)
1340 ASSERT(rit->getVal() == before_fence);
1344 for (;rit != NULL;rit=rit->getPrev()) {
1345 ModelAction *act = rit->getVal();
1346 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1353 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1354 * location). This function identifies the mutex according to the current
1355 * action, which is presumed to perform on the same mutex.
1356 * @param curr The current ModelAction; also denotes the object location to
1358 * @return The last unlock operation
1360 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1362 void *location = curr->get_location();
1364 simple_action_list_t *list = obj_map.get(location);
1368 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1369 sllnode<ModelAction*>* rit;
1370 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1371 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1372 return rit->getVal();
1376 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1378 ModelAction *parent = get_last_action(tid);
1380 parent = get_thread(tid)->get_creation();
1385 * Returns the clock vector for a given thread.
1386 * @param tid The thread whose clock vector we want
1387 * @return Desired clock vector
1389 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1391 ModelAction *firstaction=get_parent_action(tid);
1392 return firstaction != NULL ? firstaction->get_cv() : NULL;
1395 bool valequals(uint64_t val1, uint64_t val2, int size) {
1398 return ((uint8_t)val1) == ((uint8_t)val2);
1400 return ((uint16_t)val1) == ((uint16_t)val2);
1402 return ((uint32_t)val1) == ((uint32_t)val2);
1412 * Build up an initial set of all past writes that this 'read' action may read
1413 * from, as well as any previously-observed future values that must still be valid.
1415 * @param curr is the current ModelAction that we are exploring; it must be a
1418 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1420 SnapVector<simple_action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1422 ASSERT(curr->is_read());
1424 ModelAction *last_sc_write = NULL;
1426 if (curr->is_seqcst())
1427 last_sc_write = get_last_seq_cst_write(curr);
1429 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1431 /* Iterate over all threads */
1432 if (thrd_lists != NULL)
1433 for (i = 0;i < thrd_lists->size();i++) {
1434 /* Iterate over actions in thread, starting from most recent */
1435 simple_action_list_t *list = &(*thrd_lists)[i];
1436 sllnode<ModelAction *> * rit;
1437 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1438 ModelAction *act = rit->getVal();
1443 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1444 bool allow_read = true;
1446 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1449 /* Need to check whether we will have two RMW reading from the same value */
1450 if (curr->is_rmwr()) {
1451 /* It is okay if we have a failing CAS */
1452 if (!curr->is_rmwrcas() ||
1453 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1454 //Need to make sure we aren't the second RMW
1455 CycleNode * node = mo_graph->getNode_noCreate(act);
1456 if (node != NULL && node->getRMW() != NULL) {
1457 //we are the second RMW
1464 /* Only add feasible reads */
1465 rf_set->push_back(act);
1468 /* Include at most one act per-thread that "happens before" curr */
1469 if (act->happens_before(curr))
1474 if (DBG_ENABLED()) {
1475 model_print("Reached read action:\n");
1477 model_print("End printing read_from_past\n");
1482 static void print_list(action_list_t *list)
1484 sllnode<ModelAction*> *it;
1486 model_print("------------------------------------------------------------------------------------\n");
1487 model_print("# t Action type MO Location Value Rf CV\n");
1488 model_print("------------------------------------------------------------------------------------\n");
1490 unsigned int hash = 0;
1492 for (it = list->begin();it != NULL;it=it->getNext()) {
1493 const ModelAction *act = it->getVal();
1494 if (act->get_seq_number() > 0)
1496 hash = hash^(hash<<3)^(it->getVal()->hash());
1498 model_print("HASH %u\n", hash);
1499 model_print("------------------------------------------------------------------------------------\n");
1502 #if SUPPORT_MOD_ORDER_DUMP
1503 void ModelExecution::dumpGraph(char *filename)
1506 sprintf(buffer, "%s.dot", filename);
1507 FILE *file = fopen(buffer, "w");
1508 fprintf(file, "digraph %s {\n", filename);
1509 mo_graph->dumpNodes(file);
1510 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1512 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1513 ModelAction *act = it->getVal();
1514 if (act->is_read()) {
1515 mo_graph->dot_print_node(file, act);
1516 mo_graph->dot_print_edge(file,
1517 act->get_reads_from(),
1519 "label=\"rf\", color=red, weight=2");
1521 if (thread_array[act->get_tid()]) {
1522 mo_graph->dot_print_edge(file,
1523 thread_array[id_to_int(act->get_tid())],
1525 "label=\"sb\", color=blue, weight=400");
1528 thread_array[act->get_tid()] = act;
1530 fprintf(file, "}\n");
1531 model_free(thread_array);
1536 /** @brief Prints an execution trace summary. */
1537 void ModelExecution::print_summary()
1539 #if SUPPORT_MOD_ORDER_DUMP
1540 char buffername[100];
1541 sprintf(buffername, "exec%04u", get_execution_number());
1542 mo_graph->dumpGraphToFile(buffername);
1543 sprintf(buffername, "graph%04u", get_execution_number());
1544 dumpGraph(buffername);
1547 model_print("Execution trace %d:", get_execution_number());
1548 if (scheduler->all_threads_sleeping())
1549 model_print(" SLEEP-SET REDUNDANT");
1550 if (have_bug_reports())
1551 model_print(" DETECTED BUG(S)");
1555 print_list(&action_trace);
1560 void ModelExecution::print_tail()
1562 model_print("Execution trace %d:\n", get_execution_number());
1564 sllnode<ModelAction*> *it;
1566 model_print("------------------------------------------------------------------------------------\n");
1567 model_print("# t Action type MO Location Value Rf CV\n");
1568 model_print("------------------------------------------------------------------------------------\n");
1570 unsigned int hash = 0;
1574 SnapList<ModelAction *> list;
1575 for (it = action_trace.end();it != NULL;it = it->getPrev()) {
1576 if (counter > length)
1579 ModelAction * act = it->getVal();
1580 list.push_front(act);
1584 for (it = list.begin();it != NULL;it=it->getNext()) {
1585 const ModelAction *act = it->getVal();
1586 if (act->get_seq_number() > 0)
1588 hash = hash^(hash<<3)^(it->getVal()->hash());
1590 model_print("HASH %u\n", hash);
1591 model_print("------------------------------------------------------------------------------------\n");
1595 * Add a Thread to the system for the first time. Should only be called once
1597 * @param t The Thread to add
1599 void ModelExecution::add_thread(Thread *t)
1601 unsigned int i = id_to_int(t->get_id());
1602 if (i >= thread_map.size())
1603 thread_map.resize(i + 1);
1605 if (!t->is_model_thread())
1606 scheduler->add_thread(t);
1610 * @brief Get a Thread reference by its ID
1611 * @param tid The Thread's ID
1612 * @return A Thread reference
1614 Thread * ModelExecution::get_thread(thread_id_t tid) const
1616 unsigned int i = id_to_int(tid);
1617 if (i < thread_map.size())
1618 return thread_map[i];
1623 * @brief Get a reference to the Thread in which a ModelAction was executed
1624 * @param act The ModelAction
1625 * @return A Thread reference
1627 Thread * ModelExecution::get_thread(const ModelAction *act) const
1629 return get_thread(act->get_tid());
1633 * @brief Get a Thread reference by its pthread ID
1634 * @param index The pthread's ID
1635 * @return A Thread reference
1637 Thread * ModelExecution::get_pthread(pthread_t pid) {
1638 // pid 1 is reserved for the main thread, pthread ids should start from 2
1640 return get_thread(pid);
1647 uint32_t thread_id = x.v;
1649 if (thread_id < pthread_counter + 1)
1650 return pthread_map[thread_id];
1656 * @brief Check if a Thread is currently enabled
1657 * @param t The Thread to check
1658 * @return True if the Thread is currently enabled
1660 bool ModelExecution::is_enabled(Thread *t) const
1662 return scheduler->is_enabled(t);
1666 * @brief Check if a Thread is currently enabled
1667 * @param tid The ID of the Thread to check
1668 * @return True if the Thread is currently enabled
1670 bool ModelExecution::is_enabled(thread_id_t tid) const
1672 return scheduler->is_enabled(tid);
1676 * @brief Select the next thread to execute based on the curren action
1678 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1679 * actions should be followed by the execution of their child thread. In either
1680 * case, the current action should determine the next thread schedule.
1682 * @param curr The current action
1683 * @return The next thread to run, if the current action will determine this
1684 * selection; otherwise NULL
1686 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1688 /* Do not split atomic RMW */
1689 if (curr->is_rmwr())
1690 return get_thread(curr);
1691 /* Follow CREATE with the created thread */
1692 /* which is not needed, because model.cc takes care of this */
1693 if (curr->get_type() == THREAD_CREATE)
1694 return curr->get_thread_operand();
1695 if (curr->get_type() == PTHREAD_CREATE) {
1696 return curr->get_thread_operand();
1702 * Takes the next step in the execution, if possible.
1703 * @param curr The current step to take
1704 * @return Returns the next Thread to run, if any; NULL if this execution
1707 Thread * ModelExecution::take_step(ModelAction *curr)
1709 Thread *curr_thrd = get_thread(curr);
1710 ASSERT(curr_thrd->get_state() == THREAD_READY);
1712 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1713 curr = check_current_action(curr);
1716 /* Process this action in ModelHistory for records */
1718 model->get_history()->process_action( curr, curr->get_tid() );
1720 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1721 scheduler->remove_thread(curr_thrd);
1723 return action_select_next_thread(curr);
1726 /** This method removes references to an Action before we delete it. */
1728 void ModelExecution::removeAction(ModelAction *act) {
1730 action_trace.removeAction(act);
1733 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1734 (*vec)[act->get_tid()].removeAction(act);
1736 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1737 sllnode<ModelAction *> * listref = act->getActionRef();
1738 if (listref != NULL) {
1739 simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1740 list->erase(listref);
1742 } else if (act->is_wait()) {
1743 sllnode<ModelAction *> * listref = act->getActionRef();
1744 if (listref != NULL) {
1745 void *mutex_loc = (void *) act->get_value();
1746 get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
1748 } else if (act->is_free()) {
1749 sllnode<ModelAction *> * listref = act->getActionRef();
1750 if (listref != NULL) {
1751 SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1752 (*vec)[act->get_tid()].erase(listref);
1755 //Clear it from last_sc_map
1756 if (obj_last_sc_map.get(act->get_location()) == act) {
1757 obj_last_sc_map.remove(act->get_location());
1760 //Remove from Cyclegraph
1761 mo_graph->freeAction(act);
1765 /** Computes clock vector that all running threads have already synchronized to. */
1767 ClockVector * ModelExecution::computeMinimalCV() {
1768 ClockVector *cvmin = NULL;
1769 //Thread 0 isn't a real thread, so skip it..
1770 for(unsigned int i = 1;i < thread_map.size();i++) {
1771 Thread * t = thread_map[i];
1772 if (t->is_complete())
1774 thread_id_t tid = int_to_id(i);
1775 ClockVector * cv = get_cv(tid);
1777 cvmin = new ClockVector(cv, NULL);
1779 cvmin->minmerge(cv);
1785 /** 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 */
1787 void ModelExecution::fixupLastAct(ModelAction *act) {
1788 ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid()));
1789 newact->set_seq_number(get_next_seq_num());
1790 newact->create_cv(act);
1791 newact->set_last_fence_release(act->get_last_fence_release());
1792 add_action_to_lists(newact, false);
1795 /** Compute which actions to free. */
1797 void ModelExecution::collectActions() {
1798 if (priv->used_sequence_numbers < params->traceminsize)
1801 //Compute minimal clock vector for all live threads
1802 ClockVector *cvmin = computeMinimalCV();
1803 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1804 modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1806 //Next walk action trace... When we hit an action, see if it is
1807 //invisible (e.g., earlier than the first before the minimum
1808 //clock for the thread... if so erase it and all previous
1809 //actions in cyclegraph
1810 sllnode<ModelAction*> * it;
1811 for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1812 ModelAction *act = it->getVal();
1813 modelclock_t actseq = act->get_seq_number();
1815 //See if we are done
1816 if (actseq > maxtofree)
1819 thread_id_t act_tid = act->get_tid();
1820 modelclock_t tid_clock = cvmin->getClock(act_tid);
1822 //Free if it is invisible or we have set a flag to remove visible actions.
1823 if (actseq <= tid_clock || params->removevisible) {
1824 ModelAction * write;
1825 if (act->is_write()) {
1827 } else if (act->is_read()) {
1828 write = act->get_reads_from();
1832 //Mark everything earlier in MO graph to be freed
1833 CycleNode * cn = mo_graph->getNode_noCreate(write);
1835 queue->push_back(cn);
1836 while(!queue->empty()) {
1837 CycleNode * node = queue->back();
1839 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1840 CycleNode * prevnode = node->getInEdge(i);
1841 ModelAction * prevact = prevnode->getAction();
1842 if (prevact->get_type() != READY_FREE) {
1843 prevact->set_free();
1844 queue->push_back(prevnode);
1852 //We may need to remove read actions in the window we don't delete to preserve correctness.
1854 for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1855 ModelAction *act = it2->getVal();
1856 //Do iteration early in case we delete the act
1858 bool islastact = false;
1859 ModelAction *lastact = get_last_action(act->get_tid());
1860 if (act == lastact) {
1861 Thread * th = get_thread(act);
1862 islastact = !th->is_complete();
1865 if (act->is_read()) {
1866 if (act->get_reads_from()->is_free()) {
1867 if (act->is_rmw()) {
1868 //Weaken a RMW from a freed store to a write
1869 act->set_type(ATOMIC_WRITE);
1881 //If we don't delete the action, we should remove references to release fences
1883 const ModelAction *rel_fence =act->get_last_fence_release();
1884 if (rel_fence != NULL) {
1885 modelclock_t relfenceseq = rel_fence->get_seq_number();
1886 thread_id_t relfence_tid = rel_fence->get_tid();
1887 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1888 //Remove references to irrelevant release fences
1889 if (relfenceseq <= tid_clock)
1890 act->set_last_fence_release(NULL);
1893 //Now we are in the window of old actions that we remove if possible
1894 for (;it != NULL;) {
1895 ModelAction *act = it->getVal();
1896 //Do iteration early since we may delete node...
1898 bool islastact = false;
1899 ModelAction *lastact = get_last_action(act->get_tid());
1900 if (act == lastact) {
1901 Thread * th = get_thread(act);
1902 islastact = !th->is_complete();
1905 if (act->is_read()) {
1906 if (act->get_reads_from()->is_free()) {
1907 if (act->is_rmw()) {
1908 act->set_type(ATOMIC_WRITE);
1918 } else if (act->is_free()) {
1925 } else if (act->is_write()) {
1926 //Do nothing with write that hasn't been marked to be freed
1927 } else if (islastact) {
1928 //Keep the last action for non-read/write actions
1929 } else if (act->is_fence()) {
1930 //Note that acquire fences can always be safely
1931 //removed, but could incur extra overheads in
1932 //traversals. Removing them before the cvmin seems
1933 //like a good compromise.
1935 //Release fences before the cvmin don't do anything
1936 //because everyone has already synchronized.
1938 //Sequentially fences before cvmin are redundant
1939 //because happens-before will enforce same
1942 modelclock_t actseq = act->get_seq_number();
1943 thread_id_t act_tid = act->get_tid();
1944 modelclock_t tid_clock = cvmin->getClock(act_tid);
1945 if (actseq <= tid_clock) {
1947 // Remove reference to act from thrd_last_fence_release
1948 int thread_id = id_to_int( act->get_tid() );
1949 if (thrd_last_fence_release[thread_id] == act) {
1950 thrd_last_fence_release[thread_id] = NULL;
1956 //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1957 //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1958 //need to keep most recent unlock/wait for each lock
1959 if(act->is_unlock() || act->is_wait()) {
1960 ModelAction * lastlock = get_last_unlock(act);
1961 if (lastlock != act) {
1966 } else if (act->is_create()) {
1967 if (act->get_thread_operand()->is_complete()) {
1979 //If we don't delete the action, we should remove references to release fences
1980 const ModelAction *rel_fence =act->get_last_fence_release();
1981 if (rel_fence != NULL) {
1982 modelclock_t relfenceseq = rel_fence->get_seq_number();
1983 thread_id_t relfence_tid = rel_fence->get_tid();
1984 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1985 //Remove references to irrelevant release fences
1986 if (relfenceseq <= tid_clock)
1987 act->set_last_fence_release(NULL);
1995 Fuzzer * ModelExecution::getFuzzer() {