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