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) :
55 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
63 thrd_last_fence_release(),
64 priv(new struct model_snapshot_members ()),
65 mo_graph(new CycleGraph()),
66 fuzzer(new NewFuzzer()),
68 thrd_func_act_lists(),
71 /* Initialize a model-checker thread, for special ModelActions */
72 model_thread = new Thread(get_next_id());
73 add_thread(model_thread);
74 fuzzer->register_engine(m->get_history(), this);
75 scheduler->register_engine(this);
78 /** @brief Destructor */
79 ModelExecution::~ModelExecution()
81 for (unsigned int i = 0;i < get_num_threads();i++)
82 delete get_thread(int_to_id(i));
88 int ModelExecution::get_execution_number() const
90 return model->get_execution_number();
93 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
95 action_list_t *tmp = hash->get(ptr);
97 tmp = new action_list_t();
103 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
105 SnapVector<action_list_t> *tmp = hash->get(ptr);
107 tmp = new SnapVector<action_list_t>();
113 /** @return a thread ID for a new Thread */
114 thread_id_t ModelExecution::get_next_id()
116 return priv->next_thread_id++;
119 /** @return the number of user threads created during this execution */
120 unsigned int ModelExecution::get_num_threads() const
122 return priv->next_thread_id;
125 /** @return a sequence number for a new ModelAction */
126 modelclock_t ModelExecution::get_next_seq_num()
128 return ++priv->used_sequence_numbers;
131 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
132 void ModelExecution::restore_last_seq_num()
134 priv->used_sequence_numbers--;
138 * @brief Should the current action wake up a given thread?
140 * @param curr The current action
141 * @param thread The thread that we might wake up
142 * @return True, if we should wake up the sleeping thread; false otherwise
144 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
146 const ModelAction *asleep = thread->get_pending();
147 /* Don't allow partial RMW to wake anyone up */
150 /* Synchronizing actions may have been backtracked */
151 if (asleep->could_synchronize_with(curr))
153 /* All acquire/release fences and fence-acquire/store-release */
154 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
156 /* Fence-release + store can awake load-acquire on the same location */
157 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
158 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
159 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
162 /* The sleep is literally sleeping */
163 if (asleep->is_sleep()) {
164 if (fuzzer->shouldWake(asleep))
171 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
173 for (unsigned int i = 0;i < get_num_threads();i++) {
174 Thread *thr = get_thread(int_to_id(i));
175 if (scheduler->is_sleep_set(thr)) {
176 if (should_wake_up(curr, thr)) {
177 /* Remove this thread from sleep set */
178 scheduler->remove_sleep(thr);
179 if (thr->get_pending()->is_sleep())
180 thr->set_wakeup_state(true);
186 void ModelExecution::assert_bug(const char *msg)
188 priv->bugs.push_back(new bug_message(msg));
192 /** @return True, if any bugs have been reported for this execution */
193 bool ModelExecution::have_bug_reports() const
195 return priv->bugs.size() != 0;
198 SnapVector<bug_message *> * ModelExecution::get_bugs() const
204 * Check whether the current trace has triggered an assertion which should halt
207 * @return True, if the execution should be aborted; false otherwise
209 bool ModelExecution::has_asserted() const
211 return priv->asserted;
215 * Trigger a trace assertion which should cause this execution to be halted.
216 * This can be due to a detected bug or due to an infeasibility that should
219 void ModelExecution::set_assert()
221 priv->asserted = true;
225 * Check if we are in a deadlock. Should only be called at the end of an
226 * execution, although it should not give false positives in the middle of an
227 * execution (there should be some ENABLED thread).
229 * @return True if program is in a deadlock; false otherwise
231 bool ModelExecution::is_deadlocked() const
233 bool blocking_threads = false;
234 for (unsigned int i = 0;i < get_num_threads();i++) {
235 thread_id_t tid = int_to_id(i);
238 Thread *t = get_thread(tid);
239 if (!t->is_model_thread() && t->get_pending())
240 blocking_threads = true;
242 return blocking_threads;
246 * Check if this is a complete execution. That is, have all thread completed
247 * execution (rather than exiting because sleep sets have forced a redundant
250 * @return True if the execution is complete.
252 bool ModelExecution::is_complete_execution() const
254 for (unsigned int i = 0;i < get_num_threads();i++)
255 if (is_enabled(int_to_id(i)))
260 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
261 uint64_t value = *((const uint64_t *) location);
262 modelclock_t storeclock;
263 thread_id_t storethread;
264 getStoreThreadAndClock(location, &storethread, &storeclock);
265 setAtomicStoreFlag(location);
266 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
267 act->set_seq_number(storeclock);
268 add_normal_write_to_lists(act);
269 add_write_to_lists(act);
270 w_modification_order(act);
271 model->get_history()->process_action(act, act->get_tid());
276 * Processes a read model action.
277 * @param curr is the read model action to process.
278 * @param rf_set is the set of model actions we can possibly read from
279 * @return True if processing this read updates the mo_graph.
281 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
283 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
284 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
285 if (hasnonatomicstore) {
286 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
287 rf_set->push_back(nonatomicstore);
290 // Remove writes that violate read modification order
292 while (i < rf_set->size()) {
293 ModelAction * rf = (*rf_set)[i];
294 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
295 (*rf_set)[i] = rf_set->back();
302 int index = fuzzer->selectWrite(curr, rf_set);
304 ModelAction *rf = (*rf_set)[index];
307 bool canprune = false;
308 if (r_modification_order(curr, rf, priorset, &canprune)) {
309 for(unsigned int i=0;i<priorset->size();i++) {
310 mo_graph->addEdge((*priorset)[i], rf);
313 get_thread(curr)->set_return_value(curr->get_return_value());
315 if (canprune && curr->get_type() == ATOMIC_READ) {
316 int tid = id_to_int(curr->get_tid());
317 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
323 /* TODO: Following code not needed anymore */
325 (*rf_set)[index] = rf_set->back();
331 * Processes a lock, trylock, or unlock model action. @param curr is
332 * the read model action to process.
334 * The try lock operation checks whether the lock is taken. If not,
335 * it falls to the normal lock operation case. If so, it returns
338 * The lock operation has already been checked that it is enabled, so
339 * it just grabs the lock and synchronizes with the previous unlock.
341 * The unlock operation has to re-enable all of the threads that are
342 * waiting on the lock.
344 * @return True if synchronization was updated; false otherwise
346 bool ModelExecution::process_mutex(ModelAction *curr)
348 cdsc::mutex *mutex = curr->get_mutex();
349 struct cdsc::mutex_state *state = NULL;
352 state = mutex->get_state();
354 switch (curr->get_type()) {
355 case ATOMIC_TRYLOCK: {
356 bool success = !state->locked;
357 curr->set_try_lock(success);
359 get_thread(curr)->set_return_value(0);
362 get_thread(curr)->set_return_value(1);
364 //otherwise fall into the lock case
366 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
367 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
368 // assert_bug("Lock access before initialization");
369 state->locked = get_thread(curr);
370 ModelAction *unlock = get_last_unlock(curr);
371 //synchronize with the previous unlock statement
372 if (unlock != NULL) {
373 synchronize(unlock, curr);
379 /* wake up the other threads */
380 for (unsigned int i = 0;i < get_num_threads();i++) {
381 Thread *t = get_thread(int_to_id(i));
382 Thread *curr_thrd = get_thread(curr);
383 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
387 /* unlock the lock - after checking who was waiting on it */
388 state->locked = NULL;
390 if (fuzzer->shouldWait(curr)) {
391 /* disable this thread */
392 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
393 scheduler->sleep(get_thread(curr));
398 case ATOMIC_TIMEDWAIT:
399 case ATOMIC_UNLOCK: {
400 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
402 /* wake up the other threads */
403 for (unsigned int i = 0;i < get_num_threads();i++) {
404 Thread *t = get_thread(int_to_id(i));
405 Thread *curr_thrd = get_thread(curr);
406 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
410 /* unlock the lock - after checking who was waiting on it */
411 state->locked = NULL;
414 case ATOMIC_NOTIFY_ALL: {
415 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
416 //activate all the waiting threads
417 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
418 scheduler->wake(get_thread(rit->getVal()));
423 case ATOMIC_NOTIFY_ONE: {
424 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
425 if (waiters->size() != 0) {
426 Thread * thread = fuzzer->selectNotify(waiters);
427 scheduler->wake(thread);
439 * Process a write ModelAction
440 * @param curr The ModelAction to process
441 * @return True if the mo_graph was updated or promises were resolved
443 void ModelExecution::process_write(ModelAction *curr)
445 w_modification_order(curr);
446 get_thread(curr)->set_return_value(VALUE_NONE);
450 * Process a fence ModelAction
451 * @param curr The ModelAction to process
452 * @return True if synchronization was updated
454 bool ModelExecution::process_fence(ModelAction *curr)
457 * fence-relaxed: no-op
458 * fence-release: only log the occurence (not in this function), for
459 * use in later synchronization
460 * fence-acquire (this function): search for hypothetical release
462 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
464 bool updated = false;
465 if (curr->is_acquire()) {
466 action_list_t *list = &action_trace;
467 sllnode<ModelAction *> * rit;
468 /* Find X : is_read(X) && X --sb-> curr */
469 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
470 ModelAction *act = rit->getVal();
473 if (act->get_tid() != curr->get_tid())
475 /* Stop at the beginning of the thread */
476 if (act->is_thread_start())
478 /* Stop once we reach a prior fence-acquire */
479 if (act->is_fence() && act->is_acquire())
483 /* read-acquire will find its own release sequences */
484 if (act->is_acquire())
487 /* Establish hypothetical release sequences */
488 ClockVector *cv = get_hb_from_write(act->get_reads_from());
489 if (cv != NULL && curr->get_cv()->merge(cv))
497 * @brief Process the current action for thread-related activity
499 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
500 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
501 * synchronization, etc. This function is a no-op for non-THREAD actions
502 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
504 * @param curr The current action
505 * @return True if synchronization was updated or a thread completed
507 void ModelExecution::process_thread_action(ModelAction *curr)
509 switch (curr->get_type()) {
510 case THREAD_CREATE: {
511 thrd_t *thrd = (thrd_t *)curr->get_location();
512 struct thread_params *params = (struct thread_params *)curr->get_value();
513 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
514 curr->set_thread_operand(th);
516 th->set_creation(curr);
519 case PTHREAD_CREATE: {
520 (*(uint32_t *)curr->get_location()) = pthread_counter++;
522 struct pthread_params *params = (struct pthread_params *)curr->get_value();
523 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
524 curr->set_thread_operand(th);
526 th->set_creation(curr);
528 if ( pthread_map.size() < pthread_counter )
529 pthread_map.resize( pthread_counter );
530 pthread_map[ pthread_counter-1 ] = th;
535 Thread *blocking = curr->get_thread_operand();
536 ModelAction *act = get_last_action(blocking->get_id());
537 synchronize(act, curr);
541 Thread *blocking = curr->get_thread_operand();
542 ModelAction *act = get_last_action(blocking->get_id());
543 synchronize(act, curr);
544 break; // WL: to be add (modified)
547 case THREADONLY_FINISH:
548 case THREAD_FINISH: {
549 Thread *th = get_thread(curr);
550 if (curr->get_type() == THREAD_FINISH &&
551 th == model->getInitThread()) {
557 /* Wake up any joining threads */
558 for (unsigned int i = 0;i < get_num_threads();i++) {
559 Thread *waiting = get_thread(int_to_id(i));
560 if (waiting->waiting_on() == th &&
561 waiting->get_pending()->is_thread_join())
562 scheduler->wake(waiting);
571 Thread *th = get_thread(curr);
572 th->set_pending(curr);
573 scheduler->add_sleep(th);
582 * Initialize the current action by performing one or more of the following
583 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
584 * manipulating backtracking sets, allocating and
585 * initializing clock vectors, and computing the promises to fulfill.
587 * @param curr The current action, as passed from the user context; may be
588 * freed/invalidated after the execution of this function, with a different
589 * action "returned" its place (pass-by-reference)
590 * @return True if curr is a newly-explored action; false otherwise
592 bool ModelExecution::initialize_curr_action(ModelAction **curr)
594 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
595 ModelAction *newcurr = process_rmw(*curr);
601 ModelAction *newcurr = *curr;
603 newcurr->set_seq_number(get_next_seq_num());
604 /* Always compute new clock vector */
605 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
607 /* Assign most recent release fence */
608 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
610 return true; /* This was a new ModelAction */
615 * @brief Establish reads-from relation between two actions
617 * Perform basic operations involved with establishing a concrete rf relation,
618 * including setting the ModelAction data and checking for release sequences.
620 * @param act The action that is reading (must be a read)
621 * @param rf The action from which we are reading (must be a write)
623 * @return True if this read established synchronization
626 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
629 ASSERT(rf->is_write());
631 act->set_read_from(rf);
632 if (act->is_acquire()) {
633 ClockVector *cv = get_hb_from_write(rf);
636 act->get_cv()->merge(cv);
641 * @brief Synchronizes two actions
643 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
644 * This function performs the synchronization as well as providing other hooks
645 * for other checks along with synchronization.
647 * @param first The left-hand side of the synchronizes-with relation
648 * @param second The right-hand side of the synchronizes-with relation
649 * @return True if the synchronization was successful (i.e., was consistent
650 * with the execution order); false otherwise
652 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
654 if (*second < *first) {
655 ASSERT(0); //This should not happend
658 return second->synchronize_with(first);
662 * @brief Check whether a model action is enabled.
664 * Checks whether an operation would be successful (i.e., is a lock already
665 * locked, or is the joined thread already complete).
667 * For yield-blocking, yields are never enabled.
669 * @param curr is the ModelAction to check whether it is enabled.
670 * @return a bool that indicates whether the action is enabled.
672 bool ModelExecution::check_action_enabled(ModelAction *curr) {
673 if (curr->is_lock()) {
674 cdsc::mutex *lock = curr->get_mutex();
675 struct cdsc::mutex_state *state = lock->get_state();
678 } else if (curr->is_thread_join()) {
679 Thread *blocking = curr->get_thread_operand();
680 if (!blocking->is_complete()) {
683 } else if (curr->is_sleep()) {
684 if (!fuzzer->shouldSleep(curr))
692 * This is the heart of the model checker routine. It performs model-checking
693 * actions corresponding to a given "current action." Among other processes, it
694 * calculates reads-from relationships, updates synchronization clock vectors,
695 * forms a memory_order constraints graph, and handles replay/backtrack
696 * execution when running permutations of previously-observed executions.
698 * @param curr The current action to process
699 * @return The ModelAction that is actually executed; may be different than
702 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
705 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
706 bool newly_explored = initialize_curr_action(&curr);
710 wake_up_sleeping_actions(curr);
712 /* Add uninitialized actions to lists */
713 if (!second_part_of_rmw)
714 add_uninit_action_to_lists(curr);
716 SnapVector<ModelAction *> * rf_set = NULL;
717 /* Build may_read_from set for newly-created actions */
718 if (newly_explored && curr->is_read())
719 rf_set = build_may_read_from(curr);
721 if (curr->is_read() && !second_part_of_rmw) {
722 process_read(curr, rf_set);
725 ASSERT(rf_set == NULL);
727 /* Add the action to lists */
728 if (!second_part_of_rmw)
729 add_action_to_lists(curr);
731 if (curr->is_write())
732 add_write_to_lists(curr);
734 process_thread_action(curr);
736 if (curr->is_write())
739 if (curr->is_fence())
742 if (curr->is_mutex_op())
748 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
749 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
750 ModelAction *lastread = get_last_action(act->get_tid());
751 lastread->process_rmw(act);
753 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
759 * @brief Updates the mo_graph with the constraints imposed from the current
762 * Basic idea is the following: Go through each other thread and find
763 * the last action that happened before our read. Two cases:
765 * -# The action is a write: that write must either occur before
766 * the write we read from or be the write we read from.
767 * -# The action is a read: the write that that action read from
768 * must occur before the write we read from or be the same write.
770 * @param curr The current action. Must be a read.
771 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
772 * @param check_only If true, then only check whether the current action satisfies
773 * read modification order or not, without modifiying priorset and canprune.
775 * @return True if modification order edges were added; false otherwise
778 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
779 SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
781 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
783 ASSERT(curr->is_read());
785 /* Last SC fence in the current thread */
786 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
788 int tid = curr->get_tid();
789 ModelAction *prev_same_thread = NULL;
790 /* Iterate over all threads */
791 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
792 /* Last SC fence in thread tid */
793 ModelAction *last_sc_fence_thread_local = NULL;
795 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
797 /* Last SC fence in thread tid, before last SC fence in current thread */
798 ModelAction *last_sc_fence_thread_before = NULL;
799 if (last_sc_fence_local)
800 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
802 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
803 if (prev_same_thread != NULL &&
804 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
805 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
809 /* Iterate over actions in thread, starting from most recent */
810 action_list_t *list = &(*thrd_lists)[tid];
811 sllnode<ModelAction *> * rit;
812 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
813 ModelAction *act = rit->getVal();
818 /* Don't want to add reflexive edges on 'rf' */
819 if (act->equals(rf)) {
820 if (act->happens_before(curr))
826 if (act->is_write()) {
827 /* C++, Section 29.3 statement 5 */
828 if (curr->is_seqcst() && last_sc_fence_thread_local &&
829 *act < *last_sc_fence_thread_local) {
830 if (mo_graph->checkReachable(rf, act))
833 priorset->push_back(act);
836 /* C++, Section 29.3 statement 4 */
837 else if (act->is_seqcst() && last_sc_fence_local &&
838 *act < *last_sc_fence_local) {
839 if (mo_graph->checkReachable(rf, act))
842 priorset->push_back(act);
845 /* C++, Section 29.3 statement 6 */
846 else if (last_sc_fence_thread_before &&
847 *act < *last_sc_fence_thread_before) {
848 if (mo_graph->checkReachable(rf, act))
851 priorset->push_back(act);
857 * Include at most one act per-thread that "happens
860 if (act->happens_before(curr)) {
862 if (last_sc_fence_local == NULL ||
863 (*last_sc_fence_local < *act)) {
864 prev_same_thread = act;
867 if (act->is_write()) {
868 if (mo_graph->checkReachable(rf, act))
871 priorset->push_back(act);
873 const ModelAction *prevrf = act->get_reads_from();
874 if (!prevrf->equals(rf)) {
875 if (mo_graph->checkReachable(rf, prevrf))
878 priorset->push_back(prevrf);
880 if (act->get_tid() == curr->get_tid()) {
881 //Can prune curr from obj list
895 * Updates the mo_graph with the constraints imposed from the current write.
897 * Basic idea is the following: Go through each other thread and find
898 * the lastest action that happened before our write. Two cases:
900 * (1) The action is a write => that write must occur before
903 * (2) The action is a read => the write that that action read from
904 * must occur before the current write.
906 * This method also handles two other issues:
908 * (I) Sequential Consistency: Making sure that if the current write is
909 * seq_cst, that it occurs after the previous seq_cst write.
911 * (II) Sending the write back to non-synchronizing reads.
913 * @param curr The current action. Must be a write.
914 * @param send_fv A vector for stashing reads to which we may pass our future
915 * value. If NULL, then don't record any future values.
916 * @return True if modification order edges were added; false otherwise
918 void ModelExecution::w_modification_order(ModelAction *curr)
920 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
922 ASSERT(curr->is_write());
924 SnapList<ModelAction *> edgeset;
926 if (curr->is_seqcst()) {
927 /* We have to at least see the last sequentially consistent write,
928 so we are initialized. */
929 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
930 if (last_seq_cst != NULL) {
931 edgeset.push_back(last_seq_cst);
933 //update map for next query
934 obj_last_sc_map.put(curr->get_location(), curr);
937 /* Last SC fence in the current thread */
938 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
940 /* Iterate over all threads */
941 for (i = 0;i < thrd_lists->size();i++) {
942 /* Last SC fence in thread i, before last SC fence in current thread */
943 ModelAction *last_sc_fence_thread_before = NULL;
944 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
945 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
947 /* Iterate over actions in thread, starting from most recent */
948 action_list_t *list = &(*thrd_lists)[i];
949 sllnode<ModelAction*>* rit;
950 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
951 ModelAction *act = rit->getVal();
954 * 1) If RMW and it actually read from something, then we
955 * already have all relevant edges, so just skip to next
958 * 2) If RMW and it didn't read from anything, we should
959 * whatever edge we can get to speed up convergence.
961 * 3) If normal write, we need to look at earlier actions, so
962 * continue processing list.
964 if (curr->is_rmw()) {
965 if (curr->get_reads_from() != NULL)
973 /* C++, Section 29.3 statement 7 */
974 if (last_sc_fence_thread_before && act->is_write() &&
975 *act < *last_sc_fence_thread_before) {
976 edgeset.push_back(act);
981 * Include at most one act per-thread that "happens
984 if (act->happens_before(curr)) {
986 * Note: if act is RMW, just add edge:
988 * The following edge should be handled elsewhere:
989 * readfrom(act) --mo--> act
992 edgeset.push_back(act);
993 else if (act->is_read()) {
994 //if previous read accessed a null, just keep going
995 edgeset.push_back(act->get_reads_from());
1001 mo_graph->addEdges(&edgeset, curr);
1006 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1007 * some constraints. This method checks one the following constraint (others
1008 * require compiler support):
1010 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1011 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1013 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1015 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1017 /* Iterate over all threads */
1018 for (i = 0;i < thrd_lists->size();i++) {
1019 const ModelAction *write_after_read = NULL;
1021 /* Iterate over actions in thread, starting from most recent */
1022 action_list_t *list = &(*thrd_lists)[i];
1023 sllnode<ModelAction *>* rit;
1024 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1025 ModelAction *act = rit->getVal();
1027 /* Don't disallow due to act == reader */
1028 if (!reader->happens_before(act) || reader == act)
1030 else if (act->is_write())
1031 write_after_read = act;
1032 else if (act->is_read() && act->get_reads_from() != NULL)
1033 write_after_read = act->get_reads_from();
1036 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1043 * Computes the clock vector that happens before propagates from this write.
1045 * @param rf The action that might be part of a release sequence. Must be a
1047 * @return ClockVector of happens before relation.
1050 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1051 SnapVector<ModelAction *> * processset = NULL;
1052 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1053 ASSERT(rf->is_write());
1054 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1056 if (processset == NULL)
1057 processset = new SnapVector<ModelAction *>();
1058 processset->push_back(rf);
1061 int i = (processset == NULL) ? 0 : processset->size();
1063 ClockVector * vec = NULL;
1065 if (rf->get_rfcv() != NULL) {
1066 vec = rf->get_rfcv();
1067 } else if (rf->is_acquire() && rf->is_release()) {
1069 } else if (rf->is_release() && !rf->is_rmw()) {
1071 } else if (rf->is_release()) {
1072 //have rmw that is release and doesn't have a rfcv
1073 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1076 //operation that isn't release
1077 if (rf->get_last_fence_release()) {
1079 vec = rf->get_last_fence_release()->get_cv();
1081 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1087 rf = (*processset)[i];
1091 if (processset != NULL)
1097 * Performs various bookkeeping operations for the current ModelAction when it is
1098 * the first atomic action occurred at its memory location.
1100 * For instance, adds uninitialized action to the per-object, per-thread action vector
1101 * and to the action trace list of all thread actions.
1103 * @param act is the ModelAction to process.
1105 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1107 int tid = id_to_int(act->get_tid());
1108 ModelAction *uninit = NULL;
1110 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1111 if (list->empty() && act->is_atomic_var()) {
1112 uninit = get_uninitialized_action(act);
1113 uninit_id = id_to_int(uninit->get_tid());
1114 list->push_front(uninit);
1115 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1116 if ((int)vec->size() <= uninit_id) {
1117 int oldsize = (int) vec->size();
1118 vec->resize(uninit_id + 1);
1119 for(int i = oldsize;i < uninit_id + 1;i++) {
1120 new (&(*vec)[i]) action_list_t();
1123 (*vec)[uninit_id].push_front(uninit);
1126 // Update action trace, a total order of all actions
1128 action_trace.push_front(uninit);
1130 // Update obj_thrd_map, a per location, per thread, order of actions
1131 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1132 if ((int)vec->size() <= tid) {
1133 uint oldsize = vec->size();
1134 vec->resize(priv->next_thread_id);
1135 for(uint i = oldsize;i < priv->next_thread_id;i++)
1136 new (&(*vec)[i]) action_list_t();
1139 (*vec)[uninit_id].push_front(uninit);
1141 // Update thrd_last_action, the last action taken by each thrad
1142 if ((int)thrd_last_action.size() <= tid)
1143 thrd_last_action.resize(get_num_threads());
1145 thrd_last_action[uninit_id] = uninit;
1150 * Performs various bookkeeping operations for the current ModelAction. For
1151 * instance, adds action to the per-object, per-thread action vector and to the
1152 * action trace list of all thread actions.
1154 * @param act is the ModelAction to add.
1156 void ModelExecution::add_action_to_lists(ModelAction *act)
1158 int tid = id_to_int(act->get_tid());
1159 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1160 list->push_back(act);
1162 // Update action trace, a total order of all actions
1163 action_trace.push_back(act);
1165 // Update obj_thrd_map, a per location, per thread, order of actions
1166 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1167 if ((int)vec->size() <= tid) {
1168 uint oldsize = vec->size();
1169 vec->resize(priv->next_thread_id);
1170 for(uint i = oldsize;i < priv->next_thread_id;i++)
1171 new (&(*vec)[i]) action_list_t();
1173 (*vec)[tid].push_back(act);
1175 // Update thrd_last_action, the last action taken by each thrad
1176 if ((int)thrd_last_action.size() <= tid)
1177 thrd_last_action.resize(get_num_threads());
1178 thrd_last_action[tid] = act;
1180 // Update thrd_last_fence_release, the last release fence taken by each thread
1181 if (act->is_fence() && act->is_release()) {
1182 if ((int)thrd_last_fence_release.size() <= tid)
1183 thrd_last_fence_release.resize(get_num_threads());
1184 thrd_last_fence_release[tid] = act;
1187 if (act->is_wait()) {
1188 void *mutex_loc = (void *) act->get_value();
1189 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1191 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1192 if ((int)vec->size() <= tid) {
1193 uint oldsize = vec->size();
1194 vec->resize(priv->next_thread_id);
1195 for(uint i = oldsize;i < priv->next_thread_id;i++)
1196 new (&(*vec)[i]) action_list_t();
1198 (*vec)[tid].push_back(act);
1202 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1203 sllnode<ModelAction*> * rit = list->end();
1204 modelclock_t next_seq = act->get_seq_number();
1205 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1206 list->push_back(act);
1208 for(;rit != NULL;rit=rit->getPrev()) {
1209 if (rit->getVal()->get_seq_number() == next_seq) {
1210 list->insertAfter(rit, act);
1217 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1218 sllnode<ModelAction*> * rit = list->end();
1219 modelclock_t next_seq = act->get_seq_number();
1221 act->create_cv(NULL);
1222 } else if (rit->getVal()->get_seq_number() == next_seq) {
1223 act->create_cv(rit->getVal());
1224 list->push_back(act);
1226 for(;rit != NULL;rit=rit->getPrev()) {
1227 if (rit->getVal()->get_seq_number() == next_seq) {
1228 act->create_cv(rit->getVal());
1229 list->insertAfter(rit, act);
1237 * Performs various bookkeeping operations for a normal write. The
1238 * complication is that we are typically inserting a normal write
1239 * lazily, so we need to insert it into the middle of lists.
1241 * @param act is the ModelAction to add.
1244 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1246 int tid = id_to_int(act->get_tid());
1247 insertIntoActionListAndSetCV(&action_trace, act);
1249 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1250 insertIntoActionList(list, act);
1252 // Update obj_thrd_map, a per location, per thread, order of actions
1253 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1254 if (tid >= (int)vec->size()) {
1255 uint oldsize =vec->size();
1256 vec->resize(priv->next_thread_id);
1257 for(uint i=oldsize;i<priv->next_thread_id;i++)
1258 new (&(*vec)[i]) action_list_t();
1260 insertIntoActionList(&(*vec)[tid],act);
1262 // Update thrd_last_action, the last action taken by each thrad
1263 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1264 thrd_last_action[tid] = act;
1268 void ModelExecution::add_write_to_lists(ModelAction *write) {
1269 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1270 int tid = id_to_int(write->get_tid());
1271 if (tid >= (int)vec->size()) {
1272 uint oldsize =vec->size();
1273 vec->resize(priv->next_thread_id);
1274 for(uint i=oldsize;i<priv->next_thread_id;i++)
1275 new (&(*vec)[i]) action_list_t();
1277 (*vec)[tid].push_back(write);
1281 * @brief Get the last action performed by a particular Thread
1282 * @param tid The thread ID of the Thread in question
1283 * @return The last action in the thread
1285 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1287 int threadid = id_to_int(tid);
1288 if (threadid < (int)thrd_last_action.size())
1289 return thrd_last_action[id_to_int(tid)];
1295 * @brief Get the last fence release performed by a particular Thread
1296 * @param tid The thread ID of the Thread in question
1297 * @return The last fence release in the thread, if one exists; NULL otherwise
1299 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1301 int threadid = id_to_int(tid);
1302 if (threadid < (int)thrd_last_fence_release.size())
1303 return thrd_last_fence_release[id_to_int(tid)];
1309 * Gets the last memory_order_seq_cst write (in the total global sequence)
1310 * performed on a particular object (i.e., memory location), not including the
1312 * @param curr The current ModelAction; also denotes the object location to
1314 * @return The last seq_cst write
1316 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1318 void *location = curr->get_location();
1319 return obj_last_sc_map.get(location);
1323 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1324 * performed in a particular thread, prior to a particular fence.
1325 * @param tid The ID of the thread to check
1326 * @param before_fence The fence from which to begin the search; if NULL, then
1327 * search for the most recent fence in the thread.
1328 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1330 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1332 /* All fences should have location FENCE_LOCATION */
1333 action_list_t *list = obj_map.get(FENCE_LOCATION);
1338 sllnode<ModelAction*>* rit = list->end();
1341 for (;rit != NULL;rit=rit->getPrev())
1342 if (rit->getVal() == before_fence)
1345 ASSERT(rit->getVal() == before_fence);
1349 for (;rit != NULL;rit=rit->getPrev()) {
1350 ModelAction *act = rit->getVal();
1351 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1358 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1359 * location). This function identifies the mutex according to the current
1360 * action, which is presumed to perform on the same mutex.
1361 * @param curr The current ModelAction; also denotes the object location to
1363 * @return The last unlock operation
1365 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1367 void *location = curr->get_location();
1369 action_list_t *list = obj_map.get(location);
1370 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1371 sllnode<ModelAction*>* rit;
1372 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1373 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1374 return rit->getVal();
1378 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1380 ModelAction *parent = get_last_action(tid);
1382 parent = get_thread(tid)->get_creation();
1387 * Returns the clock vector for a given thread.
1388 * @param tid The thread whose clock vector we want
1389 * @return Desired clock vector
1391 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1393 ModelAction *firstaction=get_parent_action(tid);
1394 return firstaction != NULL ? firstaction->get_cv() : NULL;
1397 bool valequals(uint64_t val1, uint64_t val2, int size) {
1400 return ((uint8_t)val1) == ((uint8_t)val2);
1402 return ((uint16_t)val1) == ((uint16_t)val2);
1404 return ((uint32_t)val1) == ((uint32_t)val2);
1414 * Build up an initial set of all past writes that this 'read' action may read
1415 * from, as well as any previously-observed future values that must still be valid.
1417 * @param curr is the current ModelAction that we are exploring; it must be a
1420 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1422 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1424 ASSERT(curr->is_read());
1426 ModelAction *last_sc_write = NULL;
1428 if (curr->is_seqcst())
1429 last_sc_write = get_last_seq_cst_write(curr);
1431 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1433 /* Iterate over all threads */
1434 for (i = 0;i < thrd_lists->size();i++) {
1435 /* Iterate over actions in thread, starting from most recent */
1436 action_list_t *list = &(*thrd_lists)[i];
1437 sllnode<ModelAction *> * rit;
1438 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1439 ModelAction *act = rit->getVal();
1444 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1445 bool allow_read = true;
1447 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1450 /* Need to check whether we will have two RMW reading from the same value */
1451 if (curr->is_rmwr()) {
1452 /* It is okay if we have a failing CAS */
1453 if (!curr->is_rmwrcas() ||
1454 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1455 //Need to make sure we aren't the second RMW
1456 CycleNode * node = mo_graph->getNode_noCreate(act);
1457 if (node != NULL && node->getRMW() != NULL) {
1458 //we are the second RMW
1465 /* Only add feasible reads */
1466 rf_set->push_back(act);
1469 /* Include at most one act per-thread that "happens before" curr */
1470 if (act->happens_before(curr))
1475 if (DBG_ENABLED()) {
1476 model_print("Reached read action:\n");
1478 model_print("End printing read_from_past\n");
1484 * @brief Get an action representing an uninitialized atomic
1486 * This function may create a new one.
1488 * @param curr The current action, which prompts the creation of an UNINIT action
1489 * @return A pointer to the UNINIT ModelAction
1491 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1493 ModelAction *act = curr->get_uninit_action();
1495 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1496 curr->set_uninit_action(act);
1498 act->create_cv(NULL);
1502 static void print_list(action_list_t *list)
1504 sllnode<ModelAction*> *it;
1506 model_print("------------------------------------------------------------------------------------\n");
1507 model_print("# t Action type MO Location Value Rf CV\n");
1508 model_print("------------------------------------------------------------------------------------\n");
1510 unsigned int hash = 0;
1512 for (it = list->begin();it != NULL;it=it->getNext()) {
1513 const ModelAction *act = it->getVal();
1514 if (act->get_seq_number() > 0)
1516 hash = hash^(hash<<3)^(it->getVal()->hash());
1518 model_print("HASH %u\n", hash);
1519 model_print("------------------------------------------------------------------------------------\n");
1522 #if SUPPORT_MOD_ORDER_DUMP
1523 void ModelExecution::dumpGraph(char *filename)
1526 sprintf(buffer, "%s.dot", filename);
1527 FILE *file = fopen(buffer, "w");
1528 fprintf(file, "digraph %s {\n", filename);
1529 mo_graph->dumpNodes(file);
1530 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1532 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1533 ModelAction *act = it->getVal();
1534 if (act->is_read()) {
1535 mo_graph->dot_print_node(file, act);
1536 mo_graph->dot_print_edge(file,
1537 act->get_reads_from(),
1539 "label=\"rf\", color=red, weight=2");
1541 if (thread_array[act->get_tid()]) {
1542 mo_graph->dot_print_edge(file,
1543 thread_array[id_to_int(act->get_tid())],
1545 "label=\"sb\", color=blue, weight=400");
1548 thread_array[act->get_tid()] = act;
1550 fprintf(file, "}\n");
1551 model_free(thread_array);
1556 /** @brief Prints an execution trace summary. */
1557 void ModelExecution::print_summary()
1559 #if SUPPORT_MOD_ORDER_DUMP
1560 char buffername[100];
1561 sprintf(buffername, "exec%04u", get_execution_number());
1562 mo_graph->dumpGraphToFile(buffername);
1563 sprintf(buffername, "graph%04u", get_execution_number());
1564 dumpGraph(buffername);
1567 model_print("Execution trace %d:", get_execution_number());
1568 if (scheduler->all_threads_sleeping())
1569 model_print(" SLEEP-SET REDUNDANT");
1570 if (have_bug_reports())
1571 model_print(" DETECTED BUG(S)");
1575 print_list(&action_trace);
1581 * Add a Thread to the system for the first time. Should only be called once
1583 * @param t The Thread to add
1585 void ModelExecution::add_thread(Thread *t)
1587 unsigned int i = id_to_int(t->get_id());
1588 if (i >= thread_map.size())
1589 thread_map.resize(i + 1);
1591 if (!t->is_model_thread())
1592 scheduler->add_thread(t);
1596 * @brief Get a Thread reference by its ID
1597 * @param tid The Thread's ID
1598 * @return A Thread reference
1600 Thread * ModelExecution::get_thread(thread_id_t tid) const
1602 unsigned int i = id_to_int(tid);
1603 if (i < thread_map.size())
1604 return thread_map[i];
1609 * @brief Get a reference to the Thread in which a ModelAction was executed
1610 * @param act The ModelAction
1611 * @return A Thread reference
1613 Thread * ModelExecution::get_thread(const ModelAction *act) const
1615 return get_thread(act->get_tid());
1619 * @brief Get a Thread reference by its pthread ID
1620 * @param index The pthread's ID
1621 * @return A Thread reference
1623 Thread * ModelExecution::get_pthread(pthread_t pid) {
1629 uint32_t thread_id = x.v;
1630 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1635 * @brief Check if a Thread is currently enabled
1636 * @param t The Thread to check
1637 * @return True if the Thread is currently enabled
1639 bool ModelExecution::is_enabled(Thread *t) const
1641 return scheduler->is_enabled(t);
1645 * @brief Check if a Thread is currently enabled
1646 * @param tid The ID of the Thread to check
1647 * @return True if the Thread is currently enabled
1649 bool ModelExecution::is_enabled(thread_id_t tid) const
1651 return scheduler->is_enabled(tid);
1655 * @brief Select the next thread to execute based on the curren action
1657 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1658 * actions should be followed by the execution of their child thread. In either
1659 * case, the current action should determine the next thread schedule.
1661 * @param curr The current action
1662 * @return The next thread to run, if the current action will determine this
1663 * selection; otherwise NULL
1665 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1667 /* Do not split atomic RMW */
1668 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1669 return get_thread(curr);
1670 /* Follow CREATE with the created thread */
1671 /* which is not needed, because model.cc takes care of this */
1672 if (curr->get_type() == THREAD_CREATE)
1673 return curr->get_thread_operand();
1674 if (curr->get_type() == PTHREAD_CREATE) {
1675 return curr->get_thread_operand();
1680 /** @param act A read atomic action */
1681 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1683 ASSERT(act->is_read());
1685 // Actions paused by fuzzer have their sequence number reset to 0
1686 return act->get_seq_number() == 0;
1690 * Takes the next step in the execution, if possible.
1691 * @param curr The current step to take
1692 * @return Returns the next Thread to run, if any; NULL if this execution
1695 Thread * ModelExecution::take_step(ModelAction *curr)
1697 Thread *curr_thrd = get_thread(curr);
1698 ASSERT(curr_thrd->get_state() == THREAD_READY);
1700 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1701 curr = check_current_action(curr);
1704 /* Process this action in ModelHistory for records */
1705 model->get_history()->process_action( curr, curr->get_tid() );
1707 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1708 scheduler->remove_thread(curr_thrd);
1710 return action_select_next_thread(curr);
1713 Fuzzer * ModelExecution::getFuzzer() {