11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
34 ~model_snapshot_members() {
35 for (unsigned int i = 0;i < bugs.size();i++)
40 unsigned int next_thread_id;
41 modelclock_t used_sequence_numbers;
42 SnapVector<bug_message *> bugs;
43 /** @brief Incorrectly-ordered synchronization was made */
49 /** @brief Constructor */
50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
55 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
63 thrd_last_fence_release(),
64 priv(new struct model_snapshot_members ()),
65 mo_graph(new CycleGraph()),
66 fuzzer(new NewFuzzer()),
68 thrd_func_act_lists(),
71 /* Initialize a model-checker thread, for special ModelActions */
72 model_thread = new Thread(get_next_id());
73 add_thread(model_thread);
74 fuzzer->register_engine(m->get_history(), this);
75 scheduler->register_engine(this);
78 /** @brief Destructor */
79 ModelExecution::~ModelExecution()
81 for (unsigned int i = 0;i < get_num_threads();i++)
82 delete get_thread(int_to_id(i));
88 int ModelExecution::get_execution_number() const
90 return model->get_execution_number();
93 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
95 action_list_t *tmp = hash->get(ptr);
97 tmp = new action_list_t();
103 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
105 SnapVector<action_list_t> *tmp = hash->get(ptr);
107 tmp = new SnapVector<action_list_t>();
113 /** @return a thread ID for a new Thread */
114 thread_id_t ModelExecution::get_next_id()
116 return priv->next_thread_id++;
119 /** @return the number of user threads created during this execution */
120 unsigned int ModelExecution::get_num_threads() const
122 return priv->next_thread_id;
125 /** @return a sequence number for a new ModelAction */
126 modelclock_t ModelExecution::get_next_seq_num()
128 return ++priv->used_sequence_numbers;
131 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
132 void ModelExecution::restore_last_seq_num()
134 priv->used_sequence_numbers--;
138 * @brief Should the current action wake up a given thread?
140 * @param curr The current action
141 * @param thread The thread that we might wake up
142 * @return True, if we should wake up the sleeping thread; false otherwise
144 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
146 const ModelAction *asleep = thread->get_pending();
147 /* Don't allow partial RMW to wake anyone up */
150 /* Synchronizing actions may have been backtracked */
151 if (asleep->could_synchronize_with(curr))
153 /* All acquire/release fences and fence-acquire/store-release */
154 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
156 /* Fence-release + store can awake load-acquire on the same location */
157 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
158 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
159 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
162 /* The sleep is literally sleeping */
163 if (asleep->is_sleep()) {
164 if (fuzzer->shouldWake(asleep))
171 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
173 for (unsigned int i = 0;i < get_num_threads();i++) {
174 Thread *thr = get_thread(int_to_id(i));
175 if (scheduler->is_sleep_set(thr)) {
176 if (should_wake_up(curr, thr)) {
177 /* Remove this thread from sleep set */
178 scheduler->remove_sleep(thr);
179 if (thr->get_pending()->is_sleep())
180 thr->set_wakeup_state(true);
186 void ModelExecution::assert_bug(const char *msg)
188 priv->bugs.push_back(new bug_message(msg));
192 /** @return True, if any bugs have been reported for this execution */
193 bool ModelExecution::have_bug_reports() const
195 return priv->bugs.size() != 0;
198 SnapVector<bug_message *> * ModelExecution::get_bugs() const
204 * Check whether the current trace has triggered an assertion which should halt
207 * @return True, if the execution should be aborted; false otherwise
209 bool ModelExecution::has_asserted() const
211 return priv->asserted;
215 * Trigger a trace assertion which should cause this execution to be halted.
216 * This can be due to a detected bug or due to an infeasibility that should
219 void ModelExecution::set_assert()
221 priv->asserted = true;
225 * Check if we are in a deadlock. Should only be called at the end of an
226 * execution, although it should not give false positives in the middle of an
227 * execution (there should be some ENABLED thread).
229 * @return True if program is in a deadlock; false otherwise
231 bool ModelExecution::is_deadlocked() const
233 bool blocking_threads = false;
234 for (unsigned int i = 0;i < get_num_threads();i++) {
235 thread_id_t tid = int_to_id(i);
238 Thread *t = get_thread(tid);
239 if (!t->is_model_thread() && t->get_pending())
240 blocking_threads = true;
242 return blocking_threads;
246 * Check if this is a complete execution. That is, have all thread completed
247 * execution (rather than exiting because sleep sets have forced a redundant
250 * @return True if the execution is complete.
252 bool ModelExecution::is_complete_execution() const
254 for (unsigned int i = 0;i < get_num_threads();i++)
255 if (is_enabled(int_to_id(i)))
260 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
261 uint64_t value = *((const uint64_t *) location);
262 modelclock_t storeclock;
263 thread_id_t storethread;
264 getStoreThreadAndClock(location, &storethread, &storeclock);
265 setAtomicStoreFlag(location);
266 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
267 act->set_seq_number(storeclock);
268 add_normal_write_to_lists(act);
269 add_write_to_lists(act);
270 w_modification_order(act);
271 model->get_history()->process_action(act, act->get_tid());
276 * Processes a read model action.
277 * @param curr is the read model action to process.
278 * @param rf_set is the set of model actions we can possibly read from
279 * @return True if processing this read updates the mo_graph.
281 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
283 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
284 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
285 if (hasnonatomicstore) {
286 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
287 rf_set->push_back(nonatomicstore);
290 // Remove writes that violate read modification order
292 while (i < rf_set->size()) {
293 ModelAction * rf = (*rf_set)[i];
294 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
295 (*rf_set)[i] = rf_set->back();
302 int index = fuzzer->selectWrite(curr, rf_set);
303 if (index == -1)// no feasible write exists
306 ModelAction *rf = (*rf_set)[index];
309 bool canprune = false;
310 if (r_modification_order(curr, rf, priorset, &canprune)) {
311 for(unsigned int i=0;i<priorset->size();i++) {
312 mo_graph->addEdge((*priorset)[i], rf);
315 get_thread(curr)->set_return_value(curr->get_return_value());
317 if (canprune && curr->get_type() == ATOMIC_READ) {
318 int tid = id_to_int(curr->get_tid());
319 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
325 /* TODO: Following code not needed anymore */
327 (*rf_set)[index] = rf_set->back();
333 * Processes a lock, trylock, or unlock model action. @param curr is
334 * the read model action to process.
336 * The try lock operation checks whether the lock is taken. If not,
337 * it falls to the normal lock operation case. If so, it returns
340 * The lock operation has already been checked that it is enabled, so
341 * it just grabs the lock and synchronizes with the previous unlock.
343 * The unlock operation has to re-enable all of the threads that are
344 * waiting on the lock.
346 * @return True if synchronization was updated; false otherwise
348 bool ModelExecution::process_mutex(ModelAction *curr)
350 cdsc::mutex *mutex = curr->get_mutex();
351 struct cdsc::mutex_state *state = NULL;
354 state = mutex->get_state();
356 switch (curr->get_type()) {
357 case ATOMIC_TRYLOCK: {
358 bool success = !state->locked;
359 curr->set_try_lock(success);
361 get_thread(curr)->set_return_value(0);
364 get_thread(curr)->set_return_value(1);
366 //otherwise fall into the lock case
368 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
369 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
370 // assert_bug("Lock access before initialization");
371 state->locked = get_thread(curr);
372 ModelAction *unlock = get_last_unlock(curr);
373 //synchronize with the previous unlock statement
374 if (unlock != NULL) {
375 synchronize(unlock, curr);
381 /* wake up the other threads */
382 for (unsigned int i = 0;i < get_num_threads();i++) {
383 Thread *t = get_thread(int_to_id(i));
384 Thread *curr_thrd = get_thread(curr);
385 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
389 /* unlock the lock - after checking who was waiting on it */
390 state->locked = NULL;
392 if (fuzzer->shouldWait(curr)) {
393 /* disable this thread */
394 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
395 scheduler->sleep(get_thread(curr));
400 case ATOMIC_TIMEDWAIT:
401 case ATOMIC_UNLOCK: {
402 //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...
404 /* wake up the other threads */
405 for (unsigned int i = 0;i < get_num_threads();i++) {
406 Thread *t = get_thread(int_to_id(i));
407 Thread *curr_thrd = get_thread(curr);
408 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
412 /* unlock the lock - after checking who was waiting on it */
413 state->locked = NULL;
416 case ATOMIC_NOTIFY_ALL: {
417 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
418 //activate all the waiting threads
419 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
420 scheduler->wake(get_thread(rit->getVal()));
425 case ATOMIC_NOTIFY_ONE: {
426 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
427 if (waiters->size() != 0) {
428 Thread * thread = fuzzer->selectNotify(waiters);
429 scheduler->wake(thread);
441 * Process a write ModelAction
442 * @param curr The ModelAction to process
443 * @return True if the mo_graph was updated or promises were resolved
445 void ModelExecution::process_write(ModelAction *curr)
447 w_modification_order(curr);
448 get_thread(curr)->set_return_value(VALUE_NONE);
452 * Process a fence ModelAction
453 * @param curr The ModelAction to process
454 * @return True if synchronization was updated
456 bool ModelExecution::process_fence(ModelAction *curr)
459 * fence-relaxed: no-op
460 * fence-release: only log the occurence (not in this function), for
461 * use in later synchronization
462 * fence-acquire (this function): search for hypothetical release
464 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
466 bool updated = false;
467 if (curr->is_acquire()) {
468 action_list_t *list = &action_trace;
469 sllnode<ModelAction *> * rit;
470 /* Find X : is_read(X) && X --sb-> curr */
471 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
472 ModelAction *act = rit->getVal();
475 if (act->get_tid() != curr->get_tid())
477 /* Stop at the beginning of the thread */
478 if (act->is_thread_start())
480 /* Stop once we reach a prior fence-acquire */
481 if (act->is_fence() && act->is_acquire())
485 /* read-acquire will find its own release sequences */
486 if (act->is_acquire())
489 /* Establish hypothetical release sequences */
490 ClockVector *cv = get_hb_from_write(act->get_reads_from());
491 if (cv != NULL && curr->get_cv()->merge(cv))
499 * @brief Process the current action for thread-related activity
501 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
502 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
503 * synchronization, etc. This function is a no-op for non-THREAD actions
504 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
506 * @param curr The current action
507 * @return True if synchronization was updated or a thread completed
509 void ModelExecution::process_thread_action(ModelAction *curr)
511 switch (curr->get_type()) {
512 case THREAD_CREATE: {
513 thrd_t *thrd = (thrd_t *)curr->get_location();
514 struct thread_params *params = (struct thread_params *)curr->get_value();
515 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
516 curr->set_thread_operand(th);
518 th->set_creation(curr);
521 case PTHREAD_CREATE: {
522 (*(uint32_t *)curr->get_location()) = pthread_counter++;
524 struct pthread_params *params = (struct pthread_params *)curr->get_value();
525 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
526 curr->set_thread_operand(th);
528 th->set_creation(curr);
530 if ( pthread_map.size() < pthread_counter )
531 pthread_map.resize( pthread_counter );
532 pthread_map[ pthread_counter-1 ] = th;
537 Thread *blocking = curr->get_thread_operand();
538 ModelAction *act = get_last_action(blocking->get_id());
539 synchronize(act, curr);
543 Thread *blocking = curr->get_thread_operand();
544 ModelAction *act = get_last_action(blocking->get_id());
545 synchronize(act, curr);
546 break; // WL: to be add (modified)
549 case THREADONLY_FINISH:
550 case THREAD_FINISH: {
551 Thread *th = get_thread(curr);
552 if (curr->get_type() == THREAD_FINISH &&
553 th == model->getInitThread()) {
559 /* Wake up any joining threads */
560 for (unsigned int i = 0;i < get_num_threads();i++) {
561 Thread *waiting = get_thread(int_to_id(i));
562 if (waiting->waiting_on() == th &&
563 waiting->get_pending()->is_thread_join())
564 scheduler->wake(waiting);
573 Thread *th = get_thread(curr);
574 th->set_pending(curr);
575 scheduler->add_sleep(th);
584 * Initialize the current action by performing one or more of the following
585 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
586 * manipulating backtracking sets, allocating and
587 * initializing clock vectors, and computing the promises to fulfill.
589 * @param curr The current action, as passed from the user context; may be
590 * freed/invalidated after the execution of this function, with a different
591 * action "returned" its place (pass-by-reference)
592 * @return True if curr is a newly-explored action; false otherwise
594 bool ModelExecution::initialize_curr_action(ModelAction **curr)
596 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
597 ModelAction *newcurr = process_rmw(*curr);
603 ModelAction *newcurr = *curr;
605 newcurr->set_seq_number(get_next_seq_num());
606 /* Always compute new clock vector */
607 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
609 /* Assign most recent release fence */
610 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
612 return true; /* This was a new ModelAction */
617 * @brief Establish reads-from relation between two actions
619 * Perform basic operations involved with establishing a concrete rf relation,
620 * including setting the ModelAction data and checking for release sequences.
622 * @param act The action that is reading (must be a read)
623 * @param rf The action from which we are reading (must be a write)
625 * @return True if this read established synchronization
628 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
631 ASSERT(rf->is_write());
633 act->set_read_from(rf);
634 if (act->is_acquire()) {
635 ClockVector *cv = get_hb_from_write(rf);
638 act->get_cv()->merge(cv);
643 * @brief Synchronizes two actions
645 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
646 * This function performs the synchronization as well as providing other hooks
647 * for other checks along with synchronization.
649 * @param first The left-hand side of the synchronizes-with relation
650 * @param second The right-hand side of the synchronizes-with relation
651 * @return True if the synchronization was successful (i.e., was consistent
652 * with the execution order); false otherwise
654 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
656 if (*second < *first) {
657 ASSERT(0); //This should not happend
660 return second->synchronize_with(first);
664 * @brief Check whether a model action is enabled.
666 * Checks whether an operation would be successful (i.e., is a lock already
667 * locked, or is the joined thread already complete).
669 * For yield-blocking, yields are never enabled.
671 * @param curr is the ModelAction to check whether it is enabled.
672 * @return a bool that indicates whether the action is enabled.
674 bool ModelExecution::check_action_enabled(ModelAction *curr) {
675 if (curr->is_lock()) {
676 cdsc::mutex *lock = curr->get_mutex();
677 struct cdsc::mutex_state *state = lock->get_state();
680 } else if (curr->is_thread_join()) {
681 Thread *blocking = curr->get_thread_operand();
682 if (!blocking->is_complete()) {
685 } else if (curr->is_sleep()) {
686 if (!fuzzer->shouldSleep(curr))
694 * This is the heart of the model checker routine. It performs model-checking
695 * actions corresponding to a given "current action." Among other processes, it
696 * calculates reads-from relationships, updates synchronization clock vectors,
697 * forms a memory_order constraints graph, and handles replay/backtrack
698 * execution when running permutations of previously-observed executions.
700 * @param curr The current action to process
701 * @return The ModelAction that is actually executed; may be different than
704 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
707 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
708 bool newly_explored = initialize_curr_action(&curr);
712 wake_up_sleeping_actions(curr);
714 /* Add uninitialized actions to lists */
715 if (!second_part_of_rmw)
716 add_uninit_action_to_lists(curr);
718 SnapVector<ModelAction *> * rf_set = NULL;
719 /* Build may_read_from set for newly-created actions */
720 if (newly_explored && curr->is_read())
721 rf_set = build_may_read_from(curr);
723 if (curr->is_read() && !second_part_of_rmw) {
724 process_read(curr, rf_set);
727 /* bool success = process_read(curr, rf_set);
730 return curr; // Do not add action to lists
733 ASSERT(rf_set == NULL);
735 /* Add the action to lists */
736 if (!second_part_of_rmw)
737 add_action_to_lists(curr);
739 if (curr->is_write())
740 add_write_to_lists(curr);
742 process_thread_action(curr);
744 if (curr->is_write())
747 if (curr->is_fence())
750 if (curr->is_mutex_op())
756 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
757 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
758 ModelAction *lastread = get_last_action(act->get_tid());
759 lastread->process_rmw(act);
761 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
767 * @brief Updates the mo_graph with the constraints imposed from the current
770 * Basic idea is the following: Go through each other thread and find
771 * the last action that happened before our read. Two cases:
773 * -# The action is a write: that write must either occur before
774 * the write we read from or be the write we read from.
775 * -# The action is a read: the write that that action read from
776 * must occur before the write we read from or be the same write.
778 * @param curr The current action. Must be a read.
779 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
780 * @param check_only If true, then only check whether the current action satisfies
781 * read modification order or not, without modifiying priorset and canprune.
783 * @return True if modification order edges were added; false otherwise
786 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
787 SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
789 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
791 ASSERT(curr->is_read());
793 /* Last SC fence in the current thread */
794 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
796 int tid = curr->get_tid();
797 ModelAction *prev_same_thread = NULL;
798 /* Iterate over all threads */
799 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
800 /* Last SC fence in thread tid */
801 ModelAction *last_sc_fence_thread_local = NULL;
803 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
805 /* Last SC fence in thread tid, before last SC fence in current thread */
806 ModelAction *last_sc_fence_thread_before = NULL;
807 if (last_sc_fence_local)
808 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
810 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
811 if (prev_same_thread != NULL &&
812 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
813 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
817 /* Iterate over actions in thread, starting from most recent */
818 action_list_t *list = &(*thrd_lists)[tid];
819 sllnode<ModelAction *> * rit;
820 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
821 ModelAction *act = rit->getVal();
826 /* Don't want to add reflexive edges on 'rf' */
827 if (act->equals(rf)) {
828 if (act->happens_before(curr))
834 if (act->is_write()) {
835 /* C++, Section 29.3 statement 5 */
836 if (curr->is_seqcst() && last_sc_fence_thread_local &&
837 *act < *last_sc_fence_thread_local) {
838 if (mo_graph->checkReachable(rf, act))
841 priorset->push_back(act);
844 /* C++, Section 29.3 statement 4 */
845 else if (act->is_seqcst() && last_sc_fence_local &&
846 *act < *last_sc_fence_local) {
847 if (mo_graph->checkReachable(rf, act))
850 priorset->push_back(act);
853 /* C++, Section 29.3 statement 6 */
854 else if (last_sc_fence_thread_before &&
855 *act < *last_sc_fence_thread_before) {
856 if (mo_graph->checkReachable(rf, act))
859 priorset->push_back(act);
865 * Include at most one act per-thread that "happens
868 if (act->happens_before(curr)) {
870 if (last_sc_fence_local == NULL ||
871 (*last_sc_fence_local < *act)) {
872 prev_same_thread = act;
875 if (act->is_write()) {
876 if (mo_graph->checkReachable(rf, act))
879 priorset->push_back(act);
881 const ModelAction *prevrf = act->get_reads_from();
882 if (!prevrf->equals(rf)) {
883 if (mo_graph->checkReachable(rf, prevrf))
886 priorset->push_back(prevrf);
888 if (act->get_tid() == curr->get_tid()) {
889 //Can prune curr from obj list
903 * Updates the mo_graph with the constraints imposed from the current write.
905 * Basic idea is the following: Go through each other thread and find
906 * the lastest action that happened before our write. Two cases:
908 * (1) The action is a write => that write must occur before
911 * (2) The action is a read => the write that that action read from
912 * must occur before the current write.
914 * This method also handles two other issues:
916 * (I) Sequential Consistency: Making sure that if the current write is
917 * seq_cst, that it occurs after the previous seq_cst write.
919 * (II) Sending the write back to non-synchronizing reads.
921 * @param curr The current action. Must be a write.
922 * @param send_fv A vector for stashing reads to which we may pass our future
923 * value. If NULL, then don't record any future values.
924 * @return True if modification order edges were added; false otherwise
926 void ModelExecution::w_modification_order(ModelAction *curr)
928 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
930 ASSERT(curr->is_write());
932 SnapList<ModelAction *> edgeset;
934 if (curr->is_seqcst()) {
935 /* We have to at least see the last sequentially consistent write,
936 so we are initialized. */
937 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
938 if (last_seq_cst != NULL) {
939 edgeset.push_back(last_seq_cst);
941 //update map for next query
942 obj_last_sc_map.put(curr->get_location(), curr);
945 /* Last SC fence in the current thread */
946 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
948 /* Iterate over all threads */
949 for (i = 0;i < thrd_lists->size();i++) {
950 /* Last SC fence in thread i, before last SC fence in current thread */
951 ModelAction *last_sc_fence_thread_before = NULL;
952 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
953 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
955 /* Iterate over actions in thread, starting from most recent */
956 action_list_t *list = &(*thrd_lists)[i];
957 sllnode<ModelAction*>* rit;
958 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
959 ModelAction *act = rit->getVal();
962 * 1) If RMW and it actually read from something, then we
963 * already have all relevant edges, so just skip to next
966 * 2) If RMW and it didn't read from anything, we should
967 * whatever edge we can get to speed up convergence.
969 * 3) If normal write, we need to look at earlier actions, so
970 * continue processing list.
972 if (curr->is_rmw()) {
973 if (curr->get_reads_from() != NULL)
981 /* C++, Section 29.3 statement 7 */
982 if (last_sc_fence_thread_before && act->is_write() &&
983 *act < *last_sc_fence_thread_before) {
984 edgeset.push_back(act);
989 * Include at most one act per-thread that "happens
992 if (act->happens_before(curr)) {
994 * Note: if act is RMW, just add edge:
996 * The following edge should be handled elsewhere:
997 * readfrom(act) --mo--> act
1000 edgeset.push_back(act);
1001 else if (act->is_read()) {
1002 //if previous read accessed a null, just keep going
1003 edgeset.push_back(act->get_reads_from());
1009 mo_graph->addEdges(&edgeset, curr);
1014 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1015 * some constraints. This method checks one the following constraint (others
1016 * require compiler support):
1018 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1019 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1021 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1023 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1025 /* Iterate over all threads */
1026 for (i = 0;i < thrd_lists->size();i++) {
1027 const ModelAction *write_after_read = NULL;
1029 /* Iterate over actions in thread, starting from most recent */
1030 action_list_t *list = &(*thrd_lists)[i];
1031 sllnode<ModelAction *>* rit;
1032 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1033 ModelAction *act = rit->getVal();
1035 /* Don't disallow due to act == reader */
1036 if (!reader->happens_before(act) || reader == act)
1038 else if (act->is_write())
1039 write_after_read = act;
1040 else if (act->is_read() && act->get_reads_from() != NULL)
1041 write_after_read = act->get_reads_from();
1044 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1051 * Computes the clock vector that happens before propagates from this write.
1053 * @param rf The action that might be part of a release sequence. Must be a
1055 * @return ClockVector of happens before relation.
1058 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1059 SnapVector<ModelAction *> * processset = NULL;
1060 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1061 ASSERT(rf->is_write());
1062 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1064 if (processset == NULL)
1065 processset = new SnapVector<ModelAction *>();
1066 processset->push_back(rf);
1069 int i = (processset == NULL) ? 0 : processset->size();
1071 ClockVector * vec = NULL;
1073 if (rf->get_rfcv() != NULL) {
1074 vec = rf->get_rfcv();
1075 } else if (rf->is_acquire() && rf->is_release()) {
1077 } else if (rf->is_release() && !rf->is_rmw()) {
1079 } else if (rf->is_release()) {
1080 //have rmw that is release and doesn't have a rfcv
1081 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1084 //operation that isn't release
1085 if (rf->get_last_fence_release()) {
1087 vec = rf->get_last_fence_release()->get_cv();
1089 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1095 rf = (*processset)[i];
1099 if (processset != NULL)
1105 * Performs various bookkeeping operations for the current ModelAction when it is
1106 * the first atomic action occurred at its memory location.
1108 * For instance, adds uninitialized action to the per-object, per-thread action vector
1109 * and to the action trace list of all thread actions.
1111 * @param act is the ModelAction to process.
1113 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1115 int tid = id_to_int(act->get_tid());
1116 ModelAction *uninit = NULL;
1118 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1119 if (list->empty() && act->is_atomic_var()) {
1120 uninit = get_uninitialized_action(act);
1121 uninit_id = id_to_int(uninit->get_tid());
1122 list->push_front(uninit);
1123 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1124 if ((int)vec->size() <= uninit_id) {
1125 int oldsize = (int) vec->size();
1126 vec->resize(uninit_id + 1);
1127 for(int i = oldsize;i < uninit_id + 1;i++) {
1128 new (&(*vec)[i]) action_list_t();
1131 (*vec)[uninit_id].push_front(uninit);
1134 // Update action trace, a total order of all actions
1136 action_trace.push_front(uninit);
1138 // Update obj_thrd_map, a per location, per thread, order of actions
1139 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1140 if ((int)vec->size() <= tid) {
1141 uint oldsize = vec->size();
1142 vec->resize(priv->next_thread_id);
1143 for(uint i = oldsize;i < priv->next_thread_id;i++)
1144 new (&(*vec)[i]) action_list_t();
1147 (*vec)[uninit_id].push_front(uninit);
1149 // Update thrd_last_action, the last action taken by each thrad
1150 if ((int)thrd_last_action.size() <= tid)
1151 thrd_last_action.resize(get_num_threads());
1153 thrd_last_action[uninit_id] = uninit;
1158 * Performs various bookkeeping operations for the current ModelAction. For
1159 * instance, adds action to the per-object, per-thread action vector and to the
1160 * action trace list of all thread actions.
1162 * @param act is the ModelAction to add.
1164 void ModelExecution::add_action_to_lists(ModelAction *act)
1166 int tid = id_to_int(act->get_tid());
1167 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1168 list->push_back(act);
1170 // Update action trace, a total order of all actions
1171 action_trace.push_back(act);
1173 // Update obj_thrd_map, a per location, per thread, order of actions
1174 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1175 if ((int)vec->size() <= tid) {
1176 uint oldsize = vec->size();
1177 vec->resize(priv->next_thread_id);
1178 for(uint i = oldsize;i < priv->next_thread_id;i++)
1179 new (&(*vec)[i]) action_list_t();
1181 (*vec)[tid].push_back(act);
1183 // Update thrd_last_action, the last action taken by each thrad
1184 if ((int)thrd_last_action.size() <= tid)
1185 thrd_last_action.resize(get_num_threads());
1186 thrd_last_action[tid] = act;
1188 // Update thrd_last_fence_release, the last release fence taken by each thread
1189 if (act->is_fence() && act->is_release()) {
1190 if ((int)thrd_last_fence_release.size() <= tid)
1191 thrd_last_fence_release.resize(get_num_threads());
1192 thrd_last_fence_release[tid] = act;
1195 if (act->is_wait()) {
1196 void *mutex_loc = (void *) act->get_value();
1197 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1199 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1200 if ((int)vec->size() <= tid) {
1201 uint oldsize = vec->size();
1202 vec->resize(priv->next_thread_id);
1203 for(uint i = oldsize;i < priv->next_thread_id;i++)
1204 new (&(*vec)[i]) action_list_t();
1206 (*vec)[tid].push_back(act);
1210 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1211 sllnode<ModelAction*> * rit = list->end();
1212 modelclock_t next_seq = act->get_seq_number();
1213 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1214 list->push_back(act);
1216 for(;rit != NULL;rit=rit->getPrev()) {
1217 if (rit->getVal()->get_seq_number() == next_seq) {
1218 list->insertAfter(rit, act);
1225 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1226 sllnode<ModelAction*> * rit = list->end();
1227 modelclock_t next_seq = act->get_seq_number();
1229 act->create_cv(NULL);
1230 } else if (rit->getVal()->get_seq_number() == next_seq) {
1231 act->create_cv(rit->getVal());
1232 list->push_back(act);
1234 for(;rit != NULL;rit=rit->getPrev()) {
1235 if (rit->getVal()->get_seq_number() == next_seq) {
1236 act->create_cv(rit->getVal());
1237 list->insertAfter(rit, act);
1245 * Performs various bookkeeping operations for a normal write. The
1246 * complication is that we are typically inserting a normal write
1247 * lazily, so we need to insert it into the middle of lists.
1249 * @param act is the ModelAction to add.
1252 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1254 int tid = id_to_int(act->get_tid());
1255 insertIntoActionListAndSetCV(&action_trace, act);
1257 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1258 insertIntoActionList(list, act);
1260 // Update obj_thrd_map, a per location, per thread, order of actions
1261 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1262 if (tid >= (int)vec->size()) {
1263 uint oldsize =vec->size();
1264 vec->resize(priv->next_thread_id);
1265 for(uint i=oldsize;i<priv->next_thread_id;i++)
1266 new (&(*vec)[i]) action_list_t();
1268 insertIntoActionList(&(*vec)[tid],act);
1270 // Update thrd_last_action, the last action taken by each thrad
1271 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1272 thrd_last_action[tid] = act;
1276 void ModelExecution::add_write_to_lists(ModelAction *write) {
1277 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1278 int tid = id_to_int(write->get_tid());
1279 if (tid >= (int)vec->size()) {
1280 uint oldsize =vec->size();
1281 vec->resize(priv->next_thread_id);
1282 for(uint i=oldsize;i<priv->next_thread_id;i++)
1283 new (&(*vec)[i]) action_list_t();
1285 (*vec)[tid].push_back(write);
1289 * @brief Get the last action performed by a particular Thread
1290 * @param tid The thread ID of the Thread in question
1291 * @return The last action in the thread
1293 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1295 int threadid = id_to_int(tid);
1296 if (threadid < (int)thrd_last_action.size())
1297 return thrd_last_action[id_to_int(tid)];
1303 * @brief Get the last fence release performed by a particular Thread
1304 * @param tid The thread ID of the Thread in question
1305 * @return The last fence release in the thread, if one exists; NULL otherwise
1307 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1309 int threadid = id_to_int(tid);
1310 if (threadid < (int)thrd_last_fence_release.size())
1311 return thrd_last_fence_release[id_to_int(tid)];
1317 * Gets the last memory_order_seq_cst write (in the total global sequence)
1318 * performed on a particular object (i.e., memory location), not including the
1320 * @param curr The current ModelAction; also denotes the object location to
1322 * @return The last seq_cst write
1324 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1326 void *location = curr->get_location();
1327 return obj_last_sc_map.get(location);
1331 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1332 * performed in a particular thread, prior to a particular fence.
1333 * @param tid The ID of the thread to check
1334 * @param before_fence The fence from which to begin the search; if NULL, then
1335 * search for the most recent fence in the thread.
1336 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1338 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1340 /* All fences should have location FENCE_LOCATION */
1341 action_list_t *list = obj_map.get(FENCE_LOCATION);
1346 sllnode<ModelAction*>* rit = list->end();
1349 for (;rit != NULL;rit=rit->getPrev())
1350 if (rit->getVal() == before_fence)
1353 ASSERT(rit->getVal() == before_fence);
1357 for (;rit != NULL;rit=rit->getPrev()) {
1358 ModelAction *act = rit->getVal();
1359 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1366 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1367 * location). This function identifies the mutex according to the current
1368 * action, which is presumed to perform on the same mutex.
1369 * @param curr The current ModelAction; also denotes the object location to
1371 * @return The last unlock operation
1373 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1375 void *location = curr->get_location();
1377 action_list_t *list = obj_map.get(location);
1378 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1379 sllnode<ModelAction*>* rit;
1380 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1381 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1382 return rit->getVal();
1386 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1388 ModelAction *parent = get_last_action(tid);
1390 parent = get_thread(tid)->get_creation();
1395 * Returns the clock vector for a given thread.
1396 * @param tid The thread whose clock vector we want
1397 * @return Desired clock vector
1399 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1401 ModelAction *firstaction=get_parent_action(tid);
1402 return firstaction != NULL ? firstaction->get_cv() : NULL;
1405 bool valequals(uint64_t val1, uint64_t val2, int size) {
1408 return ((uint8_t)val1) == ((uint8_t)val2);
1410 return ((uint16_t)val1) == ((uint16_t)val2);
1412 return ((uint32_t)val1) == ((uint32_t)val2);
1422 * Build up an initial set of all past writes that this 'read' action may read
1423 * from, as well as any previously-observed future values that must still be valid.
1425 * @param curr is the current ModelAction that we are exploring; it must be a
1428 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1430 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1432 ASSERT(curr->is_read());
1434 ModelAction *last_sc_write = NULL;
1436 if (curr->is_seqcst())
1437 last_sc_write = get_last_seq_cst_write(curr);
1439 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1441 /* Iterate over all threads */
1442 for (i = 0;i < thrd_lists->size();i++) {
1443 /* Iterate over actions in thread, starting from most recent */
1444 action_list_t *list = &(*thrd_lists)[i];
1445 sllnode<ModelAction *> * rit;
1446 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1447 ModelAction *act = rit->getVal();
1452 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1453 bool allow_read = true;
1455 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1458 /* Need to check whether we will have two RMW reading from the same value */
1459 if (curr->is_rmwr()) {
1460 /* It is okay if we have a failing CAS */
1461 if (!curr->is_rmwrcas() ||
1462 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1463 //Need to make sure we aren't the second RMW
1464 CycleNode * node = mo_graph->getNode_noCreate(act);
1465 if (node != NULL && node->getRMW() != NULL) {
1466 //we are the second RMW
1473 /* Only add feasible reads */
1474 rf_set->push_back(act);
1477 /* Include at most one act per-thread that "happens before" curr */
1478 if (act->happens_before(curr))
1483 if (DBG_ENABLED()) {
1484 model_print("Reached read action:\n");
1486 model_print("End printing read_from_past\n");
1492 * @brief Get an action representing an uninitialized atomic
1494 * This function may create a new one.
1496 * @param curr The current action, which prompts the creation of an UNINIT action
1497 * @return A pointer to the UNINIT ModelAction
1499 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1501 ModelAction *act = curr->get_uninit_action();
1503 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1504 curr->set_uninit_action(act);
1506 act->create_cv(NULL);
1510 static void print_list(action_list_t *list)
1512 sllnode<ModelAction*> *it;
1514 model_print("------------------------------------------------------------------------------------\n");
1515 model_print("# t Action type MO Location Value Rf CV\n");
1516 model_print("------------------------------------------------------------------------------------\n");
1518 unsigned int hash = 0;
1520 for (it = list->begin();it != NULL;it=it->getNext()) {
1521 const ModelAction *act = it->getVal();
1522 if (act->get_seq_number() > 0)
1524 hash = hash^(hash<<3)^(it->getVal()->hash());
1526 model_print("HASH %u\n", hash);
1527 model_print("------------------------------------------------------------------------------------\n");
1530 #if SUPPORT_MOD_ORDER_DUMP
1531 void ModelExecution::dumpGraph(char *filename)
1534 sprintf(buffer, "%s.dot", filename);
1535 FILE *file = fopen(buffer, "w");
1536 fprintf(file, "digraph %s {\n", filename);
1537 mo_graph->dumpNodes(file);
1538 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1540 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1541 ModelAction *act = it->getVal();
1542 if (act->is_read()) {
1543 mo_graph->dot_print_node(file, act);
1544 mo_graph->dot_print_edge(file,
1545 act->get_reads_from(),
1547 "label=\"rf\", color=red, weight=2");
1549 if (thread_array[act->get_tid()]) {
1550 mo_graph->dot_print_edge(file,
1551 thread_array[id_to_int(act->get_tid())],
1553 "label=\"sb\", color=blue, weight=400");
1556 thread_array[act->get_tid()] = act;
1558 fprintf(file, "}\n");
1559 model_free(thread_array);
1564 /** @brief Prints an execution trace summary. */
1565 void ModelExecution::print_summary()
1567 #if SUPPORT_MOD_ORDER_DUMP
1568 char buffername[100];
1569 sprintf(buffername, "exec%04u", get_execution_number());
1570 mo_graph->dumpGraphToFile(buffername);
1571 sprintf(buffername, "graph%04u", get_execution_number());
1572 dumpGraph(buffername);
1575 model_print("Execution trace %d:", get_execution_number());
1576 if (scheduler->all_threads_sleeping())
1577 model_print(" SLEEP-SET REDUNDANT");
1578 if (have_bug_reports())
1579 model_print(" DETECTED BUG(S)");
1583 print_list(&action_trace);
1589 * Add a Thread to the system for the first time. Should only be called once
1591 * @param t The Thread to add
1593 void ModelExecution::add_thread(Thread *t)
1595 unsigned int i = id_to_int(t->get_id());
1596 if (i >= thread_map.size())
1597 thread_map.resize(i + 1);
1599 if (!t->is_model_thread())
1600 scheduler->add_thread(t);
1604 * @brief Get a Thread reference by its ID
1605 * @param tid The Thread's ID
1606 * @return A Thread reference
1608 Thread * ModelExecution::get_thread(thread_id_t tid) const
1610 unsigned int i = id_to_int(tid);
1611 if (i < thread_map.size())
1612 return thread_map[i];
1617 * @brief Get a reference to the Thread in which a ModelAction was executed
1618 * @param act The ModelAction
1619 * @return A Thread reference
1621 Thread * ModelExecution::get_thread(const ModelAction *act) const
1623 return get_thread(act->get_tid());
1627 * @brief Get a Thread reference by its pthread ID
1628 * @param index The pthread's ID
1629 * @return A Thread reference
1631 Thread * ModelExecution::get_pthread(pthread_t pid) {
1637 uint32_t thread_id = x.v;
1638 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1643 * @brief Check if a Thread is currently enabled
1644 * @param t The Thread to check
1645 * @return True if the Thread is currently enabled
1647 bool ModelExecution::is_enabled(Thread *t) const
1649 return scheduler->is_enabled(t);
1653 * @brief Check if a Thread is currently enabled
1654 * @param tid The ID of the Thread to check
1655 * @return True if the Thread is currently enabled
1657 bool ModelExecution::is_enabled(thread_id_t tid) const
1659 return scheduler->is_enabled(tid);
1663 * @brief Select the next thread to execute based on the curren action
1665 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1666 * actions should be followed by the execution of their child thread. In either
1667 * case, the current action should determine the next thread schedule.
1669 * @param curr The current action
1670 * @return The next thread to run, if the current action will determine this
1671 * selection; otherwise NULL
1673 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1675 /* Do not split atomic RMW */
1676 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1677 return get_thread(curr);
1678 /* Follow CREATE with the created thread */
1679 /* which is not needed, because model.cc takes care of this */
1680 if (curr->get_type() == THREAD_CREATE)
1681 return curr->get_thread_operand();
1682 if (curr->get_type() == PTHREAD_CREATE) {
1683 return curr->get_thread_operand();
1688 /** @param act A read atomic action */
1689 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1691 ASSERT(act->is_read());
1693 // Actions paused by fuzzer have their sequence number reset to 0
1694 return act->get_seq_number() == 0;
1698 * Takes the next step in the execution, if possible.
1699 * @param curr The current step to take
1700 * @return Returns the next Thread to run, if any; NULL if this execution
1703 Thread * ModelExecution::take_step(ModelAction *curr)
1705 Thread *curr_thrd = get_thread(curr);
1706 ASSERT(curr_thrd->get_state() == THREAD_READY);
1708 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1709 curr = check_current_action(curr);
1712 /* Process this action in ModelHistory for records */
1713 model->get_history()->process_action( curr, curr->get_tid() );
1715 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1716 scheduler->remove_thread(curr_thrd);
1718 return action_select_next_thread(curr);
1721 Fuzzer * ModelExecution::getFuzzer() {