11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
34 ~model_snapshot_members() {
35 for (unsigned int i = 0;i < bugs.size();i++)
40 unsigned int next_thread_id;
41 modelclock_t used_sequence_numbers;
42 SnapVector<bug_message *> bugs;
43 /** @brief Incorrectly-ordered synchronization was made */
49 /** @brief Constructor */
50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
54 thread_map(2), /* We'll always need at least 2 threads */
59 condvar_waiters_map(),
63 thrd_last_fence_release(),
64 priv(new struct model_snapshot_members ()),
65 mo_graph(new CycleGraph()),
66 fuzzer(new NewFuzzer()),
69 /* Initialize a model-checker thread, for special ModelActions */
70 model_thread = new Thread(get_next_id());
71 add_thread(model_thread);
72 fuzzer->register_engine(m->get_history(), this);
73 scheduler->register_engine(this);
75 pthread_key_create(&pthreadkey, tlsdestructor);
79 /** @brief Destructor */
80 ModelExecution::~ModelExecution()
82 for (unsigned int i = 0;i < get_num_threads();i++)
83 delete get_thread(int_to_id(i));
89 int ModelExecution::get_execution_number() const
91 return model->get_execution_number();
94 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
96 action_list_t *tmp = hash->get(ptr);
98 tmp = new action_list_t();
104 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
106 SnapVector<action_list_t> *tmp = hash->get(ptr);
108 tmp = new SnapVector<action_list_t>();
114 /** @return a thread ID for a new Thread */
115 thread_id_t ModelExecution::get_next_id()
117 return priv->next_thread_id++;
120 /** @return the number of user threads created during this execution */
121 unsigned int ModelExecution::get_num_threads() const
123 return priv->next_thread_id;
126 /** @return a sequence number for a new ModelAction */
127 modelclock_t ModelExecution::get_next_seq_num()
129 return ++priv->used_sequence_numbers;
132 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
133 void ModelExecution::restore_last_seq_num()
135 priv->used_sequence_numbers--;
139 * @brief Should the current action wake up a given thread?
141 * @param curr The current action
142 * @param thread The thread that we might wake up
143 * @return True, if we should wake up the sleeping thread; false otherwise
145 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
147 const ModelAction *asleep = thread->get_pending();
148 /* Don't allow partial RMW to wake anyone up */
151 /* Synchronizing actions may have been backtracked */
152 if (asleep->could_synchronize_with(curr))
154 /* All acquire/release fences and fence-acquire/store-release */
155 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
157 /* Fence-release + store can awake load-acquire on the same location */
158 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
159 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
160 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
163 /* The sleep is literally sleeping */
164 if (asleep->is_sleep()) {
165 if (fuzzer->shouldWake(asleep))
172 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
174 for (unsigned int i = 0;i < get_num_threads();i++) {
175 Thread *thr = get_thread(int_to_id(i));
176 if (scheduler->is_sleep_set(thr)) {
177 if (should_wake_up(curr, thr)) {
178 /* Remove this thread from sleep set */
179 scheduler->remove_sleep(thr);
180 if (thr->get_pending()->is_sleep())
181 thr->set_wakeup_state(true);
187 void ModelExecution::assert_bug(const char *msg)
189 priv->bugs.push_back(new bug_message(msg));
193 /** @return True, if any bugs have been reported for this execution */
194 bool ModelExecution::have_bug_reports() const
196 return priv->bugs.size() != 0;
199 SnapVector<bug_message *> * ModelExecution::get_bugs() const
205 * Check whether the current trace has triggered an assertion which should halt
208 * @return True, if the execution should be aborted; false otherwise
210 bool ModelExecution::has_asserted() const
212 return priv->asserted;
216 * Trigger a trace assertion which should cause this execution to be halted.
217 * This can be due to a detected bug or due to an infeasibility that should
220 void ModelExecution::set_assert()
222 priv->asserted = true;
226 * Check if we are in a deadlock. Should only be called at the end of an
227 * execution, although it should not give false positives in the middle of an
228 * execution (there should be some ENABLED thread).
230 * @return True if program is in a deadlock; false otherwise
232 bool ModelExecution::is_deadlocked() const
234 bool blocking_threads = false;
235 for (unsigned int i = 0;i < get_num_threads();i++) {
236 thread_id_t tid = int_to_id(i);
239 Thread *t = get_thread(tid);
240 if (!t->is_model_thread() && t->get_pending())
241 blocking_threads = true;
243 return blocking_threads;
247 * Check if this is a complete execution. That is, have all thread completed
248 * execution (rather than exiting because sleep sets have forced a redundant
251 * @return True if the execution is complete.
253 bool ModelExecution::is_complete_execution() const
255 for (unsigned int i = 0;i < get_num_threads();i++)
256 if (is_enabled(int_to_id(i)))
261 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
262 uint64_t value = *((const uint64_t *) location);
263 modelclock_t storeclock;
264 thread_id_t storethread;
265 getStoreThreadAndClock(location, &storethread, &storeclock);
266 setAtomicStoreFlag(location);
267 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
268 act->set_seq_number(storeclock);
269 add_normal_write_to_lists(act);
270 add_write_to_lists(act);
271 w_modification_order(act);
272 model->get_history()->process_action(act, act->get_tid());
277 * Processes a read model action.
278 * @param curr is the read model action to process.
279 * @param rf_set is the set of model actions we can possibly read from
280 * @return True if processing this read updates the mo_graph.
282 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
284 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
285 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
286 if (hasnonatomicstore) {
287 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
288 rf_set->push_back(nonatomicstore);
291 // Remove writes that violate read modification order
293 while (i < rf_set->size()) {
294 ModelAction * rf = (*rf_set)[i];
295 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
296 (*rf_set)[i] = rf_set->back();
303 int index = fuzzer->selectWrite(curr, rf_set);
305 ModelAction *rf = (*rf_set)[index];
308 bool canprune = false;
309 if (r_modification_order(curr, rf, priorset, &canprune)) {
310 for(unsigned int i=0;i<priorset->size();i++) {
311 mo_graph->addEdge((*priorset)[i], rf);
314 get_thread(curr)->set_return_value(curr->get_return_value());
316 if (canprune && curr->get_type() == ATOMIC_READ) {
317 int tid = id_to_int(curr->get_tid());
318 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
319 curr->setThrdMapRef(NULL);
325 /* TODO: Following code not needed anymore */
327 (*rf_set)[index] = rf_set->back();
333 * Processes a lock, trylock, or unlock model action. @param curr is
334 * the read model action to process.
336 * The try lock operation checks whether the lock is taken. If not,
337 * it falls to the normal lock operation case. If so, it returns
340 * The lock operation has already been checked that it is enabled, so
341 * it just grabs the lock and synchronizes with the previous unlock.
343 * The unlock operation has to re-enable all of the threads that are
344 * waiting on the lock.
346 * @return True if synchronization was updated; false otherwise
348 bool ModelExecution::process_mutex(ModelAction *curr)
350 cdsc::mutex *mutex = curr->get_mutex();
351 struct cdsc::mutex_state *state = NULL;
354 state = mutex->get_state();
356 switch (curr->get_type()) {
357 case ATOMIC_TRYLOCK: {
358 bool success = !state->locked;
359 curr->set_try_lock(success);
361 get_thread(curr)->set_return_value(0);
364 get_thread(curr)->set_return_value(1);
366 //otherwise fall into the lock case
368 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
369 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
370 // assert_bug("Lock access before initialization");
371 state->locked = get_thread(curr);
372 ModelAction *unlock = get_last_unlock(curr);
373 //synchronize with the previous unlock statement
374 if (unlock != NULL) {
375 synchronize(unlock, curr);
381 /* wake up the other threads */
382 for (unsigned int i = 0;i < get_num_threads();i++) {
383 Thread *t = get_thread(int_to_id(i));
384 Thread *curr_thrd = get_thread(curr);
385 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
389 /* unlock the lock - after checking who was waiting on it */
390 state->locked = NULL;
392 if (fuzzer->shouldWait(curr)) {
393 /* disable this thread */
394 get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
395 scheduler->sleep(get_thread(curr));
400 case ATOMIC_TIMEDWAIT:
401 case ATOMIC_UNLOCK: {
402 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
404 /* wake up the other threads */
405 for (unsigned int i = 0;i < get_num_threads();i++) {
406 Thread *t = get_thread(int_to_id(i));
407 Thread *curr_thrd = get_thread(curr);
408 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
412 /* unlock the lock - after checking who was waiting on it */
413 state->locked = NULL;
416 case ATOMIC_NOTIFY_ALL: {
417 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
418 //activate all the waiting threads
419 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
420 scheduler->wake(get_thread(rit->getVal()));
425 case ATOMIC_NOTIFY_ONE: {
426 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
427 if (waiters->size() != 0) {
428 Thread * thread = fuzzer->selectNotify(waiters);
429 scheduler->wake(thread);
441 * Process a write ModelAction
442 * @param curr The ModelAction to process
443 * @return True if the mo_graph was updated or promises were resolved
445 void ModelExecution::process_write(ModelAction *curr)
447 w_modification_order(curr);
448 get_thread(curr)->set_return_value(VALUE_NONE);
452 * Process a fence ModelAction
453 * @param curr The ModelAction to process
454 * @return True if synchronization was updated
456 bool ModelExecution::process_fence(ModelAction *curr)
459 * fence-relaxed: no-op
460 * fence-release: only log the occurence (not in this function), for
461 * use in later synchronization
462 * fence-acquire (this function): search for hypothetical release
464 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
466 bool updated = false;
467 if (curr->is_acquire()) {
468 action_list_t *list = &action_trace;
469 sllnode<ModelAction *> * rit;
470 /* Find X : is_read(X) && X --sb-> curr */
471 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
472 ModelAction *act = rit->getVal();
475 if (act->get_tid() != curr->get_tid())
477 /* Stop at the beginning of the thread */
478 if (act->is_thread_start())
480 /* Stop once we reach a prior fence-acquire */
481 if (act->is_fence() && act->is_acquire())
485 /* read-acquire will find its own release sequences */
486 if (act->is_acquire())
489 /* Establish hypothetical release sequences */
490 ClockVector *cv = get_hb_from_write(act->get_reads_from());
491 if (cv != NULL && curr->get_cv()->merge(cv))
499 * @brief Process the current action for thread-related activity
501 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
502 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
503 * synchronization, etc. This function is a no-op for non-THREAD actions
504 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
506 * @param curr The current action
507 * @return True if synchronization was updated or a thread completed
509 void ModelExecution::process_thread_action(ModelAction *curr)
511 switch (curr->get_type()) {
512 case THREAD_CREATE: {
513 thrd_t *thrd = (thrd_t *)curr->get_location();
514 struct thread_params *params = (struct thread_params *)curr->get_value();
515 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
516 curr->set_thread_operand(th);
518 th->set_creation(curr);
521 case PTHREAD_CREATE: {
522 (*(uint32_t *)curr->get_location()) = pthread_counter++;
524 struct pthread_params *params = (struct pthread_params *)curr->get_value();
525 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
526 curr->set_thread_operand(th);
528 th->set_creation(curr);
530 if ( pthread_map.size() < pthread_counter )
531 pthread_map.resize( pthread_counter );
532 pthread_map[ pthread_counter-1 ] = th;
537 Thread *blocking = curr->get_thread_operand();
538 ModelAction *act = get_last_action(blocking->get_id());
539 synchronize(act, curr);
543 Thread *blocking = curr->get_thread_operand();
544 ModelAction *act = get_last_action(blocking->get_id());
545 synchronize(act, curr);
546 break; // WL: to be add (modified)
549 case THREADONLY_FINISH:
550 case THREAD_FINISH: {
551 Thread *th = get_thread(curr);
552 if (curr->get_type() == THREAD_FINISH &&
553 th == model->getInitThread()) {
559 /* Wake up any joining threads */
560 for (unsigned int i = 0;i < get_num_threads();i++) {
561 Thread *waiting = get_thread(int_to_id(i));
562 if (waiting->waiting_on() == th &&
563 waiting->get_pending()->is_thread_join())
564 scheduler->wake(waiting);
573 Thread *th = get_thread(curr);
574 th->set_pending(curr);
575 scheduler->add_sleep(th);
584 * Initialize the current action by performing one or more of the following
585 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
586 * manipulating backtracking sets, allocating and
587 * initializing clock vectors, and computing the promises to fulfill.
589 * @param curr The current action, as passed from the user context; may be
590 * freed/invalidated after the execution of this function, with a different
591 * action "returned" its place (pass-by-reference)
592 * @return True if curr is a newly-explored action; false otherwise
594 bool ModelExecution::initialize_curr_action(ModelAction **curr)
596 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
597 ModelAction *newcurr = process_rmw(*curr);
603 ModelAction *newcurr = *curr;
605 newcurr->set_seq_number(get_next_seq_num());
606 /* Always compute new clock vector */
607 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
609 /* Assign most recent release fence */
610 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
612 return true; /* This was a new ModelAction */
617 * @brief Establish reads-from relation between two actions
619 * Perform basic operations involved with establishing a concrete rf relation,
620 * including setting the ModelAction data and checking for release sequences.
622 * @param act The action that is reading (must be a read)
623 * @param rf The action from which we are reading (must be a write)
625 * @return True if this read established synchronization
628 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
631 ASSERT(rf->is_write());
633 act->set_read_from(rf);
634 if (act->is_acquire()) {
635 ClockVector *cv = get_hb_from_write(rf);
638 act->get_cv()->merge(cv);
643 * @brief Synchronizes two actions
645 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
646 * This function performs the synchronization as well as providing other hooks
647 * for other checks along with synchronization.
649 * @param first The left-hand side of the synchronizes-with relation
650 * @param second The right-hand side of the synchronizes-with relation
651 * @return True if the synchronization was successful (i.e., was consistent
652 * with the execution order); false otherwise
654 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
656 if (*second < *first) {
657 ASSERT(0); //This should not happend
660 return second->synchronize_with(first);
664 * @brief Check whether a model action is enabled.
666 * Checks whether an operation would be successful (i.e., is a lock already
667 * locked, or is the joined thread already complete).
669 * For yield-blocking, yields are never enabled.
671 * @param curr is the ModelAction to check whether it is enabled.
672 * @return a bool that indicates whether the action is enabled.
674 bool ModelExecution::check_action_enabled(ModelAction *curr) {
675 if (curr->is_lock()) {
676 cdsc::mutex *lock = curr->get_mutex();
677 struct cdsc::mutex_state *state = lock->get_state();
680 } else if (curr->is_thread_join()) {
681 Thread *blocking = curr->get_thread_operand();
682 if (!blocking->is_complete()) {
685 } else if (curr->is_sleep()) {
686 if (!fuzzer->shouldSleep(curr))
694 * This is the heart of the model checker routine. It performs model-checking
695 * actions corresponding to a given "current action." Among other processes, it
696 * calculates reads-from relationships, updates synchronization clock vectors,
697 * forms a memory_order constraints graph, and handles replay/backtrack
698 * execution when running permutations of previously-observed executions.
700 * @param curr The current action to process
701 * @return The ModelAction that is actually executed; may be different than
704 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
707 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
708 bool newly_explored = initialize_curr_action(&curr);
712 wake_up_sleeping_actions(curr);
714 /* Add uninitialized actions to lists */
715 if (!second_part_of_rmw)
716 add_uninit_action_to_lists(curr);
718 SnapVector<ModelAction *> * rf_set = NULL;
719 /* Build may_read_from set for newly-created actions */
720 if (newly_explored && curr->is_read())
721 rf_set = build_may_read_from(curr);
723 if (curr->is_read() && !second_part_of_rmw) {
724 process_read(curr, rf_set);
727 ASSERT(rf_set == NULL);
729 /* Add the action to lists */
730 if (!second_part_of_rmw)
731 add_action_to_lists(curr);
733 if (curr->is_write())
734 add_write_to_lists(curr);
736 process_thread_action(curr);
738 if (curr->is_write())
741 if (curr->is_fence())
744 if (curr->is_mutex_op())
750 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
751 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
752 ModelAction *lastread = get_last_action(act->get_tid());
753 lastread->process_rmw(act);
755 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
761 * @brief Updates the mo_graph with the constraints imposed from the current
764 * Basic idea is the following: Go through each other thread and find
765 * the last action that happened before our read. Two cases:
767 * -# The action is a write: that write must either occur before
768 * the write we read from or be the write we read from.
769 * -# The action is a read: the write that that action read from
770 * must occur before the write we read from or be the same write.
772 * @param curr The current action. Must be a read.
773 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
774 * @param check_only If true, then only check whether the current action satisfies
775 * read modification order or not, without modifiying priorset and canprune.
777 * @return True if modification order edges were added; false otherwise
780 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
781 SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
783 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
785 ASSERT(curr->is_read());
787 /* Last SC fence in the current thread */
788 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
790 int tid = curr->get_tid();
791 ModelAction *prev_same_thread = NULL;
792 /* Iterate over all threads */
793 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
794 /* Last SC fence in thread tid */
795 ModelAction *last_sc_fence_thread_local = NULL;
797 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
799 /* Last SC fence in thread tid, before last SC fence in current thread */
800 ModelAction *last_sc_fence_thread_before = NULL;
801 if (last_sc_fence_local)
802 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
804 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
805 if (prev_same_thread != NULL &&
806 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
807 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
811 /* Iterate over actions in thread, starting from most recent */
812 action_list_t *list = &(*thrd_lists)[tid];
813 sllnode<ModelAction *> * rit;
814 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
815 ModelAction *act = rit->getVal();
820 /* Don't want to add reflexive edges on 'rf' */
821 if (act->equals(rf)) {
822 if (act->happens_before(curr))
828 if (act->is_write()) {
829 /* C++, Section 29.3 statement 5 */
830 if (curr->is_seqcst() && last_sc_fence_thread_local &&
831 *act < *last_sc_fence_thread_local) {
832 if (mo_graph->checkReachable(rf, act))
835 priorset->push_back(act);
838 /* C++, Section 29.3 statement 4 */
839 else if (act->is_seqcst() && last_sc_fence_local &&
840 *act < *last_sc_fence_local) {
841 if (mo_graph->checkReachable(rf, act))
844 priorset->push_back(act);
847 /* C++, Section 29.3 statement 6 */
848 else if (last_sc_fence_thread_before &&
849 *act < *last_sc_fence_thread_before) {
850 if (mo_graph->checkReachable(rf, act))
853 priorset->push_back(act);
859 * Include at most one act per-thread that "happens
862 if (act->happens_before(curr)) {
864 if (last_sc_fence_local == NULL ||
865 (*last_sc_fence_local < *act)) {
866 prev_same_thread = act;
869 if (act->is_write()) {
870 if (mo_graph->checkReachable(rf, act))
873 priorset->push_back(act);
875 const ModelAction *prevrf = act->get_reads_from();
876 if (!prevrf->equals(rf)) {
877 if (mo_graph->checkReachable(rf, prevrf))
880 priorset->push_back(prevrf);
882 if (act->get_tid() == curr->get_tid()) {
883 //Can prune curr from obj list
897 * Updates the mo_graph with the constraints imposed from the current write.
899 * Basic idea is the following: Go through each other thread and find
900 * the lastest action that happened before our write. Two cases:
902 * (1) The action is a write => that write must occur before
905 * (2) The action is a read => the write that that action read from
906 * must occur before the current write.
908 * This method also handles two other issues:
910 * (I) Sequential Consistency: Making sure that if the current write is
911 * seq_cst, that it occurs after the previous seq_cst write.
913 * (II) Sending the write back to non-synchronizing reads.
915 * @param curr The current action. Must be a write.
916 * @param send_fv A vector for stashing reads to which we may pass our future
917 * value. If NULL, then don't record any future values.
918 * @return True if modification order edges were added; false otherwise
920 void ModelExecution::w_modification_order(ModelAction *curr)
922 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
924 ASSERT(curr->is_write());
926 SnapList<ModelAction *> edgeset;
928 if (curr->is_seqcst()) {
929 /* We have to at least see the last sequentially consistent write,
930 so we are initialized. */
931 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
932 if (last_seq_cst != NULL) {
933 edgeset.push_back(last_seq_cst);
935 //update map for next query
936 obj_last_sc_map.put(curr->get_location(), curr);
939 /* Last SC fence in the current thread */
940 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
942 /* Iterate over all threads */
943 for (i = 0;i < thrd_lists->size();i++) {
944 /* Last SC fence in thread i, before last SC fence in current thread */
945 ModelAction *last_sc_fence_thread_before = NULL;
946 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
947 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
949 /* Iterate over actions in thread, starting from most recent */
950 action_list_t *list = &(*thrd_lists)[i];
951 sllnode<ModelAction*>* rit;
952 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
953 ModelAction *act = rit->getVal();
956 * 1) If RMW and it actually read from something, then we
957 * already have all relevant edges, so just skip to next
960 * 2) If RMW and it didn't read from anything, we should
961 * whatever edge we can get to speed up convergence.
963 * 3) If normal write, we need to look at earlier actions, so
964 * continue processing list.
966 if (curr->is_rmw()) {
967 if (curr->get_reads_from() != NULL)
975 /* C++, Section 29.3 statement 7 */
976 if (last_sc_fence_thread_before && act->is_write() &&
977 *act < *last_sc_fence_thread_before) {
978 edgeset.push_back(act);
983 * Include at most one act per-thread that "happens
986 if (act->happens_before(curr)) {
988 * Note: if act is RMW, just add edge:
990 * The following edge should be handled elsewhere:
991 * readfrom(act) --mo--> act
994 edgeset.push_back(act);
995 else if (act->is_read()) {
996 //if previous read accessed a null, just keep going
997 edgeset.push_back(act->get_reads_from());
1003 mo_graph->addEdges(&edgeset, curr);
1008 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1009 * some constraints. This method checks one the following constraint (others
1010 * require compiler support):
1012 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1013 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1015 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1017 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1019 /* Iterate over all threads */
1020 for (i = 0;i < thrd_lists->size();i++) {
1021 const ModelAction *write_after_read = NULL;
1023 /* Iterate over actions in thread, starting from most recent */
1024 action_list_t *list = &(*thrd_lists)[i];
1025 sllnode<ModelAction *>* rit;
1026 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1027 ModelAction *act = rit->getVal();
1029 /* Don't disallow due to act == reader */
1030 if (!reader->happens_before(act) || reader == act)
1032 else if (act->is_write())
1033 write_after_read = act;
1034 else if (act->is_read() && act->get_reads_from() != NULL)
1035 write_after_read = act->get_reads_from();
1038 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1045 * Computes the clock vector that happens before propagates from this write.
1047 * @param rf The action that might be part of a release sequence. Must be a
1049 * @return ClockVector of happens before relation.
1052 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1053 SnapVector<ModelAction *> * processset = NULL;
1054 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1055 ASSERT(rf->is_write());
1056 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1058 if (processset == NULL)
1059 processset = new SnapVector<ModelAction *>();
1060 processset->push_back(rf);
1063 int i = (processset == NULL) ? 0 : processset->size();
1065 ClockVector * vec = NULL;
1067 if (rf->get_rfcv() != NULL) {
1068 vec = rf->get_rfcv();
1069 } else if (rf->is_acquire() && rf->is_release()) {
1071 } else if (rf->is_release() && !rf->is_rmw()) {
1073 } else if (rf->is_release()) {
1074 //have rmw that is release and doesn't have a rfcv
1075 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1078 //operation that isn't release
1079 if (rf->get_last_fence_release()) {
1081 vec = rf->get_last_fence_release()->get_cv();
1083 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1089 rf = (*processset)[i];
1093 if (processset != NULL)
1099 * Performs various bookkeeping operations for the current ModelAction when it is
1100 * the first atomic action occurred at its memory location.
1102 * For instance, adds uninitialized action to the per-object, per-thread action vector
1103 * and to the action trace list of all thread actions.
1105 * @param act is the ModelAction to process.
1107 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1109 int tid = id_to_int(act->get_tid());
1110 ModelAction *uninit = NULL;
1112 SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1113 if (objvec->empty() && act->is_atomic_var()) {
1114 uninit = get_uninitialized_action(act);
1115 uninit_id = id_to_int(uninit->get_tid());
1116 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1117 if ((int)vec->size() <= uninit_id) {
1118 int oldsize = (int) vec->size();
1119 vec->resize(uninit_id + 1);
1120 for(int i = oldsize;i < uninit_id + 1;i++) {
1121 new (&(*vec)[i]) action_list_t();
1124 uninit->setActionRef((*vec)[uninit_id].add_front(uninit));
1127 // Update action trace, a total order of all actions
1129 uninit->setTraceRef(action_trace.add_front(uninit));
1131 // Update obj_thrd_map, a per location, per thread, order of actions
1132 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1133 if ((int)vec->size() <= tid) {
1134 uint oldsize = vec->size();
1135 vec->resize(priv->next_thread_id);
1136 for(uint i = oldsize;i < priv->next_thread_id;i++)
1137 new (&(*vec)[i]) action_list_t();
1140 uninit->setThrdMapRef((*vec)[uninit_id].add_front(uninit));
1142 // Update thrd_last_action, the last action taken by each thrad
1143 if ((int)thrd_last_action.size() <= tid)
1144 thrd_last_action.resize(get_num_threads());
1146 thrd_last_action[uninit_id] = uninit;
1151 * Performs various bookkeeping operations for the current ModelAction. For
1152 * instance, adds action to the per-object, per-thread action vector and to the
1153 * action trace list of all thread actions.
1155 * @param act is the ModelAction to add.
1157 void ModelExecution::add_action_to_lists(ModelAction *act)
1159 int tid = id_to_int(act->get_tid());
1160 if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1161 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1162 act->setActionRef(list->add_back(act));
1165 // Update action trace, a total order of all actions
1166 act->setTraceRef(action_trace.add_back(act));
1169 // Update obj_thrd_map, a per location, per thread, order of actions
1170 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1171 if ((int)vec->size() <= tid) {
1172 uint oldsize = vec->size();
1173 vec->resize(priv->next_thread_id);
1174 for(uint i = oldsize;i < priv->next_thread_id;i++)
1175 new (&(*vec)[i]) action_list_t();
1177 act->setThrdMapRef((*vec)[tid].add_back(act));
1179 // Update thrd_last_action, the last action taken by each thread
1180 if ((int)thrd_last_action.size() <= tid)
1181 thrd_last_action.resize(get_num_threads());
1182 thrd_last_action[tid] = act;
1184 // Update thrd_last_fence_release, the last release fence taken by each thread
1185 if (act->is_fence() && act->is_release()) {
1186 if ((int)thrd_last_fence_release.size() <= tid)
1187 thrd_last_fence_release.resize(get_num_threads());
1188 thrd_last_fence_release[tid] = act;
1191 if (act->is_wait()) {
1192 void *mutex_loc = (void *) act->get_value();
1193 act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
1195 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1196 if ((int)vec->size() <= tid) {
1197 uint oldsize = vec->size();
1198 vec->resize(priv->next_thread_id);
1199 for(uint i = oldsize;i < priv->next_thread_id;i++)
1200 new (&(*vec)[i]) action_list_t();
1202 act->setThrdMapRef((*vec)[tid].add_back(act));
1206 sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *act) {
1207 sllnode<ModelAction*> * rit = list->end();
1208 modelclock_t next_seq = act->get_seq_number();
1209 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1210 return list->add_back(act);
1212 for(;rit != NULL;rit=rit->getPrev()) {
1213 if (rit->getVal()->get_seq_number() == next_seq) {
1214 return list->insertAfter(rit, act);
1221 sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1222 sllnode<ModelAction*> * rit = list->end();
1223 modelclock_t next_seq = act->get_seq_number();
1225 act->create_cv(NULL);
1227 } else if (rit->getVal()->get_seq_number() == next_seq) {
1228 act->create_cv(rit->getVal());
1229 return list->add_back(act);
1231 for(;rit != NULL;rit=rit->getPrev()) {
1232 if (rit->getVal()->get_seq_number() == next_seq) {
1233 act->create_cv(rit->getVal());
1234 return list->insertAfter(rit, act);
1242 * Performs various bookkeeping operations for a normal write. The
1243 * complication is that we are typically inserting a normal write
1244 * lazily, so we need to insert it into the middle of lists.
1246 * @param act is the ModelAction to add.
1249 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1251 int tid = id_to_int(act->get_tid());
1252 act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
1254 // Update obj_thrd_map, a per location, per thread, order of actions
1255 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1256 if (tid >= (int)vec->size()) {
1257 uint oldsize =vec->size();
1258 vec->resize(priv->next_thread_id);
1259 for(uint i=oldsize;i<priv->next_thread_id;i++)
1260 new (&(*vec)[i]) action_list_t();
1262 act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
1264 // Update thrd_last_action, the last action taken by each thrad
1265 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1266 thrd_last_action[tid] = act;
1270 void ModelExecution::add_write_to_lists(ModelAction *write) {
1271 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1272 int tid = id_to_int(write->get_tid());
1273 if (tid >= (int)vec->size()) {
1274 uint oldsize =vec->size();
1275 vec->resize(priv->next_thread_id);
1276 for(uint i=oldsize;i<priv->next_thread_id;i++)
1277 new (&(*vec)[i]) action_list_t();
1279 write->setActionRef((*vec)[tid].add_back(write));
1283 * @brief Get the last action performed by a particular Thread
1284 * @param tid The thread ID of the Thread in question
1285 * @return The last action in the thread
1287 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1289 int threadid = id_to_int(tid);
1290 if (threadid < (int)thrd_last_action.size())
1291 return thrd_last_action[id_to_int(tid)];
1297 * @brief Get the last fence release performed by a particular Thread
1298 * @param tid The thread ID of the Thread in question
1299 * @return The last fence release in the thread, if one exists; NULL otherwise
1301 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1303 int threadid = id_to_int(tid);
1304 if (threadid < (int)thrd_last_fence_release.size())
1305 return thrd_last_fence_release[id_to_int(tid)];
1311 * Gets the last memory_order_seq_cst write (in the total global sequence)
1312 * performed on a particular object (i.e., memory location), not including the
1314 * @param curr The current ModelAction; also denotes the object location to
1316 * @return The last seq_cst write
1318 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1320 void *location = curr->get_location();
1321 return obj_last_sc_map.get(location);
1325 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1326 * performed in a particular thread, prior to a particular fence.
1327 * @param tid The ID of the thread to check
1328 * @param before_fence The fence from which to begin the search; if NULL, then
1329 * search for the most recent fence in the thread.
1330 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1332 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1334 /* All fences should have location FENCE_LOCATION */
1335 action_list_t *list = obj_map.get(FENCE_LOCATION);
1340 sllnode<ModelAction*>* rit = list->end();
1343 for (;rit != NULL;rit=rit->getPrev())
1344 if (rit->getVal() == before_fence)
1347 ASSERT(rit->getVal() == before_fence);
1351 for (;rit != NULL;rit=rit->getPrev()) {
1352 ModelAction *act = rit->getVal();
1353 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1360 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1361 * location). This function identifies the mutex according to the current
1362 * action, which is presumed to perform on the same mutex.
1363 * @param curr The current ModelAction; also denotes the object location to
1365 * @return The last unlock operation
1367 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1369 void *location = curr->get_location();
1371 action_list_t *list = obj_map.get(location);
1375 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1376 sllnode<ModelAction*>* rit;
1377 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1378 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1379 return rit->getVal();
1383 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1385 ModelAction *parent = get_last_action(tid);
1387 parent = get_thread(tid)->get_creation();
1392 * Returns the clock vector for a given thread.
1393 * @param tid The thread whose clock vector we want
1394 * @return Desired clock vector
1396 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1398 ModelAction *firstaction=get_parent_action(tid);
1399 return firstaction != NULL ? firstaction->get_cv() : NULL;
1402 bool valequals(uint64_t val1, uint64_t val2, int size) {
1405 return ((uint8_t)val1) == ((uint8_t)val2);
1407 return ((uint16_t)val1) == ((uint16_t)val2);
1409 return ((uint32_t)val1) == ((uint32_t)val2);
1419 * Build up an initial set of all past writes that this 'read' action may read
1420 * from, as well as any previously-observed future values that must still be valid.
1422 * @param curr is the current ModelAction that we are exploring; it must be a
1425 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1427 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1429 ASSERT(curr->is_read());
1431 ModelAction *last_sc_write = NULL;
1433 if (curr->is_seqcst())
1434 last_sc_write = get_last_seq_cst_write(curr);
1436 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1438 /* Iterate over all threads */
1439 for (i = 0;i < thrd_lists->size();i++) {
1440 /* Iterate over actions in thread, starting from most recent */
1441 action_list_t *list = &(*thrd_lists)[i];
1442 sllnode<ModelAction *> * rit;
1443 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1444 ModelAction *act = rit->getVal();
1449 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1450 bool allow_read = true;
1452 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1455 /* Need to check whether we will have two RMW reading from the same value */
1456 if (curr->is_rmwr()) {
1457 /* It is okay if we have a failing CAS */
1458 if (!curr->is_rmwrcas() ||
1459 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1460 //Need to make sure we aren't the second RMW
1461 CycleNode * node = mo_graph->getNode_noCreate(act);
1462 if (node != NULL && node->getRMW() != NULL) {
1463 //we are the second RMW
1470 /* Only add feasible reads */
1471 rf_set->push_back(act);
1474 /* Include at most one act per-thread that "happens before" curr */
1475 if (act->happens_before(curr))
1480 if (DBG_ENABLED()) {
1481 model_print("Reached read action:\n");
1483 model_print("End printing read_from_past\n");
1489 * @brief Get an action representing an uninitialized atomic
1491 * This function may create a new one.
1493 * @param curr The current action, which prompts the creation of an UNINIT action
1494 * @return A pointer to the UNINIT ModelAction
1496 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1498 ModelAction *act = curr->get_uninit_action();
1500 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1501 curr->set_uninit_action(act);
1503 act->create_cv(NULL);
1507 static void print_list(action_list_t *list)
1509 sllnode<ModelAction*> *it;
1511 model_print("------------------------------------------------------------------------------------\n");
1512 model_print("# t Action type MO Location Value Rf CV\n");
1513 model_print("------------------------------------------------------------------------------------\n");
1515 unsigned int hash = 0;
1517 for (it = list->begin();it != NULL;it=it->getNext()) {
1518 const ModelAction *act = it->getVal();
1519 if (act->get_seq_number() > 0)
1521 hash = hash^(hash<<3)^(it->getVal()->hash());
1523 model_print("HASH %u\n", hash);
1524 model_print("------------------------------------------------------------------------------------\n");
1527 #if SUPPORT_MOD_ORDER_DUMP
1528 void ModelExecution::dumpGraph(char *filename)
1531 sprintf(buffer, "%s.dot", filename);
1532 FILE *file = fopen(buffer, "w");
1533 fprintf(file, "digraph %s {\n", filename);
1534 mo_graph->dumpNodes(file);
1535 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1537 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1538 ModelAction *act = it->getVal();
1539 if (act->is_read()) {
1540 mo_graph->dot_print_node(file, act);
1541 mo_graph->dot_print_edge(file,
1542 act->get_reads_from(),
1544 "label=\"rf\", color=red, weight=2");
1546 if (thread_array[act->get_tid()]) {
1547 mo_graph->dot_print_edge(file,
1548 thread_array[id_to_int(act->get_tid())],
1550 "label=\"sb\", color=blue, weight=400");
1553 thread_array[act->get_tid()] = act;
1555 fprintf(file, "}\n");
1556 model_free(thread_array);
1561 /** @brief Prints an execution trace summary. */
1562 void ModelExecution::print_summary()
1564 #if SUPPORT_MOD_ORDER_DUMP
1565 char buffername[100];
1566 sprintf(buffername, "exec%04u", get_execution_number());
1567 mo_graph->dumpGraphToFile(buffername);
1568 sprintf(buffername, "graph%04u", get_execution_number());
1569 dumpGraph(buffername);
1572 model_print("Execution trace %d:", get_execution_number());
1573 if (scheduler->all_threads_sleeping())
1574 model_print(" SLEEP-SET REDUNDANT");
1575 if (have_bug_reports())
1576 model_print(" DETECTED BUG(S)");
1580 print_list(&action_trace);
1586 * Add a Thread to the system for the first time. Should only be called once
1588 * @param t The Thread to add
1590 void ModelExecution::add_thread(Thread *t)
1592 unsigned int i = id_to_int(t->get_id());
1593 if (i >= thread_map.size())
1594 thread_map.resize(i + 1);
1596 if (!t->is_model_thread())
1597 scheduler->add_thread(t);
1601 * @brief Get a Thread reference by its ID
1602 * @param tid The Thread's ID
1603 * @return A Thread reference
1605 Thread * ModelExecution::get_thread(thread_id_t tid) const
1607 unsigned int i = id_to_int(tid);
1608 if (i < thread_map.size())
1609 return thread_map[i];
1614 * @brief Get a reference to the Thread in which a ModelAction was executed
1615 * @param act The ModelAction
1616 * @return A Thread reference
1618 Thread * ModelExecution::get_thread(const ModelAction *act) const
1620 return get_thread(act->get_tid());
1624 * @brief Get a Thread reference by its pthread ID
1625 * @param index The pthread's ID
1626 * @return A Thread reference
1628 Thread * ModelExecution::get_pthread(pthread_t pid) {
1634 uint32_t thread_id = x.v;
1635 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1640 * @brief Check if a Thread is currently enabled
1641 * @param t The Thread to check
1642 * @return True if the Thread is currently enabled
1644 bool ModelExecution::is_enabled(Thread *t) const
1646 return scheduler->is_enabled(t);
1650 * @brief Check if a Thread is currently enabled
1651 * @param tid The ID of the Thread to check
1652 * @return True if the Thread is currently enabled
1654 bool ModelExecution::is_enabled(thread_id_t tid) const
1656 return scheduler->is_enabled(tid);
1660 * @brief Select the next thread to execute based on the curren action
1662 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1663 * actions should be followed by the execution of their child thread. In either
1664 * case, the current action should determine the next thread schedule.
1666 * @param curr The current action
1667 * @return The next thread to run, if the current action will determine this
1668 * selection; otherwise NULL
1670 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1672 /* Do not split atomic RMW */
1673 if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1674 return get_thread(curr);
1675 /* Follow CREATE with the created thread */
1676 /* which is not needed, because model.cc takes care of this */
1677 if (curr->get_type() == THREAD_CREATE)
1678 return curr->get_thread_operand();
1679 if (curr->get_type() == PTHREAD_CREATE) {
1680 return curr->get_thread_operand();
1685 /** @param act A read atomic action */
1686 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1688 ASSERT(act->is_read());
1690 // Actions paused by fuzzer have their sequence number reset to 0
1691 return act->get_seq_number() == 0;
1695 * Takes the next step in the execution, if possible.
1696 * @param curr The current step to take
1697 * @return Returns the next Thread to run, if any; NULL if this execution
1700 Thread * ModelExecution::take_step(ModelAction *curr)
1702 Thread *curr_thrd = get_thread(curr);
1703 ASSERT(curr_thrd->get_state() == THREAD_READY);
1705 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1706 curr = check_current_action(curr);
1709 /* Process this action in ModelHistory for records */
1710 model->get_history()->process_action( curr, curr->get_tid() );
1712 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1713 scheduler->remove_thread(curr_thrd);
1715 return action_select_next_thread(curr);
1718 Fuzzer * ModelExecution::getFuzzer() {