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()),
69 /* Initialize a model-checker thread, for special ModelActions */
70 model_thread = new Thread(get_next_id());
71 add_thread(model_thread);
72 fuzzer->register_engine(m->get_history(), this);
73 scheduler->register_engine(this);
75 pthread_key_create(&pthreadkey, tlsdestructor);
79 /** @brief Destructor */
80 ModelExecution::~ModelExecution()
82 for (unsigned int i = 0;i < get_num_threads();i++)
83 delete get_thread(int_to_id(i));
89 int ModelExecution::get_execution_number() const
91 return model->get_execution_number();
94 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
96 action_list_t *tmp = hash->get(ptr);
98 tmp = new action_list_t();
104 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
106 SnapVector<action_list_t> *tmp = hash->get(ptr);
108 tmp = new SnapVector<action_list_t>();
114 /** @return a thread ID for a new Thread */
115 thread_id_t ModelExecution::get_next_id()
117 return priv->next_thread_id++;
120 /** @return the number of user threads created during this execution */
121 unsigned int ModelExecution::get_num_threads() const
123 return priv->next_thread_id;
126 /** @return a sequence number for a new ModelAction */
127 modelclock_t ModelExecution::get_next_seq_num()
129 return ++priv->used_sequence_numbers;
132 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
133 void ModelExecution::restore_last_seq_num()
135 priv->used_sequence_numbers--;
139 * @brief Should the current action wake up a given thread?
141 * @param curr The current action
142 * @param thread The thread that we might wake up
143 * @return True, if we should wake up the sleeping thread; false otherwise
145 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
147 const ModelAction *asleep = thread->get_pending();
148 /* Don't allow partial RMW to wake anyone up */
151 /* Synchronizing actions may have been backtracked */
152 if (asleep->could_synchronize_with(curr))
154 /* All acquire/release fences and fence-acquire/store-release */
155 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
157 /* Fence-release + store can awake load-acquire on the same location */
158 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
159 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
160 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
163 /* The sleep is literally sleeping */
164 if (asleep->is_sleep()) {
165 if (fuzzer->shouldWake(asleep))
172 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
174 for (unsigned int i = 0;i < get_num_threads();i++) {
175 Thread *thr = get_thread(int_to_id(i));
176 if (scheduler->is_sleep_set(thr)) {
177 if (should_wake_up(curr, thr)) {
178 /* Remove this thread from sleep set */
179 scheduler->remove_sleep(thr);
180 if (thr->get_pending()->is_sleep())
181 thr->set_wakeup_state(true);
187 void ModelExecution::assert_bug(const char *msg)
189 priv->bugs.push_back(new bug_message(msg));
193 /** @return True, if any bugs have been reported for this execution */
194 bool ModelExecution::have_bug_reports() const
196 return priv->bugs.size() != 0;
199 SnapVector<bug_message *> * ModelExecution::get_bugs() const
205 * Check whether the current trace has triggered an assertion which should halt
208 * @return True, if the execution should be aborted; false otherwise
210 bool ModelExecution::has_asserted() const
212 return priv->asserted;
216 * Trigger a trace assertion which should cause this execution to be halted.
217 * This can be due to a detected bug or due to an infeasibility that should
220 void ModelExecution::set_assert()
222 priv->asserted = true;
226 * Check if we are in a deadlock. Should only be called at the end of an
227 * execution, although it should not give false positives in the middle of an
228 * execution (there should be some ENABLED thread).
230 * @return True if program is in a deadlock; false otherwise
232 bool ModelExecution::is_deadlocked() const
234 bool blocking_threads = false;
235 for (unsigned int i = 0;i < get_num_threads();i++) {
236 thread_id_t tid = int_to_id(i);
239 Thread *t = get_thread(tid);
240 if (!t->is_model_thread() && t->get_pending())
241 blocking_threads = true;
243 return blocking_threads;
247 * Check if this is a complete execution. That is, have all thread completed
248 * execution (rather than exiting because sleep sets have forced a redundant
251 * @return True if the execution is complete.
253 bool ModelExecution::is_complete_execution() const
255 for (unsigned int i = 0;i < get_num_threads();i++)
256 if (is_enabled(int_to_id(i)))
261 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
262 uint64_t value = *((const uint64_t *) location);
263 modelclock_t storeclock;
264 thread_id_t storethread;
265 getStoreThreadAndClock(location, &storethread, &storeclock);
266 setAtomicStoreFlag(location);
267 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
268 act->set_seq_number(storeclock);
269 add_normal_write_to_lists(act);
270 add_write_to_lists(act);
271 w_modification_order(act);
272 model->get_history()->process_action(act, act->get_tid());
277 * Processes a read model action.
278 * @param curr is the read model action to process.
279 * @param rf_set is the set of model actions we can possibly read from
280 * @return True if processing this read updates the mo_graph.
282 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
284 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
285 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
286 if (hasnonatomicstore) {
287 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
288 rf_set->push_back(nonatomicstore);
291 // Remove writes that violate read modification order
293 while (i < rf_set->size()) {
294 ModelAction * rf = (*rf_set)[i];
295 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
296 (*rf_set)[i] = rf_set->back();
303 int index = fuzzer->selectWrite(curr, rf_set);
305 ModelAction *rf = (*rf_set)[index];
308 bool canprune = false;
309 if (r_modification_order(curr, rf, priorset, &canprune)) {
310 for(unsigned int i=0;i<priorset->size();i++) {
311 mo_graph->addEdge((*priorset)[i], rf);
314 get_thread(curr)->set_return_value(curr->get_return_value());
316 if (canprune && curr->get_type() == ATOMIC_READ) {
317 int tid = id_to_int(curr->get_tid());
318 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
324 /* TODO: Following code not needed anymore */
326 (*rf_set)[index] = rf_set->back();
332 * Processes a lock, trylock, or unlock model action. @param curr is
333 * the read model action to process.
335 * The try lock operation checks whether the lock is taken. If not,
336 * it falls to the normal lock operation case. If so, it returns
339 * The lock operation has already been checked that it is enabled, so
340 * it just grabs the lock and synchronizes with the previous unlock.
342 * The unlock operation has to re-enable all of the threads that are
343 * waiting on the lock.
345 * @return True if synchronization was updated; false otherwise
347 bool ModelExecution::process_mutex(ModelAction *curr)
349 cdsc::mutex *mutex = curr->get_mutex();
350 struct cdsc::mutex_state *state = NULL;
353 state = mutex->get_state();
355 switch (curr->get_type()) {
356 case ATOMIC_TRYLOCK: {
357 bool success = !state->locked;
358 curr->set_try_lock(success);
360 get_thread(curr)->set_return_value(0);
363 get_thread(curr)->set_return_value(1);
365 //otherwise fall into the lock case
367 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
368 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
369 // assert_bug("Lock access before initialization");
370 state->locked = get_thread(curr);
371 ModelAction *unlock = get_last_unlock(curr);
372 //synchronize with the previous unlock statement
373 if (unlock != NULL) {
374 synchronize(unlock, curr);
380 /* wake up the other threads */
381 for (unsigned int i = 0;i < get_num_threads();i++) {
382 Thread *t = get_thread(int_to_id(i));
383 Thread *curr_thrd = get_thread(curr);
384 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
388 /* unlock the lock - after checking who was waiting on it */
389 state->locked = NULL;
391 if (fuzzer->shouldWait(curr)) {
392 /* disable this thread */
393 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
394 scheduler->sleep(get_thread(curr));
399 case ATOMIC_TIMEDWAIT:
400 case ATOMIC_UNLOCK: {
401 //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...
403 /* wake up the other threads */
404 for (unsigned int i = 0;i < get_num_threads();i++) {
405 Thread *t = get_thread(int_to_id(i));
406 Thread *curr_thrd = get_thread(curr);
407 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
411 /* unlock the lock - after checking who was waiting on it */
412 state->locked = NULL;
415 case ATOMIC_NOTIFY_ALL: {
416 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
417 //activate all the waiting threads
418 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
419 scheduler->wake(get_thread(rit->getVal()));
424 case ATOMIC_NOTIFY_ONE: {
425 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
426 if (waiters->size() != 0) {
427 Thread * thread = fuzzer->selectNotify(waiters);
428 scheduler->wake(thread);
440 * Process a write ModelAction
441 * @param curr The ModelAction to process
442 * @return True if the mo_graph was updated or promises were resolved
444 void ModelExecution::process_write(ModelAction *curr)
446 w_modification_order(curr);
447 get_thread(curr)->set_return_value(VALUE_NONE);
451 * Process a fence ModelAction
452 * @param curr The ModelAction to process
453 * @return True if synchronization was updated
455 bool ModelExecution::process_fence(ModelAction *curr)
458 * fence-relaxed: no-op
459 * fence-release: only log the occurence (not in this function), for
460 * use in later synchronization
461 * fence-acquire (this function): search for hypothetical release
463 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
465 bool updated = false;
466 if (curr->is_acquire()) {
467 action_list_t *list = &action_trace;
468 sllnode<ModelAction *> * rit;
469 /* Find X : is_read(X) && X --sb-> curr */
470 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
471 ModelAction *act = rit->getVal();
474 if (act->get_tid() != curr->get_tid())
476 /* Stop at the beginning of the thread */
477 if (act->is_thread_start())
479 /* Stop once we reach a prior fence-acquire */
480 if (act->is_fence() && act->is_acquire())
484 /* read-acquire will find its own release sequences */
485 if (act->is_acquire())
488 /* Establish hypothetical release sequences */
489 ClockVector *cv = get_hb_from_write(act->get_reads_from());
490 if (cv != NULL && curr->get_cv()->merge(cv))
498 * @brief Process the current action for thread-related activity
500 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
501 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
502 * synchronization, etc. This function is a no-op for non-THREAD actions
503 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
505 * @param curr The current action
506 * @return True if synchronization was updated or a thread completed
508 void ModelExecution::process_thread_action(ModelAction *curr)
510 switch (curr->get_type()) {
511 case THREAD_CREATE: {
512 thrd_t *thrd = (thrd_t *)curr->get_location();
513 struct thread_params *params = (struct thread_params *)curr->get_value();
514 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
515 curr->set_thread_operand(th);
517 th->set_creation(curr);
520 case PTHREAD_CREATE: {
521 (*(uint32_t *)curr->get_location()) = pthread_counter++;
523 struct pthread_params *params = (struct pthread_params *)curr->get_value();
524 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
525 curr->set_thread_operand(th);
527 th->set_creation(curr);
529 if ( pthread_map.size() < pthread_counter )
530 pthread_map.resize( pthread_counter );
531 pthread_map[ pthread_counter-1 ] = th;
536 Thread *blocking = curr->get_thread_operand();
537 ModelAction *act = get_last_action(blocking->get_id());
538 synchronize(act, curr);
542 Thread *blocking = curr->get_thread_operand();
543 ModelAction *act = get_last_action(blocking->get_id());
544 synchronize(act, curr);
545 break; // WL: to be add (modified)
548 case THREADONLY_FINISH:
549 case THREAD_FINISH: {
550 Thread *th = get_thread(curr);
551 if (curr->get_type() == THREAD_FINISH &&
552 th == model->getInitThread()) {
558 /* Wake up any joining threads */
559 for (unsigned int i = 0;i < get_num_threads();i++) {
560 Thread *waiting = get_thread(int_to_id(i));
561 if (waiting->waiting_on() == th &&
562 waiting->get_pending()->is_thread_join())
563 scheduler->wake(waiting);
572 Thread *th = get_thread(curr);
573 th->set_pending(curr);
574 scheduler->add_sleep(th);
583 * Initialize the current action by performing one or more of the following
584 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
585 * manipulating backtracking sets, allocating and
586 * initializing clock vectors, and computing the promises to fulfill.
588 * @param curr The current action, as passed from the user context; may be
589 * freed/invalidated after the execution of this function, with a different
590 * action "returned" its place (pass-by-reference)
591 * @return True if curr is a newly-explored action; false otherwise
593 bool ModelExecution::initialize_curr_action(ModelAction **curr)
595 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
596 ModelAction *newcurr = process_rmw(*curr);
602 ModelAction *newcurr = *curr;
604 newcurr->set_seq_number(get_next_seq_num());
605 /* Always compute new clock vector */
606 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
608 /* Assign most recent release fence */
609 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
611 return true; /* This was a new ModelAction */
616 * @brief Establish reads-from relation between two actions
618 * Perform basic operations involved with establishing a concrete rf relation,
619 * including setting the ModelAction data and checking for release sequences.
621 * @param act The action that is reading (must be a read)
622 * @param rf The action from which we are reading (must be a write)
624 * @return True if this read established synchronization
627 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
630 ASSERT(rf->is_write());
632 act->set_read_from(rf);
633 if (act->is_acquire()) {
634 ClockVector *cv = get_hb_from_write(rf);
637 act->get_cv()->merge(cv);
642 * @brief Synchronizes two actions
644 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
645 * This function performs the synchronization as well as providing other hooks
646 * for other checks along with synchronization.
648 * @param first The left-hand side of the synchronizes-with relation
649 * @param second The right-hand side of the synchronizes-with relation
650 * @return True if the synchronization was successful (i.e., was consistent
651 * with the execution order); false otherwise
653 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
655 if (*second < *first) {
656 ASSERT(0); //This should not happend
659 return second->synchronize_with(first);
663 * @brief Check whether a model action is enabled.
665 * Checks whether an operation would be successful (i.e., is a lock already
666 * locked, or is the joined thread already complete).
668 * For yield-blocking, yields are never enabled.
670 * @param curr is the ModelAction to check whether it is enabled.
671 * @return a bool that indicates whether the action is enabled.
673 bool ModelExecution::check_action_enabled(ModelAction *curr) {
674 if (curr->is_lock()) {
675 cdsc::mutex *lock = curr->get_mutex();
676 struct cdsc::mutex_state *state = lock->get_state();
679 } else if (curr->is_thread_join()) {
680 Thread *blocking = curr->get_thread_operand();
681 if (!blocking->is_complete()) {
684 } else if (curr->is_sleep()) {
685 if (!fuzzer->shouldSleep(curr))
693 * This is the heart of the model checker routine. It performs model-checking
694 * actions corresponding to a given "current action." Among other processes, it
695 * calculates reads-from relationships, updates synchronization clock vectors,
696 * forms a memory_order constraints graph, and handles replay/backtrack
697 * execution when running permutations of previously-observed executions.
699 * @param curr The current action to process
700 * @return The ModelAction that is actually executed; may be different than
703 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
706 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
707 bool newly_explored = initialize_curr_action(&curr);
711 wake_up_sleeping_actions(curr);
713 /* Add uninitialized actions to lists */
714 if (!second_part_of_rmw)
715 add_uninit_action_to_lists(curr);
717 SnapVector<ModelAction *> * rf_set = NULL;
718 /* Build may_read_from set for newly-created actions */
719 if (newly_explored && curr->is_read())
720 rf_set = build_may_read_from(curr);
722 if (curr->is_read() && !second_part_of_rmw) {
723 process_read(curr, rf_set);
726 ASSERT(rf_set == NULL);
728 /* Add the action to lists */
729 if (!second_part_of_rmw)
730 add_action_to_lists(curr);
732 if (curr->is_write())
733 add_write_to_lists(curr);
735 process_thread_action(curr);
737 if (curr->is_write())
740 if (curr->is_fence())
743 if (curr->is_mutex_op())
749 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
750 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
751 ModelAction *lastread = get_last_action(act->get_tid());
752 lastread->process_rmw(act);
754 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
760 * @brief Updates the mo_graph with the constraints imposed from the current
763 * Basic idea is the following: Go through each other thread and find
764 * the last action that happened before our read. Two cases:
766 * -# The action is a write: that write must either occur before
767 * the write we read from or be the write we read from.
768 * -# The action is a read: the write that that action read from
769 * must occur before the write we read from or be the same write.
771 * @param curr The current action. Must be a read.
772 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
773 * @param check_only If true, then only check whether the current action satisfies
774 * read modification order or not, without modifiying priorset and canprune.
776 * @return True if modification order edges were added; false otherwise
779 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
780 SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
782 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
784 ASSERT(curr->is_read());
786 /* Last SC fence in the current thread */
787 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
789 int tid = curr->get_tid();
790 ModelAction *prev_same_thread = NULL;
791 /* Iterate over all threads */
792 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
793 /* Last SC fence in thread tid */
794 ModelAction *last_sc_fence_thread_local = NULL;
796 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
798 /* Last SC fence in thread tid, before last SC fence in current thread */
799 ModelAction *last_sc_fence_thread_before = NULL;
800 if (last_sc_fence_local)
801 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
803 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
804 if (prev_same_thread != NULL &&
805 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
806 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
810 /* Iterate over actions in thread, starting from most recent */
811 action_list_t *list = &(*thrd_lists)[tid];
812 sllnode<ModelAction *> * rit;
813 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
814 ModelAction *act = rit->getVal();
819 /* Don't want to add reflexive edges on 'rf' */
820 if (act->equals(rf)) {
821 if (act->happens_before(curr))
827 if (act->is_write()) {
828 /* C++, Section 29.3 statement 5 */
829 if (curr->is_seqcst() && last_sc_fence_thread_local &&
830 *act < *last_sc_fence_thread_local) {
831 if (mo_graph->checkReachable(rf, act))
834 priorset->push_back(act);
837 /* C++, Section 29.3 statement 4 */
838 else if (act->is_seqcst() && last_sc_fence_local &&
839 *act < *last_sc_fence_local) {
840 if (mo_graph->checkReachable(rf, act))
843 priorset->push_back(act);
846 /* C++, Section 29.3 statement 6 */
847 else if (last_sc_fence_thread_before &&
848 *act < *last_sc_fence_thread_before) {
849 if (mo_graph->checkReachable(rf, act))
852 priorset->push_back(act);
858 * Include at most one act per-thread that "happens
861 if (act->happens_before(curr)) {
863 if (last_sc_fence_local == NULL ||
864 (*last_sc_fence_local < *act)) {
865 prev_same_thread = act;
868 if (act->is_write()) {
869 if (mo_graph->checkReachable(rf, act))
872 priorset->push_back(act);
874 const ModelAction *prevrf = act->get_reads_from();
875 if (!prevrf->equals(rf)) {
876 if (mo_graph->checkReachable(rf, prevrf))
879 priorset->push_back(prevrf);
881 if (act->get_tid() == curr->get_tid()) {
882 //Can prune curr from obj list
896 * Updates the mo_graph with the constraints imposed from the current write.
898 * Basic idea is the following: Go through each other thread and find
899 * the lastest action that happened before our write. Two cases:
901 * (1) The action is a write => that write must occur before
904 * (2) The action is a read => the write that that action read from
905 * must occur before the current write.
907 * This method also handles two other issues:
909 * (I) Sequential Consistency: Making sure that if the current write is
910 * seq_cst, that it occurs after the previous seq_cst write.
912 * (II) Sending the write back to non-synchronizing reads.
914 * @param curr The current action. Must be a write.
915 * @param send_fv A vector for stashing reads to which we may pass our future
916 * value. If NULL, then don't record any future values.
917 * @return True if modification order edges were added; false otherwise
919 void ModelExecution::w_modification_order(ModelAction *curr)
921 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
923 ASSERT(curr->is_write());
925 SnapList<ModelAction *> edgeset;
927 if (curr->is_seqcst()) {
928 /* We have to at least see the last sequentially consistent write,
929 so we are initialized. */
930 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
931 if (last_seq_cst != NULL) {
932 edgeset.push_back(last_seq_cst);
934 //update map for next query
935 obj_last_sc_map.put(curr->get_location(), curr);
938 /* Last SC fence in the current thread */
939 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
941 /* Iterate over all threads */
942 for (i = 0;i < thrd_lists->size();i++) {
943 /* Last SC fence in thread i, before last SC fence in current thread */
944 ModelAction *last_sc_fence_thread_before = NULL;
945 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
946 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
948 /* Iterate over actions in thread, starting from most recent */
949 action_list_t *list = &(*thrd_lists)[i];
950 sllnode<ModelAction*>* rit;
951 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
952 ModelAction *act = rit->getVal();
955 * 1) If RMW and it actually read from something, then we
956 * already have all relevant edges, so just skip to next
959 * 2) If RMW and it didn't read from anything, we should
960 * whatever edge we can get to speed up convergence.
962 * 3) If normal write, we need to look at earlier actions, so
963 * continue processing list.
965 if (curr->is_rmw()) {
966 if (curr->get_reads_from() != NULL)
974 /* C++, Section 29.3 statement 7 */
975 if (last_sc_fence_thread_before && act->is_write() &&
976 *act < *last_sc_fence_thread_before) {
977 edgeset.push_back(act);
982 * Include at most one act per-thread that "happens
985 if (act->happens_before(curr)) {
987 * Note: if act is RMW, just add edge:
989 * The following edge should be handled elsewhere:
990 * readfrom(act) --mo--> act
993 edgeset.push_back(act);
994 else if (act->is_read()) {
995 //if previous read accessed a null, just keep going
996 edgeset.push_back(act->get_reads_from());
1002 mo_graph->addEdges(&edgeset, curr);
1007 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1008 * some constraints. This method checks one the following constraint (others
1009 * require compiler support):
1011 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1012 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1014 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1016 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1018 /* Iterate over all threads */
1019 for (i = 0;i < thrd_lists->size();i++) {
1020 const ModelAction *write_after_read = NULL;
1022 /* Iterate over actions in thread, starting from most recent */
1023 action_list_t *list = &(*thrd_lists)[i];
1024 sllnode<ModelAction *>* rit;
1025 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1026 ModelAction *act = rit->getVal();
1028 /* Don't disallow due to act == reader */
1029 if (!reader->happens_before(act) || reader == act)
1031 else if (act->is_write())
1032 write_after_read = act;
1033 else if (act->is_read() && act->get_reads_from() != NULL)
1034 write_after_read = act->get_reads_from();
1037 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1044 * Computes the clock vector that happens before propagates from this write.
1046 * @param rf The action that might be part of a release sequence. Must be a
1048 * @return ClockVector of happens before relation.
1051 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1052 SnapVector<ModelAction *> * processset = NULL;
1053 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1054 ASSERT(rf->is_write());
1055 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1057 if (processset == NULL)
1058 processset = new SnapVector<ModelAction *>();
1059 processset->push_back(rf);
1062 int i = (processset == NULL) ? 0 : processset->size();
1064 ClockVector * vec = NULL;
1066 if (rf->get_rfcv() != NULL) {
1067 vec = rf->get_rfcv();
1068 } else if (rf->is_acquire() && rf->is_release()) {
1070 } else if (rf->is_release() && !rf->is_rmw()) {
1072 } else if (rf->is_release()) {
1073 //have rmw that is release and doesn't have a rfcv
1074 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1077 //operation that isn't release
1078 if (rf->get_last_fence_release()) {
1080 vec = rf->get_last_fence_release()->get_cv();
1082 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1088 rf = (*processset)[i];
1092 if (processset != NULL)
1098 * Performs various bookkeeping operations for the current ModelAction when it is
1099 * the first atomic action occurred at its memory location.
1101 * For instance, adds uninitialized action to the per-object, per-thread action vector
1102 * and to the action trace list of all thread actions.
1104 * @param act is the ModelAction to process.
1106 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1108 int tid = id_to_int(act->get_tid());
1109 ModelAction *uninit = NULL;
1111 SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1112 if (objvec->empty() && act->is_atomic_var()) {
1113 uninit = get_uninitialized_action(act);
1114 uninit_id = id_to_int(uninit->get_tid());
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 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1160 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1161 list->push_back(act);
1164 // Update action trace, a total order of all actions
1165 action_trace.push_back(act);
1167 // Update obj_thrd_map, a per location, per thread, order of actions
1168 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1169 if ((int)vec->size() <= tid) {
1170 uint oldsize = vec->size();
1171 vec->resize(priv->next_thread_id);
1172 for(uint i = oldsize;i < priv->next_thread_id;i++)
1173 new (&(*vec)[i]) action_list_t();
1175 (*vec)[tid].push_back(act);
1177 // Update thrd_last_action, the last action taken by each thrad
1178 if ((int)thrd_last_action.size() <= tid)
1179 thrd_last_action.resize(get_num_threads());
1180 thrd_last_action[tid] = act;
1182 // Update thrd_last_fence_release, the last release fence taken by each thread
1183 if (act->is_fence() && act->is_release()) {
1184 if ((int)thrd_last_fence_release.size() <= tid)
1185 thrd_last_fence_release.resize(get_num_threads());
1186 thrd_last_fence_release[tid] = act;
1189 if (act->is_wait()) {
1190 void *mutex_loc = (void *) act->get_value();
1191 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1193 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1194 if ((int)vec->size() <= tid) {
1195 uint oldsize = vec->size();
1196 vec->resize(priv->next_thread_id);
1197 for(uint i = oldsize;i < priv->next_thread_id;i++)
1198 new (&(*vec)[i]) action_list_t();
1200 (*vec)[tid].push_back(act);
1204 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1205 sllnode<ModelAction*> * rit = list->end();
1206 modelclock_t next_seq = act->get_seq_number();
1207 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1208 list->push_back(act);
1210 for(;rit != NULL;rit=rit->getPrev()) {
1211 if (rit->getVal()->get_seq_number() == next_seq) {
1212 list->insertAfter(rit, act);
1219 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1220 sllnode<ModelAction*> * rit = list->end();
1221 modelclock_t next_seq = act->get_seq_number();
1223 act->create_cv(NULL);
1224 } else if (rit->getVal()->get_seq_number() == next_seq) {
1225 act->create_cv(rit->getVal());
1226 list->push_back(act);
1228 for(;rit != NULL;rit=rit->getPrev()) {
1229 if (rit->getVal()->get_seq_number() == next_seq) {
1230 act->create_cv(rit->getVal());
1231 list->insertAfter(rit, act);
1239 * Performs various bookkeeping operations for a normal write. The
1240 * complication is that we are typically inserting a normal write
1241 * lazily, so we need to insert it into the middle of lists.
1243 * @param act is the ModelAction to add.
1246 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1248 int tid = id_to_int(act->get_tid());
1249 insertIntoActionListAndSetCV(&action_trace, act);
1251 // Update obj_thrd_map, a per location, per thread, order of actions
1252 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1253 if (tid >= (int)vec->size()) {
1254 uint oldsize =vec->size();
1255 vec->resize(priv->next_thread_id);
1256 for(uint i=oldsize;i<priv->next_thread_id;i++)
1257 new (&(*vec)[i]) action_list_t();
1259 insertIntoActionList(&(*vec)[tid],act);
1261 // Update thrd_last_action, the last action taken by each thrad
1262 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1263 thrd_last_action[tid] = act;
1267 void ModelExecution::add_write_to_lists(ModelAction *write) {
1268 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1269 int tid = id_to_int(write->get_tid());
1270 if (tid >= (int)vec->size()) {
1271 uint oldsize =vec->size();
1272 vec->resize(priv->next_thread_id);
1273 for(uint i=oldsize;i<priv->next_thread_id;i++)
1274 new (&(*vec)[i]) action_list_t();
1276 (*vec)[tid].push_back(write);
1280 * @brief Get the last action performed by a particular Thread
1281 * @param tid The thread ID of the Thread in question
1282 * @return The last action in the thread
1284 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1286 int threadid = id_to_int(tid);
1287 if (threadid < (int)thrd_last_action.size())
1288 return thrd_last_action[id_to_int(tid)];
1294 * @brief Get the last fence release performed by a particular Thread
1295 * @param tid The thread ID of the Thread in question
1296 * @return The last fence release in the thread, if one exists; NULL otherwise
1298 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1300 int threadid = id_to_int(tid);
1301 if (threadid < (int)thrd_last_fence_release.size())
1302 return thrd_last_fence_release[id_to_int(tid)];
1308 * Gets the last memory_order_seq_cst write (in the total global sequence)
1309 * performed on a particular object (i.e., memory location), not including the
1311 * @param curr The current ModelAction; also denotes the object location to
1313 * @return The last seq_cst write
1315 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1317 void *location = curr->get_location();
1318 return obj_last_sc_map.get(location);
1322 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1323 * performed in a particular thread, prior to a particular fence.
1324 * @param tid The ID of the thread to check
1325 * @param before_fence The fence from which to begin the search; if NULL, then
1326 * search for the most recent fence in the thread.
1327 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1329 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1331 /* All fences should have location FENCE_LOCATION */
1332 action_list_t *list = obj_map.get(FENCE_LOCATION);
1337 sllnode<ModelAction*>* rit = list->end();
1340 for (;rit != NULL;rit=rit->getPrev())
1341 if (rit->getVal() == before_fence)
1344 ASSERT(rit->getVal() == before_fence);
1348 for (;rit != NULL;rit=rit->getPrev()) {
1349 ModelAction *act = rit->getVal();
1350 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1357 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1358 * location). This function identifies the mutex according to the current
1359 * action, which is presumed to perform on the same mutex.
1360 * @param curr The current ModelAction; also denotes the object location to
1362 * @return The last unlock operation
1364 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1366 void *location = curr->get_location();
1368 action_list_t *list = obj_map.get(location);
1369 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1370 sllnode<ModelAction*>* rit;
1371 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1372 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1373 return rit->getVal();
1377 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1379 ModelAction *parent = get_last_action(tid);
1381 parent = get_thread(tid)->get_creation();
1386 * Returns the clock vector for a given thread.
1387 * @param tid The thread whose clock vector we want
1388 * @return Desired clock vector
1390 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1392 ModelAction *firstaction=get_parent_action(tid);
1393 return firstaction != NULL ? firstaction->get_cv() : NULL;
1396 bool valequals(uint64_t val1, uint64_t val2, int size) {
1399 return ((uint8_t)val1) == ((uint8_t)val2);
1401 return ((uint16_t)val1) == ((uint16_t)val2);
1403 return ((uint32_t)val1) == ((uint32_t)val2);
1413 * Build up an initial set of all past writes that this 'read' action may read
1414 * from, as well as any previously-observed future values that must still be valid.
1416 * @param curr is the current ModelAction that we are exploring; it must be a
1419 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1421 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1423 ASSERT(curr->is_read());
1425 ModelAction *last_sc_write = NULL;
1427 if (curr->is_seqcst())
1428 last_sc_write = get_last_seq_cst_write(curr);
1430 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1432 /* Iterate over all threads */
1433 for (i = 0;i < thrd_lists->size();i++) {
1434 /* Iterate over actions in thread, starting from most recent */
1435 action_list_t *list = &(*thrd_lists)[i];
1436 sllnode<ModelAction *> * rit;
1437 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1438 ModelAction *act = rit->getVal();
1443 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1444 bool allow_read = true;
1446 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1449 /* Need to check whether we will have two RMW reading from the same value */
1450 if (curr->is_rmwr()) {
1451 /* It is okay if we have a failing CAS */
1452 if (!curr->is_rmwrcas() ||
1453 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1454 //Need to make sure we aren't the second RMW
1455 CycleNode * node = mo_graph->getNode_noCreate(act);
1456 if (node != NULL && node->getRMW() != NULL) {
1457 //we are the second RMW
1464 /* Only add feasible reads */
1465 rf_set->push_back(act);
1468 /* Include at most one act per-thread that "happens before" curr */
1469 if (act->happens_before(curr))
1474 if (DBG_ENABLED()) {
1475 model_print("Reached read action:\n");
1477 model_print("End printing read_from_past\n");
1483 * @brief Get an action representing an uninitialized atomic
1485 * This function may create a new one.
1487 * @param curr The current action, which prompts the creation of an UNINIT action
1488 * @return A pointer to the UNINIT ModelAction
1490 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1492 ModelAction *act = curr->get_uninit_action();
1494 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1495 curr->set_uninit_action(act);
1497 act->create_cv(NULL);
1501 static void print_list(action_list_t *list)
1503 sllnode<ModelAction*> *it;
1505 model_print("------------------------------------------------------------------------------------\n");
1506 model_print("# t Action type MO Location Value Rf CV\n");
1507 model_print("------------------------------------------------------------------------------------\n");
1509 unsigned int hash = 0;
1511 for (it = list->begin();it != NULL;it=it->getNext()) {
1512 const ModelAction *act = it->getVal();
1513 if (act->get_seq_number() > 0)
1515 hash = hash^(hash<<3)^(it->getVal()->hash());
1517 model_print("HASH %u\n", hash);
1518 model_print("------------------------------------------------------------------------------------\n");
1521 #if SUPPORT_MOD_ORDER_DUMP
1522 void ModelExecution::dumpGraph(char *filename)
1525 sprintf(buffer, "%s.dot", filename);
1526 FILE *file = fopen(buffer, "w");
1527 fprintf(file, "digraph %s {\n", filename);
1528 mo_graph->dumpNodes(file);
1529 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1531 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1532 ModelAction *act = it->getVal();
1533 if (act->is_read()) {
1534 mo_graph->dot_print_node(file, act);
1535 mo_graph->dot_print_edge(file,
1536 act->get_reads_from(),
1538 "label=\"rf\", color=red, weight=2");
1540 if (thread_array[act->get_tid()]) {
1541 mo_graph->dot_print_edge(file,
1542 thread_array[id_to_int(act->get_tid())],
1544 "label=\"sb\", color=blue, weight=400");
1547 thread_array[act->get_tid()] = act;
1549 fprintf(file, "}\n");
1550 model_free(thread_array);
1555 /** @brief Prints an execution trace summary. */
1556 void ModelExecution::print_summary()
1558 #if SUPPORT_MOD_ORDER_DUMP
1559 char buffername[100];
1560 sprintf(buffername, "exec%04u", get_execution_number());
1561 mo_graph->dumpGraphToFile(buffername);
1562 sprintf(buffername, "graph%04u", get_execution_number());
1563 dumpGraph(buffername);
1566 model_print("Execution trace %d:", get_execution_number());
1567 if (scheduler->all_threads_sleeping())
1568 model_print(" SLEEP-SET REDUNDANT");
1569 if (have_bug_reports())
1570 model_print(" DETECTED BUG(S)");
1574 print_list(&action_trace);
1580 * Add a Thread to the system for the first time. Should only be called once
1582 * @param t The Thread to add
1584 void ModelExecution::add_thread(Thread *t)
1586 unsigned int i = id_to_int(t->get_id());
1587 if (i >= thread_map.size())
1588 thread_map.resize(i + 1);
1590 if (!t->is_model_thread())
1591 scheduler->add_thread(t);
1595 * @brief Get a Thread reference by its ID
1596 * @param tid The Thread's ID
1597 * @return A Thread reference
1599 Thread * ModelExecution::get_thread(thread_id_t tid) const
1601 unsigned int i = id_to_int(tid);
1602 if (i < thread_map.size())
1603 return thread_map[i];
1608 * @brief Get a reference to the Thread in which a ModelAction was executed
1609 * @param act The ModelAction
1610 * @return A Thread reference
1612 Thread * ModelExecution::get_thread(const ModelAction *act) const
1614 return get_thread(act->get_tid());
1618 * @brief Get a Thread reference by its pthread ID
1619 * @param index The pthread's ID
1620 * @return A Thread reference
1622 Thread * ModelExecution::get_pthread(pthread_t pid) {
1628 uint32_t thread_id = x.v;
1629 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1634 * @brief Check if a Thread is currently enabled
1635 * @param t The Thread to check
1636 * @return True if the Thread is currently enabled
1638 bool ModelExecution::is_enabled(Thread *t) const
1640 return scheduler->is_enabled(t);
1644 * @brief Check if a Thread is currently enabled
1645 * @param tid The ID of the Thread to check
1646 * @return True if the Thread is currently enabled
1648 bool ModelExecution::is_enabled(thread_id_t tid) const
1650 return scheduler->is_enabled(tid);
1654 * @brief Select the next thread to execute based on the curren action
1656 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1657 * actions should be followed by the execution of their child thread. In either
1658 * case, the current action should determine the next thread schedule.
1660 * @param curr The current action
1661 * @return The next thread to run, if the current action will determine this
1662 * selection; otherwise NULL
1664 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1666 /* Do not split atomic RMW */
1667 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1668 return get_thread(curr);
1669 /* Follow CREATE with the created thread */
1670 /* which is not needed, because model.cc takes care of this */
1671 if (curr->get_type() == THREAD_CREATE)
1672 return curr->get_thread_operand();
1673 if (curr->get_type() == PTHREAD_CREATE) {
1674 return curr->get_thread_operand();
1679 /** @param act A read atomic action */
1680 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1682 ASSERT(act->is_read());
1684 // Actions paused by fuzzer have their sequence number reset to 0
1685 return act->get_seq_number() == 0;
1689 * Takes the next step in the execution, if possible.
1690 * @param curr The current step to take
1691 * @return Returns the next Thread to run, if any; NULL if this execution
1694 Thread * ModelExecution::take_step(ModelAction *curr)
1696 Thread *curr_thrd = get_thread(curr);
1697 ASSERT(curr_thrd->get_state() == THREAD_READY);
1699 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1700 curr = check_current_action(curr);
1703 /* Process this action in ModelHistory for records */
1704 model->get_history()->process_action( curr, curr->get_tid() );
1706 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1707 scheduler->remove_thread(curr_thrd);
1709 return action_select_next_thread(curr);
1712 Fuzzer * ModelExecution::getFuzzer() {