11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
34 ~model_snapshot_members() {
35 for (unsigned int i = 0;i < bugs.size();i++)
40 unsigned int next_thread_id;
41 modelclock_t used_sequence_numbers;
42 SnapVector<bug_message *> bugs;
43 /** @brief Incorrectly-ordered synchronization was made */
49 /** @brief Constructor */
50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
55 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
63 thrd_last_fence_release(),
64 priv(new struct model_snapshot_members ()),
65 mo_graph(new CycleGraph()),
66 fuzzer(new NewFuzzer()),
68 thrd_func_act_lists(),
71 /* Initialize a model-checker thread, for special ModelActions */
72 model_thread = new Thread(get_next_id());
73 add_thread(model_thread);
74 fuzzer->register_engine(m->get_history(), this);
75 scheduler->register_engine(this);
78 /** @brief Destructor */
79 ModelExecution::~ModelExecution()
81 for (unsigned int i = 0;i < get_num_threads();i++)
82 delete get_thread(int_to_id(i));
88 int ModelExecution::get_execution_number() const
90 return model->get_execution_number();
93 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
95 action_list_t *tmp = hash->get(ptr);
97 tmp = new action_list_t();
103 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
105 SnapVector<action_list_t> *tmp = hash->get(ptr);
107 tmp = new SnapVector<action_list_t>();
113 /** @return a thread ID for a new Thread */
114 thread_id_t ModelExecution::get_next_id()
116 return priv->next_thread_id++;
119 /** @return the number of user threads created during this execution */
120 unsigned int ModelExecution::get_num_threads() const
122 return priv->next_thread_id;
125 /** @return a sequence number for a new ModelAction */
126 modelclock_t ModelExecution::get_next_seq_num()
128 return ++priv->used_sequence_numbers;
131 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
132 void ModelExecution::restore_last_seq_num()
134 priv->used_sequence_numbers--;
138 * @brief Should the current action wake up a given thread?
140 * @param curr The current action
141 * @param thread The thread that we might wake up
142 * @return True, if we should wake up the sleeping thread; false otherwise
144 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
146 const ModelAction *asleep = thread->get_pending();
147 /* Don't allow partial RMW to wake anyone up */
150 /* Synchronizing actions may have been backtracked */
151 if (asleep->could_synchronize_with(curr))
153 /* All acquire/release fences and fence-acquire/store-release */
154 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
156 /* Fence-release + store can awake load-acquire on the same location */
157 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
158 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
159 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
162 /* The sleep is literally sleeping */
163 if (asleep->is_sleep()) {
164 if (fuzzer->shouldWake(asleep))
171 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
173 for (unsigned int i = 0;i < get_num_threads();i++) {
174 Thread *thr = get_thread(int_to_id(i));
175 if (scheduler->is_sleep_set(thr)) {
176 if (should_wake_up(curr, thr)) {
177 /* Remove this thread from sleep set */
178 scheduler->remove_sleep(thr);
179 if (thr->get_pending()->is_sleep())
180 thr->set_wakeup_state(true);
186 void ModelExecution::assert_bug(const char *msg)
188 priv->bugs.push_back(new bug_message(msg));
192 /** @return True, if any bugs have been reported for this execution */
193 bool ModelExecution::have_bug_reports() const
195 return priv->bugs.size() != 0;
198 SnapVector<bug_message *> * ModelExecution::get_bugs() const
204 * Check whether the current trace has triggered an assertion which should halt
207 * @return True, if the execution should be aborted; false otherwise
209 bool ModelExecution::has_asserted() const
211 return priv->asserted;
215 * Trigger a trace assertion which should cause this execution to be halted.
216 * This can be due to a detected bug or due to an infeasibility that should
219 void ModelExecution::set_assert()
221 priv->asserted = true;
225 * Check if we are in a deadlock. Should only be called at the end of an
226 * execution, although it should not give false positives in the middle of an
227 * execution (there should be some ENABLED thread).
229 * @return True if program is in a deadlock; false otherwise
231 bool ModelExecution::is_deadlocked() const
233 bool blocking_threads = false;
234 for (unsigned int i = 0;i < get_num_threads();i++) {
235 thread_id_t tid = int_to_id(i);
238 Thread *t = get_thread(tid);
239 if (!t->is_model_thread() && t->get_pending())
240 blocking_threads = true;
242 return blocking_threads;
246 * Check if this is a complete execution. That is, have all thread completed
247 * execution (rather than exiting because sleep sets have forced a redundant
250 * @return True if the execution is complete.
252 bool ModelExecution::is_complete_execution() const
254 for (unsigned int i = 0;i < get_num_threads();i++)
255 if (is_enabled(int_to_id(i)))
260 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
261 uint64_t value = *((const uint64_t *) location);
262 modelclock_t storeclock;
263 thread_id_t storethread;
264 getStoreThreadAndClock(location, &storethread, &storeclock);
265 setAtomicStoreFlag(location);
266 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
267 act->set_seq_number(storeclock);
268 add_normal_write_to_lists(act);
269 add_write_to_lists(act);
270 w_modification_order(act);
271 model->get_history()->process_action(act, act->get_tid());
276 * Processes a read model action.
277 * @param curr is the read model action to process.
278 * @param rf_set is the set of model actions we can possibly read from
279 * @return True if processing this read updates the mo_graph.
281 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
283 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
284 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
285 if (hasnonatomicstore) {
286 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
287 rf_set->push_back(nonatomicstore);
290 // Remove writes that violate read modification order
291 for (uint i = 0; i < rf_set->size(); i++) {
292 ModelAction * rf = (*rf_set)[i];
293 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
294 (*rf_set)[i] = rf_set->back();
300 int index = fuzzer->selectWrite(curr, rf_set);
301 if (index == -1)// no feasible write exists
304 ModelAction *rf = (*rf_set)[index];
307 bool canprune = false;
308 if (r_modification_order(curr, rf, priorset, &canprune)) {
309 for(unsigned int i=0;i<priorset->size();i++) {
310 mo_graph->addEdge((*priorset)[i], rf);
313 get_thread(curr)->set_return_value(curr->get_return_value());
315 if (canprune && curr->get_type() == ATOMIC_READ) {
316 int tid = id_to_int(curr->get_tid());
317 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
322 (*rf_set)[index] = rf_set->back();
328 * Processes a lock, trylock, or unlock model action. @param curr is
329 * the read model action to process.
331 * The try lock operation checks whether the lock is taken. If not,
332 * it falls to the normal lock operation case. If so, it returns
335 * The lock operation has already been checked that it is enabled, so
336 * it just grabs the lock and synchronizes with the previous unlock.
338 * The unlock operation has to re-enable all of the threads that are
339 * waiting on the lock.
341 * @return True if synchronization was updated; false otherwise
343 bool ModelExecution::process_mutex(ModelAction *curr)
345 cdsc::mutex *mutex = curr->get_mutex();
346 struct cdsc::mutex_state *state = NULL;
349 state = mutex->get_state();
351 switch (curr->get_type()) {
352 case ATOMIC_TRYLOCK: {
353 bool success = !state->locked;
354 curr->set_try_lock(success);
356 get_thread(curr)->set_return_value(0);
359 get_thread(curr)->set_return_value(1);
361 //otherwise fall into the lock case
363 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
364 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
365 // assert_bug("Lock access before initialization");
366 state->locked = get_thread(curr);
367 ModelAction *unlock = get_last_unlock(curr);
368 //synchronize with the previous unlock statement
369 if (unlock != NULL) {
370 synchronize(unlock, curr);
376 /* wake up the other threads */
377 for (unsigned int i = 0;i < get_num_threads();i++) {
378 Thread *t = get_thread(int_to_id(i));
379 Thread *curr_thrd = get_thread(curr);
380 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
384 /* unlock the lock - after checking who was waiting on it */
385 state->locked = NULL;
387 if (fuzzer->shouldWait(curr)) {
388 /* disable this thread */
389 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
390 scheduler->sleep(get_thread(curr));
395 case ATOMIC_TIMEDWAIT:
396 case ATOMIC_UNLOCK: {
397 //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...
399 /* wake up the other threads */
400 for (unsigned int i = 0;i < get_num_threads();i++) {
401 Thread *t = get_thread(int_to_id(i));
402 Thread *curr_thrd = get_thread(curr);
403 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
407 /* unlock the lock - after checking who was waiting on it */
408 state->locked = NULL;
411 case ATOMIC_NOTIFY_ALL: {
412 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
413 //activate all the waiting threads
414 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
415 scheduler->wake(get_thread(rit->getVal()));
420 case ATOMIC_NOTIFY_ONE: {
421 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
422 if (waiters->size() != 0) {
423 Thread * thread = fuzzer->selectNotify(waiters);
424 scheduler->wake(thread);
436 * Process a write ModelAction
437 * @param curr The ModelAction to process
438 * @return True if the mo_graph was updated or promises were resolved
440 void ModelExecution::process_write(ModelAction *curr)
442 w_modification_order(curr);
443 get_thread(curr)->set_return_value(VALUE_NONE);
447 * Process a fence ModelAction
448 * @param curr The ModelAction to process
449 * @return True if synchronization was updated
451 bool ModelExecution::process_fence(ModelAction *curr)
454 * fence-relaxed: no-op
455 * fence-release: only log the occurence (not in this function), for
456 * use in later synchronization
457 * fence-acquire (this function): search for hypothetical release
459 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
461 bool updated = false;
462 if (curr->is_acquire()) {
463 action_list_t *list = &action_trace;
464 sllnode<ModelAction *> * rit;
465 /* Find X : is_read(X) && X --sb-> curr */
466 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
467 ModelAction *act = rit->getVal();
470 if (act->get_tid() != curr->get_tid())
472 /* Stop at the beginning of the thread */
473 if (act->is_thread_start())
475 /* Stop once we reach a prior fence-acquire */
476 if (act->is_fence() && act->is_acquire())
480 /* read-acquire will find its own release sequences */
481 if (act->is_acquire())
484 /* Establish hypothetical release sequences */
485 ClockVector *cv = get_hb_from_write(act->get_reads_from());
486 if (cv != NULL && curr->get_cv()->merge(cv))
494 * @brief Process the current action for thread-related activity
496 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
497 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
498 * synchronization, etc. This function is a no-op for non-THREAD actions
499 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
501 * @param curr The current action
502 * @return True if synchronization was updated or a thread completed
504 void ModelExecution::process_thread_action(ModelAction *curr)
506 switch (curr->get_type()) {
507 case THREAD_CREATE: {
508 thrd_t *thrd = (thrd_t *)curr->get_location();
509 struct thread_params *params = (struct thread_params *)curr->get_value();
510 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
511 curr->set_thread_operand(th);
513 th->set_creation(curr);
516 case PTHREAD_CREATE: {
517 (*(uint32_t *)curr->get_location()) = pthread_counter++;
519 struct pthread_params *params = (struct pthread_params *)curr->get_value();
520 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
521 curr->set_thread_operand(th);
523 th->set_creation(curr);
525 if ( pthread_map.size() < pthread_counter )
526 pthread_map.resize( pthread_counter );
527 pthread_map[ pthread_counter-1 ] = th;
532 Thread *blocking = curr->get_thread_operand();
533 ModelAction *act = get_last_action(blocking->get_id());
534 synchronize(act, curr);
538 Thread *blocking = curr->get_thread_operand();
539 ModelAction *act = get_last_action(blocking->get_id());
540 synchronize(act, curr);
541 break; // WL: to be add (modified)
544 case THREADONLY_FINISH:
545 case THREAD_FINISH: {
546 Thread *th = get_thread(curr);
547 if (curr->get_type() == THREAD_FINISH &&
548 th == model->getInitThread()) {
554 /* Wake up any joining threads */
555 for (unsigned int i = 0;i < get_num_threads();i++) {
556 Thread *waiting = get_thread(int_to_id(i));
557 if (waiting->waiting_on() == th &&
558 waiting->get_pending()->is_thread_join())
559 scheduler->wake(waiting);
568 Thread *th = get_thread(curr);
569 th->set_pending(curr);
570 scheduler->add_sleep(th);
579 * Initialize the current action by performing one or more of the following
580 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
581 * manipulating backtracking sets, allocating and
582 * initializing clock vectors, and computing the promises to fulfill.
584 * @param curr The current action, as passed from the user context; may be
585 * freed/invalidated after the execution of this function, with a different
586 * action "returned" its place (pass-by-reference)
587 * @return True if curr is a newly-explored action; false otherwise
589 bool ModelExecution::initialize_curr_action(ModelAction **curr)
591 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
592 ModelAction *newcurr = process_rmw(*curr);
598 ModelAction *newcurr = *curr;
600 newcurr->set_seq_number(get_next_seq_num());
601 /* Always compute new clock vector */
602 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
604 /* Assign most recent release fence */
605 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
607 return true; /* This was a new ModelAction */
612 * @brief Establish reads-from relation between two actions
614 * Perform basic operations involved with establishing a concrete rf relation,
615 * including setting the ModelAction data and checking for release sequences.
617 * @param act The action that is reading (must be a read)
618 * @param rf The action from which we are reading (must be a write)
620 * @return True if this read established synchronization
623 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
626 ASSERT(rf->is_write());
628 act->set_read_from(rf);
629 if (act->is_acquire()) {
630 ClockVector *cv = get_hb_from_write(rf);
633 act->get_cv()->merge(cv);
638 * @brief Synchronizes two actions
640 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
641 * This function performs the synchronization as well as providing other hooks
642 * for other checks along with synchronization.
644 * @param first The left-hand side of the synchronizes-with relation
645 * @param second The right-hand side of the synchronizes-with relation
646 * @return True if the synchronization was successful (i.e., was consistent
647 * with the execution order); false otherwise
649 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
651 if (*second < *first) {
652 ASSERT(0); //This should not happend
655 return second->synchronize_with(first);
659 * @brief Check whether a model action is enabled.
661 * Checks whether an operation would be successful (i.e., is a lock already
662 * locked, or is the joined thread already complete).
664 * For yield-blocking, yields are never enabled.
666 * @param curr is the ModelAction to check whether it is enabled.
667 * @return a bool that indicates whether the action is enabled.
669 bool ModelExecution::check_action_enabled(ModelAction *curr) {
670 if (curr->is_lock()) {
671 cdsc::mutex *lock = curr->get_mutex();
672 struct cdsc::mutex_state *state = lock->get_state();
675 } else if (curr->is_thread_join()) {
676 Thread *blocking = curr->get_thread_operand();
677 if (!blocking->is_complete()) {
680 } else if (curr->is_sleep()) {
681 if (!fuzzer->shouldSleep(curr))
689 * This is the heart of the model checker routine. It performs model-checking
690 * actions corresponding to a given "current action." Among other processes, it
691 * calculates reads-from relationships, updates synchronization clock vectors,
692 * forms a memory_order constraints graph, and handles replay/backtrack
693 * execution when running permutations of previously-observed executions.
695 * @param curr The current action to process
696 * @return The ModelAction that is actually executed; may be different than
699 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
702 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
703 bool newly_explored = initialize_curr_action(&curr);
707 wake_up_sleeping_actions(curr);
709 /* Add uninitialized actions to lists */
710 if (!second_part_of_rmw)
711 add_uninit_action_to_lists(curr);
713 SnapVector<ModelAction *> * rf_set = NULL;
714 /* Build may_read_from set for newly-created actions */
715 if (newly_explored && curr->is_read())
716 rf_set = build_may_read_from(curr);
718 if (curr->is_read() && !second_part_of_rmw) {
719 process_read(curr, rf_set);
722 /* bool success = process_read(curr, rf_set);
725 return curr; // Do not add action to lists
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 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1114 if (list->empty() && act->is_atomic_var()) {
1115 uninit = get_uninitialized_action(act);
1116 uninit_id = id_to_int(uninit->get_tid());
1117 list->push_front(uninit);
1118 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1119 if ((int)vec->size() <= uninit_id) {
1120 int oldsize = (int) vec->size();
1121 vec->resize(uninit_id + 1);
1122 for(int i = oldsize;i < uninit_id + 1;i++) {
1123 new (&(*vec)[i]) action_list_t();
1126 (*vec)[uninit_id].push_front(uninit);
1129 // Update action trace, a total order of all actions
1131 action_trace.push_front(uninit);
1133 // Update obj_thrd_map, a per location, per thread, order of actions
1134 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1135 if ((int)vec->size() <= tid) {
1136 uint oldsize = vec->size();
1137 vec->resize(priv->next_thread_id);
1138 for(uint i = oldsize;i < priv->next_thread_id;i++)
1139 new (&(*vec)[i]) action_list_t();
1142 (*vec)[uninit_id].push_front(uninit);
1144 // Update thrd_last_action, the last action taken by each thrad
1145 if ((int)thrd_last_action.size() <= tid)
1146 thrd_last_action.resize(get_num_threads());
1148 thrd_last_action[uninit_id] = uninit;
1153 * Performs various bookkeeping operations for the current ModelAction. For
1154 * instance, adds action to the per-object, per-thread action vector and to the
1155 * action trace list of all thread actions.
1157 * @param act is the ModelAction to add.
1159 void ModelExecution::add_action_to_lists(ModelAction *act)
1161 int tid = id_to_int(act->get_tid());
1162 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1163 list->push_back(act);
1165 // Update action trace, a total order of all actions
1166 action_trace.push_back(act);
1168 // Update obj_thrd_map, a per location, per thread, order of actions
1169 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1170 if ((int)vec->size() <= tid) {
1171 uint oldsize = vec->size();
1172 vec->resize(priv->next_thread_id);
1173 for(uint i = oldsize;i < priv->next_thread_id;i++)
1174 new (&(*vec)[i]) action_list_t();
1176 (*vec)[tid].push_back(act);
1178 // Update thrd_last_action, the last action taken by each thrad
1179 if ((int)thrd_last_action.size() <= tid)
1180 thrd_last_action.resize(get_num_threads());
1181 thrd_last_action[tid] = act;
1183 // Update thrd_last_fence_release, the last release fence taken by each thread
1184 if (act->is_fence() && act->is_release()) {
1185 if ((int)thrd_last_fence_release.size() <= tid)
1186 thrd_last_fence_release.resize(get_num_threads());
1187 thrd_last_fence_release[tid] = act;
1190 if (act->is_wait()) {
1191 void *mutex_loc = (void *) act->get_value();
1192 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1194 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1195 if ((int)vec->size() <= tid) {
1196 uint oldsize = vec->size();
1197 vec->resize(priv->next_thread_id);
1198 for(uint i = oldsize;i < priv->next_thread_id;i++)
1199 new (&(*vec)[i]) action_list_t();
1201 (*vec)[tid].push_back(act);
1205 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1206 sllnode<ModelAction*> * rit = list->end();
1207 modelclock_t next_seq = act->get_seq_number();
1208 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1209 list->push_back(act);
1211 for(;rit != NULL;rit=rit->getPrev()) {
1212 if (rit->getVal()->get_seq_number() == next_seq) {
1213 list->insertAfter(rit, act);
1220 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1221 sllnode<ModelAction*> * rit = list->end();
1222 modelclock_t next_seq = act->get_seq_number();
1224 act->create_cv(NULL);
1225 } else if (rit->getVal()->get_seq_number() == next_seq) {
1226 act->create_cv(rit->getVal());
1227 list->push_back(act);
1229 for(;rit != NULL;rit=rit->getPrev()) {
1230 if (rit->getVal()->get_seq_number() == next_seq) {
1231 act->create_cv(rit->getVal());
1232 list->insertAfter(rit, act);
1240 * Performs various bookkeeping operations for a normal write. The
1241 * complication is that we are typically inserting a normal write
1242 * lazily, so we need to insert it into the middle of lists.
1244 * @param act is the ModelAction to add.
1247 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1249 int tid = id_to_int(act->get_tid());
1250 insertIntoActionListAndSetCV(&action_trace, act);
1252 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1253 insertIntoActionList(list, act);
1255 // Update obj_thrd_map, a per location, per thread, order of actions
1256 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1257 if (tid >= (int)vec->size()) {
1258 uint oldsize =vec->size();
1259 vec->resize(priv->next_thread_id);
1260 for(uint i=oldsize;i<priv->next_thread_id;i++)
1261 new (&(*vec)[i]) action_list_t();
1263 insertIntoActionList(&(*vec)[tid],act);
1265 // Update thrd_last_action, the last action taken by each thrad
1266 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1267 thrd_last_action[tid] = act;
1271 void ModelExecution::add_write_to_lists(ModelAction *write) {
1272 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1273 int tid = id_to_int(write->get_tid());
1274 if (tid >= (int)vec->size()) {
1275 uint oldsize =vec->size();
1276 vec->resize(priv->next_thread_id);
1277 for(uint i=oldsize;i<priv->next_thread_id;i++)
1278 new (&(*vec)[i]) action_list_t();
1280 (*vec)[tid].push_back(write);
1284 * @brief Get the last action performed by a particular Thread
1285 * @param tid The thread ID of the Thread in question
1286 * @return The last action in the thread
1288 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1290 int threadid = id_to_int(tid);
1291 if (threadid < (int)thrd_last_action.size())
1292 return thrd_last_action[id_to_int(tid)];
1298 * @brief Get the last fence release performed by a particular Thread
1299 * @param tid The thread ID of the Thread in question
1300 * @return The last fence release in the thread, if one exists; NULL otherwise
1302 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1304 int threadid = id_to_int(tid);
1305 if (threadid < (int)thrd_last_fence_release.size())
1306 return thrd_last_fence_release[id_to_int(tid)];
1312 * Gets the last memory_order_seq_cst write (in the total global sequence)
1313 * performed on a particular object (i.e., memory location), not including the
1315 * @param curr The current ModelAction; also denotes the object location to
1317 * @return The last seq_cst write
1319 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1321 void *location = curr->get_location();
1322 return obj_last_sc_map.get(location);
1326 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1327 * performed in a particular thread, prior to a particular fence.
1328 * @param tid The ID of the thread to check
1329 * @param before_fence The fence from which to begin the search; if NULL, then
1330 * search for the most recent fence in the thread.
1331 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1333 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1335 /* All fences should have location FENCE_LOCATION */
1336 action_list_t *list = obj_map.get(FENCE_LOCATION);
1341 sllnode<ModelAction*>* rit = list->end();
1344 for (;rit != NULL;rit=rit->getPrev())
1345 if (rit->getVal() == before_fence)
1348 ASSERT(rit->getVal() == before_fence);
1352 for (;rit != NULL;rit=rit->getPrev()) {
1353 ModelAction *act = rit->getVal();
1354 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1361 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1362 * location). This function identifies the mutex according to the current
1363 * action, which is presumed to perform on the same mutex.
1364 * @param curr The current ModelAction; also denotes the object location to
1366 * @return The last unlock operation
1368 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1370 void *location = curr->get_location();
1372 action_list_t *list = obj_map.get(location);
1373 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1374 sllnode<ModelAction*>* rit;
1375 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1376 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1377 return rit->getVal();
1381 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1383 ModelAction *parent = get_last_action(tid);
1385 parent = get_thread(tid)->get_creation();
1390 * Returns the clock vector for a given thread.
1391 * @param tid The thread whose clock vector we want
1392 * @return Desired clock vector
1394 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1396 ModelAction *firstaction=get_parent_action(tid);
1397 return firstaction != NULL ? firstaction->get_cv() : NULL;
1400 bool valequals(uint64_t val1, uint64_t val2, int size) {
1403 return ((uint8_t)val1) == ((uint8_t)val2);
1405 return ((uint16_t)val1) == ((uint16_t)val2);
1407 return ((uint32_t)val1) == ((uint32_t)val2);
1417 * Build up an initial set of all past writes that this 'read' action may read
1418 * from, as well as any previously-observed future values that must still be valid.
1420 * @param curr is the current ModelAction that we are exploring; it must be a
1423 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1425 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1427 ASSERT(curr->is_read());
1429 ModelAction *last_sc_write = NULL;
1431 if (curr->is_seqcst())
1432 last_sc_write = get_last_seq_cst_write(curr);
1434 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1436 /* Iterate over all threads */
1437 for (i = 0;i < thrd_lists->size();i++) {
1438 /* Iterate over actions in thread, starting from most recent */
1439 action_list_t *list = &(*thrd_lists)[i];
1440 sllnode<ModelAction *> * rit;
1441 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1442 ModelAction *act = rit->getVal();
1447 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1448 bool allow_read = true;
1450 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1453 /* Need to check whether we will have two RMW reading from the same value */
1454 if (curr->is_rmwr()) {
1455 /* It is okay if we have a failing CAS */
1456 if (!curr->is_rmwrcas() ||
1457 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1458 //Need to make sure we aren't the second RMW
1459 CycleNode * node = mo_graph->getNode_noCreate(act);
1460 if (node != NULL && node->getRMW() != NULL) {
1461 //we are the second RMW
1468 /* Only add feasible reads */
1469 rf_set->push_back(act);
1472 /* Include at most one act per-thread that "happens before" curr */
1473 if (act->happens_before(curr))
1478 if (DBG_ENABLED()) {
1479 model_print("Reached read action:\n");
1481 model_print("End printing read_from_past\n");
1487 * @brief Get an action representing an uninitialized atomic
1489 * This function may create a new one.
1491 * @param curr The current action, which prompts the creation of an UNINIT action
1492 * @return A pointer to the UNINIT ModelAction
1494 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1496 ModelAction *act = curr->get_uninit_action();
1498 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1499 curr->set_uninit_action(act);
1501 act->create_cv(NULL);
1505 static void print_list(action_list_t *list)
1507 sllnode<ModelAction*> *it;
1509 model_print("------------------------------------------------------------------------------------\n");
1510 model_print("# t Action type MO Location Value Rf CV\n");
1511 model_print("------------------------------------------------------------------------------------\n");
1513 unsigned int hash = 0;
1515 for (it = list->begin();it != NULL;it=it->getNext()) {
1516 const ModelAction *act = it->getVal();
1517 if (act->get_seq_number() > 0)
1519 hash = hash^(hash<<3)^(it->getVal()->hash());
1521 model_print("HASH %u\n", hash);
1522 model_print("------------------------------------------------------------------------------------\n");
1525 #if SUPPORT_MOD_ORDER_DUMP
1526 void ModelExecution::dumpGraph(char *filename)
1529 sprintf(buffer, "%s.dot", filename);
1530 FILE *file = fopen(buffer, "w");
1531 fprintf(file, "digraph %s {\n", filename);
1532 mo_graph->dumpNodes(file);
1533 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1535 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1536 ModelAction *act = it->getVal();
1537 if (act->is_read()) {
1538 mo_graph->dot_print_node(file, act);
1539 mo_graph->dot_print_edge(file,
1540 act->get_reads_from(),
1542 "label=\"rf\", color=red, weight=2");
1544 if (thread_array[act->get_tid()]) {
1545 mo_graph->dot_print_edge(file,
1546 thread_array[id_to_int(act->get_tid())],
1548 "label=\"sb\", color=blue, weight=400");
1551 thread_array[act->get_tid()] = act;
1553 fprintf(file, "}\n");
1554 model_free(thread_array);
1559 /** @brief Prints an execution trace summary. */
1560 void ModelExecution::print_summary()
1562 #if SUPPORT_MOD_ORDER_DUMP
1563 char buffername[100];
1564 sprintf(buffername, "exec%04u", get_execution_number());
1565 mo_graph->dumpGraphToFile(buffername);
1566 sprintf(buffername, "graph%04u", get_execution_number());
1567 dumpGraph(buffername);
1570 model_print("Execution trace %d:", get_execution_number());
1571 if (scheduler->all_threads_sleeping())
1572 model_print(" SLEEP-SET REDUNDANT");
1573 if (have_bug_reports())
1574 model_print(" DETECTED BUG(S)");
1578 print_list(&action_trace);
1584 * Add a Thread to the system for the first time. Should only be called once
1586 * @param t The Thread to add
1588 void ModelExecution::add_thread(Thread *t)
1590 unsigned int i = id_to_int(t->get_id());
1591 if (i >= thread_map.size())
1592 thread_map.resize(i + 1);
1594 if (!t->is_model_thread())
1595 scheduler->add_thread(t);
1599 * @brief Get a Thread reference by its ID
1600 * @param tid The Thread's ID
1601 * @return A Thread reference
1603 Thread * ModelExecution::get_thread(thread_id_t tid) const
1605 unsigned int i = id_to_int(tid);
1606 if (i < thread_map.size())
1607 return thread_map[i];
1612 * @brief Get a reference to the Thread in which a ModelAction was executed
1613 * @param act The ModelAction
1614 * @return A Thread reference
1616 Thread * ModelExecution::get_thread(const ModelAction *act) const
1618 return get_thread(act->get_tid());
1622 * @brief Get a Thread reference by its pthread ID
1623 * @param index The pthread's ID
1624 * @return A Thread reference
1626 Thread * ModelExecution::get_pthread(pthread_t pid) {
1632 uint32_t thread_id = x.v;
1633 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1638 * @brief Check if a Thread is currently enabled
1639 * @param t The Thread to check
1640 * @return True if the Thread is currently enabled
1642 bool ModelExecution::is_enabled(Thread *t) const
1644 return scheduler->is_enabled(t);
1648 * @brief Check if a Thread is currently enabled
1649 * @param tid The ID of the Thread to check
1650 * @return True if the Thread is currently enabled
1652 bool ModelExecution::is_enabled(thread_id_t tid) const
1654 return scheduler->is_enabled(tid);
1658 * @brief Select the next thread to execute based on the curren action
1660 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1661 * actions should be followed by the execution of their child thread. In either
1662 * case, the current action should determine the next thread schedule.
1664 * @param curr The current action
1665 * @return The next thread to run, if the current action will determine this
1666 * selection; otherwise NULL
1668 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1670 /* Do not split atomic RMW */
1671 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1672 return get_thread(curr);
1673 /* Follow CREATE with the created thread */
1674 /* which is not needed, because model.cc takes care of this */
1675 if (curr->get_type() == THREAD_CREATE)
1676 return curr->get_thread_operand();
1677 if (curr->get_type() == PTHREAD_CREATE) {
1678 return curr->get_thread_operand();
1683 /** @param act A read atomic action */
1684 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1686 ASSERT(act->is_read());
1688 // Actions paused by fuzzer have their sequence number reset to 0
1689 return act->get_seq_number() == 0;
1693 * Takes the next step in the execution, if possible.
1694 * @param curr The current step to take
1695 * @return Returns the next Thread to run, if any; NULL if this execution
1698 Thread * ModelExecution::take_step(ModelAction *curr)
1700 Thread *curr_thrd = get_thread(curr);
1701 ASSERT(curr_thrd->get_state() == THREAD_READY);
1703 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1704 curr = check_current_action(curr);
1707 /* Process this action in ModelHistory for records */
1708 model->get_history()->process_action( curr, curr->get_tid() );
1710 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1711 scheduler->remove_thread(curr_thrd);
1713 return action_select_next_thread(curr);
1716 Fuzzer * ModelExecution::getFuzzer() {