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),
31 bad_synchronization(false),
35 ~model_snapshot_members() {
36 for (unsigned int i = 0;i < bugs.size();i++)
41 unsigned int next_thread_id;
42 modelclock_t used_sequence_numbers;
43 SnapVector<bug_message *> bugs;
44 /** @brief Incorrectly-ordered synchronization was made */
45 bool bad_synchronization;
51 /** @brief Constructor */
52 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
57 thread_map(2), /* We'll always need at least 2 threads */
61 condvar_waiters_map(),
65 thrd_last_fence_release(),
66 priv(new struct model_snapshot_members ()),
67 mo_graph(new CycleGraph()),
68 fuzzer(new NewFuzzer()),
70 thrd_func_act_lists(),
73 /* Initialize a model-checker thread, for special ModelActions */
74 model_thread = new Thread(get_next_id());
75 add_thread(model_thread);
76 scheduler->register_engine(this);
77 fuzzer->register_engine(m->get_history(), this);
80 /** @brief Destructor */
81 ModelExecution::~ModelExecution()
83 for (unsigned int i = 0;i < get_num_threads();i++)
84 delete get_thread(int_to_id(i));
90 int ModelExecution::get_execution_number() const
92 return model->get_execution_number();
95 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
97 action_list_t *tmp = hash->get(ptr);
99 tmp = new action_list_t();
105 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
107 SnapVector<action_list_t> *tmp = hash->get(ptr);
109 tmp = new SnapVector<action_list_t>();
115 /** @return a thread ID for a new Thread */
116 thread_id_t ModelExecution::get_next_id()
118 return priv->next_thread_id++;
121 /** @return the number of user threads created during this execution */
122 unsigned int ModelExecution::get_num_threads() const
124 return priv->next_thread_id;
127 /** @return a sequence number for a new ModelAction */
128 modelclock_t ModelExecution::get_next_seq_num()
130 return ++priv->used_sequence_numbers;
134 * @brief Should the current action wake up a given thread?
136 * @param curr The current action
137 * @param thread The thread that we might wake up
138 * @return True, if we should wake up the sleeping thread; false otherwise
140 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
142 const ModelAction *asleep = thread->get_pending();
143 /* Don't allow partial RMW to wake anyone up */
146 /* Synchronizing actions may have been backtracked */
147 if (asleep->could_synchronize_with(curr))
149 /* All acquire/release fences and fence-acquire/store-release */
150 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
152 /* Fence-release + store can awake load-acquire on the same location */
153 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
154 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
155 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
158 if (asleep->is_sleep()) {
159 if (fuzzer->shouldWake(asleep))
166 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
168 for (unsigned int i = 0;i < get_num_threads();i++) {
169 Thread *thr = get_thread(int_to_id(i));
170 if (scheduler->is_sleep_set(thr)) {
171 if (should_wake_up(curr, thr))
172 /* Remove this thread from sleep set */
173 scheduler->remove_sleep(thr);
178 /** @brief Alert the model-checker that an incorrectly-ordered
179 * synchronization was made */
180 void ModelExecution::set_bad_synchronization()
182 priv->bad_synchronization = true;
185 bool ModelExecution::assert_bug(const char *msg)
187 priv->bugs.push_back(new bug_message(msg));
189 if (isfeasibleprefix()) {
196 /** @return True, if any bugs have been reported for this execution */
197 bool ModelExecution::have_bug_reports() const
199 return priv->bugs.size() != 0;
202 SnapVector<bug_message *> * ModelExecution::get_bugs() const
208 * Check whether the current trace has triggered an assertion which should halt
211 * @return True, if the execution should be aborted; false otherwise
213 bool ModelExecution::has_asserted() const
215 return priv->asserted;
219 * Trigger a trace assertion which should cause this execution to be halted.
220 * This can be due to a detected bug or due to an infeasibility that should
223 void ModelExecution::set_assert()
225 priv->asserted = true;
229 * Check if we are in a deadlock. Should only be called at the end of an
230 * execution, although it should not give false positives in the middle of an
231 * execution (there should be some ENABLED thread).
233 * @return True if program is in a deadlock; false otherwise
235 bool ModelExecution::is_deadlocked() const
237 bool blocking_threads = false;
238 for (unsigned int i = 0;i < get_num_threads();i++) {
239 thread_id_t tid = int_to_id(i);
242 Thread *t = get_thread(tid);
243 if (!t->is_model_thread() && t->get_pending())
244 blocking_threads = true;
246 return blocking_threads;
250 * Check if this is a complete execution. That is, have all thread completed
251 * execution (rather than exiting because sleep sets have forced a redundant
254 * @return True if the execution is complete.
256 bool ModelExecution::is_complete_execution() const
258 for (unsigned int i = 0;i < get_num_threads();i++)
259 if (is_enabled(int_to_id(i)))
264 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
265 uint64_t value = *((const uint64_t *) location);
266 modelclock_t storeclock;
267 thread_id_t storethread;
268 getStoreThreadAndClock(location, &storethread, &storeclock);
269 setAtomicStoreFlag(location);
270 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
271 act->set_seq_number(storeclock);
272 add_normal_write_to_lists(act);
273 add_write_to_lists(act);
274 w_modification_order(act);
275 model->get_history()->process_action(act, act->get_tid());
280 * Processes a read model action.
281 * @param curr is the read model action to process.
282 * @param rf_set is the set of model actions we can possibly read from
283 * @return True if processing this read updates the mo_graph.
285 void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
287 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
288 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
289 if (hasnonatomicstore) {
290 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
291 rf_set->push_back(nonatomicstore);
295 int index = fuzzer->selectWrite(curr, rf_set);
296 if (index == -1) // no feasible write exists
299 ModelAction *rf = (*rf_set)[index];
302 bool canprune = false;
303 if (r_modification_order(curr, rf, priorset, &canprune)) {
304 for(unsigned int i=0;i<priorset->size();i++) {
305 mo_graph->addEdge((*priorset)[i], rf);
308 get_thread(curr)->set_return_value(curr->get_return_value());
310 if (canprune && curr->get_type() == ATOMIC_READ) {
311 int tid = id_to_int(curr->get_tid());
312 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
317 (*rf_set)[index] = rf_set->back();
323 * Processes a lock, trylock, or unlock model action. @param curr is
324 * the read model action to process.
326 * The try lock operation checks whether the lock is taken. If not,
327 * it falls to the normal lock operation case. If so, it returns
330 * The lock operation has already been checked that it is enabled, so
331 * it just grabs the lock and synchronizes with the previous unlock.
333 * The unlock operation has to re-enable all of the threads that are
334 * waiting on the lock.
336 * @return True if synchronization was updated; false otherwise
338 bool ModelExecution::process_mutex(ModelAction *curr)
340 cdsc::mutex *mutex = curr->get_mutex();
341 struct cdsc::mutex_state *state = NULL;
344 state = mutex->get_state();
346 switch (curr->get_type()) {
347 case ATOMIC_TRYLOCK: {
348 bool success = !state->locked;
349 curr->set_try_lock(success);
351 get_thread(curr)->set_return_value(0);
354 get_thread(curr)->set_return_value(1);
356 //otherwise fall into the lock case
358 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
359 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
360 // assert_bug("Lock access before initialization");
361 state->locked = get_thread(curr);
362 ModelAction *unlock = get_last_unlock(curr);
363 //synchronize with the previous unlock statement
364 if (unlock != NULL) {
365 synchronize(unlock, curr);
371 case ATOMIC_UNLOCK: {
372 //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...
374 /* wake up the other threads */
375 for (unsigned int i = 0;i < get_num_threads();i++) {
376 Thread *t = get_thread(int_to_id(i));
377 Thread *curr_thrd = get_thread(curr);
378 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
382 /* unlock the lock - after checking who was waiting on it */
383 state->locked = NULL;
385 if (!curr->is_wait())
386 break;/* The rest is only for ATOMIC_WAIT */
390 case ATOMIC_NOTIFY_ALL: {
391 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
392 //activate all the waiting threads
393 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
394 scheduler->wake(get_thread(rit->getVal()));
399 case ATOMIC_NOTIFY_ONE: {
400 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
401 if (waiters->size() != 0) {
402 Thread * thread = fuzzer->selectNotify(waiters);
403 scheduler->wake(thread);
415 * Process a write ModelAction
416 * @param curr The ModelAction to process
417 * @return True if the mo_graph was updated or promises were resolved
419 void ModelExecution::process_write(ModelAction *curr)
421 w_modification_order(curr);
422 get_thread(curr)->set_return_value(VALUE_NONE);
426 * Process a fence ModelAction
427 * @param curr The ModelAction to process
428 * @return True if synchronization was updated
430 bool ModelExecution::process_fence(ModelAction *curr)
433 * fence-relaxed: no-op
434 * fence-release: only log the occurence (not in this function), for
435 * use in later synchronization
436 * fence-acquire (this function): search for hypothetical release
438 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
440 bool updated = false;
441 if (curr->is_acquire()) {
442 action_list_t *list = &action_trace;
443 sllnode<ModelAction *> * rit;
444 /* Find X : is_read(X) && X --sb-> curr */
445 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
446 ModelAction *act = rit->getVal();
449 if (act->get_tid() != curr->get_tid())
451 /* Stop at the beginning of the thread */
452 if (act->is_thread_start())
454 /* Stop once we reach a prior fence-acquire */
455 if (act->is_fence() && act->is_acquire())
459 /* read-acquire will find its own release sequences */
460 if (act->is_acquire())
463 /* Establish hypothetical release sequences */
464 ClockVector *cv = get_hb_from_write(act->get_reads_from());
465 if (cv != NULL && curr->get_cv()->merge(cv))
473 * @brief Process the current action for thread-related activity
475 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
476 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
477 * synchronization, etc. This function is a no-op for non-THREAD actions
478 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
480 * @param curr The current action
481 * @return True if synchronization was updated or a thread completed
483 void ModelExecution::process_thread_action(ModelAction *curr)
485 switch (curr->get_type()) {
486 case THREAD_CREATE: {
487 thrd_t *thrd = (thrd_t *)curr->get_location();
488 struct thread_params *params = (struct thread_params *)curr->get_value();
489 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
490 curr->set_thread_operand(th);
492 th->set_creation(curr);
495 case PTHREAD_CREATE: {
496 (*(uint32_t *)curr->get_location()) = pthread_counter++;
498 struct pthread_params *params = (struct pthread_params *)curr->get_value();
499 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
500 curr->set_thread_operand(th);
502 th->set_creation(curr);
504 if ( pthread_map.size() < pthread_counter )
505 pthread_map.resize( pthread_counter );
506 pthread_map[ pthread_counter-1 ] = th;
511 Thread *blocking = curr->get_thread_operand();
512 ModelAction *act = get_last_action(blocking->get_id());
513 synchronize(act, curr);
517 Thread *blocking = curr->get_thread_operand();
518 ModelAction *act = get_last_action(blocking->get_id());
519 synchronize(act, curr);
520 break; // WL: to be add (modified)
523 case THREADONLY_FINISH:
524 case THREAD_FINISH: {
525 Thread *th = get_thread(curr);
526 if (curr->get_type() == THREAD_FINISH &&
527 th == model->getInitThread()) {
533 /* Wake up any joining threads */
534 for (unsigned int i = 0;i < get_num_threads();i++) {
535 Thread *waiting = get_thread(int_to_id(i));
536 if (waiting->waiting_on() == th &&
537 waiting->get_pending()->is_thread_join())
538 scheduler->wake(waiting);
552 * Initialize the current action by performing one or more of the following
553 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
554 * manipulating backtracking sets, allocating and
555 * initializing clock vectors, and computing the promises to fulfill.
557 * @param curr The current action, as passed from the user context; may be
558 * freed/invalidated after the execution of this function, with a different
559 * action "returned" its place (pass-by-reference)
560 * @return True if curr is a newly-explored action; false otherwise
562 bool ModelExecution::initialize_curr_action(ModelAction **curr)
564 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
565 ModelAction *newcurr = process_rmw(*curr);
571 ModelAction *newcurr = *curr;
573 newcurr->set_seq_number(get_next_seq_num());
574 /* Always compute new clock vector */
575 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
577 /* Assign most recent release fence */
578 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
580 return true; /* This was a new ModelAction */
585 * @brief Establish reads-from relation between two actions
587 * Perform basic operations involved with establishing a concrete rf relation,
588 * including setting the ModelAction data and checking for release sequences.
590 * @param act The action that is reading (must be a read)
591 * @param rf The action from which we are reading (must be a write)
593 * @return True if this read established synchronization
596 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
599 ASSERT(rf->is_write());
601 act->set_read_from(rf);
602 if (act->is_acquire()) {
603 ClockVector *cv = get_hb_from_write(rf);
606 act->get_cv()->merge(cv);
611 * @brief Synchronizes two actions
613 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
614 * This function performs the synchronization as well as providing other hooks
615 * for other checks along with synchronization.
617 * @param first The left-hand side of the synchronizes-with relation
618 * @param second The right-hand side of the synchronizes-with relation
619 * @return True if the synchronization was successful (i.e., was consistent
620 * with the execution order); false otherwise
622 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
624 if (*second < *first) {
625 set_bad_synchronization();
628 return second->synchronize_with(first);
632 * @brief Check whether a model action is enabled.
634 * Checks whether an operation would be successful (i.e., is a lock already
635 * locked, or is the joined thread already complete).
637 * For yield-blocking, yields are never enabled.
639 * @param curr is the ModelAction to check whether it is enabled.
640 * @return a bool that indicates whether the action is enabled.
642 bool ModelExecution::check_action_enabled(ModelAction *curr) {
643 if (curr->is_lock()) {
644 cdsc::mutex *lock = curr->get_mutex();
645 struct cdsc::mutex_state *state = lock->get_state();
648 } else if (curr->is_thread_join()) {
649 Thread *blocking = curr->get_thread_operand();
650 if (!blocking->is_complete()) {
653 } else if (curr->is_sleep()) {
654 if (!fuzzer->shouldSleep(curr))
662 * This is the heart of the model checker routine. It performs model-checking
663 * actions corresponding to a given "current action." Among other processes, it
664 * calculates reads-from relationships, updates synchronization clock vectors,
665 * forms a memory_order constraints graph, and handles replay/backtrack
666 * execution when running permutations of previously-observed executions.
668 * @param curr The current action to process
669 * @return The ModelAction that is actually executed; may be different than
672 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
675 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
676 bool newly_explored = initialize_curr_action(&curr);
680 wake_up_sleeping_actions(curr);
682 /* Add uninitialized actions to lists */
683 if (!second_part_of_rmw && curr->get_type() != NOOP)
684 add_uninit_action_to_lists(curr);
686 SnapVector<ModelAction *> * rf_set = NULL;
687 /* Build may_read_from set for newly-created actions */
688 if (newly_explored && curr->is_read())
689 rf_set = build_may_read_from(curr);
691 if (curr->is_read() && !second_part_of_rmw) {
692 process_read(curr, rf_set);
695 ASSERT(rf_set == NULL);
698 /* Add the action to lists */
699 if (!second_part_of_rmw && curr->get_type() != NOOP)
700 add_action_to_lists(curr);
702 if (curr->is_write())
703 add_write_to_lists(curr);
705 process_thread_action(curr);
707 if (curr->is_write())
710 if (curr->is_fence())
713 if (curr->is_mutex_op())
720 * This is the strongest feasibility check available.
721 * @return whether the current trace (partial or complete) must be a prefix of
724 bool ModelExecution::isfeasibleprefix() const
726 return !is_infeasible();
730 * Print disagnostic information about an infeasible execution
731 * @param prefix A string to prefix the output with; if NULL, then a default
732 * message prefix will be provided
734 void ModelExecution::print_infeasibility(const char *prefix) const
738 if (priv->bad_synchronization)
739 ptr += sprintf(ptr, "[bad sw ordering]");
741 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
745 * Check if the current partial trace is infeasible. Does not check any
746 * end-of-execution flags, which might rule out the execution. Thus, this is
747 * useful only for ruling an execution as infeasible.
748 * @return whether the current partial trace is infeasible.
750 bool ModelExecution::is_infeasible() const
752 return priv->bad_synchronization;
755 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
756 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
757 ModelAction *lastread = get_last_action(act->get_tid());
758 lastread->process_rmw(act);
760 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
766 * @brief Updates the mo_graph with the constraints imposed from the current
769 * Basic idea is the following: Go through each other thread and find
770 * the last action that happened before our read. Two cases:
772 * -# The action is a write: that write must either occur before
773 * the write we read from or be the write we read from.
774 * -# The action is a read: the write that that action read from
775 * must occur before the write we read from or be the same write.
777 * @param curr The current action. Must be a read.
778 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
779 * @return True if modification order edges were added; false otherwise
782 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
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))
835 priorset->push_back(act);
838 /* C++, Section 29.3 statement 4 */
839 else if (act->is_seqcst() && last_sc_fence_local &&
840 *act < *last_sc_fence_local) {
841 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))
851 priorset->push_back(act);
857 * Include at most one act per-thread that "happens
860 if (act->happens_before(curr)) {
862 if (last_sc_fence_local == NULL ||
863 (*last_sc_fence_local < *act)) {
864 prev_same_thread = act;
867 if (act->is_write()) {
868 if (mo_graph->checkReachable(rf, act))
870 priorset->push_back(act);
872 const ModelAction *prevrf = act->get_reads_from();
873 if (!prevrf->equals(rf)) {
874 if (mo_graph->checkReachable(rf, prevrf))
876 priorset->push_back(prevrf);
878 if (act->get_tid() == curr->get_tid()) {
879 //Can prune curr from obj list
892 * Updates the mo_graph with the constraints imposed from the current write.
894 * Basic idea is the following: Go through each other thread and find
895 * the lastest action that happened before our write. Two cases:
897 * (1) The action is a write => that write must occur before
900 * (2) The action is a read => the write that that action read from
901 * must occur before the current write.
903 * This method also handles two other issues:
905 * (I) Sequential Consistency: Making sure that if the current write is
906 * seq_cst, that it occurs after the previous seq_cst write.
908 * (II) Sending the write back to non-synchronizing reads.
910 * @param curr The current action. Must be a write.
911 * @param send_fv A vector for stashing reads to which we may pass our future
912 * value. If NULL, then don't record any future values.
913 * @return True if modification order edges were added; false otherwise
915 void ModelExecution::w_modification_order(ModelAction *curr)
917 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
919 ASSERT(curr->is_write());
921 SnapList<ModelAction *> edgeset;
923 if (curr->is_seqcst()) {
924 /* We have to at least see the last sequentially consistent write,
925 so we are initialized. */
926 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
927 if (last_seq_cst != NULL) {
928 edgeset.push_back(last_seq_cst);
930 //update map for next query
931 obj_last_sc_map.put(curr->get_location(), curr);
934 /* Last SC fence in the current thread */
935 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
937 /* Iterate over all threads */
938 for (i = 0;i < thrd_lists->size();i++) {
939 /* Last SC fence in thread i, before last SC fence in current thread */
940 ModelAction *last_sc_fence_thread_before = NULL;
941 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
942 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
944 /* Iterate over actions in thread, starting from most recent */
945 action_list_t *list = &(*thrd_lists)[i];
946 sllnode<ModelAction*>* rit;
947 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
948 ModelAction *act = rit->getVal();
951 * 1) If RMW and it actually read from something, then we
952 * already have all relevant edges, so just skip to next
955 * 2) If RMW and it didn't read from anything, we should
956 * whatever edge we can get to speed up convergence.
958 * 3) If normal write, we need to look at earlier actions, so
959 * continue processing list.
961 if (curr->is_rmw()) {
962 if (curr->get_reads_from() != NULL)
970 /* C++, Section 29.3 statement 7 */
971 if (last_sc_fence_thread_before && act->is_write() &&
972 *act < *last_sc_fence_thread_before) {
973 edgeset.push_back(act);
978 * Include at most one act per-thread that "happens
981 if (act->happens_before(curr)) {
983 * Note: if act is RMW, just add edge:
985 * The following edge should be handled elsewhere:
986 * readfrom(act) --mo--> act
989 edgeset.push_back(act);
990 else if (act->is_read()) {
991 //if previous read accessed a null, just keep going
992 edgeset.push_back(act->get_reads_from());
998 mo_graph->addEdges(&edgeset, curr);
1003 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1004 * some constraints. This method checks one the following constraint (others
1005 * require compiler support):
1007 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1008 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1010 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1012 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1014 /* Iterate over all threads */
1015 for (i = 0;i < thrd_lists->size();i++) {
1016 const ModelAction *write_after_read = NULL;
1018 /* Iterate over actions in thread, starting from most recent */
1019 action_list_t *list = &(*thrd_lists)[i];
1020 sllnode<ModelAction *>* rit;
1021 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1022 ModelAction *act = rit->getVal();
1024 /* Don't disallow due to act == reader */
1025 if (!reader->happens_before(act) || reader == act)
1027 else if (act->is_write())
1028 write_after_read = act;
1029 else if (act->is_read() && act->get_reads_from() != NULL)
1030 write_after_read = act->get_reads_from();
1033 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1040 * Computes the clock vector that happens before propagates from this write.
1042 * @param rf The action that might be part of a release sequence. Must be a
1044 * @return ClockVector of happens before relation.
1047 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1048 SnapVector<ModelAction *> * processset = NULL;
1049 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1050 ASSERT(rf->is_write());
1051 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1053 if (processset == NULL)
1054 processset = new SnapVector<ModelAction *>();
1055 processset->push_back(rf);
1058 int i = (processset == NULL) ? 0 : processset->size();
1060 ClockVector * vec = NULL;
1062 if (rf->get_rfcv() != NULL) {
1063 vec = rf->get_rfcv();
1064 } else if (rf->is_acquire() && rf->is_release()) {
1066 } else if (rf->is_release() && !rf->is_rmw()) {
1068 } else if (rf->is_release()) {
1069 //have rmw that is release and doesn't have a rfcv
1070 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1073 //operation that isn't release
1074 if (rf->get_last_fence_release()) {
1076 vec = rf->get_last_fence_release()->get_cv();
1078 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1084 rf = (*processset)[i];
1088 if (processset != NULL)
1094 * Performs various bookkeeping operations for the current ModelAction when it is
1095 * the first atomic action occurred at its memory location.
1097 * For instance, adds uninitialized action to the per-object, per-thread action vector
1098 * and to the action trace list of all thread actions.
1100 * @param act is the ModelAction to process.
1102 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1104 int tid = id_to_int(act->get_tid());
1105 ModelAction *uninit = NULL;
1107 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1108 if (list->empty() && act->is_atomic_var()) {
1109 uninit = get_uninitialized_action(act);
1110 uninit_id = id_to_int(uninit->get_tid());
1111 list->push_front(uninit);
1112 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1113 if ((int)vec->size() <= uninit_id) {
1114 int oldsize = (int) vec->size();
1115 vec->resize(uninit_id + 1);
1116 for(int i = oldsize; i < uninit_id + 1; i++) {
1117 new (&(*vec)[i]) action_list_t();
1120 (*vec)[uninit_id].push_front(uninit);
1123 // Update action trace, a total order of all actions
1125 action_trace.push_front(uninit);
1127 // Update obj_thrd_map, a per location, per thread, order of actions
1128 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1129 if ((int)vec->size() <= tid) {
1130 uint oldsize = vec->size();
1131 vec->resize(priv->next_thread_id);
1132 for(uint i = oldsize; i < priv->next_thread_id; i++)
1133 new (&(*vec)[i]) action_list_t();
1136 (*vec)[uninit_id].push_front(uninit);
1138 // Update thrd_last_action, the last action taken by each thrad
1139 if ((int)thrd_last_action.size() <= tid)
1140 thrd_last_action.resize(get_num_threads());
1142 thrd_last_action[uninit_id] = uninit;
1147 * Performs various bookkeeping operations for the current ModelAction. For
1148 * instance, adds action to the per-object, per-thread action vector and to the
1149 * action trace list of all thread actions.
1151 * @param act is the ModelAction to add.
1153 void ModelExecution::add_action_to_lists(ModelAction *act)
1155 int tid = id_to_int(act->get_tid());
1156 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1157 list->push_back(act);
1159 // Update action trace, a total order of all actions
1160 action_trace.push_back(act);
1162 // Update obj_thrd_map, a per location, per thread, order of actions
1163 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1164 if ((int)vec->size() <= tid) {
1165 uint oldsize = vec->size();
1166 vec->resize(priv->next_thread_id);
1167 for(uint i = oldsize; i < priv->next_thread_id; i++)
1168 new (&(*vec)[i]) action_list_t();
1170 (*vec)[tid].push_back(act);
1172 // Update thrd_last_action, the last action taken by each thrad
1173 if ((int)thrd_last_action.size() <= tid)
1174 thrd_last_action.resize(get_num_threads());
1175 thrd_last_action[tid] = act;
1177 // Update thrd_last_fence_release, the last release fence taken by each thread
1178 if (act->is_fence() && act->is_release()) {
1179 if ((int)thrd_last_fence_release.size() <= tid)
1180 thrd_last_fence_release.resize(get_num_threads());
1181 thrd_last_fence_release[tid] = act;
1184 if (act->is_wait()) {
1185 void *mutex_loc = (void *) act->get_value();
1186 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1188 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1189 if ((int)vec->size() <= tid) {
1190 uint oldsize = vec->size();
1191 vec->resize(priv->next_thread_id);
1192 for(uint i = oldsize; i < priv->next_thread_id; i++)
1193 new (&(*vec)[i]) action_list_t();
1195 (*vec)[tid].push_back(act);
1199 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1200 sllnode<ModelAction*> * rit = list->end();
1201 modelclock_t next_seq = act->get_seq_number();
1202 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1203 list->push_back(act);
1205 for(;rit != NULL;rit=rit->getPrev()) {
1206 if (rit->getVal()->get_seq_number() == next_seq) {
1207 list->insertAfter(rit, act);
1214 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1215 sllnode<ModelAction*> * rit = list->end();
1216 modelclock_t next_seq = act->get_seq_number();
1218 act->create_cv(NULL);
1219 } else if (rit->getVal()->get_seq_number() == next_seq) {
1220 act->create_cv(rit->getVal());
1221 list->push_back(act);
1223 for(;rit != NULL;rit=rit->getPrev()) {
1224 if (rit->getVal()->get_seq_number() == next_seq) {
1225 act->create_cv(rit->getVal());
1226 list->insertAfter(rit, act);
1234 * Performs various bookkeeping operations for a normal write. The
1235 * complication is that we are typically inserting a normal write
1236 * lazily, so we need to insert it into the middle of lists.
1238 * @param act is the ModelAction to add.
1241 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1243 int tid = id_to_int(act->get_tid());
1244 insertIntoActionListAndSetCV(&action_trace, act);
1246 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1247 insertIntoActionList(list, act);
1249 // Update obj_thrd_map, a per location, per thread, order of actions
1250 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1251 if (tid >= (int)vec->size()) {
1252 uint oldsize =vec->size();
1253 vec->resize(priv->next_thread_id);
1254 for(uint i=oldsize;i<priv->next_thread_id;i++)
1255 new (&(*vec)[i]) action_list_t();
1257 insertIntoActionList(&(*vec)[tid],act);
1259 // Update thrd_last_action, the last action taken by each thrad
1260 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1261 thrd_last_action[tid] = act;
1265 void ModelExecution::add_write_to_lists(ModelAction *write) {
1266 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1267 int tid = id_to_int(write->get_tid());
1268 if (tid >= (int)vec->size()) {
1269 uint oldsize =vec->size();
1270 vec->resize(priv->next_thread_id);
1271 for(uint i=oldsize;i<priv->next_thread_id;i++)
1272 new (&(*vec)[i]) action_list_t();
1274 (*vec)[tid].push_back(write);
1278 * @brief Get the last action performed by a particular Thread
1279 * @param tid The thread ID of the Thread in question
1280 * @return The last action in the thread
1282 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1284 int threadid = id_to_int(tid);
1285 if (threadid < (int)thrd_last_action.size())
1286 return thrd_last_action[id_to_int(tid)];
1292 * @brief Get the last fence release performed by a particular Thread
1293 * @param tid The thread ID of the Thread in question
1294 * @return The last fence release in the thread, if one exists; NULL otherwise
1296 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1298 int threadid = id_to_int(tid);
1299 if (threadid < (int)thrd_last_fence_release.size())
1300 return thrd_last_fence_release[id_to_int(tid)];
1306 * Gets the last memory_order_seq_cst write (in the total global sequence)
1307 * performed on a particular object (i.e., memory location), not including the
1309 * @param curr The current ModelAction; also denotes the object location to
1311 * @return The last seq_cst write
1313 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1315 void *location = curr->get_location();
1316 return obj_last_sc_map.get(location);
1320 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1321 * performed in a particular thread, prior to a particular fence.
1322 * @param tid The ID of the thread to check
1323 * @param before_fence The fence from which to begin the search; if NULL, then
1324 * search for the most recent fence in the thread.
1325 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1327 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1329 /* All fences should have location FENCE_LOCATION */
1330 action_list_t *list = obj_map.get(FENCE_LOCATION);
1335 sllnode<ModelAction*>* rit = list->end();
1338 for (;rit != NULL;rit=rit->getPrev())
1339 if (rit->getVal() == before_fence)
1342 ASSERT(rit->getVal() == before_fence);
1346 for (;rit != NULL;rit=rit->getPrev()) {
1347 ModelAction *act = rit->getVal();
1348 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1355 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1356 * location). This function identifies the mutex according to the current
1357 * action, which is presumed to perform on the same mutex.
1358 * @param curr The current ModelAction; also denotes the object location to
1360 * @return The last unlock operation
1362 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1364 void *location = curr->get_location();
1366 action_list_t *list = obj_map.get(location);
1367 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1368 sllnode<ModelAction*>* rit;
1369 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1370 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1371 return rit->getVal();
1375 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1377 ModelAction *parent = get_last_action(tid);
1379 parent = get_thread(tid)->get_creation();
1384 * Returns the clock vector for a given thread.
1385 * @param tid The thread whose clock vector we want
1386 * @return Desired clock vector
1388 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1390 ModelAction *firstaction=get_parent_action(tid);
1391 return firstaction != NULL ? firstaction->get_cv() : NULL;
1394 bool valequals(uint64_t val1, uint64_t val2, int size) {
1397 return ((uint8_t)val1) == ((uint8_t)val2);
1399 return ((uint16_t)val1) == ((uint16_t)val2);
1401 return ((uint32_t)val1) == ((uint32_t)val2);
1411 * Build up an initial set of all past writes that this 'read' action may read
1412 * from, as well as any previously-observed future values that must still be valid.
1414 * @param curr is the current ModelAction that we are exploring; it must be a
1417 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1419 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1421 ASSERT(curr->is_read());
1423 ModelAction *last_sc_write = NULL;
1425 if (curr->is_seqcst())
1426 last_sc_write = get_last_seq_cst_write(curr);
1428 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1430 /* Iterate over all threads */
1431 for (i = 0;i < thrd_lists->size();i++) {
1432 /* Iterate over actions in thread, starting from most recent */
1433 action_list_t *list = &(*thrd_lists)[i];
1434 sllnode<ModelAction *> * rit;
1435 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1436 ModelAction *act = rit->getVal();
1441 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1442 bool allow_read = true;
1444 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1447 /* Need to check whether we will have two RMW reading from the same value */
1448 if (curr->is_rmwr()) {
1449 /* It is okay if we have a failing CAS */
1450 if (!curr->is_rmwrcas() ||
1451 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1452 //Need to make sure we aren't the second RMW
1453 CycleNode * node = mo_graph->getNode_noCreate(act);
1454 if (node != NULL && node->getRMW() != NULL) {
1455 //we are the second RMW
1462 /* Only add feasible reads */
1463 rf_set->push_back(act);
1466 /* Include at most one act per-thread that "happens before" curr */
1467 if (act->happens_before(curr))
1472 if (DBG_ENABLED()) {
1473 model_print("Reached read action:\n");
1475 model_print("End printing read_from_past\n");
1481 * @brief Get an action representing an uninitialized atomic
1483 * This function may create a new one.
1485 * @param curr The current action, which prompts the creation of an UNINIT action
1486 * @return A pointer to the UNINIT ModelAction
1488 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1490 ModelAction *act = curr->get_uninit_action();
1492 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1493 curr->set_uninit_action(act);
1495 act->create_cv(NULL);
1499 static void print_list(action_list_t *list)
1501 sllnode<ModelAction*> *it;
1503 model_print("------------------------------------------------------------------------------------\n");
1504 model_print("# t Action type MO Location Value Rf CV\n");
1505 model_print("------------------------------------------------------------------------------------\n");
1507 unsigned int hash = 0;
1509 for (it = list->begin();it != NULL;it=it->getNext()) {
1510 const ModelAction *act = it->getVal();
1511 if (act->get_seq_number() > 0)
1513 hash = hash^(hash<<3)^(it->getVal()->hash());
1515 model_print("HASH %u\n", hash);
1516 model_print("------------------------------------------------------------------------------------\n");
1519 #if SUPPORT_MOD_ORDER_DUMP
1520 void ModelExecution::dumpGraph(char *filename)
1523 sprintf(buffer, "%s.dot", filename);
1524 FILE *file = fopen(buffer, "w");
1525 fprintf(file, "digraph %s {\n", filename);
1526 mo_graph->dumpNodes(file);
1527 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1529 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1530 ModelAction *act = it->getVal();
1531 if (act->is_read()) {
1532 mo_graph->dot_print_node(file, act);
1533 mo_graph->dot_print_edge(file,
1534 act->get_reads_from(),
1536 "label=\"rf\", color=red, weight=2");
1538 if (thread_array[act->get_tid()]) {
1539 mo_graph->dot_print_edge(file,
1540 thread_array[id_to_int(act->get_tid())],
1542 "label=\"sb\", color=blue, weight=400");
1545 thread_array[act->get_tid()] = act;
1547 fprintf(file, "}\n");
1548 model_free(thread_array);
1553 /** @brief Prints an execution trace summary. */
1554 void ModelExecution::print_summary()
1556 #if SUPPORT_MOD_ORDER_DUMP
1557 char buffername[100];
1558 sprintf(buffername, "exec%04u", get_execution_number());
1559 mo_graph->dumpGraphToFile(buffername);
1560 sprintf(buffername, "graph%04u", get_execution_number());
1561 dumpGraph(buffername);
1564 model_print("Execution trace %d:", get_execution_number());
1565 if (isfeasibleprefix()) {
1566 if (scheduler->all_threads_sleeping())
1567 model_print(" SLEEP-SET REDUNDANT");
1568 if (have_bug_reports())
1569 model_print(" DETECTED BUG(S)");
1571 print_infeasibility(" INFEASIBLE");
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())
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();
1680 * Takes the next step in the execution, if possible.
1681 * @param curr The current step to take
1682 * @return Returns the next Thread to run, if any; NULL if this execution
1685 Thread * ModelExecution::take_step(ModelAction *curr)
1687 Thread *curr_thrd = get_thread(curr);
1688 ASSERT(curr_thrd->get_state() == THREAD_READY);
1690 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1691 curr = check_current_action(curr);
1694 /* Process this action in ModelHistory for records */
1695 model->get_history()->process_action( curr, curr->get_tid() );
1697 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1698 scheduler->remove_thread(curr_thrd);
1700 return action_select_next_thread(curr);
1703 Fuzzer * ModelExecution::getFuzzer() {