11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
34 ~model_snapshot_members() {
35 for (unsigned int i = 0;i < bugs.size();i++)
40 unsigned int next_thread_id;
41 modelclock_t used_sequence_numbers;
42 SnapVector<bug_message *> bugs;
43 /** @brief Incorrectly-ordered synchronization was made */
49 /** @brief Constructor */
50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
55 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
63 thrd_last_fence_release(),
64 priv(new struct model_snapshot_members ()),
65 mo_graph(new CycleGraph()),
66 fuzzer(new NewFuzzer()),
68 thrd_func_act_lists(),
71 /* Initialize a model-checker thread, for special ModelActions */
72 model_thread = new Thread(get_next_id());
73 add_thread(model_thread);
74 fuzzer->register_engine(m->get_history(), this);
75 scheduler->register_engine(this);
77 pthread_key_create(&pthreadkey, tlsdestructor);
81 /** @brief Destructor */
82 ModelExecution::~ModelExecution()
84 for (unsigned int i = 0;i < get_num_threads();i++)
85 delete get_thread(int_to_id(i));
91 int ModelExecution::get_execution_number() const
93 return model->get_execution_number();
96 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
98 action_list_t *tmp = hash->get(ptr);
100 tmp = new action_list_t();
106 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
108 SnapVector<action_list_t> *tmp = hash->get(ptr);
110 tmp = new SnapVector<action_list_t>();
116 /** @return a thread ID for a new Thread */
117 thread_id_t ModelExecution::get_next_id()
119 return priv->next_thread_id++;
122 /** @return the number of user threads created during this execution */
123 unsigned int ModelExecution::get_num_threads() const
125 return priv->next_thread_id;
128 /** @return a sequence number for a new ModelAction */
129 modelclock_t ModelExecution::get_next_seq_num()
131 return ++priv->used_sequence_numbers;
134 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
135 void ModelExecution::restore_last_seq_num()
137 priv->used_sequence_numbers--;
141 * @brief Should the current action wake up a given thread?
143 * @param curr The current action
144 * @param thread The thread that we might wake up
145 * @return True, if we should wake up the sleeping thread; false otherwise
147 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
149 const ModelAction *asleep = thread->get_pending();
150 /* Don't allow partial RMW to wake anyone up */
153 /* Synchronizing actions may have been backtracked */
154 if (asleep->could_synchronize_with(curr))
156 /* All acquire/release fences and fence-acquire/store-release */
157 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
159 /* Fence-release + store can awake load-acquire on the same location */
160 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
161 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
162 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
165 /* The sleep is literally sleeping */
166 if (asleep->is_sleep()) {
167 if (fuzzer->shouldWake(asleep))
174 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
176 for (unsigned int i = 0;i < get_num_threads();i++) {
177 Thread *thr = get_thread(int_to_id(i));
178 if (scheduler->is_sleep_set(thr)) {
179 if (should_wake_up(curr, thr)) {
180 /* Remove this thread from sleep set */
181 scheduler->remove_sleep(thr);
182 if (thr->get_pending()->is_sleep())
183 thr->set_wakeup_state(true);
189 void ModelExecution::assert_bug(const char *msg)
191 priv->bugs.push_back(new bug_message(msg));
195 /** @return True, if any bugs have been reported for this execution */
196 bool ModelExecution::have_bug_reports() const
198 return priv->bugs.size() != 0;
201 SnapVector<bug_message *> * ModelExecution::get_bugs() const
207 * Check whether the current trace has triggered an assertion which should halt
210 * @return True, if the execution should be aborted; false otherwise
212 bool ModelExecution::has_asserted() const
214 return priv->asserted;
218 * Trigger a trace assertion which should cause this execution to be halted.
219 * This can be due to a detected bug or due to an infeasibility that should
222 void ModelExecution::set_assert()
224 priv->asserted = true;
228 * Check if we are in a deadlock. Should only be called at the end of an
229 * execution, although it should not give false positives in the middle of an
230 * execution (there should be some ENABLED thread).
232 * @return True if program is in a deadlock; false otherwise
234 bool ModelExecution::is_deadlocked() const
236 bool blocking_threads = false;
237 for (unsigned int i = 0;i < get_num_threads();i++) {
238 thread_id_t tid = int_to_id(i);
241 Thread *t = get_thread(tid);
242 if (!t->is_model_thread() && t->get_pending())
243 blocking_threads = true;
245 return blocking_threads;
249 * Check if this is a complete execution. That is, have all thread completed
250 * execution (rather than exiting because sleep sets have forced a redundant
253 * @return True if the execution is complete.
255 bool ModelExecution::is_complete_execution() const
257 for (unsigned int i = 0;i < get_num_threads();i++)
258 if (is_enabled(int_to_id(i)))
263 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
264 uint64_t value = *((const uint64_t *) location);
265 modelclock_t storeclock;
266 thread_id_t storethread;
267 getStoreThreadAndClock(location, &storethread, &storeclock);
268 setAtomicStoreFlag(location);
269 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
270 act->set_seq_number(storeclock);
271 add_normal_write_to_lists(act);
272 add_write_to_lists(act);
273 w_modification_order(act);
274 // model->get_history()->process_action(act, act->get_tid());
279 * Processes a read model action.
280 * @param curr is the read model action to process.
281 * @param rf_set is the set of model actions we can possibly read from
282 * @return True if processing this read updates the mo_graph.
284 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
286 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
287 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
288 if (hasnonatomicstore) {
289 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
290 rf_set->push_back(nonatomicstore);
293 // Remove writes that violate read modification order
295 for (uint i = 0; i < rf_set->size(); i++) {
296 ModelAction * rf = (*rf_set)[i];
297 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
298 (*rf_set)[i] = rf_set->back();
304 int index = fuzzer->selectWrite(curr, rf_set);
305 if (index == -1)// no feasible write exists
308 ModelAction *rf = (*rf_set)[index];
311 bool canprune = false;
312 if (r_modification_order(curr, rf, priorset, &canprune)) {
313 for(unsigned int i=0;i<priorset->size();i++) {
314 mo_graph->addEdge((*priorset)[i], rf);
317 get_thread(curr)->set_return_value(curr->get_return_value());
319 if (canprune && curr->get_type() == ATOMIC_READ) {
320 int tid = id_to_int(curr->get_tid());
321 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
326 (*rf_set)[index] = rf_set->back();
332 * Processes a lock, trylock, or unlock model action. @param curr is
333 * the read model action to process.
335 * The try lock operation checks whether the lock is taken. If not,
336 * it falls to the normal lock operation case. If so, it returns
339 * The lock operation has already been checked that it is enabled, so
340 * it just grabs the lock and synchronizes with the previous unlock.
342 * The unlock operation has to re-enable all of the threads that are
343 * waiting on the lock.
345 * @return True if synchronization was updated; false otherwise
347 bool ModelExecution::process_mutex(ModelAction *curr)
349 cdsc::mutex *mutex = curr->get_mutex();
350 struct cdsc::mutex_state *state = NULL;
353 state = mutex->get_state();
355 switch (curr->get_type()) {
356 case ATOMIC_TRYLOCK: {
357 bool success = !state->locked;
358 curr->set_try_lock(success);
360 get_thread(curr)->set_return_value(0);
363 get_thread(curr)->set_return_value(1);
365 //otherwise fall into the lock case
367 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
368 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
369 // assert_bug("Lock access before initialization");
370 state->locked = get_thread(curr);
371 ModelAction *unlock = get_last_unlock(curr);
372 //synchronize with the previous unlock statement
373 if (unlock != NULL) {
374 synchronize(unlock, curr);
380 /* wake up the other threads */
381 for (unsigned int i = 0;i < get_num_threads();i++) {
382 Thread *t = get_thread(int_to_id(i));
383 Thread *curr_thrd = get_thread(curr);
384 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
388 /* unlock the lock - after checking who was waiting on it */
389 state->locked = NULL;
391 if (fuzzer->shouldWait(curr)) {
392 /* disable this thread */
393 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
394 scheduler->sleep(get_thread(curr));
399 case ATOMIC_TIMEDWAIT:
400 case ATOMIC_UNLOCK: {
401 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
403 /* wake up the other threads */
404 for (unsigned int i = 0;i < get_num_threads();i++) {
405 Thread *t = get_thread(int_to_id(i));
406 Thread *curr_thrd = get_thread(curr);
407 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
411 /* unlock the lock - after checking who was waiting on it */
412 state->locked = NULL;
415 case ATOMIC_NOTIFY_ALL: {
416 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
417 //activate all the waiting threads
418 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
419 scheduler->wake(get_thread(rit->getVal()));
424 case ATOMIC_NOTIFY_ONE: {
425 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
426 if (waiters->size() != 0) {
427 Thread * thread = fuzzer->selectNotify(waiters);
428 scheduler->wake(thread);
440 * Process a write ModelAction
441 * @param curr The ModelAction to process
442 * @return True if the mo_graph was updated or promises were resolved
444 void ModelExecution::process_write(ModelAction *curr)
446 w_modification_order(curr);
447 get_thread(curr)->set_return_value(VALUE_NONE);
451 * Process a fence ModelAction
452 * @param curr The ModelAction to process
453 * @return True if synchronization was updated
455 bool ModelExecution::process_fence(ModelAction *curr)
458 * fence-relaxed: no-op
459 * fence-release: only log the occurence (not in this function), for
460 * use in later synchronization
461 * fence-acquire (this function): search for hypothetical release
463 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
465 bool updated = false;
466 if (curr->is_acquire()) {
467 action_list_t *list = &action_trace;
468 sllnode<ModelAction *> * rit;
469 /* Find X : is_read(X) && X --sb-> curr */
470 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
471 ModelAction *act = rit->getVal();
474 if (act->get_tid() != curr->get_tid())
476 /* Stop at the beginning of the thread */
477 if (act->is_thread_start())
479 /* Stop once we reach a prior fence-acquire */
480 if (act->is_fence() && act->is_acquire())
484 /* read-acquire will find its own release sequences */
485 if (act->is_acquire())
488 /* Establish hypothetical release sequences */
489 ClockVector *cv = get_hb_from_write(act->get_reads_from());
490 if (cv != NULL && curr->get_cv()->merge(cv))
498 * @brief Process the current action for thread-related activity
500 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
501 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
502 * synchronization, etc. This function is a no-op for non-THREAD actions
503 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
505 * @param curr The current action
506 * @return True if synchronization was updated or a thread completed
508 void ModelExecution::process_thread_action(ModelAction *curr)
510 switch (curr->get_type()) {
511 case THREAD_CREATE: {
512 thrd_t *thrd = (thrd_t *)curr->get_location();
513 struct thread_params *params = (struct thread_params *)curr->get_value();
514 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
515 curr->set_thread_operand(th);
517 th->set_creation(curr);
520 case PTHREAD_CREATE: {
521 (*(uint32_t *)curr->get_location()) = pthread_counter++;
523 struct pthread_params *params = (struct pthread_params *)curr->get_value();
524 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
525 curr->set_thread_operand(th);
527 th->set_creation(curr);
529 if ( pthread_map.size() < pthread_counter )
530 pthread_map.resize( pthread_counter );
531 pthread_map[ pthread_counter-1 ] = th;
536 Thread *blocking = curr->get_thread_operand();
537 ModelAction *act = get_last_action(blocking->get_id());
538 synchronize(act, curr);
542 Thread *blocking = curr->get_thread_operand();
543 ModelAction *act = get_last_action(blocking->get_id());
544 synchronize(act, curr);
545 break; // WL: to be add (modified)
548 case THREADONLY_FINISH:
549 case THREAD_FINISH: {
550 Thread *th = get_thread(curr);
551 if (curr->get_type() == THREAD_FINISH &&
552 th == model->getInitThread()) {
558 /* Wake up any joining threads */
559 for (unsigned int i = 0;i < get_num_threads();i++) {
560 Thread *waiting = get_thread(int_to_id(i));
561 if (waiting->waiting_on() == th &&
562 waiting->get_pending()->is_thread_join())
563 scheduler->wake(waiting);
572 Thread *th = get_thread(curr);
573 th->set_pending(curr);
574 scheduler->add_sleep(th);
583 * Initialize the current action by performing one or more of the following
584 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
585 * manipulating backtracking sets, allocating and
586 * initializing clock vectors, and computing the promises to fulfill.
588 * @param curr The current action, as passed from the user context; may be
589 * freed/invalidated after the execution of this function, with a different
590 * action "returned" its place (pass-by-reference)
591 * @return True if curr is a newly-explored action; false otherwise
593 bool ModelExecution::initialize_curr_action(ModelAction **curr)
595 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
596 ModelAction *newcurr = process_rmw(*curr);
602 ModelAction *newcurr = *curr;
604 newcurr->set_seq_number(get_next_seq_num());
605 /* Always compute new clock vector */
606 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
608 /* Assign most recent release fence */
609 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
611 return true; /* This was a new ModelAction */
616 * @brief Establish reads-from relation between two actions
618 * Perform basic operations involved with establishing a concrete rf relation,
619 * including setting the ModelAction data and checking for release sequences.
621 * @param act The action that is reading (must be a read)
622 * @param rf The action from which we are reading (must be a write)
624 * @return True if this read established synchronization
627 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
630 ASSERT(rf->is_write());
632 act->set_read_from(rf);
633 if (act->is_acquire()) {
634 ClockVector *cv = get_hb_from_write(rf);
637 act->get_cv()->merge(cv);
642 * @brief Synchronizes two actions
644 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
645 * This function performs the synchronization as well as providing other hooks
646 * for other checks along with synchronization.
648 * @param first The left-hand side of the synchronizes-with relation
649 * @param second The right-hand side of the synchronizes-with relation
650 * @return True if the synchronization was successful (i.e., was consistent
651 * with the execution order); false otherwise
653 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
655 if (*second < *first) {
656 ASSERT(0); //This should not happend
659 return second->synchronize_with(first);
663 * @brief Check whether a model action is enabled.
665 * Checks whether an operation would be successful (i.e., is a lock already
666 * locked, or is the joined thread already complete).
668 * For yield-blocking, yields are never enabled.
670 * @param curr is the ModelAction to check whether it is enabled.
671 * @return a bool that indicates whether the action is enabled.
673 bool ModelExecution::check_action_enabled(ModelAction *curr) {
674 if (curr->is_lock()) {
675 cdsc::mutex *lock = curr->get_mutex();
676 struct cdsc::mutex_state *state = lock->get_state();
679 } else if (curr->is_thread_join()) {
680 Thread *blocking = curr->get_thread_operand();
681 if (!blocking->is_complete()) {
684 } else if (curr->is_sleep()) {
685 if (!fuzzer->shouldSleep(curr))
693 * This is the heart of the model checker routine. It performs model-checking
694 * actions corresponding to a given "current action." Among other processes, it
695 * calculates reads-from relationships, updates synchronization clock vectors,
696 * forms a memory_order constraints graph, and handles replay/backtrack
697 * execution when running permutations of previously-observed executions.
699 * @param curr The current action to process
700 * @return The ModelAction that is actually executed; may be different than
703 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
706 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
707 bool newly_explored = initialize_curr_action(&curr);
711 wake_up_sleeping_actions(curr);
713 /* Add uninitialized actions to lists */
714 if (!second_part_of_rmw)
715 add_uninit_action_to_lists(curr);
717 SnapVector<ModelAction *> * rf_set = NULL;
718 /* Build may_read_from set for newly-created actions */
719 if (newly_explored && curr->is_read())
720 rf_set = build_may_read_from(curr);
722 if (curr->is_read() && !second_part_of_rmw) {
723 process_read(curr, rf_set);
726 /* bool success = process_read(curr, rf_set);
729 return curr; // Do not add action to lists
732 ASSERT(rf_set == NULL);
734 /* Add the action to lists */
735 if (!second_part_of_rmw)
736 add_action_to_lists(curr);
738 if (curr->is_write())
739 add_write_to_lists(curr);
741 process_thread_action(curr);
743 if (curr->is_write())
746 if (curr->is_fence())
749 if (curr->is_mutex_op())
755 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
756 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
757 ModelAction *lastread = get_last_action(act->get_tid());
758 lastread->process_rmw(act);
760 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
766 * @brief Updates the mo_graph with the constraints imposed from the current
769 * Basic idea is the following: Go through each other thread and find
770 * the last action that happened before our read. Two cases:
772 * -# The action is a write: that write must either occur before
773 * the write we read from or be the write we read from.
774 * -# The action is a read: the write that that action read from
775 * must occur before the write we read from or be the same write.
777 * @param curr The current action. Must be a read.
778 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
779 * @param check_only If true, then only check whether the current action satisfies
780 * read modification order or not, without modifiying priorset and canprune.
782 * @return True if modification order edges were added; false otherwise
785 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
786 SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
788 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
790 ASSERT(curr->is_read());
792 /* Last SC fence in the current thread */
793 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
795 int tid = curr->get_tid();
796 ModelAction *prev_same_thread = NULL;
797 /* Iterate over all threads */
798 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
799 /* Last SC fence in thread tid */
800 ModelAction *last_sc_fence_thread_local = NULL;
802 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
804 /* Last SC fence in thread tid, before last SC fence in current thread */
805 ModelAction *last_sc_fence_thread_before = NULL;
806 if (last_sc_fence_local)
807 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
809 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
810 if (prev_same_thread != NULL &&
811 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
812 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
816 /* Iterate over actions in thread, starting from most recent */
817 action_list_t *list = &(*thrd_lists)[tid];
818 sllnode<ModelAction *> * rit;
819 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
820 ModelAction *act = rit->getVal();
825 /* Don't want to add reflexive edges on 'rf' */
826 if (act->equals(rf)) {
827 if (act->happens_before(curr))
833 if (act->is_write()) {
834 /* C++, Section 29.3 statement 5 */
835 if (curr->is_seqcst() && last_sc_fence_thread_local &&
836 *act < *last_sc_fence_thread_local) {
837 if (mo_graph->checkReachable(rf, act))
840 priorset->push_back(act);
843 /* C++, Section 29.3 statement 4 */
844 else if (act->is_seqcst() && last_sc_fence_local &&
845 *act < *last_sc_fence_local) {
846 if (mo_graph->checkReachable(rf, act))
849 priorset->push_back(act);
852 /* C++, Section 29.3 statement 6 */
853 else if (last_sc_fence_thread_before &&
854 *act < *last_sc_fence_thread_before) {
855 if (mo_graph->checkReachable(rf, act))
858 priorset->push_back(act);
864 * Include at most one act per-thread that "happens
867 if (act->happens_before(curr)) {
869 if (last_sc_fence_local == NULL ||
870 (*last_sc_fence_local < *act)) {
871 prev_same_thread = act;
874 if (act->is_write()) {
875 if (mo_graph->checkReachable(rf, act))
878 priorset->push_back(act);
880 const ModelAction *prevrf = act->get_reads_from();
881 if (!prevrf->equals(rf)) {
882 if (mo_graph->checkReachable(rf, prevrf))
885 priorset->push_back(prevrf);
887 if (act->get_tid() == curr->get_tid()) {
888 //Can prune curr from obj list
902 * Updates the mo_graph with the constraints imposed from the current write.
904 * Basic idea is the following: Go through each other thread and find
905 * the lastest action that happened before our write. Two cases:
907 * (1) The action is a write => that write must occur before
910 * (2) The action is a read => the write that that action read from
911 * must occur before the current write.
913 * This method also handles two other issues:
915 * (I) Sequential Consistency: Making sure that if the current write is
916 * seq_cst, that it occurs after the previous seq_cst write.
918 * (II) Sending the write back to non-synchronizing reads.
920 * @param curr The current action. Must be a write.
921 * @param send_fv A vector for stashing reads to which we may pass our future
922 * value. If NULL, then don't record any future values.
923 * @return True if modification order edges were added; false otherwise
925 void ModelExecution::w_modification_order(ModelAction *curr)
927 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
929 ASSERT(curr->is_write());
931 SnapList<ModelAction *> edgeset;
933 if (curr->is_seqcst()) {
934 /* We have to at least see the last sequentially consistent write,
935 so we are initialized. */
936 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
937 if (last_seq_cst != NULL) {
938 edgeset.push_back(last_seq_cst);
940 //update map for next query
941 obj_last_sc_map.put(curr->get_location(), curr);
944 /* Last SC fence in the current thread */
945 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
947 /* Iterate over all threads */
948 for (i = 0;i < thrd_lists->size();i++) {
949 /* Last SC fence in thread i, before last SC fence in current thread */
950 ModelAction *last_sc_fence_thread_before = NULL;
951 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
952 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
954 /* Iterate over actions in thread, starting from most recent */
955 action_list_t *list = &(*thrd_lists)[i];
956 sllnode<ModelAction*>* rit;
957 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
958 ModelAction *act = rit->getVal();
961 * 1) If RMW and it actually read from something, then we
962 * already have all relevant edges, so just skip to next
965 * 2) If RMW and it didn't read from anything, we should
966 * whatever edge we can get to speed up convergence.
968 * 3) If normal write, we need to look at earlier actions, so
969 * continue processing list.
971 if (curr->is_rmw()) {
972 if (curr->get_reads_from() != NULL)
980 /* C++, Section 29.3 statement 7 */
981 if (last_sc_fence_thread_before && act->is_write() &&
982 *act < *last_sc_fence_thread_before) {
983 edgeset.push_back(act);
988 * Include at most one act per-thread that "happens
991 if (act->happens_before(curr)) {
993 * Note: if act is RMW, just add edge:
995 * The following edge should be handled elsewhere:
996 * readfrom(act) --mo--> act
999 edgeset.push_back(act);
1000 else if (act->is_read()) {
1001 //if previous read accessed a null, just keep going
1002 edgeset.push_back(act->get_reads_from());
1008 mo_graph->addEdges(&edgeset, curr);
1013 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1014 * some constraints. This method checks one the following constraint (others
1015 * require compiler support):
1017 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1018 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1020 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1022 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1024 /* Iterate over all threads */
1025 for (i = 0;i < thrd_lists->size();i++) {
1026 const ModelAction *write_after_read = NULL;
1028 /* Iterate over actions in thread, starting from most recent */
1029 action_list_t *list = &(*thrd_lists)[i];
1030 sllnode<ModelAction *>* rit;
1031 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1032 ModelAction *act = rit->getVal();
1034 /* Don't disallow due to act == reader */
1035 if (!reader->happens_before(act) || reader == act)
1037 else if (act->is_write())
1038 write_after_read = act;
1039 else if (act->is_read() && act->get_reads_from() != NULL)
1040 write_after_read = act->get_reads_from();
1043 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1050 * Computes the clock vector that happens before propagates from this write.
1052 * @param rf The action that might be part of a release sequence. Must be a
1054 * @return ClockVector of happens before relation.
1057 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1058 SnapVector<ModelAction *> * processset = NULL;
1059 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1060 ASSERT(rf->is_write());
1061 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1063 if (processset == NULL)
1064 processset = new SnapVector<ModelAction *>();
1065 processset->push_back(rf);
1068 int i = (processset == NULL) ? 0 : processset->size();
1070 ClockVector * vec = NULL;
1072 if (rf->get_rfcv() != NULL) {
1073 vec = rf->get_rfcv();
1074 } else if (rf->is_acquire() && rf->is_release()) {
1076 } else if (rf->is_release() && !rf->is_rmw()) {
1078 } else if (rf->is_release()) {
1079 //have rmw that is release and doesn't have a rfcv
1080 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1083 //operation that isn't release
1084 if (rf->get_last_fence_release()) {
1086 vec = rf->get_last_fence_release()->get_cv();
1088 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1094 rf = (*processset)[i];
1098 if (processset != NULL)
1104 * Performs various bookkeeping operations for the current ModelAction when it is
1105 * the first atomic action occurred at its memory location.
1107 * For instance, adds uninitialized action to the per-object, per-thread action vector
1108 * and to the action trace list of all thread actions.
1110 * @param act is the ModelAction to process.
1112 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1114 int tid = id_to_int(act->get_tid());
1115 ModelAction *uninit = NULL;
1117 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1118 if (list->empty() && act->is_atomic_var()) {
1119 uninit = get_uninitialized_action(act);
1120 uninit_id = id_to_int(uninit->get_tid());
1121 list->push_front(uninit);
1122 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1123 if ((int)vec->size() <= uninit_id) {
1124 int oldsize = (int) vec->size();
1125 vec->resize(uninit_id + 1);
1126 for(int i = oldsize;i < uninit_id + 1;i++) {
1127 new (&(*vec)[i]) action_list_t();
1130 (*vec)[uninit_id].push_front(uninit);
1133 // Update action trace, a total order of all actions
1135 action_trace.push_front(uninit);
1137 // Update obj_thrd_map, a per location, per thread, order of actions
1138 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1139 if ((int)vec->size() <= tid) {
1140 uint oldsize = vec->size();
1141 vec->resize(priv->next_thread_id);
1142 for(uint i = oldsize;i < priv->next_thread_id;i++)
1143 new (&(*vec)[i]) action_list_t();
1146 (*vec)[uninit_id].push_front(uninit);
1148 // Update thrd_last_action, the last action taken by each thrad
1149 if ((int)thrd_last_action.size() <= tid)
1150 thrd_last_action.resize(get_num_threads());
1152 thrd_last_action[uninit_id] = uninit;
1157 * Performs various bookkeeping operations for the current ModelAction. For
1158 * instance, adds action to the per-object, per-thread action vector and to the
1159 * action trace list of all thread actions.
1161 * @param act is the ModelAction to add.
1163 void ModelExecution::add_action_to_lists(ModelAction *act)
1165 int tid = id_to_int(act->get_tid());
1166 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1167 list->push_back(act);
1169 // Update action trace, a total order of all actions
1170 action_trace.push_back(act);
1172 // Update obj_thrd_map, a per location, per thread, order of actions
1173 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1174 if ((int)vec->size() <= tid) {
1175 uint oldsize = vec->size();
1176 vec->resize(priv->next_thread_id);
1177 for(uint i = oldsize;i < priv->next_thread_id;i++)
1178 new (&(*vec)[i]) action_list_t();
1180 (*vec)[tid].push_back(act);
1182 // Update thrd_last_action, the last action taken by each thrad
1183 if ((int)thrd_last_action.size() <= tid)
1184 thrd_last_action.resize(get_num_threads());
1185 thrd_last_action[tid] = act;
1187 // Update thrd_last_fence_release, the last release fence taken by each thread
1188 if (act->is_fence() && act->is_release()) {
1189 if ((int)thrd_last_fence_release.size() <= tid)
1190 thrd_last_fence_release.resize(get_num_threads());
1191 thrd_last_fence_release[tid] = act;
1194 if (act->is_wait()) {
1195 void *mutex_loc = (void *) act->get_value();
1196 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1198 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1199 if ((int)vec->size() <= tid) {
1200 uint oldsize = vec->size();
1201 vec->resize(priv->next_thread_id);
1202 for(uint i = oldsize;i < priv->next_thread_id;i++)
1203 new (&(*vec)[i]) action_list_t();
1205 (*vec)[tid].push_back(act);
1209 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1210 sllnode<ModelAction*> * rit = list->end();
1211 modelclock_t next_seq = act->get_seq_number();
1212 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1213 list->push_back(act);
1215 for(;rit != NULL;rit=rit->getPrev()) {
1216 if (rit->getVal()->get_seq_number() == next_seq) {
1217 list->insertAfter(rit, act);
1224 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1225 sllnode<ModelAction*> * rit = list->end();
1226 modelclock_t next_seq = act->get_seq_number();
1228 act->create_cv(NULL);
1229 } else if (rit->getVal()->get_seq_number() == next_seq) {
1230 act->create_cv(rit->getVal());
1231 list->push_back(act);
1233 for(;rit != NULL;rit=rit->getPrev()) {
1234 if (rit->getVal()->get_seq_number() == next_seq) {
1235 act->create_cv(rit->getVal());
1236 list->insertAfter(rit, act);
1244 * Performs various bookkeeping operations for a normal write. The
1245 * complication is that we are typically inserting a normal write
1246 * lazily, so we need to insert it into the middle of lists.
1248 * @param act is the ModelAction to add.
1251 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1253 int tid = id_to_int(act->get_tid());
1254 insertIntoActionListAndSetCV(&action_trace, act);
1256 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1257 insertIntoActionList(list, act);
1259 // Update obj_thrd_map, a per location, per thread, order of actions
1260 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1261 if (tid >= (int)vec->size()) {
1262 uint oldsize =vec->size();
1263 vec->resize(priv->next_thread_id);
1264 for(uint i=oldsize;i<priv->next_thread_id;i++)
1265 new (&(*vec)[i]) action_list_t();
1267 insertIntoActionList(&(*vec)[tid],act);
1269 // Update thrd_last_action, the last action taken by each thrad
1270 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1271 thrd_last_action[tid] = act;
1275 void ModelExecution::add_write_to_lists(ModelAction *write) {
1276 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1277 int tid = id_to_int(write->get_tid());
1278 if (tid >= (int)vec->size()) {
1279 uint oldsize =vec->size();
1280 vec->resize(priv->next_thread_id);
1281 for(uint i=oldsize;i<priv->next_thread_id;i++)
1282 new (&(*vec)[i]) action_list_t();
1284 (*vec)[tid].push_back(write);
1288 * @brief Get the last action performed by a particular Thread
1289 * @param tid The thread ID of the Thread in question
1290 * @return The last action in the thread
1292 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1294 int threadid = id_to_int(tid);
1295 if (threadid < (int)thrd_last_action.size())
1296 return thrd_last_action[id_to_int(tid)];
1302 * @brief Get the last fence release performed by a particular Thread
1303 * @param tid The thread ID of the Thread in question
1304 * @return The last fence release in the thread, if one exists; NULL otherwise
1306 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1308 int threadid = id_to_int(tid);
1309 if (threadid < (int)thrd_last_fence_release.size())
1310 return thrd_last_fence_release[id_to_int(tid)];
1316 * Gets the last memory_order_seq_cst write (in the total global sequence)
1317 * performed on a particular object (i.e., memory location), not including the
1319 * @param curr The current ModelAction; also denotes the object location to
1321 * @return The last seq_cst write
1323 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1325 void *location = curr->get_location();
1326 return obj_last_sc_map.get(location);
1330 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1331 * performed in a particular thread, prior to a particular fence.
1332 * @param tid The ID of the thread to check
1333 * @param before_fence The fence from which to begin the search; if NULL, then
1334 * search for the most recent fence in the thread.
1335 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1337 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1339 /* All fences should have location FENCE_LOCATION */
1340 action_list_t *list = obj_map.get(FENCE_LOCATION);
1345 sllnode<ModelAction*>* rit = list->end();
1348 for (;rit != NULL;rit=rit->getPrev())
1349 if (rit->getVal() == before_fence)
1352 ASSERT(rit->getVal() == before_fence);
1356 for (;rit != NULL;rit=rit->getPrev()) {
1357 ModelAction *act = rit->getVal();
1358 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1365 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1366 * location). This function identifies the mutex according to the current
1367 * action, which is presumed to perform on the same mutex.
1368 * @param curr The current ModelAction; also denotes the object location to
1370 * @return The last unlock operation
1372 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1374 void *location = curr->get_location();
1376 action_list_t *list = obj_map.get(location);
1377 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1378 sllnode<ModelAction*>* rit;
1379 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1380 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1381 return rit->getVal();
1385 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1387 ModelAction *parent = get_last_action(tid);
1389 parent = get_thread(tid)->get_creation();
1394 * Returns the clock vector for a given thread.
1395 * @param tid The thread whose clock vector we want
1396 * @return Desired clock vector
1398 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1400 ModelAction *firstaction=get_parent_action(tid);
1401 return firstaction != NULL ? firstaction->get_cv() : NULL;
1404 bool valequals(uint64_t val1, uint64_t val2, int size) {
1407 return ((uint8_t)val1) == ((uint8_t)val2);
1409 return ((uint16_t)val1) == ((uint16_t)val2);
1411 return ((uint32_t)val1) == ((uint32_t)val2);
1421 * Build up an initial set of all past writes that this 'read' action may read
1422 * from, as well as any previously-observed future values that must still be valid.
1424 * @param curr is the current ModelAction that we are exploring; it must be a
1427 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1429 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1431 ASSERT(curr->is_read());
1433 ModelAction *last_sc_write = NULL;
1435 if (curr->is_seqcst())
1436 last_sc_write = get_last_seq_cst_write(curr);
1438 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1440 /* Iterate over all threads */
1441 for (i = 0;i < thrd_lists->size();i++) {
1442 /* Iterate over actions in thread, starting from most recent */
1443 action_list_t *list = &(*thrd_lists)[i];
1444 sllnode<ModelAction *> * rit;
1445 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1446 ModelAction *act = rit->getVal();
1451 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1452 bool allow_read = true;
1454 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1457 /* Need to check whether we will have two RMW reading from the same value */
1458 if (curr->is_rmwr()) {
1459 /* It is okay if we have a failing CAS */
1460 if (!curr->is_rmwrcas() ||
1461 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1462 //Need to make sure we aren't the second RMW
1463 CycleNode * node = mo_graph->getNode_noCreate(act);
1464 if (node != NULL && node->getRMW() != NULL) {
1465 //we are the second RMW
1472 /* Only add feasible reads */
1473 rf_set->push_back(act);
1476 /* Include at most one act per-thread that "happens before" curr */
1477 if (act->happens_before(curr))
1482 if (DBG_ENABLED()) {
1483 model_print("Reached read action:\n");
1485 model_print("End printing read_from_past\n");
1491 * @brief Get an action representing an uninitialized atomic
1493 * This function may create a new one.
1495 * @param curr The current action, which prompts the creation of an UNINIT action
1496 * @return A pointer to the UNINIT ModelAction
1498 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1500 ModelAction *act = curr->get_uninit_action();
1502 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1503 curr->set_uninit_action(act);
1505 act->create_cv(NULL);
1509 static void print_list(action_list_t *list)
1511 sllnode<ModelAction*> *it;
1513 model_print("------------------------------------------------------------------------------------\n");
1514 model_print("# t Action type MO Location Value Rf CV\n");
1515 model_print("------------------------------------------------------------------------------------\n");
1517 unsigned int hash = 0;
1519 for (it = list->begin();it != NULL;it=it->getNext()) {
1520 const ModelAction *act = it->getVal();
1521 if (act->get_seq_number() > 0)
1523 hash = hash^(hash<<3)^(it->getVal()->hash());
1525 model_print("HASH %u\n", hash);
1526 model_print("------------------------------------------------------------------------------------\n");
1529 #if SUPPORT_MOD_ORDER_DUMP
1530 void ModelExecution::dumpGraph(char *filename)
1533 sprintf(buffer, "%s.dot", filename);
1534 FILE *file = fopen(buffer, "w");
1535 fprintf(file, "digraph %s {\n", filename);
1536 mo_graph->dumpNodes(file);
1537 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1539 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1540 ModelAction *act = it->getVal();
1541 if (act->is_read()) {
1542 mo_graph->dot_print_node(file, act);
1543 mo_graph->dot_print_edge(file,
1544 act->get_reads_from(),
1546 "label=\"rf\", color=red, weight=2");
1548 if (thread_array[act->get_tid()]) {
1549 mo_graph->dot_print_edge(file,
1550 thread_array[id_to_int(act->get_tid())],
1552 "label=\"sb\", color=blue, weight=400");
1555 thread_array[act->get_tid()] = act;
1557 fprintf(file, "}\n");
1558 model_free(thread_array);
1563 /** @brief Prints an execution trace summary. */
1564 void ModelExecution::print_summary()
1566 #if SUPPORT_MOD_ORDER_DUMP
1567 char buffername[100];
1568 sprintf(buffername, "exec%04u", get_execution_number());
1569 mo_graph->dumpGraphToFile(buffername);
1570 sprintf(buffername, "graph%04u", get_execution_number());
1571 dumpGraph(buffername);
1574 model_print("Execution trace %d:", get_execution_number());
1575 if (scheduler->all_threads_sleeping())
1576 model_print(" SLEEP-SET REDUNDANT");
1577 if (have_bug_reports())
1578 model_print(" DETECTED BUG(S)");
1582 print_list(&action_trace);
1588 * Add a Thread to the system for the first time. Should only be called once
1590 * @param t The Thread to add
1592 void ModelExecution::add_thread(Thread *t)
1594 unsigned int i = id_to_int(t->get_id());
1595 if (i >= thread_map.size())
1596 thread_map.resize(i + 1);
1598 if (!t->is_model_thread())
1599 scheduler->add_thread(t);
1603 * @brief Get a Thread reference by its ID
1604 * @param tid The Thread's ID
1605 * @return A Thread reference
1607 Thread * ModelExecution::get_thread(thread_id_t tid) const
1609 unsigned int i = id_to_int(tid);
1610 if (i < thread_map.size())
1611 return thread_map[i];
1616 * @brief Get a reference to the Thread in which a ModelAction was executed
1617 * @param act The ModelAction
1618 * @return A Thread reference
1620 Thread * ModelExecution::get_thread(const ModelAction *act) const
1622 return get_thread(act->get_tid());
1626 * @brief Get a Thread reference by its pthread ID
1627 * @param index The pthread's ID
1628 * @return A Thread reference
1630 Thread * ModelExecution::get_pthread(pthread_t pid) {
1636 uint32_t thread_id = x.v;
1637 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1642 * @brief Check if a Thread is currently enabled
1643 * @param t The Thread to check
1644 * @return True if the Thread is currently enabled
1646 bool ModelExecution::is_enabled(Thread *t) const
1648 return scheduler->is_enabled(t);
1652 * @brief Check if a Thread is currently enabled
1653 * @param tid The ID of the Thread to check
1654 * @return True if the Thread is currently enabled
1656 bool ModelExecution::is_enabled(thread_id_t tid) const
1658 return scheduler->is_enabled(tid);
1662 * @brief Select the next thread to execute based on the curren action
1664 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1665 * actions should be followed by the execution of their child thread. In either
1666 * case, the current action should determine the next thread schedule.
1668 * @param curr The current action
1669 * @return The next thread to run, if the current action will determine this
1670 * selection; otherwise NULL
1672 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1674 /* Do not split atomic RMW */
1675 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1676 return get_thread(curr);
1677 /* Follow CREATE with the created thread */
1678 /* which is not needed, because model.cc takes care of this */
1679 if (curr->get_type() == THREAD_CREATE)
1680 return curr->get_thread_operand();
1681 if (curr->get_type() == PTHREAD_CREATE) {
1682 return curr->get_thread_operand();
1687 /** @param act A read atomic action */
1688 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1690 ASSERT(act->is_read());
1692 // Actions paused by fuzzer have their sequence number reset to 0
1693 return act->get_seq_number() == 0;
1697 * Takes the next step in the execution, if possible.
1698 * @param curr The current step to take
1699 * @return Returns the next Thread to run, if any; NULL if this execution
1702 Thread * ModelExecution::take_step(ModelAction *curr)
1704 Thread *curr_thrd = get_thread(curr);
1705 ASSERT(curr_thrd->get_state() == THREAD_READY);
1707 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1708 curr = check_current_action(curr);
1711 /* Process this action in ModelHistory for records */
1712 // model->get_history()->process_action( curr, curr->get_tid() );
1714 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1715 scheduler->remove_thread(curr_thrd);
1717 return action_select_next_thread(curr);
1720 Fuzzer * ModelExecution::getFuzzer() {