11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
34 ~model_snapshot_members() {
35 for (unsigned int i = 0;i < bugs.size();i++)
40 unsigned int next_thread_id;
41 modelclock_t used_sequence_numbers;
42 SnapVector<bug_message *> bugs;
43 /** @brief Incorrectly-ordered synchronization was made */
49 /** @brief Constructor */
50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
54 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
66 thrd_last_fence_release(),
67 priv(new struct model_snapshot_members ()),
68 mo_graph(new CycleGraph()),
70 fuzzer(new NewFuzzer()),
76 /* Initialize a model-checker thread, for special ModelActions */
77 model_thread = new Thread(get_next_id());
78 add_thread(model_thread);
79 fuzzer->register_engine(m, this);
80 scheduler->register_engine(this);
82 pthread_key_create(&pthreadkey, tlsdestructor);
86 /** @brief Destructor */
87 ModelExecution::~ModelExecution()
89 for (unsigned int i = 0;i < get_num_threads();i++)
90 delete get_thread(int_to_id(i));
96 int ModelExecution::get_execution_number() const
98 return model->get_execution_number();
101 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
103 action_list_t *tmp = hash->get(ptr);
105 tmp = new action_list_t();
111 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
113 SnapVector<action_list_t> *tmp = hash->get(ptr);
115 tmp = new SnapVector<action_list_t>();
122 * When vectors of action lists are reallocated due to resize, the root address of
123 * action lists may change. Hence we need to fix the parent pointer of the children
126 static void fixup_action_list (SnapVector<action_list_t> * vec)
128 for (uint i = 0; i < vec->size(); i++) {
129 action_list_t * list = &(*vec)[i];
135 /** @return a thread ID for a new Thread */
136 thread_id_t ModelExecution::get_next_id()
138 return priv->next_thread_id++;
141 /** @return the number of user threads created during this execution */
142 unsigned int ModelExecution::get_num_threads() const
144 return priv->next_thread_id;
147 /** @return a sequence number for a new ModelAction */
148 modelclock_t ModelExecution::get_next_seq_num()
150 return ++priv->used_sequence_numbers;
153 /** @return a sequence number for a new ModelAction */
154 modelclock_t ModelExecution::get_curr_seq_num()
156 return priv->used_sequence_numbers;
159 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
160 void ModelExecution::restore_last_seq_num()
162 priv->used_sequence_numbers--;
166 * @brief Should the current action wake up a given thread?
168 * @param curr The current action
169 * @param thread The thread that we might wake up
170 * @return True, if we should wake up the sleeping thread; false otherwise
172 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
174 const ModelAction *asleep = thread->get_pending();
175 /* Don't allow partial RMW to wake anyone up */
178 /* Synchronizing actions may have been backtracked */
179 if (asleep->could_synchronize_with(curr))
181 /* All acquire/release fences and fence-acquire/store-release */
182 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
184 /* Fence-release + store can awake load-acquire on the same location */
185 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
186 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
187 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
190 /* The sleep is literally sleeping */
191 if (asleep->is_sleep()) {
192 if (fuzzer->shouldWake(asleep))
199 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
201 for (unsigned int i = 0;i < get_num_threads();i++) {
202 Thread *thr = get_thread(int_to_id(i));
203 if (scheduler->is_sleep_set(thr)) {
204 if (should_wake_up(curr, thr)) {
205 /* Remove this thread from sleep set */
206 scheduler->remove_sleep(thr);
207 if (thr->get_pending()->is_sleep())
208 thr->set_wakeup_state(true);
214 void ModelExecution::assert_bug(const char *msg)
216 priv->bugs.push_back(new bug_message(msg));
220 /** @return True, if any bugs have been reported for this execution */
221 bool ModelExecution::have_bug_reports() const
223 return priv->bugs.size() != 0;
226 SnapVector<bug_message *> * ModelExecution::get_bugs() const
232 * Check whether the current trace has triggered an assertion which should halt
235 * @return True, if the execution should be aborted; false otherwise
237 bool ModelExecution::has_asserted() const
239 return priv->asserted;
243 * Trigger a trace assertion which should cause this execution to be halted.
244 * This can be due to a detected bug or due to an infeasibility that should
247 void ModelExecution::set_assert()
249 priv->asserted = true;
253 * Check if we are in a deadlock. Should only be called at the end of an
254 * execution, although it should not give false positives in the middle of an
255 * execution (there should be some ENABLED thread).
257 * @return True if program is in a deadlock; false otherwise
259 bool ModelExecution::is_deadlocked() const
261 bool blocking_threads = false;
262 for (unsigned int i = 0;i < get_num_threads();i++) {
263 thread_id_t tid = int_to_id(i);
266 Thread *t = get_thread(tid);
267 if (!t->is_model_thread() && t->get_pending())
268 blocking_threads = true;
270 return blocking_threads;
274 * Check if this is a complete execution. That is, have all thread completed
275 * execution (rather than exiting because sleep sets have forced a redundant
278 * @return True if the execution is complete.
280 bool ModelExecution::is_complete_execution() const
282 for (unsigned int i = 0;i < get_num_threads();i++)
283 if (is_enabled(int_to_id(i)))
288 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
289 uint64_t value = *((const uint64_t *) location);
290 modelclock_t storeclock;
291 thread_id_t storethread;
292 getStoreThreadAndClock(location, &storethread, &storeclock);
293 setAtomicStoreFlag(location);
294 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
295 act->set_seq_number(storeclock);
296 add_normal_write_to_lists(act);
297 add_write_to_lists(act);
298 w_modification_order(act);
300 model->get_history()->process_action(act, act->get_tid());
306 * Processes a read model action.
307 * @param curr is the read model action to process.
308 * @param rf_set is the set of model actions we can possibly read from
309 * @return True if the read can be pruned from the thread map list.
311 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
313 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
314 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
315 if (hasnonatomicstore) {
316 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
317 rf_set->push_back(nonatomicstore);
320 // Remove writes that violate read modification order
323 while (i < rf_set->size()) {
324 ModelAction * rf = (*rf_set)[i];
325 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
326 (*rf_set)[i] = rf_set->back();
333 int index = fuzzer->selectWrite(curr, rf_set);
335 ModelAction *rf = (*rf_set)[index];
338 bool canprune = false;
339 if (r_modification_order(curr, rf, priorset, &canprune)) {
340 for(unsigned int i=0;i<priorset->size();i++) {
341 mo_graph->addEdge((*priorset)[i], rf);
344 get_thread(curr)->set_return_value(curr->get_return_value());
346 //Update acquire fence clock vector
347 ClockVector * hbcv = get_hb_from_write(curr->get_reads_from());
349 get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
350 return canprune && (curr->get_type() == ATOMIC_READ);
353 (*rf_set)[index] = rf_set->back();
359 * Processes a lock, trylock, or unlock model action. @param curr is
360 * the read model action to process.
362 * The try lock operation checks whether the lock is taken. If not,
363 * it falls to the normal lock operation case. If so, it returns
366 * The lock operation has already been checked that it is enabled, so
367 * it just grabs the lock and synchronizes with the previous unlock.
369 * The unlock operation has to re-enable all of the threads that are
370 * waiting on the lock.
372 * @return True if synchronization was updated; false otherwise
374 bool ModelExecution::process_mutex(ModelAction *curr)
376 cdsc::mutex *mutex = curr->get_mutex();
377 struct cdsc::mutex_state *state = NULL;
380 state = mutex->get_state();
382 switch (curr->get_type()) {
383 case ATOMIC_TRYLOCK: {
384 bool success = !state->locked;
385 curr->set_try_lock(success);
387 get_thread(curr)->set_return_value(0);
390 get_thread(curr)->set_return_value(1);
392 //otherwise fall into the lock case
394 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
395 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
396 // assert_bug("Lock access before initialization");
397 state->locked = get_thread(curr);
398 ModelAction *unlock = get_last_unlock(curr);
399 //synchronize with the previous unlock statement
400 if (unlock != NULL) {
401 synchronize(unlock, curr);
407 //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
408 if (fuzzer->shouldWait(curr)) {
409 /* wake up the other threads */
410 for (unsigned int i = 0;i < get_num_threads();i++) {
411 Thread *t = get_thread(int_to_id(i));
412 Thread *curr_thrd = get_thread(curr);
413 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
417 /* unlock the lock - after checking who was waiting on it */
418 state->locked = NULL;
420 /* disable this thread */
421 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr);
422 scheduler->sleep(get_thread(curr));
427 case ATOMIC_TIMEDWAIT:
428 case ATOMIC_UNLOCK: {
429 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
430 //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
431 //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
432 //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
433 //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
434 //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
435 //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
436 //MUST EVENMTUALLY RELEASE...
438 /* wake up the other threads */
439 for (unsigned int i = 0;i < get_num_threads();i++) {
440 Thread *t = get_thread(int_to_id(i));
441 Thread *curr_thrd = get_thread(curr);
442 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
446 /* unlock the lock - after checking who was waiting on it */
447 state->locked = NULL;
450 case ATOMIC_NOTIFY_ALL: {
451 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
452 //activate all the waiting threads
453 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
454 scheduler->wake(get_thread(rit->getVal()));
459 case ATOMIC_NOTIFY_ONE: {
460 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
461 if (waiters->size() != 0) {
462 Thread * thread = fuzzer->selectNotify(waiters);
463 scheduler->wake(thread);
475 * Process a write ModelAction
476 * @param curr The ModelAction to process
477 * @return True if the mo_graph was updated or promises were resolved
479 void ModelExecution::process_write(ModelAction *curr)
481 w_modification_order(curr);
482 get_thread(curr)->set_return_value(VALUE_NONE);
486 * Process a fence ModelAction
487 * @param curr The ModelAction to process
488 * @return True if synchronization was updated
490 void ModelExecution::process_fence(ModelAction *curr)
493 * fence-relaxed: no-op
494 * fence-release: only log the occurence (not in this function), for
495 * use in later synchronization
496 * fence-acquire (this function): search for hypothetical release
498 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
500 if (curr->is_acquire()) {
501 curr->get_cv()->merge(get_thread(curr)->get_acq_fence_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();
803 fixup_action_list(thrd_lists);
806 ModelAction *prev_same_thread = NULL;
807 /* Iterate over all threads */
808 for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
809 /* Last SC fence in thread tid */
810 ModelAction *last_sc_fence_thread_local = NULL;
812 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
814 /* Last SC fence in thread tid, before last SC fence in current thread */
815 ModelAction *last_sc_fence_thread_before = NULL;
816 if (last_sc_fence_local)
817 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
819 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
820 if (prev_same_thread != NULL &&
821 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
822 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
826 /* Iterate over actions in thread, starting from most recent */
827 action_list_t *list = &(*thrd_lists)[tid];
828 sllnode<ModelAction *> * rit;
829 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
830 ModelAction *act = rit->getVal();
835 /* Don't want to add reflexive edges on 'rf' */
836 if (act->equals(rf)) {
837 if (act->happens_before(curr))
843 if (act->is_write()) {
844 /* C++, Section 29.3 statement 5 */
845 if (curr->is_seqcst() && last_sc_fence_thread_local &&
846 *act < *last_sc_fence_thread_local) {
847 if (mo_graph->checkReachable(rf, act))
850 priorset->push_back(act);
853 /* C++, Section 29.3 statement 4 */
854 else if (act->is_seqcst() && last_sc_fence_local &&
855 *act < *last_sc_fence_local) {
856 if (mo_graph->checkReachable(rf, act))
859 priorset->push_back(act);
862 /* C++, Section 29.3 statement 6 */
863 else if (last_sc_fence_thread_before &&
864 *act < *last_sc_fence_thread_before) {
865 if (mo_graph->checkReachable(rf, act))
868 priorset->push_back(act);
874 * Include at most one act per-thread that "happens
877 if (act->happens_before(curr)) {
879 if (last_sc_fence_local == NULL ||
880 (*last_sc_fence_local < *act)) {
881 prev_same_thread = act;
884 if (act->is_write()) {
885 if (mo_graph->checkReachable(rf, act))
888 priorset->push_back(act);
890 ModelAction *prevrf = act->get_reads_from();
891 if (!prevrf->equals(rf)) {
892 if (mo_graph->checkReachable(rf, prevrf))
895 priorset->push_back(prevrf);
897 if (act->get_tid() == curr->get_tid()) {
898 //Can prune curr from obj list
912 * Updates the mo_graph with the constraints imposed from the current write.
914 * Basic idea is the following: Go through each other thread and find
915 * the lastest action that happened before our write. Two cases:
917 * (1) The action is a write => that write must occur before
920 * (2) The action is a read => the write that that action read from
921 * must occur before the current write.
923 * This method also handles two other issues:
925 * (I) Sequential Consistency: Making sure that if the current write is
926 * seq_cst, that it occurs after the previous seq_cst write.
928 * (II) Sending the write back to non-synchronizing reads.
930 * @param curr The current action. Must be a write.
931 * @param send_fv A vector for stashing reads to which we may pass our future
932 * value. If NULL, then don't record any future values.
933 * @return True if modification order edges were added; false otherwise
935 void ModelExecution::w_modification_order(ModelAction *curr)
937 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
939 ASSERT(curr->is_write());
941 SnapList<ModelAction *> edgeset;
943 if (curr->is_seqcst()) {
944 /* We have to at least see the last sequentially consistent write,
945 so we are initialized. */
946 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
947 if (last_seq_cst != NULL) {
948 edgeset.push_back(last_seq_cst);
950 //update map for next query
951 obj_last_sc_map.put(curr->get_location(), curr);
954 /* Last SC fence in the current thread */
955 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
957 /* Iterate over all threads */
958 for (i = 0;i < thrd_lists->size();i++) {
959 /* Last SC fence in thread i, before last SC fence in current thread */
960 ModelAction *last_sc_fence_thread_before = NULL;
961 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
962 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
964 /* Iterate over actions in thread, starting from most recent */
965 action_list_t *list = &(*thrd_lists)[i];
966 sllnode<ModelAction*>* rit;
967 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
968 ModelAction *act = rit->getVal();
971 * 1) If RMW and it actually read from something, then we
972 * already have all relevant edges, so just skip to next
975 * 2) If RMW and it didn't read from anything, we should
976 * whatever edge we can get to speed up convergence.
978 * 3) If normal write, we need to look at earlier actions, so
979 * continue processing list.
981 if (curr->is_rmw()) {
982 if (curr->get_reads_from() != NULL)
990 /* C++, Section 29.3 statement 7 */
991 if (last_sc_fence_thread_before && act->is_write() &&
992 *act < *last_sc_fence_thread_before) {
993 edgeset.push_back(act);
998 * Include at most one act per-thread that "happens
1001 if (act->happens_before(curr)) {
1003 * Note: if act is RMW, just add edge:
1005 * The following edge should be handled elsewhere:
1006 * readfrom(act) --mo--> act
1008 if (act->is_write())
1009 edgeset.push_back(act);
1010 else if (act->is_read()) {
1011 //if previous read accessed a null, just keep going
1012 edgeset.push_back(act->get_reads_from());
1018 mo_graph->addEdges(&edgeset, curr);
1023 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1024 * some constraints. This method checks one the following constraint (others
1025 * require compiler support):
1027 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1028 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1030 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1032 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1034 /* Iterate over all threads */
1035 for (i = 0;i < thrd_lists->size();i++) {
1036 const ModelAction *write_after_read = NULL;
1038 /* Iterate over actions in thread, starting from most recent */
1039 action_list_t *list = &(*thrd_lists)[i];
1040 sllnode<ModelAction *>* rit;
1041 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1042 ModelAction *act = rit->getVal();
1044 /* Don't disallow due to act == reader */
1045 if (!reader->happens_before(act) || reader == act)
1047 else if (act->is_write())
1048 write_after_read = act;
1049 else if (act->is_read() && act->get_reads_from() != NULL)
1050 write_after_read = act->get_reads_from();
1053 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1060 * Computes the clock vector that happens before propagates from this write.
1062 * @param rf The action that might be part of a release sequence. Must be a
1064 * @return ClockVector of happens before relation.
1067 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1068 SnapVector<ModelAction *> * processset = NULL;
1069 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1070 ASSERT(rf->is_write());
1071 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1073 if (processset == NULL)
1074 processset = new SnapVector<ModelAction *>();
1075 processset->push_back(rf);
1078 int i = (processset == NULL) ? 0 : processset->size();
1080 ClockVector * vec = NULL;
1082 if (rf->get_rfcv() != NULL) {
1083 vec = rf->get_rfcv();
1084 } else if (rf->is_acquire() && rf->is_release()) {
1086 } else if (rf->is_release() && !rf->is_rmw()) {
1088 } else if (rf->is_release()) {
1089 //have rmw that is release and doesn't have a rfcv
1090 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1093 //operation that isn't release
1094 if (rf->get_last_fence_release()) {
1096 vec = rf->get_last_fence_release()->get_cv();
1098 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1104 rf = (*processset)[i];
1108 if (processset != NULL)
1114 * Performs various bookkeeping operations for the current ModelAction. For
1115 * instance, adds action to the per-object, per-thread action vector and to the
1116 * action trace list of all thread actions.
1118 * @param act is the ModelAction to add.
1120 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1122 int tid = id_to_int(act->get_tid());
1123 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1124 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1125 list->addAction(act);
1128 // Update action trace, a total order of all actions
1129 action_trace.addAction(act);
1132 // Update obj_thrd_map, a per location, per thread, order of actions
1133 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1134 if ((int)vec->size() <= tid) {
1135 uint oldsize = vec->size();
1136 vec->resize(priv->next_thread_id);
1137 for(uint i = oldsize;i < priv->next_thread_id;i++)
1138 new (&(*vec)[i]) action_list_t();
1140 fixup_action_list(vec);
1142 if (!canprune && (act->is_read() || act->is_write()))
1143 (*vec)[tid].addAction(act);
1145 // Update thrd_last_action, the last action taken by each thread
1146 if ((int)thrd_last_action.size() <= tid)
1147 thrd_last_action.resize(get_num_threads());
1148 thrd_last_action[tid] = act;
1150 // Update thrd_last_fence_release, the last release fence taken by each thread
1151 if (act->is_fence() && act->is_release()) {
1152 if ((int)thrd_last_fence_release.size() <= tid)
1153 thrd_last_fence_release.resize(get_num_threads());
1154 thrd_last_fence_release[tid] = act;
1157 if (act->is_wait()) {
1158 void *mutex_loc = (void *) act->get_value();
1159 get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
1163 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1164 list->addAction(act);
1167 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1168 act->create_cv(NULL);
1169 list->addAction(act);
1173 * Performs various bookkeeping operations for a normal write. The
1174 * complication is that we are typically inserting a normal write
1175 * lazily, so we need to insert it into the middle of lists.
1177 * @param act is the ModelAction to add.
1180 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1182 int tid = id_to_int(act->get_tid());
1183 insertIntoActionListAndSetCV(&action_trace, act);
1185 // Update obj_thrd_map, a per location, per thread, order of actions
1186 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1187 if (tid >= (int)vec->size()) {
1188 uint oldsize =vec->size();
1189 vec->resize(priv->next_thread_id);
1190 for(uint i=oldsize;i<priv->next_thread_id;i++)
1191 new (&(*vec)[i]) action_list_t();
1193 fixup_action_list(vec);
1195 insertIntoActionList(&(*vec)[tid],act);
1197 ModelAction * lastact = thrd_last_action[tid];
1198 // Update thrd_last_action, the last action taken by each thrad
1199 if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
1200 thrd_last_action[tid] = act;
1204 void ModelExecution::add_write_to_lists(ModelAction *write) {
1205 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1206 int tid = id_to_int(write->get_tid());
1207 if (tid >= (int)vec->size()) {
1208 uint oldsize =vec->size();
1209 vec->resize(priv->next_thread_id);
1210 for(uint i=oldsize;i<priv->next_thread_id;i++)
1211 new (&(*vec)[i]) action_list_t();
1213 fixup_action_list(vec);
1215 (*vec)[tid].addAction(write);
1219 * @brief Get the last action performed by a particular Thread
1220 * @param tid The thread ID of the Thread in question
1221 * @return The last action in the thread
1223 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1225 int threadid = id_to_int(tid);
1226 if (threadid < (int)thrd_last_action.size())
1227 return thrd_last_action[id_to_int(tid)];
1233 * @brief Get the last fence release performed by a particular Thread
1234 * @param tid The thread ID of the Thread in question
1235 * @return The last fence release in the thread, if one exists; NULL otherwise
1237 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1239 int threadid = id_to_int(tid);
1240 if (threadid < (int)thrd_last_fence_release.size())
1241 return thrd_last_fence_release[id_to_int(tid)];
1247 * Gets the last memory_order_seq_cst write (in the total global sequence)
1248 * performed on a particular object (i.e., memory location), not including the
1250 * @param curr The current ModelAction; also denotes the object location to
1252 * @return The last seq_cst write
1254 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1256 void *location = curr->get_location();
1257 return obj_last_sc_map.get(location);
1261 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1262 * performed in a particular thread, prior to a particular fence.
1263 * @param tid The ID of the thread to check
1264 * @param before_fence The fence from which to begin the search; if NULL, then
1265 * search for the most recent fence in the thread.
1266 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1268 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1270 /* All fences should have location FENCE_LOCATION */
1271 action_list_t *list = obj_map.get(FENCE_LOCATION);
1276 sllnode<ModelAction*>* rit = list->end();
1279 for (;rit != NULL;rit=rit->getPrev())
1280 if (rit->getVal() == before_fence)
1283 ASSERT(rit->getVal() == before_fence);
1287 for (;rit != NULL;rit=rit->getPrev()) {
1288 ModelAction *act = rit->getVal();
1289 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1296 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1297 * location). This function identifies the mutex according to the current
1298 * action, which is presumed to perform on the same mutex.
1299 * @param curr The current ModelAction; also denotes the object location to
1301 * @return The last unlock operation
1303 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1305 void *location = curr->get_location();
1307 action_list_t *list = obj_map.get(location);
1311 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1312 sllnode<ModelAction*>* rit;
1313 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1314 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1315 return rit->getVal();
1319 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1321 ModelAction *parent = get_last_action(tid);
1323 parent = get_thread(tid)->get_creation();
1328 * Returns the clock vector for a given thread.
1329 * @param tid The thread whose clock vector we want
1330 * @return Desired clock vector
1332 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1334 ModelAction *firstaction=get_parent_action(tid);
1335 return firstaction != NULL ? firstaction->get_cv() : NULL;
1338 bool valequals(uint64_t val1, uint64_t val2, int size) {
1341 return ((uint8_t)val1) == ((uint8_t)val2);
1343 return ((uint16_t)val1) == ((uint16_t)val2);
1345 return ((uint32_t)val1) == ((uint32_t)val2);
1355 * Build up an initial set of all past writes that this 'read' action may read
1356 * from, as well as any previously-observed future values that must still be valid.
1358 * @param curr is the current ModelAction that we are exploring; it must be a
1361 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1363 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1365 ASSERT(curr->is_read());
1367 ModelAction *last_sc_write = NULL;
1369 if (curr->is_seqcst())
1370 last_sc_write = get_last_seq_cst_write(curr);
1372 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1374 /* Iterate over all threads */
1375 if (thrd_lists != NULL)
1376 for (i = 0;i < thrd_lists->size();i++) {
1377 /* Iterate over actions in thread, starting from most recent */
1378 action_list_t *list = &(*thrd_lists)[i];
1379 sllnode<ModelAction *> * rit;
1380 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1381 ModelAction *act = rit->getVal();
1386 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1387 bool allow_read = true;
1389 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1392 /* Need to check whether we will have two RMW reading from the same value */
1393 if (curr->is_rmwr()) {
1394 /* It is okay if we have a failing CAS */
1395 if (!curr->is_rmwrcas() ||
1396 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1397 //Need to make sure we aren't the second RMW
1398 CycleNode * node = mo_graph->getNode_noCreate(act);
1399 if (node != NULL && node->getRMW() != NULL) {
1400 //we are the second RMW
1407 /* Only add feasible reads */
1408 rf_set->push_back(act);
1411 /* Include at most one act per-thread that "happens before" curr */
1412 if (act->happens_before(curr))
1417 if (DBG_ENABLED()) {
1418 model_print("Reached read action:\n");
1420 model_print("End printing read_from_past\n");
1425 static void print_list(action_list_t *list)
1427 sllnode<ModelAction*> *it;
1429 model_print("------------------------------------------------------------------------------------\n");
1430 model_print("# t Action type MO Location Value Rf CV\n");
1431 model_print("------------------------------------------------------------------------------------\n");
1433 unsigned int hash = 0;
1435 for (it = list->begin();it != NULL;it=it->getNext()) {
1436 const ModelAction *act = it->getVal();
1437 if (act->get_seq_number() > 0)
1439 hash = hash^(hash<<3)^(it->getVal()->hash());
1441 model_print("HASH %u\n", hash);
1442 model_print("------------------------------------------------------------------------------------\n");
1445 #if SUPPORT_MOD_ORDER_DUMP
1446 void ModelExecution::dumpGraph(char *filename)
1449 sprintf(buffer, "%s.dot", filename);
1450 FILE *file = fopen(buffer, "w");
1451 fprintf(file, "digraph %s {\n", filename);
1452 mo_graph->dumpNodes(file);
1453 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1455 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1456 ModelAction *act = it->getVal();
1457 if (act->is_read()) {
1458 mo_graph->dot_print_node(file, act);
1459 mo_graph->dot_print_edge(file,
1460 act->get_reads_from(),
1462 "label=\"rf\", color=red, weight=2");
1464 if (thread_array[act->get_tid()]) {
1465 mo_graph->dot_print_edge(file,
1466 thread_array[id_to_int(act->get_tid())],
1468 "label=\"sb\", color=blue, weight=400");
1471 thread_array[act->get_tid()] = act;
1473 fprintf(file, "}\n");
1474 model_free(thread_array);
1479 /** @brief Prints an execution trace summary. */
1480 void ModelExecution::print_summary()
1482 #if SUPPORT_MOD_ORDER_DUMP
1483 char buffername[100];
1484 sprintf(buffername, "exec%04u", get_execution_number());
1485 mo_graph->dumpGraphToFile(buffername);
1486 sprintf(buffername, "graph%04u", get_execution_number());
1487 dumpGraph(buffername);
1490 model_print("Execution trace %d:", get_execution_number());
1491 if (scheduler->all_threads_sleeping())
1492 model_print(" SLEEP-SET REDUNDANT");
1493 if (have_bug_reports())
1494 model_print(" DETECTED BUG(S)");
1498 print_list(&action_trace);
1503 void ModelExecution::print_tail()
1505 model_print("Execution trace %d:\n", get_execution_number());
1507 sllnode<ModelAction*> *it;
1509 model_print("------------------------------------------------------------------------------------\n");
1510 model_print("# t Action type MO Location Value Rf CV\n");
1511 model_print("------------------------------------------------------------------------------------\n");
1513 unsigned int hash = 0;
1517 SnapList<ModelAction *> list;
1518 for (it = action_trace.end();it != NULL;it = it->getPrev()) {
1519 if (counter > length)
1522 ModelAction * act = it->getVal();
1523 list.push_front(act);
1527 for (it = list.begin();it != NULL;it=it->getNext()) {
1528 const ModelAction *act = it->getVal();
1529 if (act->get_seq_number() > 0)
1531 hash = hash^(hash<<3)^(it->getVal()->hash());
1533 model_print("HASH %u\n", hash);
1534 model_print("------------------------------------------------------------------------------------\n");
1538 * Add a Thread to the system for the first time. Should only be called once
1540 * @param t The Thread to add
1542 void ModelExecution::add_thread(Thread *t)
1544 unsigned int i = id_to_int(t->get_id());
1545 if (i >= thread_map.size())
1546 thread_map.resize(i + 1);
1548 if (!t->is_model_thread())
1549 scheduler->add_thread(t);
1553 * @brief Get a Thread reference by its ID
1554 * @param tid The Thread's ID
1555 * @return A Thread reference
1557 Thread * ModelExecution::get_thread(thread_id_t tid) const
1559 unsigned int i = id_to_int(tid);
1560 if (i < thread_map.size())
1561 return thread_map[i];
1566 * @brief Get a reference to the Thread in which a ModelAction was executed
1567 * @param act The ModelAction
1568 * @return A Thread reference
1570 Thread * ModelExecution::get_thread(const ModelAction *act) const
1572 return get_thread(act->get_tid());
1576 * @brief Get a Thread reference by its pthread ID
1577 * @param index The pthread's ID
1578 * @return A Thread reference
1580 Thread * ModelExecution::get_pthread(pthread_t pid) {
1581 // pid 1 is reserved for the main thread, pthread ids should start from 2
1583 return get_thread(pid);
1590 uint32_t thread_id = x.v;
1592 if (thread_id < pthread_counter + 1)
1593 return pthread_map[thread_id];
1599 * @brief Check if a Thread is currently enabled
1600 * @param t The Thread to check
1601 * @return True if the Thread is currently enabled
1603 bool ModelExecution::is_enabled(Thread *t) const
1605 return scheduler->is_enabled(t);
1609 * @brief Check if a Thread is currently enabled
1610 * @param tid The ID of the Thread to check
1611 * @return True if the Thread is currently enabled
1613 bool ModelExecution::is_enabled(thread_id_t tid) const
1615 return scheduler->is_enabled(tid);
1619 * @brief Select the next thread to execute based on the curren action
1621 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1622 * actions should be followed by the execution of their child thread. In either
1623 * case, the current action should determine the next thread schedule.
1625 * @param curr The current action
1626 * @return The next thread to run, if the current action will determine this
1627 * selection; otherwise NULL
1629 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1631 /* Do not split atomic RMW */
1632 if (curr->is_rmwr())
1633 return get_thread(curr);
1634 /* Follow CREATE with the created thread */
1635 /* which is not needed, because model.cc takes care of this */
1636 if (curr->get_type() == THREAD_CREATE)
1637 return curr->get_thread_operand();
1638 if (curr->get_type() == PTHREAD_CREATE) {
1639 return curr->get_thread_operand();
1645 * Takes the next step in the execution, if possible.
1646 * @param curr The current step to take
1647 * @return Returns the next Thread to run, if any; NULL if this execution
1650 Thread * ModelExecution::take_step(ModelAction *curr)
1652 Thread *curr_thrd = get_thread(curr);
1653 ASSERT(curr_thrd->get_state() == THREAD_READY);
1655 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1656 curr = check_current_action(curr);
1659 /* Process this action in ModelHistory for records */
1661 model->get_history()->process_action( curr, curr->get_tid() );
1663 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1664 scheduler->remove_thread(curr_thrd);
1666 return action_select_next_thread(curr);
1669 /** This method removes references to an Action before we delete it. */
1671 void ModelExecution::removeAction(ModelAction *act) {
1673 action_trace.removeAction(act);
1676 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1677 (*vec)[act->get_tid()].removeAction(act);
1679 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1680 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1681 list->removeAction(act);
1682 } else if (act->is_wait()) {
1683 void *mutex_loc = (void *) act->get_value();
1684 get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
1685 } else if (act->is_free()) {
1686 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1687 (*vec)[act->get_tid()].removeAction(act);
1689 //Clear it from last_sc_map
1690 if (obj_last_sc_map.get(act->get_location()) == act) {
1691 obj_last_sc_map.remove(act->get_location());
1694 //Remove from Cyclegraph
1695 mo_graph->freeAction(act);
1699 /** Computes clock vector that all running threads have already synchronized to. */
1701 ClockVector * ModelExecution::computeMinimalCV() {
1702 ClockVector *cvmin = NULL;
1703 //Thread 0 isn't a real thread, so skip it..
1704 for(unsigned int i = 1;i < thread_map.size();i++) {
1705 Thread * t = thread_map[i];
1706 if (t->get_state() == THREAD_COMPLETED)
1708 thread_id_t tid = int_to_id(i);
1709 ClockVector * cv = get_cv(tid);
1711 cvmin = new ClockVector(cv, NULL);
1713 cvmin->minmerge(cv);
1719 /** Sometimes we need to remove an action that is the most recent in the thread. This happens if it is mo before action in other threads. In that case we need to create a replacement latest ModelAction */
1721 void ModelExecution::fixupLastAct(ModelAction *act) {
1722 ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid()));
1723 newact->set_seq_number(get_next_seq_num());
1724 newact->create_cv(act);
1725 newact->set_last_fence_release(act->get_last_fence_release());
1726 add_action_to_lists(newact, false);
1729 /** Compute which actions to free. */
1731 void ModelExecution::collectActions() {
1732 if (priv->used_sequence_numbers < params->traceminsize)
1735 //Compute minimal clock vector for all live threads
1736 ClockVector *cvmin = computeMinimalCV();
1737 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1738 modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1740 //Next walk action trace... When we hit an action, see if it is
1741 //invisible (e.g., earlier than the first before the minimum
1742 //clock for the thread... if so erase it and all previous
1743 //actions in cyclegraph
1744 sllnode<ModelAction*> * it;
1745 for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1746 ModelAction *act = it->getVal();
1747 modelclock_t actseq = act->get_seq_number();
1749 //See if we are done
1750 if (actseq > maxtofree)
1753 thread_id_t act_tid = act->get_tid();
1754 modelclock_t tid_clock = cvmin->getClock(act_tid);
1756 //Free if it is invisible or we have set a flag to remove visible actions.
1757 if (actseq <= tid_clock || params->removevisible) {
1758 ModelAction * write;
1759 if (act->is_write()) {
1761 } else if (act->is_read()) {
1762 write = act->get_reads_from();
1766 //Mark everything earlier in MO graph to be freed
1767 CycleNode * cn = mo_graph->getNode_noCreate(write);
1769 queue->push_back(cn);
1770 while(!queue->empty()) {
1771 CycleNode * node = queue->back();
1773 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1774 CycleNode * prevnode = node->getInEdge(i);
1775 ModelAction * prevact = prevnode->getAction();
1776 if (prevact->get_type() != READY_FREE) {
1777 prevact->set_free();
1778 queue->push_back(prevnode);
1786 //We may need to remove read actions in the window we don't delete to preserve correctness.
1788 for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1789 ModelAction *act = it2->getVal();
1790 //Do iteration early in case we delete the act
1792 bool islastact = false;
1793 ModelAction *lastact = get_last_action(act->get_tid());
1794 if (act == lastact) {
1795 Thread * th = get_thread(act);
1796 islastact = !th->is_complete();
1799 if (act->is_read()) {
1800 if (act->get_reads_from()->is_free()) {
1801 if (act->is_rmw()) {
1802 //Weaken a RMW from a freed store to a write
1803 act->set_type(ATOMIC_WRITE);
1815 //If we don't delete the action, we should remove references to release fences
1817 const ModelAction *rel_fence =act->get_last_fence_release();
1818 if (rel_fence != NULL) {
1819 modelclock_t relfenceseq = rel_fence->get_seq_number();
1820 thread_id_t relfence_tid = rel_fence->get_tid();
1821 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1822 //Remove references to irrelevant release fences
1823 if (relfenceseq <= tid_clock)
1824 act->set_last_fence_release(NULL);
1827 //Now we are in the window of old actions that we remove if possible
1828 for (;it != NULL;) {
1829 ModelAction *act = it->getVal();
1830 //Do iteration early since we may delete node...
1832 bool islastact = false;
1833 ModelAction *lastact = get_last_action(act->get_tid());
1834 if (act == lastact) {
1835 Thread * th = get_thread(act);
1836 islastact = !th->is_complete();
1839 if (act->is_read()) {
1840 if (act->get_reads_from()->is_free()) {
1841 if (act->is_rmw()) {
1842 act->set_type(ATOMIC_WRITE);
1852 } else if (act->is_free()) {
1859 } else if (act->is_write()) {
1860 //Do nothing with write that hasn't been marked to be freed
1861 } else if (islastact) {
1862 //Keep the last action for non-read/write actions
1863 } else if (act->is_fence()) {
1864 //Note that acquire fences can always be safely
1865 //removed, but could incur extra overheads in
1866 //traversals. Removing them before the cvmin seems
1867 //like a good compromise.
1869 //Release fences before the cvmin don't do anything
1870 //because everyone has already synchronized.
1872 //Sequentially fences before cvmin are redundant
1873 //because happens-before will enforce same
1876 modelclock_t actseq = act->get_seq_number();
1877 thread_id_t act_tid = act->get_tid();
1878 modelclock_t tid_clock = cvmin->getClock(act_tid);
1879 if (actseq <= tid_clock) {
1881 // Remove reference to act from thrd_last_fence_release
1882 int thread_id = id_to_int( act->get_tid() );
1883 if (thrd_last_fence_release[thread_id] == act) {
1884 thrd_last_fence_release[thread_id] = NULL;
1890 //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1891 //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1892 //need to keep most recent unlock/wait for each lock
1893 if(act->is_unlock() || act->is_wait()) {
1894 ModelAction * lastlock = get_last_unlock(act);
1895 if (lastlock != act) {
1900 } else if (act->is_create()) {
1901 if (act->get_thread_operand()->is_complete()) {
1913 //If we don't delete the action, we should remove references to release fences
1914 const ModelAction *rel_fence =act->get_last_fence_release();
1915 if (rel_fence != NULL) {
1916 modelclock_t relfenceseq = rel_fence->get_seq_number();
1917 thread_id_t relfence_tid = rel_fence->get_tid();
1918 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1919 //Remove references to irrelevant release fences
1920 if (relfenceseq <= tid_clock)
1921 act->set_last_fence_release(NULL);
1929 Fuzzer * ModelExecution::getFuzzer() {