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);
77 pthread_key_create(&pthreadkey, tlsdestructor);
81 /** @brief Destructor */
82 ModelExecution::~ModelExecution()
84 for (unsigned int i = 0;i < get_num_threads();i++)
85 delete get_thread(int_to_id(i));
91 int ModelExecution::get_execution_number() const
93 return model->get_execution_number();
96 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
98 action_list_t *tmp = hash->get(ptr);
100 tmp = new action_list_t();
106 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
108 SnapVector<action_list_t> *tmp = hash->get(ptr);
110 tmp = new SnapVector<action_list_t>();
116 /** @return a thread ID for a new Thread */
117 thread_id_t ModelExecution::get_next_id()
119 return priv->next_thread_id++;
122 /** @return the number of user threads created during this execution */
123 unsigned int ModelExecution::get_num_threads() const
125 return priv->next_thread_id;
128 /** @return a sequence number for a new ModelAction */
129 modelclock_t ModelExecution::get_next_seq_num()
131 return ++priv->used_sequence_numbers;
134 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
135 void ModelExecution::restore_last_seq_num()
137 priv->used_sequence_numbers--;
141 * @brief Should the current action wake up a given thread?
143 * @param curr The current action
144 * @param thread The thread that we might wake up
145 * @return True, if we should wake up the sleeping thread; false otherwise
147 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
149 const ModelAction *asleep = thread->get_pending();
150 /* Don't allow partial RMW to wake anyone up */
153 /* Synchronizing actions may have been backtracked */
154 if (asleep->could_synchronize_with(curr))
156 /* All acquire/release fences and fence-acquire/store-release */
157 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
159 /* Fence-release + store can awake load-acquire on the same location */
160 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
161 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
162 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
165 /* The sleep is literally sleeping */
166 if (asleep->is_sleep()) {
167 if (fuzzer->shouldWake(asleep))
174 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
176 for (unsigned int i = 0;i < get_num_threads();i++) {
177 Thread *thr = get_thread(int_to_id(i));
178 if (scheduler->is_sleep_set(thr)) {
179 if (should_wake_up(curr, thr)) {
180 /* Remove this thread from sleep set */
181 scheduler->remove_sleep(thr);
182 if (thr->get_pending()->is_sleep())
183 thr->set_wakeup_state(true);
189 void ModelExecution::assert_bug(const char *msg)
191 priv->bugs.push_back(new bug_message(msg));
195 /** @return True, if any bugs have been reported for this execution */
196 bool ModelExecution::have_bug_reports() const
198 return priv->bugs.size() != 0;
201 SnapVector<bug_message *> * ModelExecution::get_bugs() const
207 * Check whether the current trace has triggered an assertion which should halt
210 * @return True, if the execution should be aborted; false otherwise
212 bool ModelExecution::has_asserted() const
214 return priv->asserted;
218 * Trigger a trace assertion which should cause this execution to be halted.
219 * This can be due to a detected bug or due to an infeasibility that should
222 void ModelExecution::set_assert()
224 priv->asserted = true;
228 * Check if we are in a deadlock. Should only be called at the end of an
229 * execution, although it should not give false positives in the middle of an
230 * execution (there should be some ENABLED thread).
232 * @return True if program is in a deadlock; false otherwise
234 bool ModelExecution::is_deadlocked() const
236 bool blocking_threads = false;
237 for (unsigned int i = 0;i < get_num_threads();i++) {
238 thread_id_t tid = int_to_id(i);
241 Thread *t = get_thread(tid);
242 if (!t->is_model_thread() && t->get_pending())
243 blocking_threads = true;
245 return blocking_threads;
249 * Check if this is a complete execution. That is, have all thread completed
250 * execution (rather than exiting because sleep sets have forced a redundant
253 * @return True if the execution is complete.
255 bool ModelExecution::is_complete_execution() const
257 for (unsigned int i = 0;i < get_num_threads();i++)
258 if (is_enabled(int_to_id(i)))
263 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
264 uint64_t value = *((const uint64_t *) location);
265 modelclock_t storeclock;
266 thread_id_t storethread;
267 getStoreThreadAndClock(location, &storethread, &storeclock);
268 setAtomicStoreFlag(location);
269 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
270 act->set_seq_number(storeclock);
271 add_normal_write_to_lists(act);
272 add_write_to_lists(act);
273 w_modification_order(act);
274 model->get_history()->process_action(act, act->get_tid());
279 * Processes a read model action.
280 * @param curr is the read model action to process.
281 * @param rf_set is the set of model actions we can possibly read from
282 * @return True if processing this read updates the mo_graph.
284 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
286 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
287 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
288 if (hasnonatomicstore) {
289 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
290 rf_set->push_back(nonatomicstore);
293 // Remove writes that violate read modification order
295 while (i < rf_set->size()) {
296 ModelAction * rf = (*rf_set)[i];
297 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
298 (*rf_set)[i] = rf_set->back();
305 int index = fuzzer->selectWrite(curr, rf_set);
307 ModelAction *rf = (*rf_set)[index];
310 bool canprune = false;
311 if (r_modification_order(curr, rf, priorset, &canprune)) {
312 for(unsigned int i=0;i<priorset->size();i++) {
313 mo_graph->addEdge((*priorset)[i], rf);
316 get_thread(curr)->set_return_value(curr->get_return_value());
318 if (canprune && curr->get_type() == ATOMIC_READ) {
319 int tid = id_to_int(curr->get_tid());
320 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
326 /* TODO: Following code not needed anymore */
328 (*rf_set)[index] = rf_set->back();
334 * Processes a lock, trylock, or unlock model action. @param curr is
335 * the read model action to process.
337 * The try lock operation checks whether the lock is taken. If not,
338 * it falls to the normal lock operation case. If so, it returns
341 * The lock operation has already been checked that it is enabled, so
342 * it just grabs the lock and synchronizes with the previous unlock.
344 * The unlock operation has to re-enable all of the threads that are
345 * waiting on the lock.
347 * @return True if synchronization was updated; false otherwise
349 bool ModelExecution::process_mutex(ModelAction *curr)
351 cdsc::mutex *mutex = curr->get_mutex();
352 struct cdsc::mutex_state *state = NULL;
355 state = mutex->get_state();
357 switch (curr->get_type()) {
358 case ATOMIC_TRYLOCK: {
359 bool success = !state->locked;
360 curr->set_try_lock(success);
362 get_thread(curr)->set_return_value(0);
365 get_thread(curr)->set_return_value(1);
367 //otherwise fall into the lock case
369 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
370 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
371 // assert_bug("Lock access before initialization");
372 state->locked = get_thread(curr);
373 ModelAction *unlock = get_last_unlock(curr);
374 //synchronize with the previous unlock statement
375 if (unlock != NULL) {
376 synchronize(unlock, curr);
382 /* wake up the other threads */
383 for (unsigned int i = 0;i < get_num_threads();i++) {
384 Thread *t = get_thread(int_to_id(i));
385 Thread *curr_thrd = get_thread(curr);
386 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
390 /* unlock the lock - after checking who was waiting on it */
391 state->locked = NULL;
393 if (fuzzer->shouldWait(curr)) {
394 /* disable this thread */
395 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
396 scheduler->sleep(get_thread(curr));
401 case ATOMIC_TIMEDWAIT:
402 case ATOMIC_UNLOCK: {
403 //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...
405 /* wake up the other threads */
406 for (unsigned int i = 0;i < get_num_threads();i++) {
407 Thread *t = get_thread(int_to_id(i));
408 Thread *curr_thrd = get_thread(curr);
409 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
413 /* unlock the lock - after checking who was waiting on it */
414 state->locked = NULL;
417 case ATOMIC_NOTIFY_ALL: {
418 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
419 //activate all the waiting threads
420 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
421 scheduler->wake(get_thread(rit->getVal()));
426 case ATOMIC_NOTIFY_ONE: {
427 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
428 if (waiters->size() != 0) {
429 Thread * thread = fuzzer->selectNotify(waiters);
430 scheduler->wake(thread);
442 * Process a write ModelAction
443 * @param curr The ModelAction to process
444 * @return True if the mo_graph was updated or promises were resolved
446 void ModelExecution::process_write(ModelAction *curr)
448 w_modification_order(curr);
449 get_thread(curr)->set_return_value(VALUE_NONE);
453 * Process a fence ModelAction
454 * @param curr The ModelAction to process
455 * @return True if synchronization was updated
457 bool ModelExecution::process_fence(ModelAction *curr)
460 * fence-relaxed: no-op
461 * fence-release: only log the occurence (not in this function), for
462 * use in later synchronization
463 * fence-acquire (this function): search for hypothetical release
465 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
467 bool updated = false;
468 if (curr->is_acquire()) {
469 action_list_t *list = &action_trace;
470 sllnode<ModelAction *> * rit;
471 /* Find X : is_read(X) && X --sb-> curr */
472 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
473 ModelAction *act = rit->getVal();
476 if (act->get_tid() != curr->get_tid())
478 /* Stop at the beginning of the thread */
479 if (act->is_thread_start())
481 /* Stop once we reach a prior fence-acquire */
482 if (act->is_fence() && act->is_acquire())
486 /* read-acquire will find its own release sequences */
487 if (act->is_acquire())
490 /* Establish hypothetical release sequences */
491 ClockVector *cv = get_hb_from_write(act->get_reads_from());
492 if (cv != NULL && curr->get_cv()->merge(cv))
500 * @brief Process the current action for thread-related activity
502 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
503 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
504 * synchronization, etc. This function is a no-op for non-THREAD actions
505 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
507 * @param curr The current action
508 * @return True if synchronization was updated or a thread completed
510 void ModelExecution::process_thread_action(ModelAction *curr)
512 switch (curr->get_type()) {
513 case THREAD_CREATE: {
514 thrd_t *thrd = (thrd_t *)curr->get_location();
515 struct thread_params *params = (struct thread_params *)curr->get_value();
516 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
517 curr->set_thread_operand(th);
519 th->set_creation(curr);
522 case PTHREAD_CREATE: {
523 (*(uint32_t *)curr->get_location()) = pthread_counter++;
525 struct pthread_params *params = (struct pthread_params *)curr->get_value();
526 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
527 curr->set_thread_operand(th);
529 th->set_creation(curr);
531 if ( pthread_map.size() < pthread_counter )
532 pthread_map.resize( pthread_counter );
533 pthread_map[ pthread_counter-1 ] = th;
538 Thread *blocking = curr->get_thread_operand();
539 ModelAction *act = get_last_action(blocking->get_id());
540 synchronize(act, curr);
544 Thread *blocking = curr->get_thread_operand();
545 ModelAction *act = get_last_action(blocking->get_id());
546 synchronize(act, curr);
547 break; // WL: to be add (modified)
550 case THREADONLY_FINISH:
551 case THREAD_FINISH: {
552 Thread *th = get_thread(curr);
553 if (curr->get_type() == THREAD_FINISH &&
554 th == model->getInitThread()) {
560 /* Wake up any joining threads */
561 for (unsigned int i = 0;i < get_num_threads();i++) {
562 Thread *waiting = get_thread(int_to_id(i));
563 if (waiting->waiting_on() == th &&
564 waiting->get_pending()->is_thread_join())
565 scheduler->wake(waiting);
574 Thread *th = get_thread(curr);
575 th->set_pending(curr);
576 scheduler->add_sleep(th);
585 * Initialize the current action by performing one or more of the following
586 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
587 * manipulating backtracking sets, allocating and
588 * initializing clock vectors, and computing the promises to fulfill.
590 * @param curr The current action, as passed from the user context; may be
591 * freed/invalidated after the execution of this function, with a different
592 * action "returned" its place (pass-by-reference)
593 * @return True if curr is a newly-explored action; false otherwise
595 bool ModelExecution::initialize_curr_action(ModelAction **curr)
597 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
598 ModelAction *newcurr = process_rmw(*curr);
604 ModelAction *newcurr = *curr;
606 newcurr->set_seq_number(get_next_seq_num());
607 /* Always compute new clock vector */
608 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
610 /* Assign most recent release fence */
611 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
613 return true; /* This was a new ModelAction */
618 * @brief Establish reads-from relation between two actions
620 * Perform basic operations involved with establishing a concrete rf relation,
621 * including setting the ModelAction data and checking for release sequences.
623 * @param act The action that is reading (must be a read)
624 * @param rf The action from which we are reading (must be a write)
626 * @return True if this read established synchronization
629 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
632 ASSERT(rf->is_write());
634 act->set_read_from(rf);
635 if (act->is_acquire()) {
636 ClockVector *cv = get_hb_from_write(rf);
639 act->get_cv()->merge(cv);
644 * @brief Synchronizes two actions
646 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
647 * This function performs the synchronization as well as providing other hooks
648 * for other checks along with synchronization.
650 * @param first The left-hand side of the synchronizes-with relation
651 * @param second The right-hand side of the synchronizes-with relation
652 * @return True if the synchronization was successful (i.e., was consistent
653 * with the execution order); false otherwise
655 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
657 if (*second < *first) {
658 ASSERT(0); //This should not happend
661 return second->synchronize_with(first);
665 * @brief Check whether a model action is enabled.
667 * Checks whether an operation would be successful (i.e., is a lock already
668 * locked, or is the joined thread already complete).
670 * For yield-blocking, yields are never enabled.
672 * @param curr is the ModelAction to check whether it is enabled.
673 * @return a bool that indicates whether the action is enabled.
675 bool ModelExecution::check_action_enabled(ModelAction *curr) {
676 if (curr->is_lock()) {
677 cdsc::mutex *lock = curr->get_mutex();
678 struct cdsc::mutex_state *state = lock->get_state();
681 } else if (curr->is_thread_join()) {
682 Thread *blocking = curr->get_thread_operand();
683 if (!blocking->is_complete()) {
686 } else if (curr->is_sleep()) {
687 if (!fuzzer->shouldSleep(curr))
695 * This is the heart of the model checker routine. It performs model-checking
696 * actions corresponding to a given "current action." Among other processes, it
697 * calculates reads-from relationships, updates synchronization clock vectors,
698 * forms a memory_order constraints graph, and handles replay/backtrack
699 * execution when running permutations of previously-observed executions.
701 * @param curr The current action to process
702 * @return The ModelAction that is actually executed; may be different than
705 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
708 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
709 bool newly_explored = initialize_curr_action(&curr);
713 wake_up_sleeping_actions(curr);
715 /* Add uninitialized actions to lists */
716 if (!second_part_of_rmw)
717 add_uninit_action_to_lists(curr);
719 SnapVector<ModelAction *> * rf_set = NULL;
720 /* Build may_read_from set for newly-created actions */
721 if (newly_explored && curr->is_read())
722 rf_set = build_may_read_from(curr);
724 if (curr->is_read() && !second_part_of_rmw) {
725 process_read(curr, rf_set);
728 ASSERT(rf_set == NULL);
730 /* Add the action to lists */
731 if (!second_part_of_rmw)
732 add_action_to_lists(curr);
734 if (curr->is_write())
735 add_write_to_lists(curr);
737 process_thread_action(curr);
739 if (curr->is_write())
742 if (curr->is_fence())
745 if (curr->is_mutex_op())
751 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
752 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
753 ModelAction *lastread = get_last_action(act->get_tid());
754 lastread->process_rmw(act);
756 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
762 * @brief Updates the mo_graph with the constraints imposed from the current
765 * Basic idea is the following: Go through each other thread and find
766 * the last action that happened before our read. Two cases:
768 * -# The action is a write: that write must either occur before
769 * the write we read from or be the write we read from.
770 * -# The action is a read: the write that that action read from
771 * must occur before the write we read from or be the same write.
773 * @param curr The current action. Must be a read.
774 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
775 * @param check_only If true, then only check whether the current action satisfies
776 * read modification order or not, without modifiying priorset and canprune.
778 * @return True if modification order edges were added; false otherwise
781 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
782 SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
784 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
786 ASSERT(curr->is_read());
788 /* Last SC fence in the current thread */
789 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
791 int tid = curr->get_tid();
792 ModelAction *prev_same_thread = NULL;
793 /* Iterate over all threads */
794 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
795 /* Last SC fence in thread tid */
796 ModelAction *last_sc_fence_thread_local = NULL;
798 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
800 /* Last SC fence in thread tid, before last SC fence in current thread */
801 ModelAction *last_sc_fence_thread_before = NULL;
802 if (last_sc_fence_local)
803 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
805 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
806 if (prev_same_thread != NULL &&
807 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
808 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
812 /* Iterate over actions in thread, starting from most recent */
813 action_list_t *list = &(*thrd_lists)[tid];
814 sllnode<ModelAction *> * rit;
815 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
816 ModelAction *act = rit->getVal();
821 /* Don't want to add reflexive edges on 'rf' */
822 if (act->equals(rf)) {
823 if (act->happens_before(curr))
829 if (act->is_write()) {
830 /* C++, Section 29.3 statement 5 */
831 if (curr->is_seqcst() && last_sc_fence_thread_local &&
832 *act < *last_sc_fence_thread_local) {
833 if (mo_graph->checkReachable(rf, act))
836 priorset->push_back(act);
839 /* C++, Section 29.3 statement 4 */
840 else if (act->is_seqcst() && last_sc_fence_local &&
841 *act < *last_sc_fence_local) {
842 if (mo_graph->checkReachable(rf, act))
845 priorset->push_back(act);
848 /* C++, Section 29.3 statement 6 */
849 else if (last_sc_fence_thread_before &&
850 *act < *last_sc_fence_thread_before) {
851 if (mo_graph->checkReachable(rf, act))
854 priorset->push_back(act);
860 * Include at most one act per-thread that "happens
863 if (act->happens_before(curr)) {
865 if (last_sc_fence_local == NULL ||
866 (*last_sc_fence_local < *act)) {
867 prev_same_thread = act;
870 if (act->is_write()) {
871 if (mo_graph->checkReachable(rf, act))
874 priorset->push_back(act);
876 const ModelAction *prevrf = act->get_reads_from();
877 if (!prevrf->equals(rf)) {
878 if (mo_graph->checkReachable(rf, prevrf))
881 priorset->push_back(prevrf);
883 if (act->get_tid() == curr->get_tid()) {
884 //Can prune curr from obj list
898 * Updates the mo_graph with the constraints imposed from the current write.
900 * Basic idea is the following: Go through each other thread and find
901 * the lastest action that happened before our write. Two cases:
903 * (1) The action is a write => that write must occur before
906 * (2) The action is a read => the write that that action read from
907 * must occur before the current write.
909 * This method also handles two other issues:
911 * (I) Sequential Consistency: Making sure that if the current write is
912 * seq_cst, that it occurs after the previous seq_cst write.
914 * (II) Sending the write back to non-synchronizing reads.
916 * @param curr The current action. Must be a write.
917 * @param send_fv A vector for stashing reads to which we may pass our future
918 * value. If NULL, then don't record any future values.
919 * @return True if modification order edges were added; false otherwise
921 void ModelExecution::w_modification_order(ModelAction *curr)
923 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
925 ASSERT(curr->is_write());
927 SnapList<ModelAction *> edgeset;
929 if (curr->is_seqcst()) {
930 /* We have to at least see the last sequentially consistent write,
931 so we are initialized. */
932 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
933 if (last_seq_cst != NULL) {
934 edgeset.push_back(last_seq_cst);
936 //update map for next query
937 obj_last_sc_map.put(curr->get_location(), curr);
940 /* Last SC fence in the current thread */
941 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
943 /* Iterate over all threads */
944 for (i = 0;i < thrd_lists->size();i++) {
945 /* Last SC fence in thread i, before last SC fence in current thread */
946 ModelAction *last_sc_fence_thread_before = NULL;
947 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
948 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
950 /* Iterate over actions in thread, starting from most recent */
951 action_list_t *list = &(*thrd_lists)[i];
952 sllnode<ModelAction*>* rit;
953 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
954 ModelAction *act = rit->getVal();
957 * 1) If RMW and it actually read from something, then we
958 * already have all relevant edges, so just skip to next
961 * 2) If RMW and it didn't read from anything, we should
962 * whatever edge we can get to speed up convergence.
964 * 3) If normal write, we need to look at earlier actions, so
965 * continue processing list.
967 if (curr->is_rmw()) {
968 if (curr->get_reads_from() != NULL)
976 /* C++, Section 29.3 statement 7 */
977 if (last_sc_fence_thread_before && act->is_write() &&
978 *act < *last_sc_fence_thread_before) {
979 edgeset.push_back(act);
984 * Include at most one act per-thread that "happens
987 if (act->happens_before(curr)) {
989 * Note: if act is RMW, just add edge:
991 * The following edge should be handled elsewhere:
992 * readfrom(act) --mo--> act
995 edgeset.push_back(act);
996 else if (act->is_read()) {
997 //if previous read accessed a null, just keep going
998 edgeset.push_back(act->get_reads_from());
1004 mo_graph->addEdges(&edgeset, curr);
1009 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1010 * some constraints. This method checks one the following constraint (others
1011 * require compiler support):
1013 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1014 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1016 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1018 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1020 /* Iterate over all threads */
1021 for (i = 0;i < thrd_lists->size();i++) {
1022 const ModelAction *write_after_read = NULL;
1024 /* Iterate over actions in thread, starting from most recent */
1025 action_list_t *list = &(*thrd_lists)[i];
1026 sllnode<ModelAction *>* rit;
1027 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1028 ModelAction *act = rit->getVal();
1030 /* Don't disallow due to act == reader */
1031 if (!reader->happens_before(act) || reader == act)
1033 else if (act->is_write())
1034 write_after_read = act;
1035 else if (act->is_read() && act->get_reads_from() != NULL)
1036 write_after_read = act->get_reads_from();
1039 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1046 * Computes the clock vector that happens before propagates from this write.
1048 * @param rf The action that might be part of a release sequence. Must be a
1050 * @return ClockVector of happens before relation.
1053 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1054 SnapVector<ModelAction *> * processset = NULL;
1055 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1056 ASSERT(rf->is_write());
1057 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1059 if (processset == NULL)
1060 processset = new SnapVector<ModelAction *>();
1061 processset->push_back(rf);
1064 int i = (processset == NULL) ? 0 : processset->size();
1066 ClockVector * vec = NULL;
1068 if (rf->get_rfcv() != NULL) {
1069 vec = rf->get_rfcv();
1070 } else if (rf->is_acquire() && rf->is_release()) {
1072 } else if (rf->is_release() && !rf->is_rmw()) {
1074 } else if (rf->is_release()) {
1075 //have rmw that is release and doesn't have a rfcv
1076 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1079 //operation that isn't release
1080 if (rf->get_last_fence_release()) {
1082 vec = rf->get_last_fence_release()->get_cv();
1084 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1090 rf = (*processset)[i];
1094 if (processset != NULL)
1100 * Performs various bookkeeping operations for the current ModelAction when it is
1101 * the first atomic action occurred at its memory location.
1103 * For instance, adds uninitialized action to the per-object, per-thread action vector
1104 * and to the action trace list of all thread actions.
1106 * @param act is the ModelAction to process.
1108 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1110 int tid = id_to_int(act->get_tid());
1111 ModelAction *uninit = NULL;
1113 SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1114 if (objvec->empty() && act->is_atomic_var()) {
1115 uninit = get_uninitialized_action(act);
1116 uninit_id = id_to_int(uninit->get_tid());
1117 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1118 if ((int)vec->size() <= uninit_id) {
1119 int oldsize = (int) vec->size();
1120 vec->resize(uninit_id + 1);
1121 for(int i = oldsize;i < uninit_id + 1;i++) {
1122 new (&(*vec)[i]) action_list_t();
1125 (*vec)[uninit_id].push_front(uninit);
1128 // Update action trace, a total order of all actions
1130 action_trace.push_front(uninit);
1132 // Update obj_thrd_map, a per location, per thread, order of actions
1133 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1134 if ((int)vec->size() <= tid) {
1135 uint oldsize = vec->size();
1136 vec->resize(priv->next_thread_id);
1137 for(uint i = oldsize;i < priv->next_thread_id;i++)
1138 new (&(*vec)[i]) action_list_t();
1141 (*vec)[uninit_id].push_front(uninit);
1143 // Update thrd_last_action, the last action taken by each thrad
1144 if ((int)thrd_last_action.size() <= tid)
1145 thrd_last_action.resize(get_num_threads());
1147 thrd_last_action[uninit_id] = uninit;
1152 * Performs various bookkeeping operations for the current ModelAction. For
1153 * instance, adds action to the per-object, per-thread action vector and to the
1154 * action trace list of all thread actions.
1156 * @param act is the ModelAction to add.
1158 void ModelExecution::add_action_to_lists(ModelAction *act)
1160 int tid = id_to_int(act->get_tid());
1161 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1162 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1163 list->push_back(act);
1166 // Update action trace, a total order of all actions
1167 action_trace.push_back(act);
1169 // Update obj_thrd_map, a per location, per thread, order of actions
1170 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1171 if ((int)vec->size() <= tid) {
1172 uint oldsize = vec->size();
1173 vec->resize(priv->next_thread_id);
1174 for(uint i = oldsize;i < priv->next_thread_id;i++)
1175 new (&(*vec)[i]) action_list_t();
1177 (*vec)[tid].push_back(act);
1179 // Update thrd_last_action, the last action taken by each thrad
1180 if ((int)thrd_last_action.size() <= tid)
1181 thrd_last_action.resize(get_num_threads());
1182 thrd_last_action[tid] = act;
1184 // Update thrd_last_fence_release, the last release fence taken by each thread
1185 if (act->is_fence() && act->is_release()) {
1186 if ((int)thrd_last_fence_release.size() <= tid)
1187 thrd_last_fence_release.resize(get_num_threads());
1188 thrd_last_fence_release[tid] = act;
1191 if (act->is_wait()) {
1192 void *mutex_loc = (void *) act->get_value();
1193 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1195 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1196 if ((int)vec->size() <= tid) {
1197 uint oldsize = vec->size();
1198 vec->resize(priv->next_thread_id);
1199 for(uint i = oldsize;i < priv->next_thread_id;i++)
1200 new (&(*vec)[i]) action_list_t();
1202 (*vec)[tid].push_back(act);
1206 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1207 sllnode<ModelAction*> * rit = list->end();
1208 modelclock_t next_seq = act->get_seq_number();
1209 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1210 list->push_back(act);
1212 for(;rit != NULL;rit=rit->getPrev()) {
1213 if (rit->getVal()->get_seq_number() == next_seq) {
1214 list->insertAfter(rit, act);
1221 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1222 sllnode<ModelAction*> * rit = list->end();
1223 modelclock_t next_seq = act->get_seq_number();
1225 act->create_cv(NULL);
1226 } else if (rit->getVal()->get_seq_number() == next_seq) {
1227 act->create_cv(rit->getVal());
1228 list->push_back(act);
1230 for(;rit != NULL;rit=rit->getPrev()) {
1231 if (rit->getVal()->get_seq_number() == next_seq) {
1232 act->create_cv(rit->getVal());
1233 list->insertAfter(rit, act);
1241 * Performs various bookkeeping operations for a normal write. The
1242 * complication is that we are typically inserting a normal write
1243 * lazily, so we need to insert it into the middle of lists.
1245 * @param act is the ModelAction to add.
1248 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1250 int tid = id_to_int(act->get_tid());
1251 insertIntoActionListAndSetCV(&action_trace, act);
1253 // Update obj_thrd_map, a per location, per thread, order of actions
1254 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1255 if (tid >= (int)vec->size()) {
1256 uint oldsize =vec->size();
1257 vec->resize(priv->next_thread_id);
1258 for(uint i=oldsize;i<priv->next_thread_id;i++)
1259 new (&(*vec)[i]) action_list_t();
1261 insertIntoActionList(&(*vec)[tid],act);
1263 // Update thrd_last_action, the last action taken by each thrad
1264 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1265 thrd_last_action[tid] = act;
1269 void ModelExecution::add_write_to_lists(ModelAction *write) {
1270 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1271 int tid = id_to_int(write->get_tid());
1272 if (tid >= (int)vec->size()) {
1273 uint oldsize =vec->size();
1274 vec->resize(priv->next_thread_id);
1275 for(uint i=oldsize;i<priv->next_thread_id;i++)
1276 new (&(*vec)[i]) action_list_t();
1278 (*vec)[tid].push_back(write);
1282 * @brief Get the last action performed by a particular Thread
1283 * @param tid The thread ID of the Thread in question
1284 * @return The last action in the thread
1286 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1288 int threadid = id_to_int(tid);
1289 if (threadid < (int)thrd_last_action.size())
1290 return thrd_last_action[id_to_int(tid)];
1296 * @brief Get the last fence release performed by a particular Thread
1297 * @param tid The thread ID of the Thread in question
1298 * @return The last fence release in the thread, if one exists; NULL otherwise
1300 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1302 int threadid = id_to_int(tid);
1303 if (threadid < (int)thrd_last_fence_release.size())
1304 return thrd_last_fence_release[id_to_int(tid)];
1310 * Gets the last memory_order_seq_cst write (in the total global sequence)
1311 * performed on a particular object (i.e., memory location), not including the
1313 * @param curr The current ModelAction; also denotes the object location to
1315 * @return The last seq_cst write
1317 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1319 void *location = curr->get_location();
1320 return obj_last_sc_map.get(location);
1324 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1325 * performed in a particular thread, prior to a particular fence.
1326 * @param tid The ID of the thread to check
1327 * @param before_fence The fence from which to begin the search; if NULL, then
1328 * search for the most recent fence in the thread.
1329 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1331 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1333 /* All fences should have location FENCE_LOCATION */
1334 action_list_t *list = obj_map.get(FENCE_LOCATION);
1339 sllnode<ModelAction*>* rit = list->end();
1342 for (;rit != NULL;rit=rit->getPrev())
1343 if (rit->getVal() == before_fence)
1346 ASSERT(rit->getVal() == before_fence);
1350 for (;rit != NULL;rit=rit->getPrev()) {
1351 ModelAction *act = rit->getVal();
1352 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1359 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1360 * location). This function identifies the mutex according to the current
1361 * action, which is presumed to perform on the same mutex.
1362 * @param curr The current ModelAction; also denotes the object location to
1364 * @return The last unlock operation
1366 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1368 void *location = curr->get_location();
1370 action_list_t *list = obj_map.get(location);
1371 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1372 sllnode<ModelAction*>* rit;
1373 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1374 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1375 return rit->getVal();
1379 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1381 ModelAction *parent = get_last_action(tid);
1383 parent = get_thread(tid)->get_creation();
1388 * Returns the clock vector for a given thread.
1389 * @param tid The thread whose clock vector we want
1390 * @return Desired clock vector
1392 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1394 ModelAction *firstaction=get_parent_action(tid);
1395 return firstaction != NULL ? firstaction->get_cv() : NULL;
1398 bool valequals(uint64_t val1, uint64_t val2, int size) {
1401 return ((uint8_t)val1) == ((uint8_t)val2);
1403 return ((uint16_t)val1) == ((uint16_t)val2);
1405 return ((uint32_t)val1) == ((uint32_t)val2);
1415 * Build up an initial set of all past writes that this 'read' action may read
1416 * from, as well as any previously-observed future values that must still be valid.
1418 * @param curr is the current ModelAction that we are exploring; it must be a
1421 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1423 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1425 ASSERT(curr->is_read());
1427 ModelAction *last_sc_write = NULL;
1429 if (curr->is_seqcst())
1430 last_sc_write = get_last_seq_cst_write(curr);
1432 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1434 /* Iterate over all threads */
1435 for (i = 0;i < thrd_lists->size();i++) {
1436 /* Iterate over actions in thread, starting from most recent */
1437 action_list_t *list = &(*thrd_lists)[i];
1438 sllnode<ModelAction *> * rit;
1439 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1440 ModelAction *act = rit->getVal();
1445 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1446 bool allow_read = true;
1448 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1451 /* Need to check whether we will have two RMW reading from the same value */
1452 if (curr->is_rmwr()) {
1453 /* It is okay if we have a failing CAS */
1454 if (!curr->is_rmwrcas() ||
1455 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1456 //Need to make sure we aren't the second RMW
1457 CycleNode * node = mo_graph->getNode_noCreate(act);
1458 if (node != NULL && node->getRMW() != NULL) {
1459 //we are the second RMW
1466 /* Only add feasible reads */
1467 rf_set->push_back(act);
1470 /* Include at most one act per-thread that "happens before" curr */
1471 if (act->happens_before(curr))
1476 if (DBG_ENABLED()) {
1477 model_print("Reached read action:\n");
1479 model_print("End printing read_from_past\n");
1485 * @brief Get an action representing an uninitialized atomic
1487 * This function may create a new one.
1489 * @param curr The current action, which prompts the creation of an UNINIT action
1490 * @return A pointer to the UNINIT ModelAction
1492 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1494 ModelAction *act = curr->get_uninit_action();
1496 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1497 curr->set_uninit_action(act);
1499 act->create_cv(NULL);
1503 static void print_list(action_list_t *list)
1505 sllnode<ModelAction*> *it;
1507 model_print("------------------------------------------------------------------------------------\n");
1508 model_print("# t Action type MO Location Value Rf CV\n");
1509 model_print("------------------------------------------------------------------------------------\n");
1511 unsigned int hash = 0;
1513 for (it = list->begin();it != NULL;it=it->getNext()) {
1514 const ModelAction *act = it->getVal();
1515 if (act->get_seq_number() > 0)
1517 hash = hash^(hash<<3)^(it->getVal()->hash());
1519 model_print("HASH %u\n", hash);
1520 model_print("------------------------------------------------------------------------------------\n");
1523 #if SUPPORT_MOD_ORDER_DUMP
1524 void ModelExecution::dumpGraph(char *filename)
1527 sprintf(buffer, "%s.dot", filename);
1528 FILE *file = fopen(buffer, "w");
1529 fprintf(file, "digraph %s {\n", filename);
1530 mo_graph->dumpNodes(file);
1531 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1533 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1534 ModelAction *act = it->getVal();
1535 if (act->is_read()) {
1536 mo_graph->dot_print_node(file, act);
1537 mo_graph->dot_print_edge(file,
1538 act->get_reads_from(),
1540 "label=\"rf\", color=red, weight=2");
1542 if (thread_array[act->get_tid()]) {
1543 mo_graph->dot_print_edge(file,
1544 thread_array[id_to_int(act->get_tid())],
1546 "label=\"sb\", color=blue, weight=400");
1549 thread_array[act->get_tid()] = act;
1551 fprintf(file, "}\n");
1552 model_free(thread_array);
1557 /** @brief Prints an execution trace summary. */
1558 void ModelExecution::print_summary()
1560 #if SUPPORT_MOD_ORDER_DUMP
1561 char buffername[100];
1562 sprintf(buffername, "exec%04u", get_execution_number());
1563 mo_graph->dumpGraphToFile(buffername);
1564 sprintf(buffername, "graph%04u", get_execution_number());
1565 dumpGraph(buffername);
1568 model_print("Execution trace %d:", get_execution_number());
1569 if (scheduler->all_threads_sleeping())
1570 model_print(" SLEEP-SET REDUNDANT");
1571 if (have_bug_reports())
1572 model_print(" DETECTED BUG(S)");
1576 print_list(&action_trace);
1582 * Add a Thread to the system for the first time. Should only be called once
1584 * @param t The Thread to add
1586 void ModelExecution::add_thread(Thread *t)
1588 unsigned int i = id_to_int(t->get_id());
1589 if (i >= thread_map.size())
1590 thread_map.resize(i + 1);
1592 if (!t->is_model_thread())
1593 scheduler->add_thread(t);
1597 * @brief Get a Thread reference by its ID
1598 * @param tid The Thread's ID
1599 * @return A Thread reference
1601 Thread * ModelExecution::get_thread(thread_id_t tid) const
1603 unsigned int i = id_to_int(tid);
1604 if (i < thread_map.size())
1605 return thread_map[i];
1610 * @brief Get a reference to the Thread in which a ModelAction was executed
1611 * @param act The ModelAction
1612 * @return A Thread reference
1614 Thread * ModelExecution::get_thread(const ModelAction *act) const
1616 return get_thread(act->get_tid());
1620 * @brief Get a Thread reference by its pthread ID
1621 * @param index The pthread's ID
1622 * @return A Thread reference
1624 Thread * ModelExecution::get_pthread(pthread_t pid) {
1630 uint32_t thread_id = x.v;
1631 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1636 * @brief Check if a Thread is currently enabled
1637 * @param t The Thread to check
1638 * @return True if the Thread is currently enabled
1640 bool ModelExecution::is_enabled(Thread *t) const
1642 return scheduler->is_enabled(t);
1646 * @brief Check if a Thread is currently enabled
1647 * @param tid The ID of the Thread to check
1648 * @return True if the Thread is currently enabled
1650 bool ModelExecution::is_enabled(thread_id_t tid) const
1652 return scheduler->is_enabled(tid);
1656 * @brief Select the next thread to execute based on the curren action
1658 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1659 * actions should be followed by the execution of their child thread. In either
1660 * case, the current action should determine the next thread schedule.
1662 * @param curr The current action
1663 * @return The next thread to run, if the current action will determine this
1664 * selection; otherwise NULL
1666 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1668 /* Do not split atomic RMW */
1669 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1670 return get_thread(curr);
1671 /* Follow CREATE with the created thread */
1672 /* which is not needed, because model.cc takes care of this */
1673 if (curr->get_type() == THREAD_CREATE)
1674 return curr->get_thread_operand();
1675 if (curr->get_type() == PTHREAD_CREATE) {
1676 return curr->get_thread_operand();
1681 /** @param act A read atomic action */
1682 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1684 ASSERT(act->is_read());
1686 // Actions paused by fuzzer have their sequence number reset to 0
1687 return act->get_seq_number() == 0;
1691 * Takes the next step in the execution, if possible.
1692 * @param curr The current step to take
1693 * @return Returns the next Thread to run, if any; NULL if this execution
1696 Thread * ModelExecution::take_step(ModelAction *curr)
1698 Thread *curr_thrd = get_thread(curr);
1699 ASSERT(curr_thrd->get_state() == THREAD_READY);
1701 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1702 curr = check_current_action(curr);
1705 /* Process this action in ModelHistory for records */
1706 model->get_history()->process_action( curr, curr->get_tid() );
1708 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1709 scheduler->remove_thread(curr_thrd);
1711 return action_select_next_thread(curr);
1714 Fuzzer * ModelExecution::getFuzzer() {