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