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()),
67 fuzzer(new NewFuzzer()),
73 /* Initialize a model-checker thread, for special ModelActions */
74 model_thread = new Thread(get_next_id());
75 add_thread(model_thread);
76 fuzzer->register_engine(m, this);
77 scheduler->register_engine(this);
79 pthread_key_create(&pthreadkey, tlsdestructor);
83 /** @brief Destructor */
84 ModelExecution::~ModelExecution()
86 for (unsigned int i = 0;i < get_num_threads();i++)
87 delete get_thread(int_to_id(i));
93 int ModelExecution::get_execution_number() const
95 return model->get_execution_number();
98 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
100 action_list_t *tmp = hash->get(ptr);
102 tmp = new action_list_t();
108 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
110 SnapVector<action_list_t> *tmp = hash->get(ptr);
112 tmp = new SnapVector<action_list_t>();
118 /** @return a thread ID for a new Thread */
119 thread_id_t ModelExecution::get_next_id()
121 return priv->next_thread_id++;
124 /** @return the number of user threads created during this execution */
125 unsigned int ModelExecution::get_num_threads() const
127 return priv->next_thread_id;
130 /** @return a sequence number for a new ModelAction */
131 modelclock_t ModelExecution::get_next_seq_num()
133 return ++priv->used_sequence_numbers;
136 /** @return a sequence number for a new ModelAction */
137 modelclock_t ModelExecution::get_curr_seq_num()
139 return priv->used_sequence_numbers;
142 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
143 void ModelExecution::restore_last_seq_num()
145 priv->used_sequence_numbers--;
149 * @brief Should the current action wake up a given thread?
151 * @param curr The current action
152 * @param thread The thread that we might wake up
153 * @return True, if we should wake up the sleeping thread; false otherwise
155 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
157 const ModelAction *asleep = thread->get_pending();
158 /* Don't allow partial RMW to wake anyone up */
161 /* Synchronizing actions may have been backtracked */
162 if (asleep->could_synchronize_with(curr))
164 /* All acquire/release fences and fence-acquire/store-release */
165 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
167 /* Fence-release + store can awake load-acquire on the same location */
168 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
169 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
170 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
173 /* The sleep is literally sleeping */
174 if (asleep->is_sleep()) {
175 if (fuzzer->shouldWake(asleep))
182 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
184 for (unsigned int i = 0;i < get_num_threads();i++) {
185 Thread *thr = get_thread(int_to_id(i));
186 if (scheduler->is_sleep_set(thr)) {
187 if (should_wake_up(curr, thr)) {
188 /* Remove this thread from sleep set */
189 scheduler->remove_sleep(thr);
190 if (thr->get_pending()->is_sleep())
191 thr->set_wakeup_state(true);
197 void ModelExecution::assert_bug(const char *msg)
199 priv->bugs.push_back(new bug_message(msg));
203 /** @return True, if any bugs have been reported for this execution */
204 bool ModelExecution::have_bug_reports() const
206 return priv->bugs.size() != 0;
209 SnapVector<bug_message *> * ModelExecution::get_bugs() const
215 * Check whether the current trace has triggered an assertion which should halt
218 * @return True, if the execution should be aborted; false otherwise
220 bool ModelExecution::has_asserted() const
222 return priv->asserted;
226 * Trigger a trace assertion which should cause this execution to be halted.
227 * This can be due to a detected bug or due to an infeasibility that should
230 void ModelExecution::set_assert()
232 priv->asserted = true;
236 * Check if we are in a deadlock. Should only be called at the end of an
237 * execution, although it should not give false positives in the middle of an
238 * execution (there should be some ENABLED thread).
240 * @return True if program is in a deadlock; false otherwise
242 bool ModelExecution::is_deadlocked() const
244 bool blocking_threads = false;
245 for (unsigned int i = 0;i < get_num_threads();i++) {
246 thread_id_t tid = int_to_id(i);
249 Thread *t = get_thread(tid);
250 if (!t->is_model_thread() && t->get_pending())
251 blocking_threads = true;
253 return blocking_threads;
257 * Check if this is a complete execution. That is, have all thread completed
258 * execution (rather than exiting because sleep sets have forced a redundant
261 * @return True if the execution is complete.
263 bool ModelExecution::is_complete_execution() const
265 for (unsigned int i = 0;i < get_num_threads();i++)
266 if (is_enabled(int_to_id(i)))
271 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
272 uint64_t value = *((const uint64_t *) location);
273 modelclock_t storeclock;
274 thread_id_t storethread;
275 getStoreThreadAndClock(location, &storethread, &storeclock);
276 setAtomicStoreFlag(location);
277 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
278 act->set_seq_number(storeclock);
279 add_normal_write_to_lists(act);
280 add_write_to_lists(act);
281 w_modification_order(act);
283 model->get_history()->process_action(act, act->get_tid());
289 * Processes a read model action.
290 * @param curr is the read model action to process.
291 * @param rf_set is the set of model actions we can possibly read from
292 * @return True if the read can be pruned from the thread map list.
294 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
296 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
297 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
298 if (hasnonatomicstore) {
299 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
300 rf_set->push_back(nonatomicstore);
303 // Remove writes that violate read modification order
306 while (i < rf_set->size()) {
307 ModelAction * rf = (*rf_set)[i];
308 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
309 (*rf_set)[i] = rf_set->back();
316 int index = fuzzer->selectWrite(curr, rf_set);
318 ModelAction *rf = (*rf_set)[index];
321 bool canprune = false;
322 if (r_modification_order(curr, rf, priorset, &canprune)) {
323 for(unsigned int i=0;i<priorset->size();i++) {
324 mo_graph->addEdge((*priorset)[i], rf);
327 get_thread(curr)->set_return_value(curr->get_return_value());
329 return canprune && (curr->get_type() == ATOMIC_READ);
332 (*rf_set)[index] = rf_set->back();
338 * Processes a lock, trylock, or unlock model action. @param curr is
339 * the read model action to process.
341 * The try lock operation checks whether the lock is taken. If not,
342 * it falls to the normal lock operation case. If so, it returns
345 * The lock operation has already been checked that it is enabled, so
346 * it just grabs the lock and synchronizes with the previous unlock.
348 * The unlock operation has to re-enable all of the threads that are
349 * waiting on the lock.
351 * @return True if synchronization was updated; false otherwise
353 bool ModelExecution::process_mutex(ModelAction *curr)
355 cdsc::mutex *mutex = curr->get_mutex();
356 struct cdsc::mutex_state *state = NULL;
359 state = mutex->get_state();
361 switch (curr->get_type()) {
362 case ATOMIC_TRYLOCK: {
363 bool success = !state->locked;
364 curr->set_try_lock(success);
366 get_thread(curr)->set_return_value(0);
369 get_thread(curr)->set_return_value(1);
371 //otherwise fall into the lock case
373 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
374 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
375 // assert_bug("Lock access before initialization");
376 state->locked = get_thread(curr);
377 ModelAction *unlock = get_last_unlock(curr);
378 //synchronize with the previous unlock statement
379 if (unlock != NULL) {
380 synchronize(unlock, curr);
386 //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
387 if (fuzzer->shouldWait(curr)) {
388 /* wake up the other threads */
389 for (unsigned int i = 0;i < get_num_threads();i++) {
390 Thread *t = get_thread(int_to_id(i));
391 Thread *curr_thrd = get_thread(curr);
392 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
396 /* unlock the lock - after checking who was waiting on it */
397 state->locked = NULL;
399 /* disable this thread */
400 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
401 scheduler->sleep(get_thread(curr));
406 case ATOMIC_TIMEDWAIT:
407 case ATOMIC_UNLOCK: {
408 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
409 //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
410 //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
411 //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
412 //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
413 //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
414 //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
415 //MUST EVENMTUALLY RELEASE...
417 /* wake up the other threads */
418 for (unsigned int i = 0;i < get_num_threads();i++) {
419 Thread *t = get_thread(int_to_id(i));
420 Thread *curr_thrd = get_thread(curr);
421 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
425 /* unlock the lock - after checking who was waiting on it */
426 state->locked = NULL;
429 case ATOMIC_NOTIFY_ALL: {
430 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
431 //activate all the waiting threads
432 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
433 scheduler->wake(get_thread(rit->getVal()));
438 case ATOMIC_NOTIFY_ONE: {
439 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
440 if (waiters->size() != 0) {
441 Thread * thread = fuzzer->selectNotify(waiters);
442 scheduler->wake(thread);
454 * Process a write ModelAction
455 * @param curr The ModelAction to process
456 * @return True if the mo_graph was updated or promises were resolved
458 void ModelExecution::process_write(ModelAction *curr)
460 w_modification_order(curr);
461 get_thread(curr)->set_return_value(VALUE_NONE);
465 * Process a fence ModelAction
466 * @param curr The ModelAction to process
467 * @return True if synchronization was updated
469 bool ModelExecution::process_fence(ModelAction *curr)
472 * fence-relaxed: no-op
473 * fence-release: only log the occurence (not in this function), for
474 * use in later synchronization
475 * fence-acquire (this function): search for hypothetical release
477 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
479 bool updated = false;
480 if (curr->is_acquire()) {
481 action_list_t *list = &action_trace;
482 sllnode<ModelAction *> * rit;
483 /* Find X : is_read(X) && X --sb-> curr */
484 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
485 ModelAction *act = rit->getVal();
488 if (act->get_tid() != curr->get_tid())
490 /* Stop at the beginning of the thread */
491 if (act->is_thread_start())
493 /* Stop once we reach a prior fence-acquire */
494 if (act->is_fence() && act->is_acquire())
498 /* read-acquire will find its own release sequences */
499 if (act->is_acquire())
502 /* Establish hypothetical release sequences */
503 ClockVector *cv = get_hb_from_write(act->get_reads_from());
504 if (cv != NULL && curr->get_cv()->merge(cv))
512 * @brief Process the current action for thread-related activity
514 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
515 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
516 * synchronization, etc. This function is a no-op for non-THREAD actions
517 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
519 * @param curr The current action
520 * @return True if synchronization was updated or a thread completed
522 void ModelExecution::process_thread_action(ModelAction *curr)
524 switch (curr->get_type()) {
525 case THREAD_CREATE: {
526 thrd_t *thrd = (thrd_t *)curr->get_location();
527 struct thread_params *params = (struct thread_params *)curr->get_value();
528 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
529 curr->set_thread_operand(th);
531 th->set_creation(curr);
534 case PTHREAD_CREATE: {
535 (*(uint32_t *)curr->get_location()) = pthread_counter++;
537 struct pthread_params *params = (struct pthread_params *)curr->get_value();
538 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
539 curr->set_thread_operand(th);
541 th->set_creation(curr);
543 if ( pthread_map.size() < pthread_counter )
544 pthread_map.resize( pthread_counter );
545 pthread_map[ pthread_counter-1 ] = th;
550 Thread *blocking = curr->get_thread_operand();
551 ModelAction *act = get_last_action(blocking->get_id());
552 synchronize(act, curr);
556 Thread *blocking = curr->get_thread_operand();
557 ModelAction *act = get_last_action(blocking->get_id());
558 synchronize(act, curr);
559 break; // WL: to be add (modified)
562 case THREADONLY_FINISH:
563 case THREAD_FINISH: {
564 Thread *th = get_thread(curr);
565 if (curr->get_type() == THREAD_FINISH &&
566 th == model->getInitThread()) {
572 /* Wake up any joining threads */
573 for (unsigned int i = 0;i < get_num_threads();i++) {
574 Thread *waiting = get_thread(int_to_id(i));
575 if (waiting->waiting_on() == th &&
576 waiting->get_pending()->is_thread_join())
577 scheduler->wake(waiting);
586 Thread *th = get_thread(curr);
587 th->set_pending(curr);
588 scheduler->add_sleep(th);
597 * Initialize the current action by performing one or more of the following
598 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
599 * manipulating backtracking sets, allocating and
600 * initializing clock vectors, and computing the promises to fulfill.
602 * @param curr The current action, as passed from the user context; may be
603 * freed/invalidated after the execution of this function, with a different
604 * action "returned" its place (pass-by-reference)
605 * @return True if curr is a newly-explored action; false otherwise
607 bool ModelExecution::initialize_curr_action(ModelAction **curr)
609 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
610 ModelAction *newcurr = process_rmw(*curr);
616 ModelAction *newcurr = *curr;
618 newcurr->set_seq_number(get_next_seq_num());
619 /* Always compute new clock vector */
620 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
622 /* Assign most recent release fence */
623 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
625 return true; /* This was a new ModelAction */
630 * @brief Establish reads-from relation between two actions
632 * Perform basic operations involved with establishing a concrete rf relation,
633 * including setting the ModelAction data and checking for release sequences.
635 * @param act The action that is reading (must be a read)
636 * @param rf The action from which we are reading (must be a write)
638 * @return True if this read established synchronization
641 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
644 ASSERT(rf->is_write());
646 act->set_read_from(rf);
647 if (act->is_acquire()) {
648 ClockVector *cv = get_hb_from_write(rf);
651 act->get_cv()->merge(cv);
656 * @brief Synchronizes two actions
658 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
659 * This function performs the synchronization as well as providing other hooks
660 * for other checks along with synchronization.
662 * @param first The left-hand side of the synchronizes-with relation
663 * @param second The right-hand side of the synchronizes-with relation
664 * @return True if the synchronization was successful (i.e., was consistent
665 * with the execution order); false otherwise
667 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
669 if (*second < *first) {
670 ASSERT(0); //This should not happend
673 return second->synchronize_with(first);
677 * @brief Check whether a model action is enabled.
679 * Checks whether an operation would be successful (i.e., is a lock already
680 * locked, or is the joined thread already complete).
682 * For yield-blocking, yields are never enabled.
684 * @param curr is the ModelAction to check whether it is enabled.
685 * @return a bool that indicates whether the action is enabled.
687 bool ModelExecution::check_action_enabled(ModelAction *curr) {
688 if (curr->is_lock()) {
689 cdsc::mutex *lock = curr->get_mutex();
690 struct cdsc::mutex_state *state = lock->get_state();
693 } else if (curr->is_thread_join()) {
694 Thread *blocking = curr->get_thread_operand();
695 if (!blocking->is_complete()) {
698 } else if (curr->is_sleep()) {
699 if (!fuzzer->shouldSleep(curr))
707 * This is the heart of the model checker routine. It performs model-checking
708 * actions corresponding to a given "current action." Among other processes, it
709 * calculates reads-from relationships, updates synchronization clock vectors,
710 * forms a memory_order constraints graph, and handles replay/backtrack
711 * execution when running permutations of previously-observed executions.
713 * @param curr The current action to process
714 * @return The ModelAction that is actually executed; may be different than
717 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
720 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
721 bool newly_explored = initialize_curr_action(&curr);
725 wake_up_sleeping_actions(curr);
727 SnapVector<ModelAction *> * rf_set = NULL;
728 /* Build may_read_from set for newly-created actions */
729 if (newly_explored && curr->is_read())
730 rf_set = build_may_read_from(curr);
732 bool canprune = false;
734 if (curr->is_read() && !second_part_of_rmw) {
735 canprune = process_read(curr, rf_set);
738 ASSERT(rf_set == NULL);
740 /* Add the action to lists */
741 if (!second_part_of_rmw)
742 add_action_to_lists(curr, canprune);
744 if (curr->is_write())
745 add_write_to_lists(curr);
747 process_thread_action(curr);
749 if (curr->is_write())
752 if (curr->is_fence())
755 if (curr->is_mutex_op())
761 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
762 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
763 ModelAction *lastread = get_last_action(act->get_tid());
764 lastread->process_rmw(act);
766 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
772 * @brief Updates the mo_graph with the constraints imposed from the current
775 * Basic idea is the following: Go through each other thread and find
776 * the last action that happened before our read. Two cases:
778 * -# The action is a write: that write must either occur before
779 * the write we read from or be the write we read from.
780 * -# The action is a read: the write that that action read from
781 * must occur before the write we read from or be the same write.
783 * @param curr The current action. Must be a read.
784 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
785 * @param check_only If true, then only check whether the current action satisfies
786 * read modification order or not, without modifiying priorset and canprune.
788 * @return True if modification order edges were added; false otherwise
791 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
792 SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
794 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
795 ASSERT(curr->is_read());
797 /* Last SC fence in the current thread */
798 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
800 int tid = curr->get_tid();
802 /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
803 if ((int)thrd_lists->size() <= tid) {
804 uint oldsize = thrd_lists->size();
805 thrd_lists->resize(priv->next_thread_id);
806 for(uint i = oldsize;i < priv->next_thread_id;i++)
807 new (&(*thrd_lists)[i]) action_list_t();
810 ModelAction *prev_same_thread = NULL;
811 /* Iterate over all threads */
812 for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
813 /* Last SC fence in thread tid */
814 ModelAction *last_sc_fence_thread_local = NULL;
816 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
818 /* Last SC fence in thread tid, before last SC fence in current thread */
819 ModelAction *last_sc_fence_thread_before = NULL;
820 if (last_sc_fence_local)
821 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
823 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
824 if (prev_same_thread != NULL &&
825 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
826 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
830 /* Iterate over actions in thread, starting from most recent */
831 action_list_t *list = &(*thrd_lists)[tid];
832 sllnode<ModelAction *> * rit;
833 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
834 ModelAction *act = rit->getVal();
839 /* Don't want to add reflexive edges on 'rf' */
840 if (act->equals(rf)) {
841 if (act->happens_before(curr))
847 if (act->is_write()) {
848 /* C++, Section 29.3 statement 5 */
849 if (curr->is_seqcst() && last_sc_fence_thread_local &&
850 *act < *last_sc_fence_thread_local) {
851 if (mo_graph->checkReachable(rf, act))
854 priorset->push_back(act);
857 /* C++, Section 29.3 statement 4 */
858 else if (act->is_seqcst() && last_sc_fence_local &&
859 *act < *last_sc_fence_local) {
860 if (mo_graph->checkReachable(rf, act))
863 priorset->push_back(act);
866 /* C++, Section 29.3 statement 6 */
867 else if (last_sc_fence_thread_before &&
868 *act < *last_sc_fence_thread_before) {
869 if (mo_graph->checkReachable(rf, act))
872 priorset->push_back(act);
878 * Include at most one act per-thread that "happens
881 if (act->happens_before(curr)) {
883 if (last_sc_fence_local == NULL ||
884 (*last_sc_fence_local < *act)) {
885 prev_same_thread = act;
888 if (act->is_write()) {
889 if (mo_graph->checkReachable(rf, act))
892 priorset->push_back(act);
894 ModelAction *prevrf = act->get_reads_from();
895 if (!prevrf->equals(rf)) {
896 if (mo_graph->checkReachable(rf, prevrf))
899 priorset->push_back(prevrf);
901 if (act->get_tid() == curr->get_tid()) {
902 //Can prune curr from obj list
916 * Updates the mo_graph with the constraints imposed from the current write.
918 * Basic idea is the following: Go through each other thread and find
919 * the lastest action that happened before our write. Two cases:
921 * (1) The action is a write => that write must occur before
924 * (2) The action is a read => the write that that action read from
925 * must occur before the current write.
927 * This method also handles two other issues:
929 * (I) Sequential Consistency: Making sure that if the current write is
930 * seq_cst, that it occurs after the previous seq_cst write.
932 * (II) Sending the write back to non-synchronizing reads.
934 * @param curr The current action. Must be a write.
935 * @param send_fv A vector for stashing reads to which we may pass our future
936 * value. If NULL, then don't record any future values.
937 * @return True if modification order edges were added; false otherwise
939 void ModelExecution::w_modification_order(ModelAction *curr)
941 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
943 ASSERT(curr->is_write());
945 SnapList<ModelAction *> edgeset;
947 if (curr->is_seqcst()) {
948 /* We have to at least see the last sequentially consistent write,
949 so we are initialized. */
950 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
951 if (last_seq_cst != NULL) {
952 edgeset.push_back(last_seq_cst);
954 //update map for next query
955 obj_last_sc_map.put(curr->get_location(), curr);
958 /* Last SC fence in the current thread */
959 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
961 /* Iterate over all threads */
962 for (i = 0;i < thrd_lists->size();i++) {
963 /* Last SC fence in thread i, before last SC fence in current thread */
964 ModelAction *last_sc_fence_thread_before = NULL;
965 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
966 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
968 /* Iterate over actions in thread, starting from most recent */
969 action_list_t *list = &(*thrd_lists)[i];
970 sllnode<ModelAction*>* rit;
971 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
972 ModelAction *act = rit->getVal();
975 * 1) If RMW and it actually read from something, then we
976 * already have all relevant edges, so just skip to next
979 * 2) If RMW and it didn't read from anything, we should
980 * whatever edge we can get to speed up convergence.
982 * 3) If normal write, we need to look at earlier actions, so
983 * continue processing list.
985 if (curr->is_rmw()) {
986 if (curr->get_reads_from() != NULL)
994 /* C++, Section 29.3 statement 7 */
995 if (last_sc_fence_thread_before && act->is_write() &&
996 *act < *last_sc_fence_thread_before) {
997 edgeset.push_back(act);
1002 * Include at most one act per-thread that "happens
1005 if (act->happens_before(curr)) {
1007 * Note: if act is RMW, just add edge:
1009 * The following edge should be handled elsewhere:
1010 * readfrom(act) --mo--> act
1012 if (act->is_write())
1013 edgeset.push_back(act);
1014 else if (act->is_read()) {
1015 //if previous read accessed a null, just keep going
1016 edgeset.push_back(act->get_reads_from());
1022 mo_graph->addEdges(&edgeset, curr);
1027 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1028 * some constraints. This method checks one the following constraint (others
1029 * require compiler support):
1031 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1032 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1034 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1036 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1038 /* Iterate over all threads */
1039 for (i = 0;i < thrd_lists->size();i++) {
1040 const ModelAction *write_after_read = NULL;
1042 /* Iterate over actions in thread, starting from most recent */
1043 action_list_t *list = &(*thrd_lists)[i];
1044 sllnode<ModelAction *>* rit;
1045 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1046 ModelAction *act = rit->getVal();
1048 /* Don't disallow due to act == reader */
1049 if (!reader->happens_before(act) || reader == act)
1051 else if (act->is_write())
1052 write_after_read = act;
1053 else if (act->is_read() && act->get_reads_from() != NULL)
1054 write_after_read = act->get_reads_from();
1057 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1064 * Computes the clock vector that happens before propagates from this write.
1066 * @param rf The action that might be part of a release sequence. Must be a
1068 * @return ClockVector of happens before relation.
1071 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1072 SnapVector<ModelAction *> * processset = NULL;
1073 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1074 ASSERT(rf->is_write());
1075 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1077 if (processset == NULL)
1078 processset = new SnapVector<ModelAction *>();
1079 processset->push_back(rf);
1082 int i = (processset == NULL) ? 0 : processset->size();
1084 ClockVector * vec = NULL;
1086 if (rf->get_rfcv() != NULL) {
1087 vec = rf->get_rfcv();
1088 } else if (rf->is_acquire() && rf->is_release()) {
1090 } else if (rf->is_release() && !rf->is_rmw()) {
1092 } else if (rf->is_release()) {
1093 //have rmw that is release and doesn't have a rfcv
1094 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1097 //operation that isn't release
1098 if (rf->get_last_fence_release()) {
1100 vec = rf->get_last_fence_release()->get_cv();
1102 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1108 rf = (*processset)[i];
1112 if (processset != NULL)
1118 * Performs various bookkeeping operations for the current ModelAction. For
1119 * instance, adds action to the per-object, per-thread action vector and to the
1120 * action trace list of all thread actions.
1122 * @param act is the ModelAction to add.
1124 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1126 int tid = id_to_int(act->get_tid());
1127 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1128 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1129 act->setActionRef(list->add_back(act));
1132 // Update action trace, a total order of all actions
1133 act->setTraceRef(action_trace.add_back(act));
1136 // Update obj_thrd_map, a per location, per thread, order of actions
1137 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1138 if ((int)vec->size() <= tid) {
1139 uint oldsize = vec->size();
1140 vec->resize(priv->next_thread_id);
1141 for(uint i = oldsize;i < priv->next_thread_id;i++)
1142 new (&(*vec)[i]) action_list_t();
1144 if (!canprune && (act->is_read() || act->is_write()))
1145 act->setThrdMapRef((*vec)[tid].add_back(act));
1147 // Update thrd_last_action, the last action taken by each thread
1148 if ((int)thrd_last_action.size() <= tid)
1149 thrd_last_action.resize(get_num_threads());
1150 thrd_last_action[tid] = act;
1152 // Update thrd_last_fence_release, the last release fence taken by each thread
1153 if (act->is_fence() && act->is_release()) {
1154 if ((int)thrd_last_fence_release.size() <= tid)
1155 thrd_last_fence_release.resize(get_num_threads());
1156 thrd_last_fence_release[tid] = act;
1159 if (act->is_wait()) {
1160 void *mutex_loc = (void *) act->get_value();
1161 act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
1165 sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *act) {
1166 sllnode<ModelAction*> * rit = list->end();
1167 modelclock_t next_seq = act->get_seq_number();
1168 if (rit == NULL || (rit->getVal()->get_seq_number() <= next_seq))
1169 return list->add_back(act);
1171 for(;rit != NULL;rit=rit->getPrev()) {
1172 if (rit->getVal()->get_seq_number() <= next_seq) {
1173 return list->insertAfter(rit, act);
1176 return list->add_front(act);
1180 sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1181 sllnode<ModelAction*> * rit = list->end();
1182 modelclock_t next_seq = act->get_seq_number();
1184 act->create_cv(NULL);
1185 return list->add_back(act);
1186 } else if (rit->getVal()->get_seq_number() <= next_seq) {
1187 act->create_cv(rit->getVal());
1188 return list->add_back(act);
1190 for(;rit != NULL;rit=rit->getPrev()) {
1191 if (rit->getVal()->get_seq_number() <= next_seq) {
1192 act->create_cv(rit->getVal());
1193 return list->insertAfter(rit, act);
1196 return list->add_front(act);
1201 * Performs various bookkeeping operations for a normal write. The
1202 * complication is that we are typically inserting a normal write
1203 * lazily, so we need to insert it into the middle of lists.
1205 * @param act is the ModelAction to add.
1208 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1210 int tid = id_to_int(act->get_tid());
1211 act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
1213 // Update obj_thrd_map, a per location, per thread, order of actions
1214 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1215 if (tid >= (int)vec->size()) {
1216 uint oldsize =vec->size();
1217 vec->resize(priv->next_thread_id);
1218 for(uint i=oldsize;i<priv->next_thread_id;i++)
1219 new (&(*vec)[i]) action_list_t();
1221 act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
1223 ModelAction * lastact = thrd_last_action[tid];
1224 // Update thrd_last_action, the last action taken by each thrad
1225 if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
1226 thrd_last_action[tid] = act;
1230 void ModelExecution::add_write_to_lists(ModelAction *write) {
1231 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1232 int tid = id_to_int(write->get_tid());
1233 if (tid >= (int)vec->size()) {
1234 uint oldsize =vec->size();
1235 vec->resize(priv->next_thread_id);
1236 for(uint i=oldsize;i<priv->next_thread_id;i++)
1237 new (&(*vec)[i]) action_list_t();
1239 write->setActionRef((*vec)[tid].add_back(write));
1243 * @brief Get the last action performed by a particular Thread
1244 * @param tid The thread ID of the Thread in question
1245 * @return The last action in the thread
1247 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1249 int threadid = id_to_int(tid);
1250 if (threadid < (int)thrd_last_action.size())
1251 return thrd_last_action[id_to_int(tid)];
1257 * @brief Get the last fence release performed by a particular Thread
1258 * @param tid The thread ID of the Thread in question
1259 * @return The last fence release in the thread, if one exists; NULL otherwise
1261 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1263 int threadid = id_to_int(tid);
1264 if (threadid < (int)thrd_last_fence_release.size())
1265 return thrd_last_fence_release[id_to_int(tid)];
1271 * Gets the last memory_order_seq_cst write (in the total global sequence)
1272 * performed on a particular object (i.e., memory location), not including the
1274 * @param curr The current ModelAction; also denotes the object location to
1276 * @return The last seq_cst write
1278 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1280 void *location = curr->get_location();
1281 return obj_last_sc_map.get(location);
1285 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1286 * performed in a particular thread, prior to a particular fence.
1287 * @param tid The ID of the thread to check
1288 * @param before_fence The fence from which to begin the search; if NULL, then
1289 * search for the most recent fence in the thread.
1290 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1292 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1294 /* All fences should have location FENCE_LOCATION */
1295 action_list_t *list = obj_map.get(FENCE_LOCATION);
1300 sllnode<ModelAction*>* rit = list->end();
1303 for (;rit != NULL;rit=rit->getPrev())
1304 if (rit->getVal() == before_fence)
1307 ASSERT(rit->getVal() == before_fence);
1311 for (;rit != NULL;rit=rit->getPrev()) {
1312 ModelAction *act = rit->getVal();
1313 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1320 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1321 * location). This function identifies the mutex according to the current
1322 * action, which is presumed to perform on the same mutex.
1323 * @param curr The current ModelAction; also denotes the object location to
1325 * @return The last unlock operation
1327 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1329 void *location = curr->get_location();
1331 action_list_t *list = obj_map.get(location);
1335 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1336 sllnode<ModelAction*>* rit;
1337 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1338 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1339 return rit->getVal();
1343 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1345 ModelAction *parent = get_last_action(tid);
1347 parent = get_thread(tid)->get_creation();
1352 * Returns the clock vector for a given thread.
1353 * @param tid The thread whose clock vector we want
1354 * @return Desired clock vector
1356 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1358 ModelAction *firstaction=get_parent_action(tid);
1359 return firstaction != NULL ? firstaction->get_cv() : NULL;
1362 bool valequals(uint64_t val1, uint64_t val2, int size) {
1365 return ((uint8_t)val1) == ((uint8_t)val2);
1367 return ((uint16_t)val1) == ((uint16_t)val2);
1369 return ((uint32_t)val1) == ((uint32_t)val2);
1379 * Build up an initial set of all past writes that this 'read' action may read
1380 * from, as well as any previously-observed future values that must still be valid.
1382 * @param curr is the current ModelAction that we are exploring; it must be a
1385 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1387 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1389 ASSERT(curr->is_read());
1391 ModelAction *last_sc_write = NULL;
1393 if (curr->is_seqcst())
1394 last_sc_write = get_last_seq_cst_write(curr);
1396 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1398 /* Iterate over all threads */
1399 if (thrd_lists != NULL)
1400 for (i = 0;i < thrd_lists->size();i++) {
1401 /* Iterate over actions in thread, starting from most recent */
1402 action_list_t *list = &(*thrd_lists)[i];
1403 sllnode<ModelAction *> * rit;
1404 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1405 ModelAction *act = rit->getVal();
1410 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1411 bool allow_read = true;
1413 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1416 /* Need to check whether we will have two RMW reading from the same value */
1417 if (curr->is_rmwr()) {
1418 /* It is okay if we have a failing CAS */
1419 if (!curr->is_rmwrcas() ||
1420 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1421 //Need to make sure we aren't the second RMW
1422 CycleNode * node = mo_graph->getNode_noCreate(act);
1423 if (node != NULL && node->getRMW() != NULL) {
1424 //we are the second RMW
1431 /* Only add feasible reads */
1432 rf_set->push_back(act);
1435 /* Include at most one act per-thread that "happens before" curr */
1436 if (act->happens_before(curr))
1441 if (DBG_ENABLED()) {
1442 model_print("Reached read action:\n");
1444 model_print("End printing read_from_past\n");
1449 static void print_list(action_list_t *list)
1451 sllnode<ModelAction*> *it;
1453 model_print("------------------------------------------------------------------------------------\n");
1454 model_print("# t Action type MO Location Value Rf CV\n");
1455 model_print("------------------------------------------------------------------------------------\n");
1457 unsigned int hash = 0;
1459 for (it = list->begin();it != NULL;it=it->getNext()) {
1460 const ModelAction *act = it->getVal();
1461 if (act->get_seq_number() > 0)
1463 hash = hash^(hash<<3)^(it->getVal()->hash());
1465 model_print("HASH %u\n", hash);
1466 model_print("------------------------------------------------------------------------------------\n");
1469 #if SUPPORT_MOD_ORDER_DUMP
1470 void ModelExecution::dumpGraph(char *filename)
1473 sprintf(buffer, "%s.dot", filename);
1474 FILE *file = fopen(buffer, "w");
1475 fprintf(file, "digraph %s {\n", filename);
1476 mo_graph->dumpNodes(file);
1477 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1479 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1480 ModelAction *act = it->getVal();
1481 if (act->is_read()) {
1482 mo_graph->dot_print_node(file, act);
1483 mo_graph->dot_print_edge(file,
1484 act->get_reads_from(),
1486 "label=\"rf\", color=red, weight=2");
1488 if (thread_array[act->get_tid()]) {
1489 mo_graph->dot_print_edge(file,
1490 thread_array[id_to_int(act->get_tid())],
1492 "label=\"sb\", color=blue, weight=400");
1495 thread_array[act->get_tid()] = act;
1497 fprintf(file, "}\n");
1498 model_free(thread_array);
1503 /** @brief Prints an execution trace summary. */
1504 void ModelExecution::print_summary()
1506 #if SUPPORT_MOD_ORDER_DUMP
1507 char buffername[100];
1508 sprintf(buffername, "exec%04u", get_execution_number());
1509 mo_graph->dumpGraphToFile(buffername);
1510 sprintf(buffername, "graph%04u", get_execution_number());
1511 dumpGraph(buffername);
1514 model_print("Execution trace %d:", get_execution_number());
1515 if (scheduler->all_threads_sleeping())
1516 model_print(" SLEEP-SET REDUNDANT");
1517 if (have_bug_reports())
1518 model_print(" DETECTED BUG(S)");
1522 print_list(&action_trace);
1528 * Add a Thread to the system for the first time. Should only be called once
1530 * @param t The Thread to add
1532 void ModelExecution::add_thread(Thread *t)
1534 unsigned int i = id_to_int(t->get_id());
1535 if (i >= thread_map.size())
1536 thread_map.resize(i + 1);
1538 if (!t->is_model_thread())
1539 scheduler->add_thread(t);
1543 * @brief Get a Thread reference by its ID
1544 * @param tid The Thread's ID
1545 * @return A Thread reference
1547 Thread * ModelExecution::get_thread(thread_id_t tid) const
1549 unsigned int i = id_to_int(tid);
1550 if (i < thread_map.size())
1551 return thread_map[i];
1556 * @brief Get a reference to the Thread in which a ModelAction was executed
1557 * @param act The ModelAction
1558 * @return A Thread reference
1560 Thread * ModelExecution::get_thread(const ModelAction *act) const
1562 return get_thread(act->get_tid());
1566 * @brief Get a Thread reference by its pthread ID
1567 * @param index The pthread's ID
1568 * @return A Thread reference
1570 Thread * ModelExecution::get_pthread(pthread_t pid) {
1576 uint32_t thread_id = x.v;
1577 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1582 * @brief Check if a Thread is currently enabled
1583 * @param t The Thread to check
1584 * @return True if the Thread is currently enabled
1586 bool ModelExecution::is_enabled(Thread *t) const
1588 return scheduler->is_enabled(t);
1592 * @brief Check if a Thread is currently enabled
1593 * @param tid The ID of the Thread to check
1594 * @return True if the Thread is currently enabled
1596 bool ModelExecution::is_enabled(thread_id_t tid) const
1598 return scheduler->is_enabled(tid);
1602 * @brief Select the next thread to execute based on the curren action
1604 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1605 * actions should be followed by the execution of their child thread. In either
1606 * case, the current action should determine the next thread schedule.
1608 * @param curr The current action
1609 * @return The next thread to run, if the current action will determine this
1610 * selection; otherwise NULL
1612 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1614 /* Do not split atomic RMW */
1615 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1616 return get_thread(curr);
1617 /* Follow CREATE with the created thread */
1618 /* which is not needed, because model.cc takes care of this */
1619 if (curr->get_type() == THREAD_CREATE)
1620 return curr->get_thread_operand();
1621 if (curr->get_type() == PTHREAD_CREATE) {
1622 return curr->get_thread_operand();
1627 /** @param act A read atomic action */
1628 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1630 ASSERT(act->is_read());
1632 // Actions paused by fuzzer have their sequence number reset to 0
1633 return act->get_seq_number() == 0;
1637 * Takes the next step in the execution, if possible.
1638 * @param curr The current step to take
1639 * @return Returns the next Thread to run, if any; NULL if this execution
1642 Thread * ModelExecution::take_step(ModelAction *curr)
1644 Thread *curr_thrd = get_thread(curr);
1645 ASSERT(curr_thrd->get_state() == THREAD_READY);
1647 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1648 curr = check_current_action(curr);
1651 /* Process this action in ModelHistory for records */
1653 model->get_history()->process_action( curr, curr->get_tid() );
1655 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1656 scheduler->remove_thread(curr_thrd);
1658 return action_select_next_thread(curr);
1661 /** This method removes references to an Action before we delete it. */
1663 void ModelExecution::removeAction(ModelAction *act) {
1665 sllnode<ModelAction *> * listref = act->getTraceRef();
1666 if (listref != NULL) {
1667 action_trace.erase(listref);
1671 sllnode<ModelAction *> * listref = act->getThrdMapRef();
1672 if (listref != NULL) {
1673 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1674 (*vec)[act->get_tid()].erase(listref);
1677 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1678 sllnode<ModelAction *> * listref = act->getActionRef();
1679 if (listref != NULL) {
1680 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1681 list->erase(listref);
1683 } else if (act->is_wait()) {
1684 sllnode<ModelAction *> * listref = act->getActionRef();
1685 if (listref != NULL) {
1686 void *mutex_loc = (void *) act->get_value();
1687 get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
1689 } else if (act->is_free()) {
1690 sllnode<ModelAction *> * listref = act->getActionRef();
1691 if (listref != NULL) {
1692 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1693 (*vec)[act->get_tid()].erase(listref);
1695 //Clear it from last_sc_map
1696 if (obj_last_sc_map.get(act->get_location()) == act) {
1697 obj_last_sc_map.remove(act->get_location());
1700 //Remove from Cyclegraph
1701 mo_graph->freeAction(act);
1705 /** Computes clock vector that all running threads have already synchronized to. */
1707 ClockVector * ModelExecution::computeMinimalCV() {
1708 ClockVector *cvmin = NULL;
1709 //Thread 0 isn't a real thread, so skip it..
1710 for(unsigned int i = 1;i < thread_map.size();i++) {
1711 Thread * t = thread_map[i];
1712 if (t->get_state() == THREAD_COMPLETED)
1714 thread_id_t tid = int_to_id(i);
1715 ClockVector * cv = get_cv(tid);
1717 cvmin = new ClockVector(cv, NULL);
1719 cvmin->minmerge(cv);
1725 /** 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 */
1727 void ModelExecution::fixupLastAct(ModelAction *act) {
1728 ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, get_thread(act->get_tid()));
1729 newact->set_seq_number(get_next_seq_num());
1730 newact->create_cv(act);
1731 newact->set_last_fence_release(act->get_last_fence_release());
1732 add_action_to_lists(newact, false);
1735 /** Compute which actions to free. */
1737 void ModelExecution::collectActions() {
1738 //Compute minimal clock vector for all live threads
1739 ClockVector *cvmin = computeMinimalCV();
1740 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1741 modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1743 //Next walk action trace... When we hit an action, see if it is
1744 //invisible (e.g., earlier than the first before the minimum
1745 //clock for the thread... if so erase it and all previous
1746 //actions in cyclegraph
1747 sllnode<ModelAction*> * it;
1748 for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1749 ModelAction *act = it->getVal();
1750 modelclock_t actseq = act->get_seq_number();
1752 //See if we are done
1753 if (actseq > maxtofree)
1756 thread_id_t act_tid = act->get_tid();
1757 modelclock_t tid_clock = cvmin->getClock(act_tid);
1759 //Free if it is invisible or we have set a flag to remove visible actions.
1760 if (actseq <= tid_clock || params->removevisible) {
1761 ModelAction * write;
1762 if (act->is_write()) {
1764 } else if (act->is_read()) {
1765 write = act->get_reads_from();
1769 //Mark everything earlier in MO graph to be freed
1770 CycleNode * cn = mo_graph->getNode_noCreate(write);
1772 queue->push_back(cn);
1773 while(!queue->empty()) {
1774 CycleNode * node = queue->back();
1776 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1777 CycleNode * prevnode = node->getInEdge(i);
1778 ModelAction * prevact = prevnode->getAction();
1779 if (prevact->get_type() != READY_FREE) {
1780 prevact->set_free();
1781 queue->push_back(prevnode);
1789 //We may need to remove read actions in the window we don't delete to preserve correctness.
1791 for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1792 ModelAction *act = it2->getVal();
1793 //Do iteration early in case we delete the act
1795 bool islastact = false;
1796 ModelAction *lastact = get_last_action(act->get_tid());
1797 if (act == lastact) {
1798 Thread * th = get_thread(act);
1799 islastact = !th->is_complete();
1802 if (act->is_read()) {
1803 if (act->get_reads_from()->is_free()) {
1804 if (act->is_rmw()) {
1805 //Weaken a RMW from a freed store to a write
1806 act->set_type(ATOMIC_WRITE);
1817 //If we don't delete the action, we should remove references to release fences
1819 const ModelAction *rel_fence =act->get_last_fence_release();
1820 if (rel_fence != NULL) {
1821 modelclock_t relfenceseq = rel_fence->get_seq_number();
1822 thread_id_t relfence_tid = rel_fence->get_tid();
1823 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1824 //Remove references to irrelevant release fences
1825 if (relfenceseq <= tid_clock)
1826 act->set_last_fence_release(NULL);
1829 //Now we are in the window of old actions that we remove if possible
1830 for (;it != NULL;) {
1831 ModelAction *act = it->getVal();
1832 //Do iteration early since we may delete node...
1834 bool islastact = false;
1835 ModelAction *lastact = get_last_action(act->get_tid());
1836 if (act == lastact) {
1837 Thread * th = get_thread(act);
1838 islastact = !th->is_complete();
1841 if (act->is_read()) {
1842 if (act->get_reads_from()->is_free()) {
1843 if (act->is_rmw()) {
1844 act->set_type(ATOMIC_WRITE);
1854 } else if (act->is_free()) {
1861 } else if (act->is_write()) {
1862 //Do nothing with write that hasn't been marked to be freed
1863 } else if (islastact) {
1864 //Keep the last action for non-read/write actions
1865 } else if (act->is_fence()) {
1866 //Note that acquire fences can always be safely
1867 //removed, but could incur extra overheads in
1868 //traversals. Removing them before the cvmin seems
1869 //like a good compromise.
1871 //Release fences before the cvmin don't do anything
1872 //because everyone has already synchronized.
1874 //Sequentially fences before cvmin are redundant
1875 //because happens-before will enforce same
1878 modelclock_t actseq = act->get_seq_number();
1879 thread_id_t act_tid = act->get_tid();
1880 modelclock_t tid_clock = cvmin->getClock(act_tid);
1881 if (actseq <= tid_clock) {
1887 //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1888 //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1889 //need to keep most recent unlock/wait for each lock
1890 if(act->is_unlock() || act->is_wait()) {
1891 ModelAction * lastlock = get_last_unlock(act);
1892 if (lastlock != act) {
1897 } else if (act->is_create()) {
1898 if (act->get_thread_operand()->is_complete()) {
1909 //If we don't delete the action, we should remove references to release fences
1910 const ModelAction *rel_fence =act->get_last_fence_release();
1911 if (rel_fence != NULL) {
1912 modelclock_t relfenceseq = rel_fence->get_seq_number();
1913 thread_id_t relfence_tid = rel_fence->get_tid();
1914 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1915 //Remove references to irrelevant release fences
1916 if (relfenceseq <= tid_clock)
1917 act->set_last_fence_release(NULL);
1927 Fuzzer * ModelExecution::getFuzzer() {