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 static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)
123 simple_action_list_t *tmp = hash->get(ptr);
125 tmp = new simple_action_list_t();
131 /** @return a thread ID for a new Thread */
132 thread_id_t ModelExecution::get_next_id()
134 return priv->next_thread_id++;
137 /** @return the number of user threads created during this execution */
138 unsigned int ModelExecution::get_num_threads() const
140 return priv->next_thread_id;
143 /** @return a sequence number for a new ModelAction */
144 modelclock_t ModelExecution::get_next_seq_num()
146 return ++priv->used_sequence_numbers;
149 /** @return a sequence number for a new ModelAction */
150 modelclock_t ModelExecution::get_curr_seq_num()
152 return priv->used_sequence_numbers;
155 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
156 void ModelExecution::restore_last_seq_num()
158 priv->used_sequence_numbers--;
162 * @brief Should the current action wake up a given thread?
164 * @param curr The current action
165 * @param thread The thread that we might wake up
166 * @return True, if we should wake up the sleeping thread; false otherwise
168 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
170 const ModelAction *asleep = thread->get_pending();
171 /* Don't allow partial RMW to wake anyone up */
174 /* Synchronizing actions may have been backtracked */
175 if (asleep->could_synchronize_with(curr))
177 /* All acquire/release fences and fence-acquire/store-release */
178 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
180 /* Fence-release + store can awake load-acquire on the same location */
181 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
182 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
183 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
186 /* The sleep is literally sleeping */
187 if (asleep->is_sleep()) {
188 if (fuzzer->shouldWake(asleep))
195 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
197 for (unsigned int i = 0;i < get_num_threads();i++) {
198 Thread *thr = get_thread(int_to_id(i));
199 if (scheduler->is_sleep_set(thr)) {
200 if (should_wake_up(curr, thr)) {
201 /* Remove this thread from sleep set */
202 scheduler->remove_sleep(thr);
203 if (thr->get_pending()->is_sleep())
204 thr->set_wakeup_state(true);
210 void ModelExecution::assert_bug(const char *msg)
212 priv->bugs.push_back(new bug_message(msg));
216 /** @return True, if any bugs have been reported for this execution */
217 bool ModelExecution::have_bug_reports() const
219 return priv->bugs.size() != 0;
222 SnapVector<bug_message *> * ModelExecution::get_bugs() const
228 * Check whether the current trace has triggered an assertion which should halt
231 * @return True, if the execution should be aborted; false otherwise
233 bool ModelExecution::has_asserted() const
235 return priv->asserted;
239 * Trigger a trace assertion which should cause this execution to be halted.
240 * This can be due to a detected bug or due to an infeasibility that should
243 void ModelExecution::set_assert()
245 priv->asserted = true;
249 * Check if we are in a deadlock. Should only be called at the end of an
250 * execution, although it should not give false positives in the middle of an
251 * execution (there should be some ENABLED thread).
253 * @return True if program is in a deadlock; false otherwise
255 bool ModelExecution::is_deadlocked() const
257 bool blocking_threads = false;
258 for (unsigned int i = 0;i < get_num_threads();i++) {
259 thread_id_t tid = int_to_id(i);
262 Thread *t = get_thread(tid);
263 if (!t->is_model_thread() && t->get_pending())
264 blocking_threads = true;
266 return blocking_threads;
270 * Check if this is a complete execution. That is, have all thread completed
271 * execution (rather than exiting because sleep sets have forced a redundant
274 * @return True if the execution is complete.
276 bool ModelExecution::is_complete_execution() const
278 for (unsigned int i = 0;i < get_num_threads();i++)
279 if (is_enabled(int_to_id(i)))
284 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
285 uint64_t value = *((const uint64_t *) location);
286 modelclock_t storeclock;
287 thread_id_t storethread;
288 getStoreThreadAndClock(location, &storethread, &storeclock);
289 setAtomicStoreFlag(location);
290 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
291 act->set_seq_number(storeclock);
292 add_normal_write_to_lists(act);
293 add_write_to_lists(act);
294 w_modification_order(act);
296 model->get_history()->process_action(act, act->get_tid());
302 * Processes a read model action.
303 * @param curr is the read model action to process.
304 * @param rf_set is the set of model actions we can possibly read from
305 * @return True if the read can be pruned from the thread map list.
307 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
309 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
310 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
311 if (hasnonatomicstore) {
312 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
313 rf_set->push_back(nonatomicstore);
316 // Remove writes that violate read modification order
319 while (i < rf_set->size()) {
320 ModelAction * rf = (*rf_set)[i];
321 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
322 (*rf_set)[i] = rf_set->back();
329 int index = fuzzer->selectWrite(curr, rf_set);
331 ModelAction *rf = (*rf_set)[index];
334 bool canprune = false;
335 if (r_modification_order(curr, rf, priorset, &canprune)) {
336 for(unsigned int i=0;i<priorset->size();i++) {
337 mo_graph->addEdge((*priorset)[i], rf);
340 get_thread(curr)->set_return_value(curr->get_return_value());
342 //Update acquire fence clock vector
343 ClockVector * hbcv = get_hb_from_write(curr->get_reads_from());
345 get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
346 return canprune && (curr->get_type() == ATOMIC_READ);
349 (*rf_set)[index] = rf_set->back();
355 * Processes a lock, trylock, or unlock model action. @param curr is
356 * the read model action to process.
358 * The try lock operation checks whether the lock is taken. If not,
359 * it falls to the normal lock operation case. If so, it returns
362 * The lock operation has already been checked that it is enabled, so
363 * it just grabs the lock and synchronizes with the previous unlock.
365 * The unlock operation has to re-enable all of the threads that are
366 * waiting on the lock.
368 * @return True if synchronization was updated; false otherwise
370 bool ModelExecution::process_mutex(ModelAction *curr)
372 cdsc::mutex *mutex = curr->get_mutex();
373 struct cdsc::mutex_state *state = NULL;
376 state = mutex->get_state();
378 switch (curr->get_type()) {
379 case ATOMIC_TRYLOCK: {
380 bool success = !state->locked;
381 curr->set_try_lock(success);
383 get_thread(curr)->set_return_value(0);
386 get_thread(curr)->set_return_value(1);
388 //otherwise fall into the lock case
390 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
391 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
392 // assert_bug("Lock access before initialization");
394 // TODO: lock count for recursive mutexes
395 state->locked = get_thread(curr);
396 ModelAction *unlock = get_last_unlock(curr);
397 //synchronize with the previous unlock statement
398 if (unlock != NULL) {
399 synchronize(unlock, curr);
405 //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
406 if (fuzzer->shouldWait(curr)) {
407 /* wake up the other threads */
408 for (unsigned int i = 0;i < get_num_threads();i++) {
409 Thread *t = get_thread(int_to_id(i));
410 Thread *curr_thrd = get_thread(curr);
411 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
415 /* unlock the lock - after checking who was waiting on it */
416 state->locked = NULL;
418 /* remove old wait action and disable this thread */
419 simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
420 for (sllnode<ModelAction *> * it = waiters->begin(); it != NULL; it = it->getNext()) {
421 ModelAction * wait = it->getVal();
422 if (wait->get_tid() == curr->get_tid()) {
428 waiters->push_back(curr);
429 scheduler->sleep(get_thread(curr));
434 case ATOMIC_TIMEDWAIT:
435 case ATOMIC_UNLOCK: {
436 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
437 //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
438 //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
439 //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
440 //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
441 //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
442 //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
443 //MUST EVENMTUALLY RELEASE...
445 // TODO: lock count for recursive mutexes
446 /* wake up the other threads */
447 for (unsigned int i = 0;i < get_num_threads();i++) {
448 Thread *t = get_thread(int_to_id(i));
449 Thread *curr_thrd = get_thread(curr);
450 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
454 /* unlock the lock - after checking who was waiting on it */
455 state->locked = NULL;
458 case ATOMIC_NOTIFY_ALL: {
459 simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
460 //activate all the waiting threads
461 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
462 scheduler->wake(get_thread(rit->getVal()));
467 case ATOMIC_NOTIFY_ONE: {
468 simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
469 if (waiters->size() != 0) {
470 Thread * thread = fuzzer->selectNotify(waiters);
471 scheduler->wake(thread);
483 * Process a write ModelAction
484 * @param curr The ModelAction to process
485 * @return True if the mo_graph was updated or promises were resolved
487 void ModelExecution::process_write(ModelAction *curr)
489 w_modification_order(curr);
490 get_thread(curr)->set_return_value(VALUE_NONE);
494 * Process a fence ModelAction
495 * @param curr The ModelAction to process
496 * @return True if synchronization was updated
498 void ModelExecution::process_fence(ModelAction *curr)
501 * fence-relaxed: no-op
502 * fence-release: only log the occurence (not in this function), for
503 * use in later synchronization
504 * fence-acquire (this function): search for hypothetical release
506 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
508 if (curr->is_acquire()) {
509 curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
514 * @brief Process the current action for thread-related activity
516 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
517 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
518 * synchronization, etc. This function is a no-op for non-THREAD actions
519 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
521 * @param curr The current action
522 * @return True if synchronization was updated or a thread completed
524 void ModelExecution::process_thread_action(ModelAction *curr)
526 switch (curr->get_type()) {
527 case THREAD_CREATE: {
528 thrd_t *thrd = (thrd_t *)curr->get_location();
529 struct thread_params *params = (struct thread_params *)curr->get_value();
530 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
531 curr->set_thread_operand(th);
533 th->set_creation(curr);
536 case PTHREAD_CREATE: {
537 (*(uint32_t *)curr->get_location()) = pthread_counter++;
539 struct pthread_params *params = (struct pthread_params *)curr->get_value();
540 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
541 curr->set_thread_operand(th);
543 th->set_creation(curr);
545 if ( pthread_map.size() < pthread_counter )
546 pthread_map.resize( pthread_counter );
547 pthread_map[ pthread_counter-1 ] = th;
552 Thread *blocking = curr->get_thread_operand();
553 ModelAction *act = get_last_action(blocking->get_id());
554 synchronize(act, curr);
558 Thread *blocking = curr->get_thread_operand();
559 ModelAction *act = get_last_action(blocking->get_id());
560 synchronize(act, curr);
561 break; // WL: to be add (modified)
564 case THREADONLY_FINISH:
565 case THREAD_FINISH: {
566 Thread *th = get_thread(curr);
567 if (curr->get_type() == THREAD_FINISH &&
568 th == model->getInitThread()) {
574 /* Wake up any joining threads */
575 for (unsigned int i = 0;i < get_num_threads();i++) {
576 Thread *waiting = get_thread(int_to_id(i));
577 if (waiting->waiting_on() == th &&
578 waiting->get_pending()->is_thread_join())
579 scheduler->wake(waiting);
588 Thread *th = get_thread(curr);
589 th->set_pending(curr);
590 scheduler->add_sleep(th);
599 * Initialize the current action by performing one or more of the following
600 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
601 * manipulating backtracking sets, allocating and
602 * initializing clock vectors, and computing the promises to fulfill.
604 * @param curr The current action, as passed from the user context; may be
605 * freed/invalidated after the execution of this function, with a different
606 * action "returned" its place (pass-by-reference)
607 * @return True if curr is a newly-explored action; false otherwise
609 bool ModelExecution::initialize_curr_action(ModelAction **curr)
611 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
612 ModelAction *newcurr = process_rmw(*curr);
618 ModelAction *newcurr = *curr;
620 newcurr->set_seq_number(get_next_seq_num());
621 /* Always compute new clock vector */
622 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
624 /* Assign most recent release fence */
625 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
627 return true; /* This was a new ModelAction */
632 * @brief Establish reads-from relation between two actions
634 * Perform basic operations involved with establishing a concrete rf relation,
635 * including setting the ModelAction data and checking for release sequences.
637 * @param act The action that is reading (must be a read)
638 * @param rf The action from which we are reading (must be a write)
640 * @return True if this read established synchronization
643 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
646 ASSERT(rf->is_write());
648 act->set_read_from(rf);
649 if (act->is_acquire()) {
650 ClockVector *cv = get_hb_from_write(rf);
653 act->get_cv()->merge(cv);
658 * @brief Synchronizes two actions
660 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
661 * This function performs the synchronization as well as providing other hooks
662 * for other checks along with synchronization.
664 * @param first The left-hand side of the synchronizes-with relation
665 * @param second The right-hand side of the synchronizes-with relation
666 * @return True if the synchronization was successful (i.e., was consistent
667 * with the execution order); false otherwise
669 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
671 if (*second < *first) {
672 ASSERT(0); //This should not happend
675 return second->synchronize_with(first);
679 * @brief Check whether a model action is enabled.
681 * Checks whether an operation would be successful (i.e., is a lock already
682 * locked, or is the joined thread already complete).
684 * For yield-blocking, yields are never enabled.
686 * @param curr is the ModelAction to check whether it is enabled.
687 * @return a bool that indicates whether the action is enabled.
689 bool ModelExecution::check_action_enabled(ModelAction *curr) {
690 if (curr->is_lock()) {
691 cdsc::mutex *lock = curr->get_mutex();
692 struct cdsc::mutex_state *state = lock->get_state();
694 Thread *lock_owner = (Thread *)state->locked;
695 Thread *curr_thread = get_thread(curr);
696 if (lock_owner == curr_thread && state->type == PTHREAD_MUTEX_RECURSIVE) {
702 } else if (curr->is_thread_join()) {
703 Thread *blocking = curr->get_thread_operand();
704 if (!blocking->is_complete()) {
707 } else if (curr->is_sleep()) {
708 if (!fuzzer->shouldSleep(curr))
716 * This is the heart of the model checker routine. It performs model-checking
717 * actions corresponding to a given "current action." Among other processes, it
718 * calculates reads-from relationships, updates synchronization clock vectors,
719 * forms a memory_order constraints graph, and handles replay/backtrack
720 * execution when running permutations of previously-observed executions.
722 * @param curr The current action to process
723 * @return The ModelAction that is actually executed; may be different than
726 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
729 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
730 bool newly_explored = initialize_curr_action(&curr);
734 wake_up_sleeping_actions(curr);
736 SnapVector<ModelAction *> * rf_set = NULL;
737 /* Build may_read_from set for newly-created actions */
738 if (newly_explored && curr->is_read())
739 rf_set = build_may_read_from(curr);
741 bool canprune = false;
743 if (curr->is_read() && !second_part_of_rmw) {
744 canprune = process_read(curr, rf_set);
747 ASSERT(rf_set == NULL);
749 /* Add the action to lists */
750 if (!second_part_of_rmw)
751 add_action_to_lists(curr, canprune);
753 if (curr->is_write())
754 add_write_to_lists(curr);
756 process_thread_action(curr);
758 if (curr->is_write())
761 if (curr->is_fence())
764 if (curr->is_mutex_op())
770 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
771 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
772 ModelAction *lastread = get_last_action(act->get_tid());
773 lastread->process_rmw(act);
775 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
781 * @brief Updates the mo_graph with the constraints imposed from the current
784 * Basic idea is the following: Go through each other thread and find
785 * the last action that happened before our read. Two cases:
787 * -# The action is a write: that write must either occur before
788 * the write we read from or be the write we read from.
789 * -# The action is a read: the write that that action read from
790 * must occur before the write we read from or be the same write.
792 * @param curr The current action. Must be a read.
793 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
794 * @param check_only If true, then only check whether the current action satisfies
795 * read modification order or not, without modifiying priorset and canprune.
797 * @return True if modification order edges were added; false otherwise
800 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
801 SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
803 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
804 ASSERT(curr->is_read());
806 /* Last SC fence in the current thread */
807 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
809 int tid = curr->get_tid();
811 /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
812 if ((int)thrd_lists->size() <= tid) {
813 uint oldsize = thrd_lists->size();
814 thrd_lists->resize(priv->next_thread_id);
815 for(uint i = oldsize;i < priv->next_thread_id;i++)
816 new (&(*thrd_lists)[i]) action_list_t();
819 ModelAction *prev_same_thread = NULL;
820 /* Iterate over all threads */
821 for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
822 /* Last SC fence in thread tid */
823 ModelAction *last_sc_fence_thread_local = NULL;
825 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
827 /* Last SC fence in thread tid, before last SC fence in current thread */
828 ModelAction *last_sc_fence_thread_before = NULL;
829 if (last_sc_fence_local)
830 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
832 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
833 if (prev_same_thread != NULL &&
834 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
835 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
839 /* Iterate over actions in thread, starting from most recent */
840 action_list_t *list = &(*thrd_lists)[tid];
841 sllnode<ModelAction *> * rit;
842 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
843 ModelAction *act = rit->getVal();
848 /* Don't want to add reflexive edges on 'rf' */
849 if (act->equals(rf)) {
850 if (act->happens_before(curr))
856 if (act->is_write()) {
857 /* C++, Section 29.3 statement 5 */
858 if (curr->is_seqcst() && last_sc_fence_thread_local &&
859 *act < *last_sc_fence_thread_local) {
860 if (mo_graph->checkReachable(rf, act))
863 priorset->push_back(act);
866 /* C++, Section 29.3 statement 4 */
867 else if (act->is_seqcst() && last_sc_fence_local &&
868 *act < *last_sc_fence_local) {
869 if (mo_graph->checkReachable(rf, act))
872 priorset->push_back(act);
875 /* C++, Section 29.3 statement 6 */
876 else if (last_sc_fence_thread_before &&
877 *act < *last_sc_fence_thread_before) {
878 if (mo_graph->checkReachable(rf, act))
881 priorset->push_back(act);
887 * Include at most one act per-thread that "happens
890 if (act->happens_before(curr)) {
892 if (last_sc_fence_local == NULL ||
893 (*last_sc_fence_local < *act)) {
894 prev_same_thread = act;
897 if (act->is_write()) {
898 if (mo_graph->checkReachable(rf, act))
901 priorset->push_back(act);
903 ModelAction *prevrf = act->get_reads_from();
904 if (!prevrf->equals(rf)) {
905 if (mo_graph->checkReachable(rf, prevrf))
908 priorset->push_back(prevrf);
910 if (act->get_tid() == curr->get_tid()) {
911 //Can prune curr from obj list
925 * Updates the mo_graph with the constraints imposed from the current write.
927 * Basic idea is the following: Go through each other thread and find
928 * the lastest action that happened before our write. Two cases:
930 * (1) The action is a write => that write must occur before
933 * (2) The action is a read => the write that that action read from
934 * must occur before the current write.
936 * This method also handles two other issues:
938 * (I) Sequential Consistency: Making sure that if the current write is
939 * seq_cst, that it occurs after the previous seq_cst write.
941 * (II) Sending the write back to non-synchronizing reads.
943 * @param curr The current action. Must be a write.
944 * @param send_fv A vector for stashing reads to which we may pass our future
945 * value. If NULL, then don't record any future values.
946 * @return True if modification order edges were added; false otherwise
948 void ModelExecution::w_modification_order(ModelAction *curr)
950 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
952 ASSERT(curr->is_write());
954 SnapList<ModelAction *> edgeset;
956 if (curr->is_seqcst()) {
957 /* We have to at least see the last sequentially consistent write,
958 so we are initialized. */
959 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
960 if (last_seq_cst != NULL) {
961 edgeset.push_back(last_seq_cst);
963 //update map for next query
964 obj_last_sc_map.put(curr->get_location(), curr);
967 /* Last SC fence in the current thread */
968 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
970 /* Iterate over all threads */
971 for (i = 0;i < thrd_lists->size();i++) {
972 /* Last SC fence in thread i, before last SC fence in current thread */
973 ModelAction *last_sc_fence_thread_before = NULL;
974 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
975 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
977 /* Iterate over actions in thread, starting from most recent */
978 action_list_t *list = &(*thrd_lists)[i];
979 sllnode<ModelAction*>* rit;
980 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
981 ModelAction *act = rit->getVal();
984 * 1) If RMW and it actually read from something, then we
985 * already have all relevant edges, so just skip to next
988 * 2) If RMW and it didn't read from anything, we should
989 * whatever edge we can get to speed up convergence.
991 * 3) If normal write, we need to look at earlier actions, so
992 * continue processing list.
994 if (curr->is_rmw()) {
995 if (curr->get_reads_from() != NULL)
1003 /* C++, Section 29.3 statement 7 */
1004 if (last_sc_fence_thread_before && act->is_write() &&
1005 *act < *last_sc_fence_thread_before) {
1006 edgeset.push_back(act);
1011 * Include at most one act per-thread that "happens
1014 if (act->happens_before(curr)) {
1016 * Note: if act is RMW, just add edge:
1018 * The following edge should be handled elsewhere:
1019 * readfrom(act) --mo--> act
1021 if (act->is_write())
1022 edgeset.push_back(act);
1023 else if (act->is_read()) {
1024 //if previous read accessed a null, just keep going
1025 edgeset.push_back(act->get_reads_from());
1031 mo_graph->addEdges(&edgeset, curr);
1036 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1037 * some constraints. This method checks one the following constraint (others
1038 * require compiler support):
1040 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1041 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1043 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1045 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1047 /* Iterate over all threads */
1048 for (i = 0;i < thrd_lists->size();i++) {
1049 const ModelAction *write_after_read = NULL;
1051 /* Iterate over actions in thread, starting from most recent */
1052 action_list_t *list = &(*thrd_lists)[i];
1053 sllnode<ModelAction *>* rit;
1054 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1055 ModelAction *act = rit->getVal();
1057 /* Don't disallow due to act == reader */
1058 if (!reader->happens_before(act) || reader == act)
1060 else if (act->is_write())
1061 write_after_read = act;
1062 else if (act->is_read() && act->get_reads_from() != NULL)
1063 write_after_read = act->get_reads_from();
1066 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1073 * Computes the clock vector that happens before propagates from this write.
1075 * @param rf The action that might be part of a release sequence. Must be a
1077 * @return ClockVector of happens before relation.
1080 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1081 SnapVector<ModelAction *> * processset = NULL;
1082 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1083 ASSERT(rf->is_write());
1084 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1086 if (processset == NULL)
1087 processset = new SnapVector<ModelAction *>();
1088 processset->push_back(rf);
1091 int i = (processset == NULL) ? 0 : processset->size();
1093 ClockVector * vec = NULL;
1095 if (rf->get_rfcv() != NULL) {
1096 vec = rf->get_rfcv();
1097 } else if (rf->is_acquire() && rf->is_release()) {
1099 } else if (rf->is_release() && !rf->is_rmw()) {
1101 } else if (rf->is_release()) {
1102 //have rmw that is release and doesn't have a rfcv
1103 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1106 //operation that isn't release
1107 if (rf->get_last_fence_release()) {
1109 vec = rf->get_last_fence_release()->get_cv();
1111 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1117 rf = (*processset)[i];
1121 if (processset != NULL)
1127 * Performs various bookkeeping operations for the current ModelAction. For
1128 * instance, adds action to the per-object, per-thread action vector and to the
1129 * action trace list of all thread actions.
1131 * @param act is the ModelAction to add.
1133 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1135 int tid = id_to_int(act->get_tid());
1136 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1137 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1138 list->addAction(act);
1141 // Update action trace, a total order of all actions
1142 action_trace.addAction(act);
1145 // Update obj_thrd_map, a per location, per thread, order of actions
1146 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1147 if ((int)vec->size() <= tid) {
1148 uint oldsize = vec->size();
1149 vec->resize(priv->next_thread_id);
1150 for(uint i = oldsize;i < priv->next_thread_id;i++)
1151 new (&(*vec)[i]) action_list_t();
1153 if (!canprune && (act->is_read() || act->is_write()))
1154 (*vec)[tid].addAction(act);
1156 // Update thrd_last_action, the last action taken by each thread
1157 if ((int)thrd_last_action.size() <= tid)
1158 thrd_last_action.resize(get_num_threads());
1159 thrd_last_action[tid] = act;
1161 // Update thrd_last_fence_release, the last release fence taken by each thread
1162 if (act->is_fence() && act->is_release()) {
1163 if ((int)thrd_last_fence_release.size() <= tid)
1164 thrd_last_fence_release.resize(get_num_threads());
1165 thrd_last_fence_release[tid] = act;
1168 if (act->is_wait()) {
1169 void *mutex_loc = (void *) act->get_value();
1170 get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
1174 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1175 list->addAction(act);
1178 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1179 act->create_cv(NULL);
1180 list->addAction(act);
1184 * Performs various bookkeeping operations for a normal write. The
1185 * complication is that we are typically inserting a normal write
1186 * lazily, so we need to insert it into the middle of lists.
1188 * @param act is the ModelAction to add.
1191 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1193 int tid = id_to_int(act->get_tid());
1194 insertIntoActionListAndSetCV(&action_trace, act);
1196 // Update obj_thrd_map, a per location, per thread, order of actions
1197 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1198 if (tid >= (int)vec->size()) {
1199 uint oldsize =vec->size();
1200 vec->resize(priv->next_thread_id);
1201 for(uint i=oldsize;i<priv->next_thread_id;i++)
1202 new (&(*vec)[i]) action_list_t();
1204 insertIntoActionList(&(*vec)[tid],act);
1206 ModelAction * lastact = thrd_last_action[tid];
1207 // Update thrd_last_action, the last action taken by each thrad
1208 if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
1209 thrd_last_action[tid] = act;
1213 void ModelExecution::add_write_to_lists(ModelAction *write) {
1214 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1215 int tid = id_to_int(write->get_tid());
1216 if (tid >= (int)vec->size()) {
1217 uint oldsize =vec->size();
1218 vec->resize(priv->next_thread_id);
1219 for(uint i=oldsize;i<priv->next_thread_id;i++)
1220 new (&(*vec)[i]) action_list_t();
1222 (*vec)[tid].addAction(write);
1226 * @brief Get the last action performed by a particular Thread
1227 * @param tid The thread ID of the Thread in question
1228 * @return The last action in the thread
1230 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1232 int threadid = id_to_int(tid);
1233 if (threadid < (int)thrd_last_action.size())
1234 return thrd_last_action[id_to_int(tid)];
1240 * @brief Get the last fence release performed by a particular Thread
1241 * @param tid The thread ID of the Thread in question
1242 * @return The last fence release in the thread, if one exists; NULL otherwise
1244 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1246 int threadid = id_to_int(tid);
1247 if (threadid < (int)thrd_last_fence_release.size())
1248 return thrd_last_fence_release[id_to_int(tid)];
1254 * Gets the last memory_order_seq_cst write (in the total global sequence)
1255 * performed on a particular object (i.e., memory location), not including the
1257 * @param curr The current ModelAction; also denotes the object location to
1259 * @return The last seq_cst write
1261 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1263 void *location = curr->get_location();
1264 return obj_last_sc_map.get(location);
1268 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1269 * performed in a particular thread, prior to a particular fence.
1270 * @param tid The ID of the thread to check
1271 * @param before_fence The fence from which to begin the search; if NULL, then
1272 * search for the most recent fence in the thread.
1273 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1275 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1277 /* All fences should have location FENCE_LOCATION */
1278 action_list_t *list = obj_map.get(FENCE_LOCATION);
1283 sllnode<ModelAction*>* rit = list->end();
1286 for (;rit != NULL;rit=rit->getPrev())
1287 if (rit->getVal() == before_fence)
1290 ASSERT(rit->getVal() == before_fence);
1294 for (;rit != NULL;rit=rit->getPrev()) {
1295 ModelAction *act = rit->getVal();
1296 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1303 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1304 * location). This function identifies the mutex according to the current
1305 * action, which is presumed to perform on the same mutex.
1306 * @param curr The current ModelAction; also denotes the object location to
1308 * @return The last unlock operation
1310 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1312 void *location = curr->get_location();
1314 action_list_t *list = obj_map.get(location);
1318 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1319 sllnode<ModelAction*>* rit;
1320 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1321 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1322 return rit->getVal();
1326 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1328 ModelAction *parent = get_last_action(tid);
1330 parent = get_thread(tid)->get_creation();
1335 * Returns the clock vector for a given thread.
1336 * @param tid The thread whose clock vector we want
1337 * @return Desired clock vector
1339 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1341 ModelAction *firstaction=get_parent_action(tid);
1342 return firstaction != NULL ? firstaction->get_cv() : NULL;
1345 bool valequals(uint64_t val1, uint64_t val2, int size) {
1348 return ((uint8_t)val1) == ((uint8_t)val2);
1350 return ((uint16_t)val1) == ((uint16_t)val2);
1352 return ((uint32_t)val1) == ((uint32_t)val2);
1362 * Build up an initial set of all past writes that this 'read' action may read
1363 * from, as well as any previously-observed future values that must still be valid.
1365 * @param curr is the current ModelAction that we are exploring; it must be a
1368 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1370 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1372 ASSERT(curr->is_read());
1374 ModelAction *last_sc_write = NULL;
1376 if (curr->is_seqcst())
1377 last_sc_write = get_last_seq_cst_write(curr);
1379 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1381 /* Iterate over all threads */
1382 if (thrd_lists != NULL)
1383 for (i = 0;i < thrd_lists->size();i++) {
1384 /* Iterate over actions in thread, starting from most recent */
1385 action_list_t *list = &(*thrd_lists)[i];
1386 sllnode<ModelAction *> * rit;
1387 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1388 ModelAction *act = rit->getVal();
1393 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1394 bool allow_read = true;
1396 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1399 /* Need to check whether we will have two RMW reading from the same value */
1400 if (curr->is_rmwr()) {
1401 /* It is okay if we have a failing CAS */
1402 if (!curr->is_rmwrcas() ||
1403 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1404 //Need to make sure we aren't the second RMW
1405 CycleNode * node = mo_graph->getNode_noCreate(act);
1406 if (node != NULL && node->getRMW() != NULL) {
1407 //we are the second RMW
1414 /* Only add feasible reads */
1415 rf_set->push_back(act);
1418 /* Include at most one act per-thread that "happens before" curr */
1419 if (act->happens_before(curr))
1424 if (DBG_ENABLED()) {
1425 model_print("Reached read action:\n");
1427 model_print("End printing read_from_past\n");
1432 static void print_list(action_list_t *list)
1434 sllnode<ModelAction*> *it;
1436 model_print("------------------------------------------------------------------------------------\n");
1437 model_print("# t Action type MO Location Value Rf CV\n");
1438 model_print("------------------------------------------------------------------------------------\n");
1440 unsigned int hash = 0;
1442 for (it = list->begin();it != NULL;it=it->getNext()) {
1443 const ModelAction *act = it->getVal();
1444 if (act->get_seq_number() > 0)
1446 hash = hash^(hash<<3)^(it->getVal()->hash());
1448 model_print("HASH %u\n", hash);
1449 model_print("------------------------------------------------------------------------------------\n");
1452 #if SUPPORT_MOD_ORDER_DUMP
1453 void ModelExecution::dumpGraph(char *filename)
1456 sprintf(buffer, "%s.dot", filename);
1457 FILE *file = fopen(buffer, "w");
1458 fprintf(file, "digraph %s {\n", filename);
1459 mo_graph->dumpNodes(file);
1460 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1462 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1463 ModelAction *act = it->getVal();
1464 if (act->is_read()) {
1465 mo_graph->dot_print_node(file, act);
1466 mo_graph->dot_print_edge(file,
1467 act->get_reads_from(),
1469 "label=\"rf\", color=red, weight=2");
1471 if (thread_array[act->get_tid()]) {
1472 mo_graph->dot_print_edge(file,
1473 thread_array[id_to_int(act->get_tid())],
1475 "label=\"sb\", color=blue, weight=400");
1478 thread_array[act->get_tid()] = act;
1480 fprintf(file, "}\n");
1481 model_free(thread_array);
1486 /** @brief Prints an execution trace summary. */
1487 void ModelExecution::print_summary()
1489 #if SUPPORT_MOD_ORDER_DUMP
1490 char buffername[100];
1491 sprintf(buffername, "exec%04u", get_execution_number());
1492 mo_graph->dumpGraphToFile(buffername);
1493 sprintf(buffername, "graph%04u", get_execution_number());
1494 dumpGraph(buffername);
1497 model_print("Execution trace %d:", get_execution_number());
1498 if (scheduler->all_threads_sleeping())
1499 model_print(" SLEEP-SET REDUNDANT");
1500 if (have_bug_reports())
1501 model_print(" DETECTED BUG(S)");
1505 print_list(&action_trace);
1510 void ModelExecution::print_tail()
1512 model_print("Execution trace %d:\n", get_execution_number());
1514 sllnode<ModelAction*> *it;
1516 model_print("------------------------------------------------------------------------------------\n");
1517 model_print("# t Action type MO Location Value Rf CV\n");
1518 model_print("------------------------------------------------------------------------------------\n");
1520 unsigned int hash = 0;
1524 SnapList<ModelAction *> list;
1525 for (it = action_trace.end();it != NULL;it = it->getPrev()) {
1526 if (counter > length)
1529 ModelAction * act = it->getVal();
1530 list.push_front(act);
1534 for (it = list.begin();it != NULL;it=it->getNext()) {
1535 const ModelAction *act = it->getVal();
1536 if (act->get_seq_number() > 0)
1538 hash = hash^(hash<<3)^(it->getVal()->hash());
1540 model_print("HASH %u\n", hash);
1541 model_print("------------------------------------------------------------------------------------\n");
1545 * Add a Thread to the system for the first time. Should only be called once
1547 * @param t The Thread to add
1549 void ModelExecution::add_thread(Thread *t)
1551 unsigned int i = id_to_int(t->get_id());
1552 if (i >= thread_map.size())
1553 thread_map.resize(i + 1);
1555 if (!t->is_model_thread())
1556 scheduler->add_thread(t);
1560 * @brief Get a Thread reference by its ID
1561 * @param tid The Thread's ID
1562 * @return A Thread reference
1564 Thread * ModelExecution::get_thread(thread_id_t tid) const
1566 unsigned int i = id_to_int(tid);
1567 if (i < thread_map.size())
1568 return thread_map[i];
1573 * @brief Get a reference to the Thread in which a ModelAction was executed
1574 * @param act The ModelAction
1575 * @return A Thread reference
1577 Thread * ModelExecution::get_thread(const ModelAction *act) const
1579 return get_thread(act->get_tid());
1583 * @brief Get a Thread reference by its pthread ID
1584 * @param index The pthread's ID
1585 * @return A Thread reference
1587 Thread * ModelExecution::get_pthread(pthread_t pid) {
1588 // pid 1 is reserved for the main thread, pthread ids should start from 2
1590 return get_thread(pid);
1597 uint32_t thread_id = x.v;
1599 if (thread_id < pthread_counter + 1)
1600 return pthread_map[thread_id];
1606 * @brief Check if a Thread is currently enabled
1607 * @param t The Thread to check
1608 * @return True if the Thread is currently enabled
1610 bool ModelExecution::is_enabled(Thread *t) const
1612 return scheduler->is_enabled(t);
1616 * @brief Check if a Thread is currently enabled
1617 * @param tid The ID of the Thread to check
1618 * @return True if the Thread is currently enabled
1620 bool ModelExecution::is_enabled(thread_id_t tid) const
1622 return scheduler->is_enabled(tid);
1626 * @brief Select the next thread to execute based on the curren action
1628 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1629 * actions should be followed by the execution of their child thread. In either
1630 * case, the current action should determine the next thread schedule.
1632 * @param curr The current action
1633 * @return The next thread to run, if the current action will determine this
1634 * selection; otherwise NULL
1636 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1638 /* Do not split atomic RMW */
1639 if (curr->is_rmwr())
1640 return get_thread(curr);
1641 /* Follow CREATE with the created thread */
1642 /* which is not needed, because model.cc takes care of this */
1643 if (curr->get_type() == THREAD_CREATE)
1644 return curr->get_thread_operand();
1645 if (curr->get_type() == PTHREAD_CREATE) {
1646 return curr->get_thread_operand();
1652 * Takes the next step in the execution, if possible.
1653 * @param curr The current step to take
1654 * @return Returns the next Thread to run, if any; NULL if this execution
1657 Thread * ModelExecution::take_step(ModelAction *curr)
1659 Thread *curr_thrd = get_thread(curr);
1660 ASSERT(curr_thrd->get_state() == THREAD_READY);
1662 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1663 curr = check_current_action(curr);
1666 /* Process this action in ModelHistory for records */
1668 model->get_history()->process_action( curr, curr->get_tid() );
1670 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1671 scheduler->remove_thread(curr_thrd);
1673 return action_select_next_thread(curr);
1676 /** This method removes references to an Action before we delete it. */
1678 void ModelExecution::removeAction(ModelAction *act) {
1680 action_trace.removeAction(act);
1683 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1684 (*vec)[act->get_tid()].removeAction(act);
1686 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1687 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1688 list->removeAction(act);
1689 } else if (act->is_wait()) {
1690 void *mutex_loc = (void *) act->get_value();
1691 get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
1692 } else if (act->is_free()) {
1693 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1694 (*vec)[act->get_tid()].removeAction(act);
1696 //Clear it from last_sc_map
1697 if (obj_last_sc_map.get(act->get_location()) == act) {
1698 obj_last_sc_map.remove(act->get_location());
1701 //Remove from Cyclegraph
1702 mo_graph->freeAction(act);
1706 /** Computes clock vector that all running threads have already synchronized to. */
1708 ClockVector * ModelExecution::computeMinimalCV() {
1709 ClockVector *cvmin = NULL;
1710 //Thread 0 isn't a real thread, so skip it..
1711 for(unsigned int i = 1;i < thread_map.size();i++) {
1712 Thread * t = thread_map[i];
1713 if (t->get_state() == THREAD_COMPLETED)
1715 thread_id_t tid = int_to_id(i);
1716 ClockVector * cv = get_cv(tid);
1718 cvmin = new ClockVector(cv, NULL);
1720 cvmin->minmerge(cv);
1726 /** 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 */
1728 void ModelExecution::fixupLastAct(ModelAction *act) {
1729 ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid()));
1730 newact->set_seq_number(get_next_seq_num());
1731 newact->create_cv(act);
1732 newact->set_last_fence_release(act->get_last_fence_release());
1733 add_action_to_lists(newact, false);
1736 /** Compute which actions to free. */
1738 void ModelExecution::collectActions() {
1739 if (priv->used_sequence_numbers < params->traceminsize)
1742 //Compute minimal clock vector for all live threads
1743 ClockVector *cvmin = computeMinimalCV();
1744 SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1745 modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1747 //Next walk action trace... When we hit an action, see if it is
1748 //invisible (e.g., earlier than the first before the minimum
1749 //clock for the thread... if so erase it and all previous
1750 //actions in cyclegraph
1751 sllnode<ModelAction*> * it;
1752 for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1753 ModelAction *act = it->getVal();
1754 modelclock_t actseq = act->get_seq_number();
1756 //See if we are done
1757 if (actseq > maxtofree)
1760 thread_id_t act_tid = act->get_tid();
1761 modelclock_t tid_clock = cvmin->getClock(act_tid);
1763 //Free if it is invisible or we have set a flag to remove visible actions.
1764 if (actseq <= tid_clock || params->removevisible) {
1765 ModelAction * write;
1766 if (act->is_write()) {
1768 } else if (act->is_read()) {
1769 write = act->get_reads_from();
1773 //Mark everything earlier in MO graph to be freed
1774 CycleNode * cn = mo_graph->getNode_noCreate(write);
1776 queue->push_back(cn);
1777 while(!queue->empty()) {
1778 CycleNode * node = queue->back();
1780 for(unsigned int i=0;i<node->getNumInEdges();i++) {
1781 CycleNode * prevnode = node->getInEdge(i);
1782 ModelAction * prevact = prevnode->getAction();
1783 if (prevact->get_type() != READY_FREE) {
1784 prevact->set_free();
1785 queue->push_back(prevnode);
1793 //We may need to remove read actions in the window we don't delete to preserve correctness.
1795 for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1796 ModelAction *act = it2->getVal();
1797 //Do iteration early in case we delete the act
1799 bool islastact = false;
1800 ModelAction *lastact = get_last_action(act->get_tid());
1801 if (act == lastact) {
1802 Thread * th = get_thread(act);
1803 islastact = !th->is_complete();
1806 if (act->is_read()) {
1807 if (act->get_reads_from()->is_free()) {
1808 if (act->is_rmw()) {
1809 //Weaken a RMW from a freed store to a write
1810 act->set_type(ATOMIC_WRITE);
1822 //If we don't delete the action, we should remove references to release fences
1824 const ModelAction *rel_fence =act->get_last_fence_release();
1825 if (rel_fence != NULL) {
1826 modelclock_t relfenceseq = rel_fence->get_seq_number();
1827 thread_id_t relfence_tid = rel_fence->get_tid();
1828 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1829 //Remove references to irrelevant release fences
1830 if (relfenceseq <= tid_clock)
1831 act->set_last_fence_release(NULL);
1834 //Now we are in the window of old actions that we remove if possible
1835 for (;it != NULL;) {
1836 ModelAction *act = it->getVal();
1837 //Do iteration early since we may delete node...
1839 bool islastact = false;
1840 ModelAction *lastact = get_last_action(act->get_tid());
1841 if (act == lastact) {
1842 Thread * th = get_thread(act);
1843 islastact = !th->is_complete();
1846 if (act->is_read()) {
1847 if (act->get_reads_from()->is_free()) {
1848 if (act->is_rmw()) {
1849 act->set_type(ATOMIC_WRITE);
1859 } else if (act->is_free()) {
1866 } else if (act->is_write()) {
1867 //Do nothing with write that hasn't been marked to be freed
1868 } else if (islastact) {
1869 //Keep the last action for non-read/write actions
1870 } else if (act->is_fence()) {
1871 //Note that acquire fences can always be safely
1872 //removed, but could incur extra overheads in
1873 //traversals. Removing them before the cvmin seems
1874 //like a good compromise.
1876 //Release fences before the cvmin don't do anything
1877 //because everyone has already synchronized.
1879 //Sequentially fences before cvmin are redundant
1880 //because happens-before will enforce same
1883 modelclock_t actseq = act->get_seq_number();
1884 thread_id_t act_tid = act->get_tid();
1885 modelclock_t tid_clock = cvmin->getClock(act_tid);
1886 if (actseq <= tid_clock) {
1888 // Remove reference to act from thrd_last_fence_release
1889 int thread_id = id_to_int( act->get_tid() );
1890 if (thrd_last_fence_release[thread_id] == act) {
1891 thrd_last_fence_release[thread_id] = NULL;
1897 //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1898 //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1899 //need to keep most recent unlock/wait for each lock
1900 if(act->is_unlock() || act->is_wait()) {
1901 ModelAction * lastlock = get_last_unlock(act);
1902 if (lastlock != act) {
1907 } else if (act->is_create()) {
1908 if (act->get_thread_operand()->is_complete()) {
1920 //If we don't delete the action, we should remove references to release fences
1921 const ModelAction *rel_fence =act->get_last_fence_release();
1922 if (rel_fence != NULL) {
1923 modelclock_t relfenceseq = rel_fence->get_seq_number();
1924 thread_id_t relfence_tid = rel_fence->get_tid();
1925 modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1926 //Remove references to irrelevant release fences
1927 if (relfenceseq <= tid_clock)
1928 act->set_last_fence_release(NULL);
1936 Fuzzer * ModelExecution::getFuzzer() {