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
306 for (uint i = 0; i < rf_set->size(); i++) {
307 ModelAction * rf = (*rf_set)[i];
308 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
309 (*rf_set)[i] = rf_set->back();
315 int index = fuzzer->selectWrite(curr, rf_set);
316 if (index == -1) // no feasible write exists
319 ModelAction *rf = (*rf_set)[index];
322 bool canprune = false;
323 if (r_modification_order(curr, rf, priorset, &canprune)) {
324 for(unsigned int i=0;i<priorset->size();i++) {
325 mo_graph->addEdge((*priorset)[i], rf);
328 get_thread(curr)->set_return_value(curr->get_return_value());
330 if (canprune && curr->get_type() == ATOMIC_READ) {
331 int tid = id_to_int(curr->get_tid());
332 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
337 (*rf_set)[index] = rf_set->back();
343 * Processes a lock, trylock, or unlock model action. @param curr is
344 * the read model action to process.
346 * The try lock operation checks whether the lock is taken. If not,
347 * it falls to the normal lock operation case. If so, it returns
350 * The lock operation has already been checked that it is enabled, so
351 * it just grabs the lock and synchronizes with the previous unlock.
353 * The unlock operation has to re-enable all of the threads that are
354 * waiting on the lock.
356 * @return True if synchronization was updated; false otherwise
358 bool ModelExecution::process_mutex(ModelAction *curr)
360 cdsc::mutex *mutex = curr->get_mutex();
361 struct cdsc::mutex_state *state = NULL;
364 state = mutex->get_state();
366 switch (curr->get_type()) {
367 case ATOMIC_TRYLOCK: {
368 bool success = !state->locked;
369 curr->set_try_lock(success);
371 get_thread(curr)->set_return_value(0);
374 get_thread(curr)->set_return_value(1);
376 //otherwise fall into the lock case
378 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
379 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
380 // assert_bug("Lock access before initialization");
381 state->locked = get_thread(curr);
382 ModelAction *unlock = get_last_unlock(curr);
383 //synchronize with the previous unlock statement
384 if (unlock != NULL) {
385 synchronize(unlock, curr);
391 /* wake up the other threads */
392 for (unsigned int i = 0;i < get_num_threads();i++) {
393 Thread *t = get_thread(int_to_id(i));
394 Thread *curr_thrd = get_thread(curr);
395 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
399 /* unlock the lock - after checking who was waiting on it */
400 state->locked = NULL;
402 if (fuzzer->shouldWait(curr)) {
403 /* disable this thread */
404 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
405 scheduler->sleep(get_thread(curr));
410 case ATOMIC_TIMEDWAIT:
411 case ATOMIC_UNLOCK: {
412 //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...
414 /* wake up the other threads */
415 for (unsigned int i = 0;i < get_num_threads();i++) {
416 Thread *t = get_thread(int_to_id(i));
417 Thread *curr_thrd = get_thread(curr);
418 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
422 /* unlock the lock - after checking who was waiting on it */
423 state->locked = NULL;
426 case ATOMIC_NOTIFY_ALL: {
427 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
428 //activate all the waiting threads
429 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
430 scheduler->wake(get_thread(rit->getVal()));
435 case ATOMIC_NOTIFY_ONE: {
436 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
437 if (waiters->size() != 0) {
438 Thread * thread = fuzzer->selectNotify(waiters);
439 scheduler->wake(thread);
451 * Process a write ModelAction
452 * @param curr The ModelAction to process
453 * @return True if the mo_graph was updated or promises were resolved
455 void ModelExecution::process_write(ModelAction *curr)
457 w_modification_order(curr);
458 get_thread(curr)->set_return_value(VALUE_NONE);
462 * Process a fence ModelAction
463 * @param curr The ModelAction to process
464 * @return True if synchronization was updated
466 bool ModelExecution::process_fence(ModelAction *curr)
469 * fence-relaxed: no-op
470 * fence-release: only log the occurence (not in this function), for
471 * use in later synchronization
472 * fence-acquire (this function): search for hypothetical release
474 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
476 bool updated = false;
477 if (curr->is_acquire()) {
478 action_list_t *list = &action_trace;
479 sllnode<ModelAction *> * rit;
480 /* Find X : is_read(X) && X --sb-> curr */
481 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
482 ModelAction *act = rit->getVal();
485 if (act->get_tid() != curr->get_tid())
487 /* Stop at the beginning of the thread */
488 if (act->is_thread_start())
490 /* Stop once we reach a prior fence-acquire */
491 if (act->is_fence() && act->is_acquire())
495 /* read-acquire will find its own release sequences */
496 if (act->is_acquire())
499 /* Establish hypothetical release sequences */
500 ClockVector *cv = get_hb_from_write(act->get_reads_from());
501 if (cv != NULL && curr->get_cv()->merge(cv))
509 * @brief Process the current action for thread-related activity
511 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
512 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
513 * synchronization, etc. This function is a no-op for non-THREAD actions
514 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
516 * @param curr The current action
517 * @return True if synchronization was updated or a thread completed
519 void ModelExecution::process_thread_action(ModelAction *curr)
521 switch (curr->get_type()) {
522 case THREAD_CREATE: {
523 thrd_t *thrd = (thrd_t *)curr->get_location();
524 struct thread_params *params = (struct thread_params *)curr->get_value();
525 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
526 curr->set_thread_operand(th);
528 th->set_creation(curr);
531 case PTHREAD_CREATE: {
532 (*(uint32_t *)curr->get_location()) = pthread_counter++;
534 struct pthread_params *params = (struct pthread_params *)curr->get_value();
535 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
536 curr->set_thread_operand(th);
538 th->set_creation(curr);
540 if ( pthread_map.size() < pthread_counter )
541 pthread_map.resize( pthread_counter );
542 pthread_map[ pthread_counter-1 ] = th;
547 Thread *blocking = curr->get_thread_operand();
548 ModelAction *act = get_last_action(blocking->get_id());
549 synchronize(act, curr);
553 Thread *blocking = curr->get_thread_operand();
554 ModelAction *act = get_last_action(blocking->get_id());
555 synchronize(act, curr);
556 break; // WL: to be add (modified)
559 case THREADONLY_FINISH:
560 case THREAD_FINISH: {
561 Thread *th = get_thread(curr);
562 if (curr->get_type() == THREAD_FINISH &&
563 th == model->getInitThread()) {
569 /* Wake up any joining threads */
570 for (unsigned int i = 0;i < get_num_threads();i++) {
571 Thread *waiting = get_thread(int_to_id(i));
572 if (waiting->waiting_on() == th &&
573 waiting->get_pending()->is_thread_join())
574 scheduler->wake(waiting);
583 Thread *th = get_thread(curr);
584 th->set_pending(curr);
585 scheduler->add_sleep(th);
594 * Initialize the current action by performing one or more of the following
595 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
596 * manipulating backtracking sets, allocating and
597 * initializing clock vectors, and computing the promises to fulfill.
599 * @param curr The current action, as passed from the user context; may be
600 * freed/invalidated after the execution of this function, with a different
601 * action "returned" its place (pass-by-reference)
602 * @return True if curr is a newly-explored action; false otherwise
604 bool ModelExecution::initialize_curr_action(ModelAction **curr)
606 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
607 ModelAction *newcurr = process_rmw(*curr);
613 ModelAction *newcurr = *curr;
615 newcurr->set_seq_number(get_next_seq_num());
616 /* Always compute new clock vector */
617 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
619 /* Assign most recent release fence */
620 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
622 return true; /* This was a new ModelAction */
627 * @brief Establish reads-from relation between two actions
629 * Perform basic operations involved with establishing a concrete rf relation,
630 * including setting the ModelAction data and checking for release sequences.
632 * @param act The action that is reading (must be a read)
633 * @param rf The action from which we are reading (must be a write)
635 * @return True if this read established synchronization
638 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
641 ASSERT(rf->is_write());
643 act->set_read_from(rf);
644 if (act->is_acquire()) {
645 ClockVector *cv = get_hb_from_write(rf);
648 act->get_cv()->merge(cv);
653 * @brief Synchronizes two actions
655 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
656 * This function performs the synchronization as well as providing other hooks
657 * for other checks along with synchronization.
659 * @param first The left-hand side of the synchronizes-with relation
660 * @param second The right-hand side of the synchronizes-with relation
661 * @return True if the synchronization was successful (i.e., was consistent
662 * with the execution order); false otherwise
664 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
666 if (*second < *first) {
667 set_bad_synchronization();
670 return second->synchronize_with(first);
674 * @brief Check whether a model action is enabled.
676 * Checks whether an operation would be successful (i.e., is a lock already
677 * locked, or is the joined thread already complete).
679 * For yield-blocking, yields are never enabled.
681 * @param curr is the ModelAction to check whether it is enabled.
682 * @return a bool that indicates whether the action is enabled.
684 bool ModelExecution::check_action_enabled(ModelAction *curr) {
685 if (curr->is_lock()) {
686 cdsc::mutex *lock = curr->get_mutex();
687 struct cdsc::mutex_state *state = lock->get_state();
690 } else if (curr->is_thread_join()) {
691 Thread *blocking = curr->get_thread_operand();
692 if (!blocking->is_complete()) {
695 } else if (curr->is_sleep()) {
696 if (!fuzzer->shouldSleep(curr))
704 * This is the heart of the model checker routine. It performs model-checking
705 * actions corresponding to a given "current action." Among other processes, it
706 * calculates reads-from relationships, updates synchronization clock vectors,
707 * forms a memory_order constraints graph, and handles replay/backtrack
708 * execution when running permutations of previously-observed executions.
710 * @param curr The current action to process
711 * @return The ModelAction that is actually executed; may be different than
714 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
717 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
718 bool newly_explored = initialize_curr_action(&curr);
722 wake_up_sleeping_actions(curr);
724 /* Add uninitialized actions to lists */
725 if (!second_part_of_rmw)
726 add_uninit_action_to_lists(curr);
728 SnapVector<ModelAction *> * rf_set = NULL;
729 /* Build may_read_from set for newly-created actions */
730 if (newly_explored && curr->is_read())
731 rf_set = build_may_read_from(curr);
733 if (curr->is_read() && !second_part_of_rmw) {
734 process_read(curr, rf_set);
737 /* bool success = process_read(curr, rf_set);
740 return curr; // Do not add action to lists
743 ASSERT(rf_set == NULL);
745 /* Add the action to lists */
746 if (!second_part_of_rmw)
747 add_action_to_lists(curr);
749 if (curr->is_write())
750 add_write_to_lists(curr);
752 process_thread_action(curr);
754 if (curr->is_write())
757 if (curr->is_fence())
760 if (curr->is_mutex_op())
767 * This is the strongest feasibility check available.
768 * @return whether the current trace (partial or complete) must be a prefix of
771 bool ModelExecution::isfeasibleprefix() const
773 return !is_infeasible();
777 * Print disagnostic information about an infeasible execution
778 * @param prefix A string to prefix the output with; if NULL, then a default
779 * message prefix will be provided
781 void ModelExecution::print_infeasibility(const char *prefix) const
785 if (priv->bad_synchronization)
786 ptr += sprintf(ptr, "[bad sw ordering]");
788 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
792 * Check if the current partial trace is infeasible. Does not check any
793 * end-of-execution flags, which might rule out the execution. Thus, this is
794 * useful only for ruling an execution as infeasible.
795 * @return whether the current partial trace is infeasible.
797 bool ModelExecution::is_infeasible() const
799 return priv->bad_synchronization;
802 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
803 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
804 ModelAction *lastread = get_last_action(act->get_tid());
805 lastread->process_rmw(act);
807 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
813 * @brief Updates the mo_graph with the constraints imposed from the current
816 * Basic idea is the following: Go through each other thread and find
817 * the last action that happened before our read. Two cases:
819 * -# The action is a write: that write must either occur before
820 * the write we read from or be the write we read from.
821 * -# The action is a read: the write that that action read from
822 * must occur before the write we read from or be the same write.
824 * @param curr The current action. Must be a read.
825 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
826 * @param check_only If true, then only check whether the current action satisfies
827 * read modification order or not, without modifiying priorset and canprune.
829 * @return True if modification order edges were added; false otherwise
832 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
833 SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
835 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
837 ASSERT(curr->is_read());
839 /* Last SC fence in the current thread */
840 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
842 int tid = curr->get_tid();
843 ModelAction *prev_same_thread = NULL;
844 /* Iterate over all threads */
845 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
846 /* Last SC fence in thread tid */
847 ModelAction *last_sc_fence_thread_local = NULL;
849 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
851 /* Last SC fence in thread tid, before last SC fence in current thread */
852 ModelAction *last_sc_fence_thread_before = NULL;
853 if (last_sc_fence_local)
854 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
856 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
857 if (prev_same_thread != NULL &&
858 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
859 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
863 /* Iterate over actions in thread, starting from most recent */
864 action_list_t *list = &(*thrd_lists)[tid];
865 sllnode<ModelAction *> * rit;
866 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
867 ModelAction *act = rit->getVal();
872 /* Don't want to add reflexive edges on 'rf' */
873 if (act->equals(rf)) {
874 if (act->happens_before(curr))
880 if (act->is_write()) {
881 /* C++, Section 29.3 statement 5 */
882 if (curr->is_seqcst() && last_sc_fence_thread_local &&
883 *act < *last_sc_fence_thread_local) {
884 if (mo_graph->checkReachable(rf, act))
887 priorset->push_back(act);
890 /* C++, Section 29.3 statement 4 */
891 else if (act->is_seqcst() && last_sc_fence_local &&
892 *act < *last_sc_fence_local) {
893 if (mo_graph->checkReachable(rf, act))
896 priorset->push_back(act);
899 /* C++, Section 29.3 statement 6 */
900 else if (last_sc_fence_thread_before &&
901 *act < *last_sc_fence_thread_before) {
902 if (mo_graph->checkReachable(rf, act))
905 priorset->push_back(act);
911 * Include at most one act per-thread that "happens
914 if (act->happens_before(curr)) {
916 if (last_sc_fence_local == NULL ||
917 (*last_sc_fence_local < *act)) {
918 prev_same_thread = act;
921 if (act->is_write()) {
922 if (mo_graph->checkReachable(rf, act))
925 priorset->push_back(act);
927 const ModelAction *prevrf = act->get_reads_from();
928 if (!prevrf->equals(rf)) {
929 if (mo_graph->checkReachable(rf, prevrf))
932 priorset->push_back(prevrf);
934 if (act->get_tid() == curr->get_tid()) {
935 //Can prune curr from obj list
949 * Updates the mo_graph with the constraints imposed from the current write.
951 * Basic idea is the following: Go through each other thread and find
952 * the lastest action that happened before our write. Two cases:
954 * (1) The action is a write => that write must occur before
957 * (2) The action is a read => the write that that action read from
958 * must occur before the current write.
960 * This method also handles two other issues:
962 * (I) Sequential Consistency: Making sure that if the current write is
963 * seq_cst, that it occurs after the previous seq_cst write.
965 * (II) Sending the write back to non-synchronizing reads.
967 * @param curr The current action. Must be a write.
968 * @param send_fv A vector for stashing reads to which we may pass our future
969 * value. If NULL, then don't record any future values.
970 * @return True if modification order edges were added; false otherwise
972 void ModelExecution::w_modification_order(ModelAction *curr)
974 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
976 ASSERT(curr->is_write());
978 SnapList<ModelAction *> edgeset;
980 if (curr->is_seqcst()) {
981 /* We have to at least see the last sequentially consistent write,
982 so we are initialized. */
983 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
984 if (last_seq_cst != NULL) {
985 edgeset.push_back(last_seq_cst);
987 //update map for next query
988 obj_last_sc_map.put(curr->get_location(), curr);
991 /* Last SC fence in the current thread */
992 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
994 /* Iterate over all threads */
995 for (i = 0;i < thrd_lists->size();i++) {
996 /* Last SC fence in thread i, before last SC fence in current thread */
997 ModelAction *last_sc_fence_thread_before = NULL;
998 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
999 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1001 /* Iterate over actions in thread, starting from most recent */
1002 action_list_t *list = &(*thrd_lists)[i];
1003 sllnode<ModelAction*>* rit;
1004 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1005 ModelAction *act = rit->getVal();
1008 * 1) If RMW and it actually read from something, then we
1009 * already have all relevant edges, so just skip to next
1012 * 2) If RMW and it didn't read from anything, we should
1013 * whatever edge we can get to speed up convergence.
1015 * 3) If normal write, we need to look at earlier actions, so
1016 * continue processing list.
1018 if (curr->is_rmw()) {
1019 if (curr->get_reads_from() != NULL)
1027 /* C++, Section 29.3 statement 7 */
1028 if (last_sc_fence_thread_before && act->is_write() &&
1029 *act < *last_sc_fence_thread_before) {
1030 edgeset.push_back(act);
1035 * Include at most one act per-thread that "happens
1038 if (act->happens_before(curr)) {
1040 * Note: if act is RMW, just add edge:
1042 * The following edge should be handled elsewhere:
1043 * readfrom(act) --mo--> act
1045 if (act->is_write())
1046 edgeset.push_back(act);
1047 else if (act->is_read()) {
1048 //if previous read accessed a null, just keep going
1049 edgeset.push_back(act->get_reads_from());
1055 mo_graph->addEdges(&edgeset, curr);
1060 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1061 * some constraints. This method checks one the following constraint (others
1062 * require compiler support):
1064 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1065 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1067 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1069 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1071 /* Iterate over all threads */
1072 for (i = 0;i < thrd_lists->size();i++) {
1073 const ModelAction *write_after_read = NULL;
1075 /* Iterate over actions in thread, starting from most recent */
1076 action_list_t *list = &(*thrd_lists)[i];
1077 sllnode<ModelAction *>* rit;
1078 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1079 ModelAction *act = rit->getVal();
1081 /* Don't disallow due to act == reader */
1082 if (!reader->happens_before(act) || reader == act)
1084 else if (act->is_write())
1085 write_after_read = act;
1086 else if (act->is_read() && act->get_reads_from() != NULL)
1087 write_after_read = act->get_reads_from();
1090 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1097 * Computes the clock vector that happens before propagates from this write.
1099 * @param rf The action that might be part of a release sequence. Must be a
1101 * @return ClockVector of happens before relation.
1104 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1105 SnapVector<ModelAction *> * processset = NULL;
1106 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1107 ASSERT(rf->is_write());
1108 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1110 if (processset == NULL)
1111 processset = new SnapVector<ModelAction *>();
1112 processset->push_back(rf);
1115 int i = (processset == NULL) ? 0 : processset->size();
1117 ClockVector * vec = NULL;
1119 if (rf->get_rfcv() != NULL) {
1120 vec = rf->get_rfcv();
1121 } else if (rf->is_acquire() && rf->is_release()) {
1123 } else if (rf->is_release() && !rf->is_rmw()) {
1125 } else if (rf->is_release()) {
1126 //have rmw that is release and doesn't have a rfcv
1127 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1130 //operation that isn't release
1131 if (rf->get_last_fence_release()) {
1133 vec = rf->get_last_fence_release()->get_cv();
1135 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1141 rf = (*processset)[i];
1145 if (processset != NULL)
1151 * Performs various bookkeeping operations for the current ModelAction when it is
1152 * the first atomic action occurred at its memory location.
1154 * For instance, adds uninitialized action to the per-object, per-thread action vector
1155 * and to the action trace list of all thread actions.
1157 * @param act is the ModelAction to process.
1159 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1161 int tid = id_to_int(act->get_tid());
1162 ModelAction *uninit = NULL;
1164 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1165 if (list->empty() && act->is_atomic_var()) {
1166 uninit = get_uninitialized_action(act);
1167 uninit_id = id_to_int(uninit->get_tid());
1168 list->push_front(uninit);
1169 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1170 if ((int)vec->size() <= uninit_id) {
1171 int oldsize = (int) vec->size();
1172 vec->resize(uninit_id + 1);
1173 for(int i = oldsize; i < uninit_id + 1; i++) {
1174 new (&(*vec)[i]) action_list_t();
1177 (*vec)[uninit_id].push_front(uninit);
1180 // Update action trace, a total order of all actions
1182 action_trace.push_front(uninit);
1184 // Update obj_thrd_map, a per location, per thread, order of actions
1185 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1186 if ((int)vec->size() <= tid) {
1187 uint oldsize = vec->size();
1188 vec->resize(priv->next_thread_id);
1189 for(uint i = oldsize; i < priv->next_thread_id; i++)
1190 new (&(*vec)[i]) action_list_t();
1193 (*vec)[uninit_id].push_front(uninit);
1195 // Update thrd_last_action, the last action taken by each thrad
1196 if ((int)thrd_last_action.size() <= tid)
1197 thrd_last_action.resize(get_num_threads());
1199 thrd_last_action[uninit_id] = uninit;
1204 * Performs various bookkeeping operations for the current ModelAction. For
1205 * instance, adds action to the per-object, per-thread action vector and to the
1206 * action trace list of all thread actions.
1208 * @param act is the ModelAction to add.
1210 void ModelExecution::add_action_to_lists(ModelAction *act)
1212 int tid = id_to_int(act->get_tid());
1213 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1214 list->push_back(act);
1216 // Update action trace, a total order of all actions
1217 action_trace.push_back(act);
1219 // Update obj_thrd_map, a per location, per thread, order of actions
1220 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1221 if ((int)vec->size() <= tid) {
1222 uint oldsize = vec->size();
1223 vec->resize(priv->next_thread_id);
1224 for(uint i = oldsize; i < priv->next_thread_id; i++)
1225 new (&(*vec)[i]) action_list_t();
1227 (*vec)[tid].push_back(act);
1229 // Update thrd_last_action, the last action taken by each thrad
1230 if ((int)thrd_last_action.size() <= tid)
1231 thrd_last_action.resize(get_num_threads());
1232 thrd_last_action[tid] = act;
1234 // Update thrd_last_fence_release, the last release fence taken by each thread
1235 if (act->is_fence() && act->is_release()) {
1236 if ((int)thrd_last_fence_release.size() <= tid)
1237 thrd_last_fence_release.resize(get_num_threads());
1238 thrd_last_fence_release[tid] = act;
1241 if (act->is_wait()) {
1242 void *mutex_loc = (void *) act->get_value();
1243 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1245 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1246 if ((int)vec->size() <= tid) {
1247 uint oldsize = vec->size();
1248 vec->resize(priv->next_thread_id);
1249 for(uint i = oldsize; i < priv->next_thread_id; i++)
1250 new (&(*vec)[i]) action_list_t();
1252 (*vec)[tid].push_back(act);
1256 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1257 sllnode<ModelAction*> * rit = list->end();
1258 modelclock_t next_seq = act->get_seq_number();
1259 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1260 list->push_back(act);
1262 for(;rit != NULL;rit=rit->getPrev()) {
1263 if (rit->getVal()->get_seq_number() == next_seq) {
1264 list->insertAfter(rit, act);
1271 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1272 sllnode<ModelAction*> * rit = list->end();
1273 modelclock_t next_seq = act->get_seq_number();
1275 act->create_cv(NULL);
1276 } else if (rit->getVal()->get_seq_number() == next_seq) {
1277 act->create_cv(rit->getVal());
1278 list->push_back(act);
1280 for(;rit != NULL;rit=rit->getPrev()) {
1281 if (rit->getVal()->get_seq_number() == next_seq) {
1282 act->create_cv(rit->getVal());
1283 list->insertAfter(rit, act);
1291 * Performs various bookkeeping operations for a normal write. The
1292 * complication is that we are typically inserting a normal write
1293 * lazily, so we need to insert it into the middle of lists.
1295 * @param act is the ModelAction to add.
1298 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1300 int tid = id_to_int(act->get_tid());
1301 insertIntoActionListAndSetCV(&action_trace, act);
1303 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1304 insertIntoActionList(list, act);
1306 // Update obj_thrd_map, a per location, per thread, order of actions
1307 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1308 if (tid >= (int)vec->size()) {
1309 uint oldsize =vec->size();
1310 vec->resize(priv->next_thread_id);
1311 for(uint i=oldsize;i<priv->next_thread_id;i++)
1312 new (&(*vec)[i]) action_list_t();
1314 insertIntoActionList(&(*vec)[tid],act);
1316 // Update thrd_last_action, the last action taken by each thrad
1317 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1318 thrd_last_action[tid] = act;
1322 void ModelExecution::add_write_to_lists(ModelAction *write) {
1323 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1324 int tid = id_to_int(write->get_tid());
1325 if (tid >= (int)vec->size()) {
1326 uint oldsize =vec->size();
1327 vec->resize(priv->next_thread_id);
1328 for(uint i=oldsize;i<priv->next_thread_id;i++)
1329 new (&(*vec)[i]) action_list_t();
1331 (*vec)[tid].push_back(write);
1335 * @brief Get the last action performed by a particular Thread
1336 * @param tid The thread ID of the Thread in question
1337 * @return The last action in the thread
1339 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1341 int threadid = id_to_int(tid);
1342 if (threadid < (int)thrd_last_action.size())
1343 return thrd_last_action[id_to_int(tid)];
1349 * @brief Get the last fence release performed by a particular Thread
1350 * @param tid The thread ID of the Thread in question
1351 * @return The last fence release in the thread, if one exists; NULL otherwise
1353 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1355 int threadid = id_to_int(tid);
1356 if (threadid < (int)thrd_last_fence_release.size())
1357 return thrd_last_fence_release[id_to_int(tid)];
1363 * Gets the last memory_order_seq_cst write (in the total global sequence)
1364 * performed on a particular object (i.e., memory location), not including the
1366 * @param curr The current ModelAction; also denotes the object location to
1368 * @return The last seq_cst write
1370 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1372 void *location = curr->get_location();
1373 return obj_last_sc_map.get(location);
1377 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1378 * performed in a particular thread, prior to a particular fence.
1379 * @param tid The ID of the thread to check
1380 * @param before_fence The fence from which to begin the search; if NULL, then
1381 * search for the most recent fence in the thread.
1382 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1384 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1386 /* All fences should have location FENCE_LOCATION */
1387 action_list_t *list = obj_map.get(FENCE_LOCATION);
1392 sllnode<ModelAction*>* rit = list->end();
1395 for (;rit != NULL;rit=rit->getPrev())
1396 if (rit->getVal() == before_fence)
1399 ASSERT(rit->getVal() == before_fence);
1403 for (;rit != NULL;rit=rit->getPrev()) {
1404 ModelAction *act = rit->getVal();
1405 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1412 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1413 * location). This function identifies the mutex according to the current
1414 * action, which is presumed to perform on the same mutex.
1415 * @param curr The current ModelAction; also denotes the object location to
1417 * @return The last unlock operation
1419 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1421 void *location = curr->get_location();
1423 action_list_t *list = obj_map.get(location);
1424 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1425 sllnode<ModelAction*>* rit;
1426 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1427 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1428 return rit->getVal();
1432 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1434 ModelAction *parent = get_last_action(tid);
1436 parent = get_thread(tid)->get_creation();
1441 * Returns the clock vector for a given thread.
1442 * @param tid The thread whose clock vector we want
1443 * @return Desired clock vector
1445 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1447 ModelAction *firstaction=get_parent_action(tid);
1448 return firstaction != NULL ? firstaction->get_cv() : NULL;
1451 bool valequals(uint64_t val1, uint64_t val2, int size) {
1454 return ((uint8_t)val1) == ((uint8_t)val2);
1456 return ((uint16_t)val1) == ((uint16_t)val2);
1458 return ((uint32_t)val1) == ((uint32_t)val2);
1468 * Build up an initial set of all past writes that this 'read' action may read
1469 * from, as well as any previously-observed future values that must still be valid.
1471 * @param curr is the current ModelAction that we are exploring; it must be a
1474 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1476 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1478 ASSERT(curr->is_read());
1480 ModelAction *last_sc_write = NULL;
1482 if (curr->is_seqcst())
1483 last_sc_write = get_last_seq_cst_write(curr);
1485 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1487 /* Iterate over all threads */
1488 for (i = 0;i < thrd_lists->size();i++) {
1489 /* Iterate over actions in thread, starting from most recent */
1490 action_list_t *list = &(*thrd_lists)[i];
1491 sllnode<ModelAction *> * rit;
1492 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1493 ModelAction *act = rit->getVal();
1498 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1499 bool allow_read = true;
1501 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1504 /* Need to check whether we will have two RMW reading from the same value */
1505 if (curr->is_rmwr()) {
1506 /* It is okay if we have a failing CAS */
1507 if (!curr->is_rmwrcas() ||
1508 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1509 //Need to make sure we aren't the second RMW
1510 CycleNode * node = mo_graph->getNode_noCreate(act);
1511 if (node != NULL && node->getRMW() != NULL) {
1512 //we are the second RMW
1519 /* Only add feasible reads */
1520 rf_set->push_back(act);
1523 /* Include at most one act per-thread that "happens before" curr */
1524 if (act->happens_before(curr))
1529 if (DBG_ENABLED()) {
1530 model_print("Reached read action:\n");
1532 model_print("End printing read_from_past\n");
1538 * @brief Get an action representing an uninitialized atomic
1540 * This function may create a new one.
1542 * @param curr The current action, which prompts the creation of an UNINIT action
1543 * @return A pointer to the UNINIT ModelAction
1545 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1547 ModelAction *act = curr->get_uninit_action();
1549 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1550 curr->set_uninit_action(act);
1552 act->create_cv(NULL);
1556 static void print_list(action_list_t *list)
1558 sllnode<ModelAction*> *it;
1560 model_print("------------------------------------------------------------------------------------\n");
1561 model_print("# t Action type MO Location Value Rf CV\n");
1562 model_print("------------------------------------------------------------------------------------\n");
1564 unsigned int hash = 0;
1566 for (it = list->begin();it != NULL;it=it->getNext()) {
1567 const ModelAction *act = it->getVal();
1568 if (act->get_seq_number() > 0)
1570 hash = hash^(hash<<3)^(it->getVal()->hash());
1572 model_print("HASH %u\n", hash);
1573 model_print("------------------------------------------------------------------------------------\n");
1576 #if SUPPORT_MOD_ORDER_DUMP
1577 void ModelExecution::dumpGraph(char *filename)
1580 sprintf(buffer, "%s.dot", filename);
1581 FILE *file = fopen(buffer, "w");
1582 fprintf(file, "digraph %s {\n", filename);
1583 mo_graph->dumpNodes(file);
1584 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1586 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1587 ModelAction *act = it->getVal();
1588 if (act->is_read()) {
1589 mo_graph->dot_print_node(file, act);
1590 mo_graph->dot_print_edge(file,
1591 act->get_reads_from(),
1593 "label=\"rf\", color=red, weight=2");
1595 if (thread_array[act->get_tid()]) {
1596 mo_graph->dot_print_edge(file,
1597 thread_array[id_to_int(act->get_tid())],
1599 "label=\"sb\", color=blue, weight=400");
1602 thread_array[act->get_tid()] = act;
1604 fprintf(file, "}\n");
1605 model_free(thread_array);
1610 /** @brief Prints an execution trace summary. */
1611 void ModelExecution::print_summary()
1613 #if SUPPORT_MOD_ORDER_DUMP
1614 char buffername[100];
1615 sprintf(buffername, "exec%04u", get_execution_number());
1616 mo_graph->dumpGraphToFile(buffername);
1617 sprintf(buffername, "graph%04u", get_execution_number());
1618 dumpGraph(buffername);
1621 model_print("Execution trace %d:", get_execution_number());
1622 if (isfeasibleprefix()) {
1623 if (scheduler->all_threads_sleeping())
1624 model_print(" SLEEP-SET REDUNDANT");
1625 if (have_bug_reports())
1626 model_print(" DETECTED BUG(S)");
1628 print_infeasibility(" INFEASIBLE");
1631 print_list(&action_trace);
1637 * Add a Thread to the system for the first time. Should only be called once
1639 * @param t The Thread to add
1641 void ModelExecution::add_thread(Thread *t)
1643 unsigned int i = id_to_int(t->get_id());
1644 if (i >= thread_map.size())
1645 thread_map.resize(i + 1);
1647 if (!t->is_model_thread())
1648 scheduler->add_thread(t);
1652 * @brief Get a Thread reference by its ID
1653 * @param tid The Thread's ID
1654 * @return A Thread reference
1656 Thread * ModelExecution::get_thread(thread_id_t tid) const
1658 unsigned int i = id_to_int(tid);
1659 if (i < thread_map.size())
1660 return thread_map[i];
1665 * @brief Get a reference to the Thread in which a ModelAction was executed
1666 * @param act The ModelAction
1667 * @return A Thread reference
1669 Thread * ModelExecution::get_thread(const ModelAction *act) const
1671 return get_thread(act->get_tid());
1675 * @brief Get a Thread reference by its pthread ID
1676 * @param index The pthread's ID
1677 * @return A Thread reference
1679 Thread * ModelExecution::get_pthread(pthread_t pid) {
1685 uint32_t thread_id = x.v;
1686 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1691 * @brief Check if a Thread is currently enabled
1692 * @param t The Thread to check
1693 * @return True if the Thread is currently enabled
1695 bool ModelExecution::is_enabled(Thread *t) const
1697 return scheduler->is_enabled(t);
1701 * @brief Check if a Thread is currently enabled
1702 * @param tid The ID of the Thread to check
1703 * @return True if the Thread is currently enabled
1705 bool ModelExecution::is_enabled(thread_id_t tid) const
1707 return scheduler->is_enabled(tid);
1711 * @brief Select the next thread to execute based on the curren action
1713 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1714 * actions should be followed by the execution of their child thread. In either
1715 * case, the current action should determine the next thread schedule.
1717 * @param curr The current action
1718 * @return The next thread to run, if the current action will determine this
1719 * selection; otherwise NULL
1721 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1723 /* Do not split atomic RMW */
1724 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1725 return get_thread(curr);
1726 /* Follow CREATE with the created thread */
1727 /* which is not needed, because model.cc takes care of this */
1728 if (curr->get_type() == THREAD_CREATE)
1729 return curr->get_thread_operand();
1730 if (curr->get_type() == PTHREAD_CREATE) {
1731 return curr->get_thread_operand();
1736 /** @param act A read atomic action */
1737 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1739 ASSERT(act->is_read());
1741 // Actions paused by fuzzer have their sequence number reset to 0
1742 return act->get_seq_number() == 0;
1746 * Takes the next step in the execution, if possible.
1747 * @param curr The current step to take
1748 * @return Returns the next Thread to run, if any; NULL if this execution
1751 Thread * ModelExecution::take_step(ModelAction *curr)
1753 Thread *curr_thrd = get_thread(curr);
1754 ASSERT(curr_thrd->get_state() == THREAD_READY);
1756 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1757 curr = check_current_action(curr);
1760 /* Process this action in ModelHistory for records */
1761 // model->get_history()->process_action( curr, curr->get_tid() );
1763 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1764 scheduler->remove_thread(curr_thrd);
1766 return action_select_next_thread(curr);
1769 Fuzzer * ModelExecution::getFuzzer() {