11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
31 bad_synchronization(false),
35 ~model_snapshot_members() {
36 for (unsigned int i = 0;i < bugs.size();i++)
41 unsigned int next_thread_id;
42 modelclock_t used_sequence_numbers;
43 SnapVector<bug_message *> bugs;
44 /** @brief Incorrectly-ordered synchronization was made */
45 bool bad_synchronization;
51 /** @brief Constructor */
52 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
57 thread_map(2), /* We'll always need at least 2 threads */
61 condvar_waiters_map(),
65 thrd_last_fence_release(),
66 priv(new struct model_snapshot_members ()),
67 mo_graph(new CycleGraph()),
68 fuzzer(new NewFuzzer()),
70 thrd_func_act_lists(),
73 /* Initialize a model-checker thread, for special ModelActions */
74 model_thread = new Thread(get_next_id());
75 add_thread(model_thread);
76 fuzzer->register_engine(m->get_history(), this);
77 scheduler->register_engine(this);
80 /** @brief Destructor */
81 ModelExecution::~ModelExecution()
83 for (unsigned int i = 0;i < get_num_threads();i++)
84 delete get_thread(int_to_id(i));
90 int ModelExecution::get_execution_number() const
92 return model->get_execution_number();
95 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
97 action_list_t *tmp = hash->get(ptr);
99 tmp = new action_list_t();
105 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
107 SnapVector<action_list_t> *tmp = hash->get(ptr);
109 tmp = new SnapVector<action_list_t>();
115 /** @return a thread ID for a new Thread */
116 thread_id_t ModelExecution::get_next_id()
118 return priv->next_thread_id++;
121 /** @return the number of user threads created during this execution */
122 unsigned int ModelExecution::get_num_threads() const
124 return priv->next_thread_id;
127 /** @return a sequence number for a new ModelAction */
128 modelclock_t ModelExecution::get_next_seq_num()
130 return ++priv->used_sequence_numbers;
133 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
134 void ModelExecution::restore_last_seq_num()
136 priv->used_sequence_numbers--;
140 * @brief Should the current action wake up a given thread?
142 * @param curr The current action
143 * @param thread The thread that we might wake up
144 * @return True, if we should wake up the sleeping thread; false otherwise
146 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
148 const ModelAction *asleep = thread->get_pending();
149 /* Don't allow partial RMW to wake anyone up */
152 /* Synchronizing actions may have been backtracked */
153 if (asleep->could_synchronize_with(curr))
155 /* All acquire/release fences and fence-acquire/store-release */
156 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
158 /* Fence-release + store can awake load-acquire on the same location */
159 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
160 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
161 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
164 /* The sleep is literally sleeping */
165 if (asleep->is_sleep()) {
166 if (fuzzer->shouldWake(asleep))
173 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
175 for (unsigned int i = 0;i < get_num_threads();i++) {
176 Thread *thr = get_thread(int_to_id(i));
177 if (scheduler->is_sleep_set(thr)) {
178 if (should_wake_up(curr, thr)) {
179 /* Remove this thread from sleep set */
180 scheduler->remove_sleep(thr);
181 if (thr->get_pending()->is_sleep())
182 thr->set_wakeup_state(true);
188 /** @brief Alert the model-checker that an incorrectly-ordered
189 * synchronization was made */
190 void ModelExecution::set_bad_synchronization()
192 priv->bad_synchronization = true;
195 bool ModelExecution::assert_bug(const char *msg)
197 priv->bugs.push_back(new bug_message(msg));
199 if (isfeasibleprefix()) {
206 /** @return True, if any bugs have been reported for this execution */
207 bool ModelExecution::have_bug_reports() const
209 return priv->bugs.size() != 0;
212 SnapVector<bug_message *> * ModelExecution::get_bugs() const
218 * Check whether the current trace has triggered an assertion which should halt
221 * @return True, if the execution should be aborted; false otherwise
223 bool ModelExecution::has_asserted() const
225 return priv->asserted;
229 * Trigger a trace assertion which should cause this execution to be halted.
230 * This can be due to a detected bug or due to an infeasibility that should
233 void ModelExecution::set_assert()
235 priv->asserted = true;
239 * Check if we are in a deadlock. Should only be called at the end of an
240 * execution, although it should not give false positives in the middle of an
241 * execution (there should be some ENABLED thread).
243 * @return True if program is in a deadlock; false otherwise
245 bool ModelExecution::is_deadlocked() const
247 bool blocking_threads = false;
248 for (unsigned int i = 0;i < get_num_threads();i++) {
249 thread_id_t tid = int_to_id(i);
252 Thread *t = get_thread(tid);
253 if (!t->is_model_thread() && t->get_pending())
254 blocking_threads = true;
256 return blocking_threads;
260 * Check if this is a complete execution. That is, have all thread completed
261 * execution (rather than exiting because sleep sets have forced a redundant
264 * @return True if the execution is complete.
266 bool ModelExecution::is_complete_execution() const
268 for (unsigned int i = 0;i < get_num_threads();i++)
269 if (is_enabled(int_to_id(i)))
274 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
275 uint64_t value = *((const uint64_t *) location);
276 modelclock_t storeclock;
277 thread_id_t storethread;
278 getStoreThreadAndClock(location, &storethread, &storeclock);
279 setAtomicStoreFlag(location);
280 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
281 act->set_seq_number(storeclock);
282 add_normal_write_to_lists(act);
283 add_write_to_lists(act);
284 w_modification_order(act);
285 model->get_history()->process_action(act, act->get_tid());
290 * Processes a read model action.
291 * @param curr is the read model action to process.
292 * @param rf_set is the set of model actions we can possibly read from
293 * @return True if processing this read updates the mo_graph.
295 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
297 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
298 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
299 if (hasnonatomicstore) {
300 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
301 rf_set->push_back(nonatomicstore);
304 // Remove writes that violate read modification order
305 for (uint i = 0; i < rf_set->size(); i++) {
306 ModelAction * rf = (*rf_set)[i];
307 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
308 (*rf_set)[i] = rf_set->back();
314 int index = fuzzer->selectWrite(curr, rf_set);
315 if (index == -1) // no feasible write exists
318 ModelAction *rf = (*rf_set)[index];
321 bool canprune = false;
322 if (r_modification_order(curr, rf, priorset, &canprune)) {
323 for(unsigned int i=0;i<priorset->size();i++) {
324 mo_graph->addEdge((*priorset)[i], rf);
327 get_thread(curr)->set_return_value(curr->get_return_value());
329 if (canprune && curr->get_type() == ATOMIC_READ) {
330 int tid = id_to_int(curr->get_tid());
331 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
336 (*rf_set)[index] = rf_set->back();
342 * Processes a lock, trylock, or unlock model action. @param curr is
343 * the read model action to process.
345 * The try lock operation checks whether the lock is taken. If not,
346 * it falls to the normal lock operation case. If so, it returns
349 * The lock operation has already been checked that it is enabled, so
350 * it just grabs the lock and synchronizes with the previous unlock.
352 * The unlock operation has to re-enable all of the threads that are
353 * waiting on the lock.
355 * @return True if synchronization was updated; false otherwise
357 bool ModelExecution::process_mutex(ModelAction *curr)
359 cdsc::mutex *mutex = curr->get_mutex();
360 struct cdsc::mutex_state *state = NULL;
363 state = mutex->get_state();
365 switch (curr->get_type()) {
366 case ATOMIC_TRYLOCK: {
367 bool success = !state->locked;
368 curr->set_try_lock(success);
370 get_thread(curr)->set_return_value(0);
373 get_thread(curr)->set_return_value(1);
375 //otherwise fall into the lock case
377 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
378 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
379 // assert_bug("Lock access before initialization");
380 state->locked = get_thread(curr);
381 ModelAction *unlock = get_last_unlock(curr);
382 //synchronize with the previous unlock statement
383 if (unlock != NULL) {
384 synchronize(unlock, curr);
390 /* wake up the other threads */
391 for (unsigned int i = 0;i < get_num_threads();i++) {
392 Thread *t = get_thread(int_to_id(i));
393 Thread *curr_thrd = get_thread(curr);
394 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
398 /* unlock the lock - after checking who was waiting on it */
399 state->locked = NULL;
401 if (fuzzer->shouldWait(curr)) {
402 /* disable this thread */
403 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
404 scheduler->sleep(get_thread(curr));
409 case ATOMIC_TIMEDWAIT:
410 case ATOMIC_UNLOCK: {
411 //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...
413 /* wake up the other threads */
414 for (unsigned int i = 0;i < get_num_threads();i++) {
415 Thread *t = get_thread(int_to_id(i));
416 Thread *curr_thrd = get_thread(curr);
417 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
421 /* unlock the lock - after checking who was waiting on it */
422 state->locked = NULL;
425 case ATOMIC_NOTIFY_ALL: {
426 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
427 //activate all the waiting threads
428 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
429 scheduler->wake(get_thread(rit->getVal()));
434 case ATOMIC_NOTIFY_ONE: {
435 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
436 if (waiters->size() != 0) {
437 Thread * thread = fuzzer->selectNotify(waiters);
438 scheduler->wake(thread);
450 * Process a write ModelAction
451 * @param curr The ModelAction to process
452 * @return True if the mo_graph was updated or promises were resolved
454 void ModelExecution::process_write(ModelAction *curr)
456 w_modification_order(curr);
457 get_thread(curr)->set_return_value(VALUE_NONE);
461 * Process a fence ModelAction
462 * @param curr The ModelAction to process
463 * @return True if synchronization was updated
465 bool ModelExecution::process_fence(ModelAction *curr)
468 * fence-relaxed: no-op
469 * fence-release: only log the occurence (not in this function), for
470 * use in later synchronization
471 * fence-acquire (this function): search for hypothetical release
473 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
475 bool updated = false;
476 if (curr->is_acquire()) {
477 action_list_t *list = &action_trace;
478 sllnode<ModelAction *> * rit;
479 /* Find X : is_read(X) && X --sb-> curr */
480 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
481 ModelAction *act = rit->getVal();
484 if (act->get_tid() != curr->get_tid())
486 /* Stop at the beginning of the thread */
487 if (act->is_thread_start())
489 /* Stop once we reach a prior fence-acquire */
490 if (act->is_fence() && act->is_acquire())
494 /* read-acquire will find its own release sequences */
495 if (act->is_acquire())
498 /* Establish hypothetical release sequences */
499 ClockVector *cv = get_hb_from_write(act->get_reads_from());
500 if (cv != NULL && curr->get_cv()->merge(cv))
508 * @brief Process the current action for thread-related activity
510 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
511 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
512 * synchronization, etc. This function is a no-op for non-THREAD actions
513 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
515 * @param curr The current action
516 * @return True if synchronization was updated or a thread completed
518 void ModelExecution::process_thread_action(ModelAction *curr)
520 switch (curr->get_type()) {
521 case THREAD_CREATE: {
522 thrd_t *thrd = (thrd_t *)curr->get_location();
523 struct thread_params *params = (struct thread_params *)curr->get_value();
524 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
525 curr->set_thread_operand(th);
527 th->set_creation(curr);
530 case PTHREAD_CREATE: {
531 (*(uint32_t *)curr->get_location()) = pthread_counter++;
533 struct pthread_params *params = (struct pthread_params *)curr->get_value();
534 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
535 curr->set_thread_operand(th);
537 th->set_creation(curr);
539 if ( pthread_map.size() < pthread_counter )
540 pthread_map.resize( pthread_counter );
541 pthread_map[ pthread_counter-1 ] = th;
546 Thread *blocking = curr->get_thread_operand();
547 ModelAction *act = get_last_action(blocking->get_id());
548 synchronize(act, curr);
552 Thread *blocking = curr->get_thread_operand();
553 ModelAction *act = get_last_action(blocking->get_id());
554 synchronize(act, curr);
555 break; // WL: to be add (modified)
558 case THREADONLY_FINISH:
559 case THREAD_FINISH: {
560 Thread *th = get_thread(curr);
561 if (curr->get_type() == THREAD_FINISH &&
562 th == model->getInitThread()) {
568 /* Wake up any joining threads */
569 for (unsigned int i = 0;i < get_num_threads();i++) {
570 Thread *waiting = get_thread(int_to_id(i));
571 if (waiting->waiting_on() == th &&
572 waiting->get_pending()->is_thread_join())
573 scheduler->wake(waiting);
582 Thread *th = get_thread(curr);
583 th->set_pending(curr);
584 scheduler->add_sleep(th);
593 * Initialize the current action by performing one or more of the following
594 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
595 * manipulating backtracking sets, allocating and
596 * initializing clock vectors, and computing the promises to fulfill.
598 * @param curr The current action, as passed from the user context; may be
599 * freed/invalidated after the execution of this function, with a different
600 * action "returned" its place (pass-by-reference)
601 * @return True if curr is a newly-explored action; false otherwise
603 bool ModelExecution::initialize_curr_action(ModelAction **curr)
605 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
606 ModelAction *newcurr = process_rmw(*curr);
612 ModelAction *newcurr = *curr;
614 newcurr->set_seq_number(get_next_seq_num());
615 /* Always compute new clock vector */
616 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
618 /* Assign most recent release fence */
619 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
621 return true; /* This was a new ModelAction */
626 * @brief Establish reads-from relation between two actions
628 * Perform basic operations involved with establishing a concrete rf relation,
629 * including setting the ModelAction data and checking for release sequences.
631 * @param act The action that is reading (must be a read)
632 * @param rf The action from which we are reading (must be a write)
634 * @return True if this read established synchronization
637 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
640 ASSERT(rf->is_write());
642 act->set_read_from(rf);
643 if (act->is_acquire()) {
644 ClockVector *cv = get_hb_from_write(rf);
647 act->get_cv()->merge(cv);
652 * @brief Synchronizes two actions
654 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
655 * This function performs the synchronization as well as providing other hooks
656 * for other checks along with synchronization.
658 * @param first The left-hand side of the synchronizes-with relation
659 * @param second The right-hand side of the synchronizes-with relation
660 * @return True if the synchronization was successful (i.e., was consistent
661 * with the execution order); false otherwise
663 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
665 if (*second < *first) {
666 set_bad_synchronization();
669 return second->synchronize_with(first);
673 * @brief Check whether a model action is enabled.
675 * Checks whether an operation would be successful (i.e., is a lock already
676 * locked, or is the joined thread already complete).
678 * For yield-blocking, yields are never enabled.
680 * @param curr is the ModelAction to check whether it is enabled.
681 * @return a bool that indicates whether the action is enabled.
683 bool ModelExecution::check_action_enabled(ModelAction *curr) {
684 if (curr->is_lock()) {
685 cdsc::mutex *lock = curr->get_mutex();
686 struct cdsc::mutex_state *state = lock->get_state();
689 } else if (curr->is_thread_join()) {
690 Thread *blocking = curr->get_thread_operand();
691 if (!blocking->is_complete()) {
694 } else if (curr->is_sleep()) {
695 if (!fuzzer->shouldSleep(curr))
703 * This is the heart of the model checker routine. It performs model-checking
704 * actions corresponding to a given "current action." Among other processes, it
705 * calculates reads-from relationships, updates synchronization clock vectors,
706 * forms a memory_order constraints graph, and handles replay/backtrack
707 * execution when running permutations of previously-observed executions.
709 * @param curr The current action to process
710 * @return The ModelAction that is actually executed; may be different than
713 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
716 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
717 bool newly_explored = initialize_curr_action(&curr);
721 wake_up_sleeping_actions(curr);
723 /* Add uninitialized actions to lists */
724 if (!second_part_of_rmw)
725 add_uninit_action_to_lists(curr);
727 SnapVector<ModelAction *> * rf_set = NULL;
728 /* Build may_read_from set for newly-created actions */
729 if (newly_explored && curr->is_read())
730 rf_set = build_may_read_from(curr);
732 if (curr->is_read() && !second_part_of_rmw) {
733 process_read(curr, rf_set);
736 /* bool success = process_read(curr, rf_set);
739 return curr; // Do not add action to lists
742 ASSERT(rf_set == NULL);
744 /* Add the action to lists */
745 if (!second_part_of_rmw)
746 add_action_to_lists(curr);
748 if (curr->is_write())
749 add_write_to_lists(curr);
751 process_thread_action(curr);
753 if (curr->is_write())
756 if (curr->is_fence())
759 if (curr->is_mutex_op())
766 * This is the strongest feasibility check available.
767 * @return whether the current trace (partial or complete) must be a prefix of
770 bool ModelExecution::isfeasibleprefix() const
772 return !is_infeasible();
776 * Print disagnostic information about an infeasible execution
777 * @param prefix A string to prefix the output with; if NULL, then a default
778 * message prefix will be provided
780 void ModelExecution::print_infeasibility(const char *prefix) const
784 if (priv->bad_synchronization)
785 ptr += sprintf(ptr, "[bad sw ordering]");
787 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
791 * Check if the current partial trace is infeasible. Does not check any
792 * end-of-execution flags, which might rule out the execution. Thus, this is
793 * useful only for ruling an execution as infeasible.
794 * @return whether the current partial trace is infeasible.
796 bool ModelExecution::is_infeasible() const
798 return priv->bad_synchronization;
801 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
802 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
803 ModelAction *lastread = get_last_action(act->get_tid());
804 lastread->process_rmw(act);
806 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
812 * @brief Updates the mo_graph with the constraints imposed from the current
815 * Basic idea is the following: Go through each other thread and find
816 * the last action that happened before our read. Two cases:
818 * -# The action is a write: that write must either occur before
819 * the write we read from or be the write we read from.
820 * -# The action is a read: the write that that action read from
821 * must occur before the write we read from or be the same write.
823 * @param curr The current action. Must be a read.
824 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
825 * @param check_only If true, then only check whether the current action satisfies
826 * read modification order or not, without modifiying priorset and canprune.
828 * @return True if modification order edges were added; false otherwise
831 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
832 SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
834 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
836 ASSERT(curr->is_read());
838 /* Last SC fence in the current thread */
839 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
841 int tid = curr->get_tid();
842 ModelAction *prev_same_thread = NULL;
843 /* Iterate over all threads */
844 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
845 /* Last SC fence in thread tid */
846 ModelAction *last_sc_fence_thread_local = NULL;
848 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
850 /* Last SC fence in thread tid, before last SC fence in current thread */
851 ModelAction *last_sc_fence_thread_before = NULL;
852 if (last_sc_fence_local)
853 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
855 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
856 if (prev_same_thread != NULL &&
857 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
858 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
862 /* Iterate over actions in thread, starting from most recent */
863 action_list_t *list = &(*thrd_lists)[tid];
864 sllnode<ModelAction *> * rit;
865 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
866 ModelAction *act = rit->getVal();
871 /* Don't want to add reflexive edges on 'rf' */
872 if (act->equals(rf)) {
873 if (act->happens_before(curr))
879 if (act->is_write()) {
880 /* C++, Section 29.3 statement 5 */
881 if (curr->is_seqcst() && last_sc_fence_thread_local &&
882 *act < *last_sc_fence_thread_local) {
883 if (mo_graph->checkReachable(rf, act))
886 priorset->push_back(act);
889 /* C++, Section 29.3 statement 4 */
890 else if (act->is_seqcst() && last_sc_fence_local &&
891 *act < *last_sc_fence_local) {
892 if (mo_graph->checkReachable(rf, act))
895 priorset->push_back(act);
898 /* C++, Section 29.3 statement 6 */
899 else if (last_sc_fence_thread_before &&
900 *act < *last_sc_fence_thread_before) {
901 if (mo_graph->checkReachable(rf, act))
904 priorset->push_back(act);
910 * Include at most one act per-thread that "happens
913 if (act->happens_before(curr)) {
915 if (last_sc_fence_local == NULL ||
916 (*last_sc_fence_local < *act)) {
917 prev_same_thread = act;
920 if (act->is_write()) {
921 if (mo_graph->checkReachable(rf, act))
924 priorset->push_back(act);
926 const ModelAction *prevrf = act->get_reads_from();
927 if (!prevrf->equals(rf)) {
928 if (mo_graph->checkReachable(rf, prevrf))
931 priorset->push_back(prevrf);
933 if (act->get_tid() == curr->get_tid()) {
934 //Can prune curr from obj list
948 * Updates the mo_graph with the constraints imposed from the current write.
950 * Basic idea is the following: Go through each other thread and find
951 * the lastest action that happened before our write. Two cases:
953 * (1) The action is a write => that write must occur before
956 * (2) The action is a read => the write that that action read from
957 * must occur before the current write.
959 * This method also handles two other issues:
961 * (I) Sequential Consistency: Making sure that if the current write is
962 * seq_cst, that it occurs after the previous seq_cst write.
964 * (II) Sending the write back to non-synchronizing reads.
966 * @param curr The current action. Must be a write.
967 * @param send_fv A vector for stashing reads to which we may pass our future
968 * value. If NULL, then don't record any future values.
969 * @return True if modification order edges were added; false otherwise
971 void ModelExecution::w_modification_order(ModelAction *curr)
973 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
975 ASSERT(curr->is_write());
977 SnapList<ModelAction *> edgeset;
979 if (curr->is_seqcst()) {
980 /* We have to at least see the last sequentially consistent write,
981 so we are initialized. */
982 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
983 if (last_seq_cst != NULL) {
984 edgeset.push_back(last_seq_cst);
986 //update map for next query
987 obj_last_sc_map.put(curr->get_location(), curr);
990 /* Last SC fence in the current thread */
991 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
993 /* Iterate over all threads */
994 for (i = 0;i < thrd_lists->size();i++) {
995 /* Last SC fence in thread i, before last SC fence in current thread */
996 ModelAction *last_sc_fence_thread_before = NULL;
997 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
998 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1000 /* Iterate over actions in thread, starting from most recent */
1001 action_list_t *list = &(*thrd_lists)[i];
1002 sllnode<ModelAction*>* rit;
1003 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1004 ModelAction *act = rit->getVal();
1007 * 1) If RMW and it actually read from something, then we
1008 * already have all relevant edges, so just skip to next
1011 * 2) If RMW and it didn't read from anything, we should
1012 * whatever edge we can get to speed up convergence.
1014 * 3) If normal write, we need to look at earlier actions, so
1015 * continue processing list.
1017 if (curr->is_rmw()) {
1018 if (curr->get_reads_from() != NULL)
1026 /* C++, Section 29.3 statement 7 */
1027 if (last_sc_fence_thread_before && act->is_write() &&
1028 *act < *last_sc_fence_thread_before) {
1029 edgeset.push_back(act);
1034 * Include at most one act per-thread that "happens
1037 if (act->happens_before(curr)) {
1039 * Note: if act is RMW, just add edge:
1041 * The following edge should be handled elsewhere:
1042 * readfrom(act) --mo--> act
1044 if (act->is_write())
1045 edgeset.push_back(act);
1046 else if (act->is_read()) {
1047 //if previous read accessed a null, just keep going
1048 edgeset.push_back(act->get_reads_from());
1054 mo_graph->addEdges(&edgeset, curr);
1059 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1060 * some constraints. This method checks one the following constraint (others
1061 * require compiler support):
1063 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1064 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1066 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1068 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1070 /* Iterate over all threads */
1071 for (i = 0;i < thrd_lists->size();i++) {
1072 const ModelAction *write_after_read = NULL;
1074 /* Iterate over actions in thread, starting from most recent */
1075 action_list_t *list = &(*thrd_lists)[i];
1076 sllnode<ModelAction *>* rit;
1077 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1078 ModelAction *act = rit->getVal();
1080 /* Don't disallow due to act == reader */
1081 if (!reader->happens_before(act) || reader == act)
1083 else if (act->is_write())
1084 write_after_read = act;
1085 else if (act->is_read() && act->get_reads_from() != NULL)
1086 write_after_read = act->get_reads_from();
1089 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1096 * Computes the clock vector that happens before propagates from this write.
1098 * @param rf The action that might be part of a release sequence. Must be a
1100 * @return ClockVector of happens before relation.
1103 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1104 SnapVector<ModelAction *> * processset = NULL;
1105 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1106 ASSERT(rf->is_write());
1107 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1109 if (processset == NULL)
1110 processset = new SnapVector<ModelAction *>();
1111 processset->push_back(rf);
1114 int i = (processset == NULL) ? 0 : processset->size();
1116 ClockVector * vec = NULL;
1118 if (rf->get_rfcv() != NULL) {
1119 vec = rf->get_rfcv();
1120 } else if (rf->is_acquire() && rf->is_release()) {
1122 } else if (rf->is_release() && !rf->is_rmw()) {
1124 } else if (rf->is_release()) {
1125 //have rmw that is release and doesn't have a rfcv
1126 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1129 //operation that isn't release
1130 if (rf->get_last_fence_release()) {
1132 vec = rf->get_last_fence_release()->get_cv();
1134 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1140 rf = (*processset)[i];
1144 if (processset != NULL)
1150 * Performs various bookkeeping operations for the current ModelAction when it is
1151 * the first atomic action occurred at its memory location.
1153 * For instance, adds uninitialized action to the per-object, per-thread action vector
1154 * and to the action trace list of all thread actions.
1156 * @param act is the ModelAction to process.
1158 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1160 int tid = id_to_int(act->get_tid());
1161 ModelAction *uninit = NULL;
1163 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1164 if (list->empty() && act->is_atomic_var()) {
1165 uninit = get_uninitialized_action(act);
1166 uninit_id = id_to_int(uninit->get_tid());
1167 list->push_front(uninit);
1168 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1169 if ((int)vec->size() <= uninit_id) {
1170 int oldsize = (int) vec->size();
1171 vec->resize(uninit_id + 1);
1172 for(int i = oldsize; i < uninit_id + 1; i++) {
1173 new (&(*vec)[i]) action_list_t();
1176 (*vec)[uninit_id].push_front(uninit);
1179 // Update action trace, a total order of all actions
1181 action_trace.push_front(uninit);
1183 // Update obj_thrd_map, a per location, per thread, order of actions
1184 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1185 if ((int)vec->size() <= tid) {
1186 uint oldsize = vec->size();
1187 vec->resize(priv->next_thread_id);
1188 for(uint i = oldsize; i < priv->next_thread_id; i++)
1189 new (&(*vec)[i]) action_list_t();
1192 (*vec)[uninit_id].push_front(uninit);
1194 // Update thrd_last_action, the last action taken by each thrad
1195 if ((int)thrd_last_action.size() <= tid)
1196 thrd_last_action.resize(get_num_threads());
1198 thrd_last_action[uninit_id] = uninit;
1203 * Performs various bookkeeping operations for the current ModelAction. For
1204 * instance, adds action to the per-object, per-thread action vector and to the
1205 * action trace list of all thread actions.
1207 * @param act is the ModelAction to add.
1209 void ModelExecution::add_action_to_lists(ModelAction *act)
1211 int tid = id_to_int(act->get_tid());
1212 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1213 list->push_back(act);
1215 // Update action trace, a total order of all actions
1216 action_trace.push_back(act);
1218 // Update obj_thrd_map, a per location, per thread, order of actions
1219 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1220 if ((int)vec->size() <= tid) {
1221 uint oldsize = vec->size();
1222 vec->resize(priv->next_thread_id);
1223 for(uint i = oldsize; i < priv->next_thread_id; i++)
1224 new (&(*vec)[i]) action_list_t();
1226 (*vec)[tid].push_back(act);
1228 // Update thrd_last_action, the last action taken by each thrad
1229 if ((int)thrd_last_action.size() <= tid)
1230 thrd_last_action.resize(get_num_threads());
1231 thrd_last_action[tid] = act;
1233 // Update thrd_last_fence_release, the last release fence taken by each thread
1234 if (act->is_fence() && act->is_release()) {
1235 if ((int)thrd_last_fence_release.size() <= tid)
1236 thrd_last_fence_release.resize(get_num_threads());
1237 thrd_last_fence_release[tid] = act;
1240 if (act->is_wait()) {
1241 void *mutex_loc = (void *) act->get_value();
1242 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1244 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1245 if ((int)vec->size() <= tid) {
1246 uint oldsize = vec->size();
1247 vec->resize(priv->next_thread_id);
1248 for(uint i = oldsize; i < priv->next_thread_id; i++)
1249 new (&(*vec)[i]) action_list_t();
1251 (*vec)[tid].push_back(act);
1255 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1256 sllnode<ModelAction*> * rit = list->end();
1257 modelclock_t next_seq = act->get_seq_number();
1258 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1259 list->push_back(act);
1261 for(;rit != NULL;rit=rit->getPrev()) {
1262 if (rit->getVal()->get_seq_number() == next_seq) {
1263 list->insertAfter(rit, act);
1270 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1271 sllnode<ModelAction*> * rit = list->end();
1272 modelclock_t next_seq = act->get_seq_number();
1274 act->create_cv(NULL);
1275 } else if (rit->getVal()->get_seq_number() == next_seq) {
1276 act->create_cv(rit->getVal());
1277 list->push_back(act);
1279 for(;rit != NULL;rit=rit->getPrev()) {
1280 if (rit->getVal()->get_seq_number() == next_seq) {
1281 act->create_cv(rit->getVal());
1282 list->insertAfter(rit, act);
1290 * Performs various bookkeeping operations for a normal write. The
1291 * complication is that we are typically inserting a normal write
1292 * lazily, so we need to insert it into the middle of lists.
1294 * @param act is the ModelAction to add.
1297 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1299 int tid = id_to_int(act->get_tid());
1300 insertIntoActionListAndSetCV(&action_trace, act);
1302 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1303 insertIntoActionList(list, act);
1305 // Update obj_thrd_map, a per location, per thread, order of actions
1306 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1307 if (tid >= (int)vec->size()) {
1308 uint oldsize =vec->size();
1309 vec->resize(priv->next_thread_id);
1310 for(uint i=oldsize;i<priv->next_thread_id;i++)
1311 new (&(*vec)[i]) action_list_t();
1313 insertIntoActionList(&(*vec)[tid],act);
1315 // Update thrd_last_action, the last action taken by each thrad
1316 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1317 thrd_last_action[tid] = act;
1321 void ModelExecution::add_write_to_lists(ModelAction *write) {
1322 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1323 int tid = id_to_int(write->get_tid());
1324 if (tid >= (int)vec->size()) {
1325 uint oldsize =vec->size();
1326 vec->resize(priv->next_thread_id);
1327 for(uint i=oldsize;i<priv->next_thread_id;i++)
1328 new (&(*vec)[i]) action_list_t();
1330 (*vec)[tid].push_back(write);
1334 * @brief Get the last action performed by a particular Thread
1335 * @param tid The thread ID of the Thread in question
1336 * @return The last action in the thread
1338 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1340 int threadid = id_to_int(tid);
1341 if (threadid < (int)thrd_last_action.size())
1342 return thrd_last_action[id_to_int(tid)];
1348 * @brief Get the last fence release performed by a particular Thread
1349 * @param tid The thread ID of the Thread in question
1350 * @return The last fence release in the thread, if one exists; NULL otherwise
1352 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1354 int threadid = id_to_int(tid);
1355 if (threadid < (int)thrd_last_fence_release.size())
1356 return thrd_last_fence_release[id_to_int(tid)];
1362 * Gets the last memory_order_seq_cst write (in the total global sequence)
1363 * performed on a particular object (i.e., memory location), not including the
1365 * @param curr The current ModelAction; also denotes the object location to
1367 * @return The last seq_cst write
1369 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1371 void *location = curr->get_location();
1372 return obj_last_sc_map.get(location);
1376 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1377 * performed in a particular thread, prior to a particular fence.
1378 * @param tid The ID of the thread to check
1379 * @param before_fence The fence from which to begin the search; if NULL, then
1380 * search for the most recent fence in the thread.
1381 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1383 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1385 /* All fences should have location FENCE_LOCATION */
1386 action_list_t *list = obj_map.get(FENCE_LOCATION);
1391 sllnode<ModelAction*>* rit = list->end();
1394 for (;rit != NULL;rit=rit->getPrev())
1395 if (rit->getVal() == before_fence)
1398 ASSERT(rit->getVal() == before_fence);
1402 for (;rit != NULL;rit=rit->getPrev()) {
1403 ModelAction *act = rit->getVal();
1404 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1411 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1412 * location). This function identifies the mutex according to the current
1413 * action, which is presumed to perform on the same mutex.
1414 * @param curr The current ModelAction; also denotes the object location to
1416 * @return The last unlock operation
1418 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1420 void *location = curr->get_location();
1422 action_list_t *list = obj_map.get(location);
1423 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1424 sllnode<ModelAction*>* rit;
1425 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1426 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1427 return rit->getVal();
1431 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1433 ModelAction *parent = get_last_action(tid);
1435 parent = get_thread(tid)->get_creation();
1440 * Returns the clock vector for a given thread.
1441 * @param tid The thread whose clock vector we want
1442 * @return Desired clock vector
1444 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1446 ModelAction *firstaction=get_parent_action(tid);
1447 return firstaction != NULL ? firstaction->get_cv() : NULL;
1450 bool valequals(uint64_t val1, uint64_t val2, int size) {
1453 return ((uint8_t)val1) == ((uint8_t)val2);
1455 return ((uint16_t)val1) == ((uint16_t)val2);
1457 return ((uint32_t)val1) == ((uint32_t)val2);
1467 * Build up an initial set of all past writes that this 'read' action may read
1468 * from, as well as any previously-observed future values that must still be valid.
1470 * @param curr is the current ModelAction that we are exploring; it must be a
1473 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1475 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1477 ASSERT(curr->is_read());
1479 ModelAction *last_sc_write = NULL;
1481 if (curr->is_seqcst())
1482 last_sc_write = get_last_seq_cst_write(curr);
1484 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1486 /* Iterate over all threads */
1487 for (i = 0;i < thrd_lists->size();i++) {
1488 /* Iterate over actions in thread, starting from most recent */
1489 action_list_t *list = &(*thrd_lists)[i];
1490 sllnode<ModelAction *> * rit;
1491 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1492 ModelAction *act = rit->getVal();
1497 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1498 bool allow_read = true;
1500 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1503 /* Need to check whether we will have two RMW reading from the same value */
1504 if (curr->is_rmwr()) {
1505 /* It is okay if we have a failing CAS */
1506 if (!curr->is_rmwrcas() ||
1507 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1508 //Need to make sure we aren't the second RMW
1509 CycleNode * node = mo_graph->getNode_noCreate(act);
1510 if (node != NULL && node->getRMW() != NULL) {
1511 //we are the second RMW
1518 /* Only add feasible reads */
1519 rf_set->push_back(act);
1522 /* Include at most one act per-thread that "happens before" curr */
1523 if (act->happens_before(curr))
1528 if (DBG_ENABLED()) {
1529 model_print("Reached read action:\n");
1531 model_print("End printing read_from_past\n");
1537 * @brief Get an action representing an uninitialized atomic
1539 * This function may create a new one.
1541 * @param curr The current action, which prompts the creation of an UNINIT action
1542 * @return A pointer to the UNINIT ModelAction
1544 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1546 ModelAction *act = curr->get_uninit_action();
1548 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1549 curr->set_uninit_action(act);
1551 act->create_cv(NULL);
1555 static void print_list(action_list_t *list)
1557 sllnode<ModelAction*> *it;
1559 model_print("------------------------------------------------------------------------------------\n");
1560 model_print("# t Action type MO Location Value Rf CV\n");
1561 model_print("------------------------------------------------------------------------------------\n");
1563 unsigned int hash = 0;
1565 for (it = list->begin();it != NULL;it=it->getNext()) {
1566 const ModelAction *act = it->getVal();
1567 if (act->get_seq_number() > 0)
1569 hash = hash^(hash<<3)^(it->getVal()->hash());
1571 model_print("HASH %u\n", hash);
1572 model_print("------------------------------------------------------------------------------------\n");
1575 #if SUPPORT_MOD_ORDER_DUMP
1576 void ModelExecution::dumpGraph(char *filename)
1579 sprintf(buffer, "%s.dot", filename);
1580 FILE *file = fopen(buffer, "w");
1581 fprintf(file, "digraph %s {\n", filename);
1582 mo_graph->dumpNodes(file);
1583 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1585 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1586 ModelAction *act = it->getVal();
1587 if (act->is_read()) {
1588 mo_graph->dot_print_node(file, act);
1589 mo_graph->dot_print_edge(file,
1590 act->get_reads_from(),
1592 "label=\"rf\", color=red, weight=2");
1594 if (thread_array[act->get_tid()]) {
1595 mo_graph->dot_print_edge(file,
1596 thread_array[id_to_int(act->get_tid())],
1598 "label=\"sb\", color=blue, weight=400");
1601 thread_array[act->get_tid()] = act;
1603 fprintf(file, "}\n");
1604 model_free(thread_array);
1609 /** @brief Prints an execution trace summary. */
1610 void ModelExecution::print_summary()
1612 #if SUPPORT_MOD_ORDER_DUMP
1613 char buffername[100];
1614 sprintf(buffername, "exec%04u", get_execution_number());
1615 mo_graph->dumpGraphToFile(buffername);
1616 sprintf(buffername, "graph%04u", get_execution_number());
1617 dumpGraph(buffername);
1620 model_print("Execution trace %d:", get_execution_number());
1621 if (isfeasibleprefix()) {
1622 if (scheduler->all_threads_sleeping())
1623 model_print(" SLEEP-SET REDUNDANT");
1624 if (have_bug_reports())
1625 model_print(" DETECTED BUG(S)");
1627 print_infeasibility(" INFEASIBLE");
1630 print_list(&action_trace);
1636 * Add a Thread to the system for the first time. Should only be called once
1638 * @param t The Thread to add
1640 void ModelExecution::add_thread(Thread *t)
1642 unsigned int i = id_to_int(t->get_id());
1643 if (i >= thread_map.size())
1644 thread_map.resize(i + 1);
1646 if (!t->is_model_thread())
1647 scheduler->add_thread(t);
1651 * @brief Get a Thread reference by its ID
1652 * @param tid The Thread's ID
1653 * @return A Thread reference
1655 Thread * ModelExecution::get_thread(thread_id_t tid) const
1657 unsigned int i = id_to_int(tid);
1658 if (i < thread_map.size())
1659 return thread_map[i];
1664 * @brief Get a reference to the Thread in which a ModelAction was executed
1665 * @param act The ModelAction
1666 * @return A Thread reference
1668 Thread * ModelExecution::get_thread(const ModelAction *act) const
1670 return get_thread(act->get_tid());
1674 * @brief Get a Thread reference by its pthread ID
1675 * @param index The pthread's ID
1676 * @return A Thread reference
1678 Thread * ModelExecution::get_pthread(pthread_t pid) {
1684 uint32_t thread_id = x.v;
1685 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1690 * @brief Check if a Thread is currently enabled
1691 * @param t The Thread to check
1692 * @return True if the Thread is currently enabled
1694 bool ModelExecution::is_enabled(Thread *t) const
1696 return scheduler->is_enabled(t);
1700 * @brief Check if a Thread is currently enabled
1701 * @param tid The ID of the Thread to check
1702 * @return True if the Thread is currently enabled
1704 bool ModelExecution::is_enabled(thread_id_t tid) const
1706 return scheduler->is_enabled(tid);
1710 * @brief Select the next thread to execute based on the curren action
1712 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1713 * actions should be followed by the execution of their child thread. In either
1714 * case, the current action should determine the next thread schedule.
1716 * @param curr The current action
1717 * @return The next thread to run, if the current action will determine this
1718 * selection; otherwise NULL
1720 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1722 /* Do not split atomic RMW */
1723 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1724 return get_thread(curr);
1725 /* Follow CREATE with the created thread */
1726 /* which is not needed, because model.cc takes care of this */
1727 if (curr->get_type() == THREAD_CREATE)
1728 return curr->get_thread_operand();
1729 if (curr->get_type() == PTHREAD_CREATE) {
1730 return curr->get_thread_operand();
1735 /** @param act A read atomic action */
1736 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1738 ASSERT(act->is_read());
1740 // Actions paused by fuzzer have their sequence number reset to 0
1741 return act->get_seq_number() == 0;
1745 * Takes the next step in the execution, if possible.
1746 * @param curr The current step to take
1747 * @return Returns the next Thread to run, if any; NULL if this execution
1750 Thread * ModelExecution::take_step(ModelAction *curr)
1752 Thread *curr_thrd = get_thread(curr);
1753 ASSERT(curr_thrd->get_state() == THREAD_READY);
1755 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1756 curr = check_current_action(curr);
1759 /* Process this action in ModelHistory for records */
1760 model->get_history()->process_action( curr, curr->get_tid() );
1762 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1763 scheduler->remove_thread(curr_thrd);
1765 return action_select_next_thread(curr);
1768 Fuzzer * ModelExecution::getFuzzer() {