11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
34 ~model_snapshot_members() {
35 for (unsigned int i = 0;i < bugs.size();i++)
40 unsigned int next_thread_id;
41 modelclock_t used_sequence_numbers;
42 SnapVector<bug_message *> bugs;
43 /** @brief Incorrectly-ordered synchronization was made */
49 /** @brief Constructor */
50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
54 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
66 thrd_last_fence_release(),
67 priv(new struct model_snapshot_members ()),
68 mo_graph(new CycleGraph()),
70 fuzzer(new NewFuzzer()),
76 /* Initialize a model-checker thread, for special ModelActions */
77 model_thread = new Thread(get_next_id());
78 add_thread(model_thread);
79 fuzzer->register_engine(m, this);
80 scheduler->register_engine(this);
82 pthread_key_create(&pthreadkey, tlsdestructor);
86 /** @brief Destructor */
87 ModelExecution::~ModelExecution()
89 for (unsigned int i = 0;i < get_num_threads();i++)
90 delete get_thread(int_to_id(i));
96 int ModelExecution::get_execution_number() const
98 return model->get_execution_number();
101 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
103 action_list_t *tmp = hash->get(ptr);
105 tmp = new action_list_t();
111 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
113 SnapVector<action_list_t> *tmp = hash->get(ptr);
115 tmp = new SnapVector<action_list_t>();
121 /** @return a thread ID for a new Thread */
122 thread_id_t ModelExecution::get_next_id()
124 return priv->next_thread_id++;
127 /** @return the number of user threads created during this execution */
128 unsigned int ModelExecution::get_num_threads() const
130 return priv->next_thread_id;
133 /** @return a sequence number for a new ModelAction */
134 modelclock_t ModelExecution::get_next_seq_num()
136 return ++priv->used_sequence_numbers;
139 /** @return a sequence number for a new ModelAction */
140 modelclock_t ModelExecution::get_curr_seq_num()
142 return priv->used_sequence_numbers;
145 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
146 void ModelExecution::restore_last_seq_num()
148 priv->used_sequence_numbers--;
152 * @brief Should the current action wake up a given thread?
154 * @param curr The current action
155 * @param thread The thread that we might wake up
156 * @return True, if we should wake up the sleeping thread; false otherwise
158 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
160 const ModelAction *asleep = thread->get_pending();
161 /* Don't allow partial RMW to wake anyone up */
164 /* Synchronizing actions may have been backtracked */
165 if (asleep->could_synchronize_with(curr))
167 /* All acquire/release fences and fence-acquire/store-release */
168 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
170 /* Fence-release + store can awake load-acquire on the same location */
171 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
172 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
173 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
176 /* The sleep is literally sleeping */
177 if (asleep->is_sleep()) {
178 if (fuzzer->shouldWake(asleep))
185 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
187 for (unsigned int i = 0;i < get_num_threads();i++) {
188 Thread *thr = get_thread(int_to_id(i));
189 if (scheduler->is_sleep_set(thr)) {
190 if (should_wake_up(curr, thr)) {
191 /* Remove this thread from sleep set */
192 scheduler->remove_sleep(thr);
193 if (thr->get_pending()->is_sleep())
194 thr->set_wakeup_state(true);
200 void ModelExecution::assert_bug(const char *msg)
202 priv->bugs.push_back(new bug_message(msg));
206 /** @return True, if any bugs have been reported for this execution */
207 bool ModelExecution::have_bug_reports() const
209 return priv->bugs.size() != 0;
212 SnapVector<bug_message *> * ModelExecution::get_bugs() const
218 * Check whether the current trace has triggered an assertion which should halt
221 * @return True, if the execution should be aborted; false otherwise
223 bool ModelExecution::has_asserted() const
225 return priv->asserted;
229 * Trigger a trace assertion which should cause this execution to be halted.
230 * This can be due to a detected bug or due to an infeasibility that should
233 void ModelExecution::set_assert()
235 priv->asserted = true;
239 * Check if we are in a deadlock. Should only be called at the end of an
240 * execution, although it should not give false positives in the middle of an
241 * execution (there should be some ENABLED thread).
243 * @return True if program is in a deadlock; false otherwise
245 bool ModelExecution::is_deadlocked() const
247 bool blocking_threads = false;
248 for (unsigned int i = 0;i < get_num_threads();i++) {
249 thread_id_t tid = int_to_id(i);
252 Thread *t = get_thread(tid);
253 if (!t->is_model_thread() && t->get_pending())
254 blocking_threads = true;
256 return blocking_threads;
260 * Check if this is a complete execution. That is, have all thread completed
261 * execution (rather than exiting because sleep sets have forced a redundant
264 * @return True if the execution is complete.
266 bool ModelExecution::is_complete_execution() const
268 for (unsigned int i = 0;i < get_num_threads();i++)
269 if (is_enabled(int_to_id(i)))
274 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
275 uint64_t value = *((const uint64_t *) location);
276 modelclock_t storeclock;
277 thread_id_t storethread;
278 getStoreThreadAndClock(location, &storethread, &storeclock);
279 setAtomicStoreFlag(location);
280 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
281 act->set_seq_number(storeclock);
282 add_normal_write_to_lists(act);
283 add_write_to_lists(act);
284 w_modification_order(act);
286 model->get_history()->process_action(act, act->get_tid());
292 * Processes a read model action.
293 * @param curr is the read model action to process.
294 * @param rf_set is the set of model actions we can possibly read from
295 * @return True if the read can be pruned from the thread map list.
297 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
299 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
300 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
301 if (hasnonatomicstore) {
302 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
303 rf_set->push_back(nonatomicstore);
306 // Remove writes that violate read modification order
309 while (i < rf_set->size()) {
310 ModelAction * rf = (*rf_set)[i];
311 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
312 (*rf_set)[i] = rf_set->back();
319 int index = fuzzer->selectWrite(curr, rf_set);
321 ModelAction *rf = (*rf_set)[index];
324 bool canprune = false;
325 if (r_modification_order(curr, rf, priorset, &canprune)) {
326 for(unsigned int i=0;i<priorset->size();i++) {
327 mo_graph->addEdge((*priorset)[i], rf);
330 get_thread(curr)->set_return_value(curr->get_return_value());
332 //Update acquire fence clock vector
333 ClockVector * hbcv = get_hb_from_write(curr->get_reads_from());
335 get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
336 return canprune && (curr->get_type() == ATOMIC_READ);
339 (*rf_set)[index] = rf_set->back();
345 * Processes a lock, trylock, or unlock model action. @param curr is
346 * the read model action to process.
348 * The try lock operation checks whether the lock is taken. If not,
349 * it falls to the normal lock operation case. If so, it returns
352 * The lock operation has already been checked that it is enabled, so
353 * it just grabs the lock and synchronizes with the previous unlock.
355 * The unlock operation has to re-enable all of the threads that are
356 * waiting on the lock.
358 * @return True if synchronization was updated; false otherwise
360 bool ModelExecution::process_mutex(ModelAction *curr)
362 cdsc::mutex *mutex = curr->get_mutex();
363 struct cdsc::mutex_state *state = NULL;
366 state = mutex->get_state();
368 switch (curr->get_type()) {
369 case ATOMIC_TRYLOCK: {
370 bool success = !state->locked;
371 curr->set_try_lock(success);
373 get_thread(curr)->set_return_value(0);
376 get_thread(curr)->set_return_value(1);
378 //otherwise fall into the lock case
380 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
381 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
382 // assert_bug("Lock access before initialization");
383 state->locked = get_thread(curr);
384 ModelAction *unlock = get_last_unlock(curr);
385 //synchronize with the previous unlock statement
386 if (unlock != NULL) {
387 synchronize(unlock, curr);
393 //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
394 if (fuzzer->shouldWait(curr)) {
395 /* wake up the other threads */
396 for (unsigned int i = 0;i < get_num_threads();i++) {
397 Thread *t = get_thread(int_to_id(i));
398 Thread *curr_thrd = get_thread(curr);
399 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
403 /* unlock the lock - after checking who was waiting on it */
404 state->locked = NULL;
406 /* disable this thread */
407 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr);
408 scheduler->sleep(get_thread(curr));
413 case ATOMIC_TIMEDWAIT:
414 case ATOMIC_UNLOCK: {
415 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
416 //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
417 //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
418 //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
419 //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
420 //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
421 //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
422 //MUST EVENMTUALLY RELEASE...
424 /* wake up the other threads */
425 for (unsigned int i = 0;i < get_num_threads();i++) {
426 Thread *t = get_thread(int_to_id(i));
427 Thread *curr_thrd = get_thread(curr);
428 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
432 /* unlock the lock - after checking who was waiting on it */
433 state->locked = NULL;
436 case ATOMIC_NOTIFY_ALL: {
437 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
438 //activate all the waiting threads
439 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
440 scheduler->wake(get_thread(rit->getVal()));
445 case ATOMIC_NOTIFY_ONE: {
446 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
447 if (waiters->size() != 0) {
448 Thread * thread = fuzzer->selectNotify(waiters);
449 scheduler->wake(thread);
461 * Process a write ModelAction
462 * @param curr The ModelAction to process
463 * @return True if the mo_graph was updated or promises were resolved
465 void ModelExecution::process_write(ModelAction *curr)
467 w_modification_order(curr);
468 get_thread(curr)->set_return_value(VALUE_NONE);
472 * Process a fence ModelAction
473 * @param curr The ModelAction to process
474 * @return True if synchronization was updated
476 void ModelExecution::process_fence(ModelAction *curr)
479 * fence-relaxed: no-op
480 * fence-release: only log the occurence (not in this function), for
481 * use in later synchronization
482 * fence-acquire (this function): search for hypothetical release
484 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
486 if (curr->is_acquire()) {
487 curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
492 * @brief Process the current action for thread-related activity
494 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
495 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
496 * synchronization, etc. This function is a no-op for non-THREAD actions
497 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
499 * @param curr The current action
500 * @return True if synchronization was updated or a thread completed
502 void ModelExecution::process_thread_action(ModelAction *curr)
504 switch (curr->get_type()) {
505 case THREAD_CREATE: {
506 thrd_t *thrd = (thrd_t *)curr->get_location();
507 struct thread_params *params = (struct thread_params *)curr->get_value();
508 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
509 curr->set_thread_operand(th);
511 th->set_creation(curr);
514 case PTHREAD_CREATE: {
515 (*(uint32_t *)curr->get_location()) = pthread_counter++;
517 struct pthread_params *params = (struct pthread_params *)curr->get_value();
518 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
519 curr->set_thread_operand(th);
521 th->set_creation(curr);
523 if ( pthread_map.size() < pthread_counter )
524 pthread_map.resize( pthread_counter );
525 pthread_map[ pthread_counter-1 ] = th;
530 Thread *blocking = curr->get_thread_operand();
531 ModelAction *act = get_last_action(blocking->get_id());
532 synchronize(act, curr);
536 Thread *blocking = curr->get_thread_operand();
537 ModelAction *act = get_last_action(blocking->get_id());
538 synchronize(act, curr);
539 break; // WL: to be add (modified)
542 case THREADONLY_FINISH:
543 case THREAD_FINISH: {
544 Thread *th = get_thread(curr);
545 if (curr->get_type() == THREAD_FINISH &&
546 th == model->getInitThread()) {
552 /* Wake up any joining threads */
553 for (unsigned int i = 0;i < get_num_threads();i++) {
554 Thread *waiting = get_thread(int_to_id(i));
555 if (waiting->waiting_on() == th &&
556 waiting->get_pending()->is_thread_join())
557 scheduler->wake(waiting);
566 Thread *th = get_thread(curr);
567 th->set_pending(curr);
568 scheduler->add_sleep(th);
577 * Initialize the current action by performing one or more of the following
578 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
579 * manipulating backtracking sets, allocating and
580 * initializing clock vectors, and computing the promises to fulfill.
582 * @param curr The current action, as passed from the user context; may be
583 * freed/invalidated after the execution of this function, with a different
584 * action "returned" its place (pass-by-reference)
585 * @return True if curr is a newly-explored action; false otherwise
587 bool ModelExecution::initialize_curr_action(ModelAction **curr)
589 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
590 ModelAction *newcurr = process_rmw(*curr);
596 ModelAction *newcurr = *curr;
598 newcurr->set_seq_number(get_next_seq_num());
599 /* Always compute new clock vector */
600 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
602 /* Assign most recent release fence */
603 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
605 return true; /* This was a new ModelAction */
610 * @brief Establish reads-from relation between two actions
612 * Perform basic operations involved with establishing a concrete rf relation,
613 * including setting the ModelAction data and checking for release sequences.
615 * @param act The action that is reading (must be a read)
616 * @param rf The action from which we are reading (must be a write)
618 * @return True if this read established synchronization
621 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
624 ASSERT(rf->is_write());
626 act->set_read_from(rf);
627 if (act->is_acquire()) {
628 ClockVector *cv = get_hb_from_write(rf);
631 act->get_cv()->merge(cv);
636 * @brief Synchronizes two actions
638 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
639 * This function performs the synchronization as well as providing other hooks
640 * for other checks along with synchronization.
642 * @param first The left-hand side of the synchronizes-with relation
643 * @param second The right-hand side of the synchronizes-with relation
644 * @return True if the synchronization was successful (i.e., was consistent
645 * with the execution order); false otherwise
647 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
649 if (*second < *first) {
650 ASSERT(0); //This should not happend
653 return second->synchronize_with(first);
657 * @brief Check whether a model action is enabled.
659 * Checks whether an operation would be successful (i.e., is a lock already
660 * locked, or is the joined thread already complete).
662 * For yield-blocking, yields are never enabled.
664 * @param curr is the ModelAction to check whether it is enabled.
665 * @return a bool that indicates whether the action is enabled.
667 bool ModelExecution::check_action_enabled(ModelAction *curr) {
668 if (curr->is_lock()) {
669 cdsc::mutex *lock = curr->get_mutex();
670 struct cdsc::mutex_state *state = lock->get_state();
673 } else if (curr->is_thread_join()) {
674 Thread *blocking = curr->get_thread_operand();
675 if (!blocking->is_complete()) {
678 } else if (curr->is_sleep()) {
679 if (!fuzzer->shouldSleep(curr))
687 * This is the heart of the model checker routine. It performs model-checking
688 * actions corresponding to a given "current action." Among other processes, it
689 * calculates reads-from relationships, updates synchronization clock vectors,
690 * forms a memory_order constraints graph, and handles replay/backtrack
691 * execution when running permutations of previously-observed executions.
693 * @param curr The current action to process
694 * @return The ModelAction that is actually executed; may be different than
697 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
700 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
701 bool newly_explored = initialize_curr_action(&curr);
705 wake_up_sleeping_actions(curr);
707 SnapVector<ModelAction *> * rf_set = NULL;
708 /* Build may_read_from set for newly-created actions */
709 if (newly_explored && curr->is_read())
710 rf_set = build_may_read_from(curr);
712 bool canprune = false;
714 if (curr->is_read() && !second_part_of_rmw) {
715 canprune = process_read(curr, rf_set);
718 ASSERT(rf_set == NULL);
720 /* Add the action to lists */
721 if (!second_part_of_rmw)
722 add_action_to_lists(curr, canprune);
724 if (curr->is_write())
725 add_write_to_lists(curr);
727 process_thread_action(curr);
729 if (curr->is_write())
732 if (curr->is_fence())
735 if (curr->is_mutex_op())
741 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
742 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
743 ModelAction *lastread = get_last_action(act->get_tid());
744 lastread->process_rmw(act);
746 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
752 * @brief Updates the mo_graph with the constraints imposed from the current
755 * Basic idea is the following: Go through each other thread and find
756 * the last action that happened before our read. Two cases:
758 * -# The action is a write: that write must either occur before
759 * the write we read from or be the write we read from.
760 * -# The action is a read: the write that that action read from
761 * must occur before the write we read from or be the same write.
763 * @param curr The current action. Must be a read.
764 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
765 * @param check_only If true, then only check whether the current action satisfies
766 * read modification order or not, without modifiying priorset and canprune.
768 * @return True if modification order edges were added; false otherwise
771 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
772 SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
774 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
775 ASSERT(curr->is_read());
777 /* Last SC fence in the current thread */
778 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
780 int tid = curr->get_tid();
782 /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
783 if ((int)thrd_lists->size() <= tid) {
784 uint oldsize = thrd_lists->size();
785 thrd_lists->resize(priv->next_thread_id);
786 for(uint i = oldsize;i < priv->next_thread_id;i++)
787 new (&(*thrd_lists)[i]) action_list_t();
790 ModelAction *prev_same_thread = NULL;
791 /* Iterate over all threads */
792 for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
793 /* Last SC fence in thread tid */
794 ModelAction *last_sc_fence_thread_local = NULL;
796 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
798 /* Last SC fence in thread tid, before last SC fence in current thread */
799 ModelAction *last_sc_fence_thread_before = NULL;
800 if (last_sc_fence_local)
801 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
803 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
804 if (prev_same_thread != NULL &&
805 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
806 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
810 /* Iterate over actions in thread, starting from most recent */
811 action_list_t *list = &(*thrd_lists)[tid];
812 sllnode<ModelAction *> * rit;
813 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
814 ModelAction *act = rit->getVal();
819 /* Don't want to add reflexive edges on 'rf' */
820 if (act->equals(rf)) {
821 if (act->happens_before(curr))
827 if (act->is_write()) {
828 /* C++, Section 29.3 statement 5 */
829 if (curr->is_seqcst() && last_sc_fence_thread_local &&
830 *act < *last_sc_fence_thread_local) {
831 if (mo_graph->checkReachable(rf, act))
834 priorset->push_back(act);
837 /* C++, Section 29.3 statement 4 */
838 else if (act->is_seqcst() && last_sc_fence_local &&
839 *act < *last_sc_fence_local) {
840 if (mo_graph->checkReachable(rf, act))
843 priorset->push_back(act);
846 /* C++, Section 29.3 statement 6 */
847 else if (last_sc_fence_thread_before &&
848 *act < *last_sc_fence_thread_before) {
849 if (mo_graph->checkReachable(rf, act))
852 priorset->push_back(act);
858 * Include at most one act per-thread that "happens
861 if (act->happens_before(curr)) {
863 if (last_sc_fence_local == NULL ||
864 (*last_sc_fence_local < *act)) {
865 prev_same_thread = act;
868 if (act->is_write()) {
869 if (mo_graph->checkReachable(rf, act))
872 priorset->push_back(act);
874 ModelAction *prevrf = act->get_reads_from();
875 if (!prevrf->equals(rf)) {
876 if (mo_graph->checkReachable(rf, prevrf))
879 priorset->push_back(prevrf);
881 if (act->get_tid() == curr->get_tid()) {
882 //Can prune curr from obj list
896 * Updates the mo_graph with the constraints imposed from the current write.
898 * Basic idea is the following: Go through each other thread and find
899 * the lastest action that happened before our write. Two cases:
901 * (1) The action is a write => that write must occur before
904 * (2) The action is a read => the write that that action read from
905 * must occur before the current write.
907 * This method also handles two other issues:
909 * (I) Sequential Consistency: Making sure that if the current write is
910 * seq_cst, that it occurs after the previous seq_cst write.
912 * (II) Sending the write back to non-synchronizing reads.
914 * @param curr The current action. Must be a write.
915 * @param send_fv A vector for stashing reads to which we may pass our future
916 * value. If NULL, then don't record any future values.
917 * @return True if modification order edges were added; false otherwise
919 void ModelExecution::w_modification_order(ModelAction *curr)
921 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
923 ASSERT(curr->is_write());
925 SnapList<ModelAction *> edgeset;
927 if (curr->is_seqcst()) {
928 /* We have to at least see the last sequentially consistent write,
929 so we are initialized. */
930 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
931 if (last_seq_cst != NULL) {
932 edgeset.push_back(last_seq_cst);
934 //update map for next query
935 obj_last_sc_map.put(curr->get_location(), curr);
938 /* Last SC fence in the current thread */
939 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
941 /* Iterate over all threads */
942 for (i = 0;i < thrd_lists->size();i++) {
943 /* Last SC fence in thread i, before last SC fence in current thread */
944 ModelAction *last_sc_fence_thread_before = NULL;
945 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
946 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
948 /* Iterate over actions in thread, starting from most recent */
949 action_list_t *list = &(*thrd_lists)[i];
950 sllnode<ModelAction*>* rit;
951 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
952 ModelAction *act = rit->getVal();
955 * 1) If RMW and it actually read from something, then we
956 * already have all relevant edges, so just skip to next
959 * 2) If RMW and it didn't read from anything, we should
960 * whatever edge we can get to speed up convergence.
962 * 3) If normal write, we need to look at earlier actions, so
963 * continue processing list.
965 if (curr->is_rmw()) {
966 if (curr->get_reads_from() != NULL)
974 /* C++, Section 29.3 statement 7 */
975 if (last_sc_fence_thread_before && act->is_write() &&
976 *act < *last_sc_fence_thread_before) {
977 edgeset.push_back(act);
982 * Include at most one act per-thread that "happens
985 if (act->happens_before(curr)) {
987 * Note: if act is RMW, just add edge:
989 * The following edge should be handled elsewhere:
990 * readfrom(act) --mo--> act
993 edgeset.push_back(act);
994 else if (act->is_read()) {
995 //if previous read accessed a null, just keep going
996 edgeset.push_back(act->get_reads_from());
1002 mo_graph->addEdges(&edgeset, curr);
1007 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1008 * some constraints. This method checks one the following constraint (others
1009 * require compiler support):
1011 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1012 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1014 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1016 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1018 /* Iterate over all threads */
1019 for (i = 0;i < thrd_lists->size();i++) {
1020 const ModelAction *write_after_read = NULL;
1022 /* Iterate over actions in thread, starting from most recent */
1023 action_list_t *list = &(*thrd_lists)[i];
1024 sllnode<ModelAction *>* rit;
1025 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1026 ModelAction *act = rit->getVal();
1028 /* Don't disallow due to act == reader */
1029 if (!reader->happens_before(act) || reader == act)
1031 else if (act->is_write())
1032 write_after_read = act;
1033 else if (act->is_read() && act->get_reads_from() != NULL)
1034 write_after_read = act->get_reads_from();
1037 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1044 * Computes the clock vector that happens before propagates from this write.
1046 * @param rf The action that might be part of a release sequence. Must be a
1048 * @return ClockVector of happens before relation.
1051 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1052 SnapVector<ModelAction *> * processset = NULL;
1053 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1054 ASSERT(rf->is_write());
1055 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1057 if (processset == NULL)
1058 processset = new SnapVector<ModelAction *>();
1059 processset->push_back(rf);
1062 int i = (processset == NULL) ? 0 : processset->size();
1064 ClockVector * vec = NULL;
1066 if (rf->get_rfcv() != NULL) {
1067 vec = rf->get_rfcv();
1068 } else if (rf->is_acquire() && rf->is_release()) {
1070 } else if (rf->is_release() && !rf->is_rmw()) {
1072 } else if (rf->is_release()) {
1073 //have rmw that is release and doesn't have a rfcv
1074 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1077 //operation that isn't release
1078 if (rf->get_last_fence_release()) {
1080 vec = rf->get_last_fence_release()->get_cv();
1082 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1088 rf = (*processset)[i];
1092 if (processset != NULL)
1098 * Performs various bookkeeping operations for the current ModelAction. For
1099 * instance, adds action to the per-object, per-thread action vector and to the
1100 * action trace list of all thread actions.
1102 * @param act is the ModelAction to add.
1104 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1106 int tid = id_to_int(act->get_tid());
1107 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1108 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1109 list->addAction(act);
1112 // Update action trace, a total order of all actions
1113 action_trace.addAction(act);
1116 // Update obj_thrd_map, a per location, per thread, order of actions
1117 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1118 if ((int)vec->size() <= tid) {
1119 uint oldsize = vec->size();
1120 vec->resize(priv->next_thread_id);
1121 for(uint i = oldsize;i < priv->next_thread_id;i++)
1122 new (&(*vec)[i]) action_list_t();
1124 if (!canprune && (act->is_read() || act->is_write()))
1125 (*vec)[tid].addAction(act);
1127 // Update thrd_last_action, the last action taken by each thread
1128 if ((int)thrd_last_action.size() <= tid)
1129 thrd_last_action.resize(get_num_threads());
1130 thrd_last_action[tid] = act;
1132 // Update thrd_last_fence_release, the last release fence taken by each thread
1133 if (act->is_fence() && act->is_release()) {
1134 if ((int)thrd_last_fence_release.size() <= tid)
1135 thrd_last_fence_release.resize(get_num_threads());
1136 thrd_last_fence_release[tid] = act;
1139 if (act->is_wait()) {
1140 void *mutex_loc = (void *) act->get_value();
1141 get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
1145 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1146 list->addAction(act);
1149 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1150 act->create_cv(NULL);
1151 list->addAction(act);
1155 * Performs various bookkeeping operations for a normal write. The
1156 * complication is that we are typically inserting a normal write
1157 * lazily, so we need to insert it into the middle of lists.
1159 * @param act is the ModelAction to add.
1162 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1164 int tid = id_to_int(act->get_tid());
1165 insertIntoActionListAndSetCV(&action_trace, act);
1167 // Update obj_thrd_map, a per location, per thread, order of actions
1168 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1169 if (tid >= (int)vec->size()) {
1170 uint oldsize =vec->size();
1171 vec->resize(priv->next_thread_id);
1172 for(uint i=oldsize;i<priv->next_thread_id;i++)
1173 new (&(*vec)[i]) action_list_t();
1175 insertIntoActionList(&(*vec)[tid],act);
1177 ModelAction * lastact = thrd_last_action[tid];
1178 // Update thrd_last_action, the last action taken by each thrad
1179 if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
1180 thrd_last_action[tid] = act;
1184 void ModelExecution::add_write_to_lists(ModelAction *write) {
1185 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1186 int tid = id_to_int(write->get_tid());
1187 if (tid >= (int)vec->size()) {
1188 uint oldsize =vec->size();
1189 vec->resize(priv->next_thread_id);
1190 for(uint i=oldsize;i<priv->next_thread_id;i++)
1191 new (&(*vec)[i]) action_list_t();
1193 (*vec)[tid].addAction(write);
1197 * @brief Get the last action performed by a particular Thread
1198 * @param tid The thread ID of the Thread in question
1199 * @return The last action in the thread
1201 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1203 int threadid = id_to_int(tid);
1204 if (threadid < (int)thrd_last_action.size())
1205 return thrd_last_action[id_to_int(tid)];
1211 * @brief Get the last fence release performed by a particular Thread
1212 * @param tid The thread ID of the Thread in question
1213 * @return The last fence release in the thread, if one exists; NULL otherwise
1215 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1217 int threadid = id_to_int(tid);
1218 if (threadid < (int)thrd_last_fence_release.size())
1219 return thrd_last_fence_release[id_to_int(tid)];
1225 * Gets the last memory_order_seq_cst write (in the total global sequence)
1226 * performed on a particular object (i.e., memory location), not including the
1228 * @param curr The current ModelAction; also denotes the object location to
1230 * @return The last seq_cst write
1232 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1234 void *location = curr->get_location();
1235 return obj_last_sc_map.get(location);
1239 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1240 * performed in a particular thread, prior to a particular fence.
1241 * @param tid The ID of the thread to check
1242 * @param before_fence The fence from which to begin the search; if NULL, then
1243 * search for the most recent fence in the thread.
1244 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1246 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1248 /* All fences should have location FENCE_LOCATION */
1249 action_list_t *list = obj_map.get(FENCE_LOCATION);
1254 sllnode<ModelAction*>* rit = list->end();
1257 for (;rit != NULL;rit=rit->getPrev())
1258 if (rit->getVal() == before_fence)
1261 ASSERT(rit->getVal() == before_fence);
1265 for (;rit != NULL;rit=rit->getPrev()) {
1266 ModelAction *act = rit->getVal();
1267 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1274 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1275 * location). This function identifies the mutex according to the current
1276 * action, which is presumed to perform on the same mutex.
1277 * @param curr The current ModelAction; also denotes the object location to
1279 * @return The last unlock operation
1281 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1283 void *location = curr->get_location();
1285 action_list_t *list = obj_map.get(location);
1289 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1290 sllnode<ModelAction*>* rit;
1291 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1292 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1293 return rit->getVal();
1297 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1299 ModelAction *parent = get_last_action(tid);
1301 parent = get_thread(tid)->get_creation();
1306 * Returns the clock vector for a given thread.
1307 * @param tid The thread whose clock vector we want
1308 * @return Desired clock vector
1310 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1312 ModelAction *firstaction=get_parent_action(tid);
1313 return firstaction != NULL ? firstaction->get_cv() : NULL;
1316 bool valequals(uint64_t val1, uint64_t val2, int size) {
1319 return ((uint8_t)val1) == ((uint8_t)val2);
1321 return ((uint16_t)val1) == ((uint16_t)val2);
1323 return ((uint32_t)val1) == ((uint32_t)val2);
1333 * Build up an initial set of all past writes that this 'read' action may read
1334 * from, as well as any previously-observed future values that must still be valid.
1336 * @param curr is the current ModelAction that we are exploring; it must be a
1339 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1341 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1343 ASSERT(curr->is_read());
1345 ModelAction *last_sc_write = NULL;
1347 if (curr->is_seqcst())
1348 last_sc_write = get_last_seq_cst_write(curr);
1350 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1352 /* Iterate over all threads */
1353 if (thrd_lists != NULL)
1354 for (i = 0;i < thrd_lists->size();i++) {
1355 /* Iterate over actions in thread, starting from most recent */
1356 action_list_t *list = &(*thrd_lists)[i];
1357 sllnode<ModelAction *> * rit;
1358 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1359 ModelAction *act = rit->getVal();
1364 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1365 bool allow_read = true;
1367 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1370 /* Need to check whether we will have two RMW reading from the same value */
1371 if (curr->is_rmwr()) {
1372 /* It is okay if we have a failing CAS */
1373 if (!curr->is_rmwrcas() ||
1374 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1375 //Need to make sure we aren't the second RMW
1376 CycleNode * node = mo_graph->getNode_noCreate(act);
1377 if (node != NULL && node->getRMW() != NULL) {
1378 //we are the second RMW
1385 /* Only add feasible reads */
1386 rf_set->push_back(act);
1389 /* Include at most one act per-thread that "happens before" curr */
1390 if (act->happens_before(curr))
1395 if (DBG_ENABLED()) {
1396 model_print("Reached read action:\n");
1398 model_print("End printing read_from_past\n");
1403 static void print_list(action_list_t *list)
1405 sllnode<ModelAction*> *it;
1407 model_print("------------------------------------------------------------------------------------\n");
1408 model_print("# t Action type MO Location Value Rf CV\n");
1409 model_print("------------------------------------------------------------------------------------\n");
1411 unsigned int hash = 0;
1413 for (it = list->begin();it != NULL;it=it->getNext()) {
1414 const ModelAction *act = it->getVal();
1415 if (act->get_seq_number() > 0)
1417 hash = hash^(hash<<3)^(it->getVal()->hash());
1419 model_print("HASH %u\n", hash);
1420 model_print("------------------------------------------------------------------------------------\n");
1423 #if SUPPORT_MOD_ORDER_DUMP
1424 void ModelExecution::dumpGraph(char *filename)
1427 sprintf(buffer, "%s.dot", filename);
1428 FILE *file = fopen(buffer, "w");
1429 fprintf(file, "digraph %s {\n", filename);
1430 mo_graph->dumpNodes(file);
1431 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1433 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1434 ModelAction *act = it->getVal();
1435 if (act->is_read()) {
1436 mo_graph->dot_print_node(file, act);
1437 mo_graph->dot_print_edge(file,
1438 act->get_reads_from(),
1440 "label=\"rf\", color=red, weight=2");
1442 if (thread_array[act->get_tid()]) {
1443 mo_graph->dot_print_edge(file,
1444 thread_array[id_to_int(act->get_tid())],
1446 "label=\"sb\", color=blue, weight=400");
1449 thread_array[act->get_tid()] = act;
1451 fprintf(file, "}\n");
1452 model_free(thread_array);
1457 /** @brief Prints an execution trace summary. */
1458 void ModelExecution::print_summary()
1460 #if SUPPORT_MOD_ORDER_DUMP
1461 char buffername[100];
1462 sprintf(buffername, "exec%04u", get_execution_number());
1463 mo_graph->dumpGraphToFile(buffername);
1464 sprintf(buffername, "graph%04u", get_execution_number());
1465 dumpGraph(buffername);
1468 model_print("Execution trace %d:", get_execution_number());
1469 if (scheduler->all_threads_sleeping())
1470 model_print(" SLEEP-SET REDUNDANT");
1471 if (have_bug_reports())
1472 model_print(" DETECTED BUG(S)");
1476 print_list(&action_trace);
1481 void ModelExecution::print_tail()
1483 model_print("Execution trace %d:\n", get_execution_number());
1485 sllnode<ModelAction*> *it;
1487 model_print("------------------------------------------------------------------------------------\n");
1488 model_print("# t Action type MO Location Value Rf CV\n");
1489 model_print("------------------------------------------------------------------------------------\n");
1491 unsigned int hash = 0;
1495 SnapList<ModelAction *> list;
1496 for (it = action_trace.end();it != NULL;it = it->getPrev()) {
1497 if (counter > length)
1500 ModelAction * act = it->getVal();
1501 list.push_front(act);
1505 for (it = list.begin();it != NULL;it=it->getNext()) {
1506 const ModelAction *act = it->getVal();
1507 if (act->get_seq_number() > 0)
1509 hash = hash^(hash<<3)^(it->getVal()->hash());
1511 model_print("HASH %u\n", hash);
1512 model_print("------------------------------------------------------------------------------------\n");
1516 * Add a Thread to the system for the first time. Should only be called once
1518 * @param t The Thread to add
1520 void ModelExecution::add_thread(Thread *t)
1522 unsigned int i = id_to_int(t->get_id());
1523 if (i >= thread_map.size())
1524 thread_map.resize(i + 1);
1526 if (!t->is_model_thread())
1527 scheduler->add_thread(t);
1531 * @brief Get a Thread reference by its ID
1532 * @param tid The Thread's ID
1533 * @return A Thread reference
1535 Thread * ModelExecution::get_thread(thread_id_t tid) const
1537 unsigned int i = id_to_int(tid);
1538 if (i < thread_map.size())
1539 return thread_map[i];
1544 * @brief Get a reference to the Thread in which a ModelAction was executed
1545 * @param act The ModelAction
1546 * @return A Thread reference
1548 Thread * ModelExecution::get_thread(const ModelAction *act) const
1550 return get_thread(act->get_tid());
1554 * @brief Get a Thread reference by its pthread ID
1555 * @param index The pthread's ID
1556 * @return A Thread reference
1558 Thread * ModelExecution::get_pthread(pthread_t pid) {
1559 // pid 1 is reserved for the main thread, pthread ids should start from 2
1561 return get_thread(pid);
1568 uint32_t thread_id = x.v;
1570 if (thread_id < pthread_counter + 1)
1571 return pthread_map[thread_id];
1577 * @brief Check if a Thread is currently enabled
1578 * @param t The Thread to check
1579 * @return True if the Thread is currently enabled
1581 bool ModelExecution::is_enabled(Thread *t) const
1583 return scheduler->is_enabled(t);
1587 * @brief Check if a Thread is currently enabled
1588 * @param tid The ID of the Thread to check
1589 * @return True if the Thread is currently enabled
1591 bool ModelExecution::is_enabled(thread_id_t tid) const
1593 return scheduler->is_enabled(tid);
1597 * @brief Select the next thread to execute based on the curren action
1599 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1600 * actions should be followed by the execution of their child thread. In either
1601 * case, the current action should determine the next thread schedule.
1603 * @param curr The current action
1604 * @return The next thread to run, if the current action will determine this
1605 * selection; otherwise NULL
1607 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1609 /* Do not split atomic RMW */
1610 if (curr->is_rmwr())
1611 return get_thread(curr);
1612 /* Follow CREATE with the created thread */
1613 /* which is not needed, because model.cc takes care of this */
1614 if (curr->get_type() == THREAD_CREATE)
1615 return curr->get_thread_operand();
1616 if (curr->get_type() == PTHREAD_CREATE) {
1617 return curr->get_thread_operand();
1623 * Takes the next step in the execution, if possible.
1624 * @param curr The current step to take
1625 * @return Returns the next Thread to run, if any; NULL if this execution
1628 Thread * ModelExecution::take_step(ModelAction *curr)
1630 Thread *curr_thrd = get_thread(curr);
1631 ASSERT(curr_thrd->get_state() == THREAD_READY);
1633 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1634 curr = check_current_action(curr);
1637 /* Process this action in ModelHistory for records */
1639 model->get_history()->process_action( curr, curr->get_tid() );
1641 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1642 scheduler->remove_thread(curr_thrd);
1644 return action_select_next_thread(curr);
1647 /** This method removes references to an Action before we delete it. */
1649 void ModelExecution::removeAction(ModelAction *act) {
1651 action_trace.removeAction(act);
1654 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1655 (*vec)[act->get_tid()].removeAction(act);
1657 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1658 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1659 list->removeAction(act);
1660 } else if (act->is_wait()) {
1661 void *mutex_loc = (void *) act->get_value();
1662 get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
1663 } else if (act->is_free()) {
1664 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1665 (*vec)[act->get_tid()].removeAction(act);
1667 //Clear it from last_sc_map
1668 if (obj_last_sc_map.get(act->get_location()) == act) {
1669 obj_last_sc_map.remove(act->get_location());
1672 //Remove from Cyclegraph
1673 mo_graph->freeAction(act);
1677 /** Computes clock vector that all running threads have already synchronized to. */
1679 ClockVector * ModelExecution::computeMinimalCV() {
1680 ClockVector *cvmin = NULL;
1681 //Thread 0 isn't a real thread, so skip it..
1682 for(unsigned int i = 1;i < thread_map.size();i++) {
1683 Thread * t = thread_map[i];
1684 if (t->get_state() == THREAD_COMPLETED)
1686 thread_id_t tid = int_to_id(i);
1687 ClockVector * cv = get_cv(tid);
1689 cvmin = new ClockVector(cv, NULL);
1691 cvmin->minmerge(cv);
1697 /** 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 */
1699 void ModelExecution::fixupLastAct(ModelAction *act) {
1700 ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid()));
1701 newact->set_seq_number(get_next_seq_num());
1702 newact->create_cv(act);
1703 newact->set_last_fence_release(act->get_last_fence_release());
1704 add_action_to_lists(newact, false);
1707 /** Compute which actions to free. */
1709 void ModelExecution::collectActions() {
1710 if (priv->used_sequence_numbers < params->traceminsize)
1713 //Compute minimal clock vector for all live threads
1714 ClockVector *cvmin = computeMinimalCV();
1715 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1716 modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1718 //Next walk action trace... When we hit an action, see if it is
1719 //invisible (e.g., earlier than the first before the minimum
1720 //clock for the thread... if so erase it and all previous
1721 //actions in cyclegraph
1722 sllnode<ModelAction*> * it;
1723 for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1724 ModelAction *act = it->getVal();
1725 modelclock_t actseq = act->get_seq_number();
1727 //See if we are done
1728 if (actseq > maxtofree)
1731 thread_id_t act_tid = act->get_tid();
1732 modelclock_t tid_clock = cvmin->getClock(act_tid);
1734 //Free if it is invisible or we have set a flag to remove visible actions.
1735 if (actseq <= tid_clock || params->removevisible) {
1736 ModelAction * write;
1737 if (act->is_write()) {
1739 } else if (act->is_read()) {
1740 write = act->get_reads_from();
1744 //Mark everything earlier in MO graph to be freed
1745 CycleNode * cn = mo_graph->getNode_noCreate(write);
1747 queue->push_back(cn);
1748 while(!queue->empty()) {
1749 CycleNode * node = queue->back();
1751 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1752 CycleNode * prevnode = node->getInEdge(i);
1753 ModelAction * prevact = prevnode->getAction();
1754 if (prevact->get_type() != READY_FREE) {
1755 prevact->set_free();
1756 queue->push_back(prevnode);
1764 //We may need to remove read actions in the window we don't delete to preserve correctness.
1766 for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1767 ModelAction *act = it2->getVal();
1768 //Do iteration early in case we delete the act
1770 bool islastact = false;
1771 ModelAction *lastact = get_last_action(act->get_tid());
1772 if (act == lastact) {
1773 Thread * th = get_thread(act);
1774 islastact = !th->is_complete();
1777 if (act->is_read()) {
1778 if (act->get_reads_from()->is_free()) {
1779 if (act->is_rmw()) {
1780 //Weaken a RMW from a freed store to a write
1781 act->set_type(ATOMIC_WRITE);
1793 //If we don't delete the action, we should remove references to release fences
1795 const ModelAction *rel_fence =act->get_last_fence_release();
1796 if (rel_fence != NULL) {
1797 modelclock_t relfenceseq = rel_fence->get_seq_number();
1798 thread_id_t relfence_tid = rel_fence->get_tid();
1799 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1800 //Remove references to irrelevant release fences
1801 if (relfenceseq <= tid_clock)
1802 act->set_last_fence_release(NULL);
1805 //Now we are in the window of old actions that we remove if possible
1806 for (;it != NULL;) {
1807 ModelAction *act = it->getVal();
1808 //Do iteration early since we may delete node...
1810 bool islastact = false;
1811 ModelAction *lastact = get_last_action(act->get_tid());
1812 if (act == lastact) {
1813 Thread * th = get_thread(act);
1814 islastact = !th->is_complete();
1817 if (act->is_read()) {
1818 if (act->get_reads_from()->is_free()) {
1819 if (act->is_rmw()) {
1820 act->set_type(ATOMIC_WRITE);
1830 } else if (act->is_free()) {
1837 } else if (act->is_write()) {
1838 //Do nothing with write that hasn't been marked to be freed
1839 } else if (islastact) {
1840 //Keep the last action for non-read/write actions
1841 } else if (act->is_fence()) {
1842 //Note that acquire fences can always be safely
1843 //removed, but could incur extra overheads in
1844 //traversals. Removing them before the cvmin seems
1845 //like a good compromise.
1847 //Release fences before the cvmin don't do anything
1848 //because everyone has already synchronized.
1850 //Sequentially fences before cvmin are redundant
1851 //because happens-before will enforce same
1854 modelclock_t actseq = act->get_seq_number();
1855 thread_id_t act_tid = act->get_tid();
1856 modelclock_t tid_clock = cvmin->getClock(act_tid);
1857 if (actseq <= tid_clock) {
1859 // Remove reference to act from thrd_last_fence_release
1860 int thread_id = id_to_int( act->get_tid() );
1861 if (thrd_last_fence_release[thread_id] == act) {
1862 thrd_last_fence_release[thread_id] = NULL;
1868 //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1869 //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1870 //need to keep most recent unlock/wait for each lock
1871 if(act->is_unlock() || act->is_wait()) {
1872 ModelAction * lastlock = get_last_unlock(act);
1873 if (lastlock != act) {
1878 } else if (act->is_create()) {
1879 if (act->get_thread_operand()->is_complete()) {
1891 //If we don't delete the action, we should remove references to release fences
1892 const ModelAction *rel_fence =act->get_last_fence_release();
1893 if (rel_fence != NULL) {
1894 modelclock_t relfenceseq = rel_fence->get_seq_number();
1895 thread_id_t relfence_tid = rel_fence->get_tid();
1896 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1897 //Remove references to irrelevant release fences
1898 if (relfenceseq <= tid_clock)
1899 act->set_last_fence_release(NULL);
1907 Fuzzer * ModelExecution::getFuzzer() {