11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
19 #define INITIAL_THREAD_ID 0
22 * Structure for holding small ModelChecker members that should be snapshotted
24 struct model_snapshot_members {
25 model_snapshot_members() :
26 /* First thread created will have id INITIAL_THREAD_ID */
27 next_thread_id(INITIAL_THREAD_ID),
28 used_sequence_numbers(0),
30 bad_synchronization(false),
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 */
44 bool bad_synchronization;
50 /** @brief Constructor */
51 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
56 thread_map(2), /* We'll always need at least 2 threads */
60 condvar_waiters_map(),
64 thrd_last_fence_release(),
65 priv(new struct model_snapshot_members ()),
66 mo_graph(new CycleGraph()),
69 thrd_func_inst_lists()
71 /* Initialize a model-checker thread, for special ModelActions */
72 model_thread = new Thread(get_next_id());
73 add_thread(model_thread);
74 scheduler->register_engine(this);
77 /** @brief Destructor */
78 ModelExecution::~ModelExecution()
80 for (unsigned int i = 0;i < get_num_threads();i++)
81 delete get_thread(int_to_id(i));
87 int ModelExecution::get_execution_number() const
89 return model->get_execution_number();
92 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
94 action_list_t *tmp = hash->get(ptr);
96 tmp = new action_list_t();
102 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
104 SnapVector<action_list_t> *tmp = hash->get(ptr);
106 tmp = new SnapVector<action_list_t>();
112 /** @return a thread ID for a new Thread */
113 thread_id_t ModelExecution::get_next_id()
115 return priv->next_thread_id++;
118 /** @return the number of user threads created during this execution */
119 unsigned int ModelExecution::get_num_threads() const
121 return priv->next_thread_id;
124 /** @return a sequence number for a new ModelAction */
125 modelclock_t ModelExecution::get_next_seq_num()
127 return ++priv->used_sequence_numbers;
131 * @brief Should the current action wake up a given thread?
133 * @param curr The current action
134 * @param thread The thread that we might wake up
135 * @return True, if we should wake up the sleeping thread; false otherwise
137 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
139 const ModelAction *asleep = thread->get_pending();
140 /* Don't allow partial RMW to wake anyone up */
143 /* Synchronizing actions may have been backtracked */
144 if (asleep->could_synchronize_with(curr))
146 /* All acquire/release fences and fence-acquire/store-release */
147 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
149 /* Fence-release + store can awake load-acquire on the same location */
150 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
151 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
152 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
158 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
160 for (unsigned int i = 0;i < get_num_threads();i++) {
161 Thread *thr = get_thread(int_to_id(i));
162 if (scheduler->is_sleep_set(thr)) {
163 if (should_wake_up(curr, thr))
164 /* Remove this thread from sleep set */
165 scheduler->remove_sleep(thr);
170 /** @brief Alert the model-checker that an incorrectly-ordered
171 * synchronization was made */
172 void ModelExecution::set_bad_synchronization()
174 priv->bad_synchronization = true;
177 bool ModelExecution::assert_bug(const char *msg)
179 priv->bugs.push_back(new bug_message(msg));
181 if (isfeasibleprefix()) {
188 /** @return True, if any bugs have been reported for this execution */
189 bool ModelExecution::have_bug_reports() const
191 return priv->bugs.size() != 0;
194 SnapVector<bug_message *> * ModelExecution::get_bugs() const
200 * Check whether the current trace has triggered an assertion which should halt
203 * @return True, if the execution should be aborted; false otherwise
205 bool ModelExecution::has_asserted() const
207 return priv->asserted;
211 * Trigger a trace assertion which should cause this execution to be halted.
212 * This can be due to a detected bug or due to an infeasibility that should
215 void ModelExecution::set_assert()
217 priv->asserted = true;
221 * Check if we are in a deadlock. Should only be called at the end of an
222 * execution, although it should not give false positives in the middle of an
223 * execution (there should be some ENABLED thread).
225 * @return True if program is in a deadlock; false otherwise
227 bool ModelExecution::is_deadlocked() const
229 bool blocking_threads = false;
230 for (unsigned int i = 0;i < get_num_threads();i++) {
231 thread_id_t tid = int_to_id(i);
234 Thread *t = get_thread(tid);
235 if (!t->is_model_thread() && t->get_pending())
236 blocking_threads = true;
238 return blocking_threads;
242 * Check if this is a complete execution. That is, have all thread completed
243 * execution (rather than exiting because sleep sets have forced a redundant
246 * @return True if the execution is complete.
248 bool ModelExecution::is_complete_execution() const
250 for (unsigned int i = 0;i < get_num_threads();i++)
251 if (is_enabled(int_to_id(i)))
256 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
257 uint64_t value = *((const uint64_t *) location);
258 modelclock_t storeclock;
259 thread_id_t storethread;
260 getStoreThreadAndClock(location, &storethread, &storeclock);
261 setAtomicStoreFlag(location);
262 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
263 act->set_seq_number(storeclock);
264 add_normal_write_to_lists(act);
265 add_write_to_lists(act);
266 w_modification_order(act);
272 * Processes a read model action.
273 * @param curr is the read model action to process.
274 * @param rf_set is the set of model actions we can possibly read from
275 * @return True if processing this read updates the mo_graph.
277 void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
279 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
280 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
281 if (hasnonatomicstore) {
282 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
283 rf_set->push_back(nonatomicstore);
287 int index = fuzzer->selectWrite(curr, rf_set);
288 ModelAction *rf = (*rf_set)[index];
292 bool canprune = false;
293 if (r_modification_order(curr, rf, priorset, &canprune)) {
294 for(unsigned int i=0;i<priorset->size();i++) {
295 mo_graph->addEdge((*priorset)[i], rf);
298 get_thread(curr)->set_return_value(curr->get_return_value());
300 if (canprune && curr->get_type() == ATOMIC_READ) {
301 int tid = id_to_int(curr->get_tid());
302 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
307 (*rf_set)[index] = rf_set->back();
313 * Processes a lock, trylock, or unlock model action. @param curr is
314 * the read model action to process.
316 * The try lock operation checks whether the lock is taken. If not,
317 * it falls to the normal lock operation case. If so, it returns
320 * The lock operation has already been checked that it is enabled, so
321 * it just grabs the lock and synchronizes with the previous unlock.
323 * The unlock operation has to re-enable all of the threads that are
324 * waiting on the lock.
326 * @return True if synchronization was updated; false otherwise
328 bool ModelExecution::process_mutex(ModelAction *curr)
330 cdsc::mutex *mutex = curr->get_mutex();
331 struct cdsc::mutex_state *state = NULL;
334 state = mutex->get_state();
336 switch (curr->get_type()) {
337 case ATOMIC_TRYLOCK: {
338 bool success = !state->locked;
339 curr->set_try_lock(success);
341 get_thread(curr)->set_return_value(0);
344 get_thread(curr)->set_return_value(1);
346 //otherwise fall into the lock case
348 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
349 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
350 // assert_bug("Lock access before initialization");
351 state->locked = get_thread(curr);
352 ModelAction *unlock = get_last_unlock(curr);
353 //synchronize with the previous unlock statement
354 if (unlock != NULL) {
355 synchronize(unlock, curr);
361 case ATOMIC_UNLOCK: {
362 //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...
364 /* wake up the other threads */
365 for (unsigned int i = 0;i < get_num_threads();i++) {
366 Thread *t = get_thread(int_to_id(i));
367 Thread *curr_thrd = get_thread(curr);
368 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
372 /* unlock the lock - after checking who was waiting on it */
373 state->locked = NULL;
375 if (!curr->is_wait())
376 break;/* The rest is only for ATOMIC_WAIT */
380 case ATOMIC_NOTIFY_ALL: {
381 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
382 //activate all the waiting threads
383 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
384 scheduler->wake(get_thread(*rit));
389 case ATOMIC_NOTIFY_ONE: {
390 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
391 if (waiters->size() != 0) {
392 Thread * thread = fuzzer->selectNotify(waiters);
393 scheduler->wake(thread);
405 * Process a write ModelAction
406 * @param curr The ModelAction to process
407 * @return True if the mo_graph was updated or promises were resolved
409 void ModelExecution::process_write(ModelAction *curr)
411 w_modification_order(curr);
412 get_thread(curr)->set_return_value(VALUE_NONE);
416 * Process a fence ModelAction
417 * @param curr The ModelAction to process
418 * @return True if synchronization was updated
420 bool ModelExecution::process_fence(ModelAction *curr)
423 * fence-relaxed: no-op
424 * fence-release: only log the occurence (not in this function), for
425 * use in later synchronization
426 * fence-acquire (this function): search for hypothetical release
428 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
430 bool updated = false;
431 if (curr->is_acquire()) {
432 action_list_t *list = &action_trace;
433 action_list_t::reverse_iterator rit;
434 /* Find X : is_read(X) && X --sb-> curr */
435 for (rit = list->rbegin();rit != list->rend();rit++) {
436 ModelAction *act = *rit;
439 if (act->get_tid() != curr->get_tid())
441 /* Stop at the beginning of the thread */
442 if (act->is_thread_start())
444 /* Stop once we reach a prior fence-acquire */
445 if (act->is_fence() && act->is_acquire())
449 /* read-acquire will find its own release sequences */
450 if (act->is_acquire())
453 /* Establish hypothetical release sequences */
454 ClockVector *cv = get_hb_from_write(act);
455 if (curr->get_cv()->merge(cv))
463 * @brief Process the current action for thread-related activity
465 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
466 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
467 * synchronization, etc. This function is a no-op for non-THREAD actions
468 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
470 * @param curr The current action
471 * @return True if synchronization was updated or a thread completed
473 bool ModelExecution::process_thread_action(ModelAction *curr)
475 bool updated = false;
477 switch (curr->get_type()) {
478 case THREAD_CREATE: {
479 thrd_t *thrd = (thrd_t *)curr->get_location();
480 struct thread_params *params = (struct thread_params *)curr->get_value();
481 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
482 curr->set_thread_operand(th);
484 th->set_creation(curr);
487 case PTHREAD_CREATE: {
488 (*(uint32_t *)curr->get_location()) = pthread_counter++;
490 struct pthread_params *params = (struct pthread_params *)curr->get_value();
491 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
492 curr->set_thread_operand(th);
494 th->set_creation(curr);
496 if ( pthread_map.size() < pthread_counter )
497 pthread_map.resize( pthread_counter );
498 pthread_map[ pthread_counter-1 ] = th;
503 Thread *blocking = curr->get_thread_operand();
504 ModelAction *act = get_last_action(blocking->get_id());
505 synchronize(act, curr);
506 updated = true; /* trigger rel-seq checks */
510 Thread *blocking = curr->get_thread_operand();
511 ModelAction *act = get_last_action(blocking->get_id());
512 synchronize(act, curr);
513 updated = true; /* trigger rel-seq checks */
514 break; // WL: to be add (modified)
517 case THREAD_FINISH: {
518 Thread *th = get_thread(curr);
519 /* Wake up any joining threads */
520 for (unsigned int i = 0;i < get_num_threads();i++) {
521 Thread *waiting = get_thread(int_to_id(i));
522 if (waiting->waiting_on() == th &&
523 waiting->get_pending()->is_thread_join())
524 scheduler->wake(waiting);
527 updated = true; /* trigger rel-seq checks */
541 * Initialize the current action by performing one or more of the following
542 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
543 * manipulating backtracking sets, allocating and
544 * initializing clock vectors, and computing the promises to fulfill.
546 * @param curr The current action, as passed from the user context; may be
547 * freed/invalidated after the execution of this function, with a different
548 * action "returned" its place (pass-by-reference)
549 * @return True if curr is a newly-explored action; false otherwise
551 bool ModelExecution::initialize_curr_action(ModelAction **curr)
553 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
554 ModelAction *newcurr = process_rmw(*curr);
560 ModelAction *newcurr = *curr;
562 newcurr->set_seq_number(get_next_seq_num());
563 /* Always compute new clock vector */
564 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
566 /* Assign most recent release fence */
567 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
569 return true; /* This was a new ModelAction */
574 * @brief Establish reads-from relation between two actions
576 * Perform basic operations involved with establishing a concrete rf relation,
577 * including setting the ModelAction data and checking for release sequences.
579 * @param act The action that is reading (must be a read)
580 * @param rf The action from which we are reading (must be a write)
582 * @return True if this read established synchronization
585 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
588 ASSERT(rf->is_write());
590 act->set_read_from(rf);
591 if (act->is_acquire()) {
592 ClockVector *cv = get_hb_from_write(rf);
595 act->get_cv()->merge(cv);
600 * @brief Synchronizes two actions
602 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
603 * This function performs the synchronization as well as providing other hooks
604 * for other checks along with synchronization.
606 * @param first The left-hand side of the synchronizes-with relation
607 * @param second The right-hand side of the synchronizes-with relation
608 * @return True if the synchronization was successful (i.e., was consistent
609 * with the execution order); false otherwise
611 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
613 if (*second < *first) {
614 set_bad_synchronization();
617 return second->synchronize_with(first);
621 * @brief Check whether a model action is enabled.
623 * Checks whether an operation would be successful (i.e., is a lock already
624 * locked, or is the joined thread already complete).
626 * For yield-blocking, yields are never enabled.
628 * @param curr is the ModelAction to check whether it is enabled.
629 * @return a bool that indicates whether the action is enabled.
631 bool ModelExecution::check_action_enabled(ModelAction *curr) {
632 if (curr->is_lock()) {
633 cdsc::mutex *lock = curr->get_mutex();
634 struct cdsc::mutex_state *state = lock->get_state();
637 } else if (curr->is_thread_join()) {
638 Thread *blocking = curr->get_thread_operand();
639 if (!blocking->is_complete()) {
648 * This is the heart of the model checker routine. It performs model-checking
649 * actions corresponding to a given "current action." Among other processes, it
650 * calculates reads-from relationships, updates synchronization clock vectors,
651 * forms a memory_order constraints graph, and handles replay/backtrack
652 * execution when running permutations of previously-observed executions.
654 * @param curr The current action to process
655 * @return The ModelAction that is actually executed; may be different than
658 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
661 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
662 bool newly_explored = initialize_curr_action(&curr);
666 wake_up_sleeping_actions(curr);
668 /* Add the action to lists before any other model-checking tasks */
669 if (!second_part_of_rmw && curr->get_type() != NOOP)
670 add_action_to_lists(curr);
672 if (curr->is_write())
673 add_write_to_lists(curr);
675 SnapVector<ModelAction *> * rf_set = NULL;
676 /* Build may_read_from set for newly-created actions */
677 if (newly_explored && curr->is_read())
678 rf_set = build_may_read_from(curr);
680 process_thread_action(curr);
682 if (curr->is_read() && !second_part_of_rmw) {
683 process_read(curr, rf_set);
686 ASSERT(rf_set == NULL);
689 if (curr->is_write())
692 if (curr->is_fence())
695 if (curr->is_mutex_op())
702 * This is the strongest feasibility check available.
703 * @return whether the current trace (partial or complete) must be a prefix of
706 bool ModelExecution::isfeasibleprefix() const
708 return !is_infeasible();
712 * Print disagnostic information about an infeasible execution
713 * @param prefix A string to prefix the output with; if NULL, then a default
714 * message prefix will be provided
716 void ModelExecution::print_infeasibility(const char *prefix) const
720 if (priv->bad_synchronization)
721 ptr += sprintf(ptr, "[bad sw ordering]");
723 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
727 * Check if the current partial trace is infeasible. Does not check any
728 * end-of-execution flags, which might rule out the execution. Thus, this is
729 * useful only for ruling an execution as infeasible.
730 * @return whether the current partial trace is infeasible.
732 bool ModelExecution::is_infeasible() const
734 return priv->bad_synchronization;
737 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
738 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
739 ModelAction *lastread = get_last_action(act->get_tid());
740 lastread->process_rmw(act);
742 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
748 * @brief Updates the mo_graph with the constraints imposed from the current
751 * Basic idea is the following: Go through each other thread and find
752 * the last action that happened before our read. Two cases:
754 * -# The action is a write: that write must either occur before
755 * the write we read from or be the write we read from.
756 * -# The action is a read: the write that that action read from
757 * must occur before the write we read from or be the same write.
759 * @param curr The current action. Must be a read.
760 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
761 * @return True if modification order edges were added; false otherwise
764 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
766 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
768 ASSERT(curr->is_read());
770 /* Last SC fence in the current thread */
771 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
773 int tid = curr->get_tid();
774 ModelAction *prev_same_thread = NULL;
775 /* Iterate over all threads */
776 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
777 /* Last SC fence in thread tid */
778 ModelAction *last_sc_fence_thread_local = NULL;
780 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
782 /* Last SC fence in thread tid, before last SC fence in current thread */
783 ModelAction *last_sc_fence_thread_before = NULL;
784 if (last_sc_fence_local)
785 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
787 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
788 if (prev_same_thread != NULL &&
789 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
790 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
794 /* Iterate over actions in thread, starting from most recent */
795 action_list_t *list = &(*thrd_lists)[tid];
796 action_list_t::reverse_iterator rit;
797 for (rit = list->rbegin();rit != list->rend();rit++) {
798 ModelAction *act = *rit;
803 /* Don't want to add reflexive edges on 'rf' */
804 if (act->equals(rf)) {
805 if (act->happens_before(curr))
811 if (act->is_write()) {
812 /* C++, Section 29.3 statement 5 */
813 if (curr->is_seqcst() && last_sc_fence_thread_local &&
814 *act < *last_sc_fence_thread_local) {
815 if (mo_graph->checkReachable(rf, act))
817 priorset->push_back(act);
820 /* C++, Section 29.3 statement 4 */
821 else if (act->is_seqcst() && last_sc_fence_local &&
822 *act < *last_sc_fence_local) {
823 if (mo_graph->checkReachable(rf, act))
825 priorset->push_back(act);
828 /* C++, Section 29.3 statement 6 */
829 else if (last_sc_fence_thread_before &&
830 *act < *last_sc_fence_thread_before) {
831 if (mo_graph->checkReachable(rf, act))
833 priorset->push_back(act);
839 * Include at most one act per-thread that "happens
842 if (act->happens_before(curr)) {
844 if (last_sc_fence_local == NULL ||
845 (*last_sc_fence_local < *prev_same_thread)) {
846 prev_same_thread = act;
849 if (act->is_write()) {
850 if (mo_graph->checkReachable(rf, act))
852 priorset->push_back(act);
854 const ModelAction *prevrf = act->get_reads_from();
855 if (!prevrf->equals(rf)) {
856 if (mo_graph->checkReachable(rf, prevrf))
858 priorset->push_back(prevrf);
860 if (act->get_tid() == curr->get_tid()) {
861 //Can prune curr from obj list
874 * Updates the mo_graph with the constraints imposed from the current write.
876 * Basic idea is the following: Go through each other thread and find
877 * the lastest action that happened before our write. Two cases:
879 * (1) The action is a write => that write must occur before
882 * (2) The action is a read => the write that that action read from
883 * must occur before the current write.
885 * This method also handles two other issues:
887 * (I) Sequential Consistency: Making sure that if the current write is
888 * seq_cst, that it occurs after the previous seq_cst write.
890 * (II) Sending the write back to non-synchronizing reads.
892 * @param curr The current action. Must be a write.
893 * @param send_fv A vector for stashing reads to which we may pass our future
894 * value. If NULL, then don't record any future values.
895 * @return True if modification order edges were added; false otherwise
897 void ModelExecution::w_modification_order(ModelAction *curr)
899 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
901 ASSERT(curr->is_write());
903 if (curr->is_seqcst()) {
904 /* We have to at least see the last sequentially consistent write,
905 so we are initialized. */
906 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
907 if (last_seq_cst != NULL) {
908 mo_graph->addEdge(last_seq_cst, curr);
912 /* Last SC fence in the current thread */
913 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
915 /* Iterate over all threads */
916 for (i = 0;i < thrd_lists->size();i++) {
917 /* Last SC fence in thread i, before last SC fence in current thread */
918 ModelAction *last_sc_fence_thread_before = NULL;
919 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
920 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
922 /* Iterate over actions in thread, starting from most recent */
923 action_list_t *list = &(*thrd_lists)[i];
924 action_list_t::reverse_iterator rit;
925 bool force_edge = false;
926 for (rit = list->rbegin();rit != list->rend();rit++) {
927 ModelAction *act = *rit;
930 * 1) If RMW and it actually read from something, then we
931 * already have all relevant edges, so just skip to next
934 * 2) If RMW and it didn't read from anything, we should
935 * whatever edge we can get to speed up convergence.
937 * 3) If normal write, we need to look at earlier actions, so
938 * continue processing list.
941 if (curr->is_rmw()) {
942 if (curr->get_reads_from() != NULL)
950 /* C++, Section 29.3 statement 7 */
951 if (last_sc_fence_thread_before && act->is_write() &&
952 *act < *last_sc_fence_thread_before) {
953 mo_graph->addEdge(act, curr, force_edge);
958 * Include at most one act per-thread that "happens
961 if (act->happens_before(curr)) {
963 * Note: if act is RMW, just add edge:
965 * The following edge should be handled elsewhere:
966 * readfrom(act) --mo--> act
969 mo_graph->addEdge(act, curr, force_edge);
970 else if (act->is_read()) {
971 //if previous read accessed a null, just keep going
972 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
981 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
982 * some constraints. This method checks one the following constraint (others
983 * require compiler support):
985 * If X --hb-> Y --mo-> Z, then X should not read from Z.
986 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
988 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
990 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
992 /* Iterate over all threads */
993 for (i = 0;i < thrd_lists->size();i++) {
994 const ModelAction *write_after_read = NULL;
996 /* Iterate over actions in thread, starting from most recent */
997 action_list_t *list = &(*thrd_lists)[i];
998 action_list_t::reverse_iterator rit;
999 for (rit = list->rbegin();rit != list->rend();rit++) {
1000 ModelAction *act = *rit;
1002 /* Don't disallow due to act == reader */
1003 if (!reader->happens_before(act) || reader == act)
1005 else if (act->is_write())
1006 write_after_read = act;
1007 else if (act->is_read() && act->get_reads_from() != NULL)
1008 write_after_read = act->get_reads_from();
1011 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1018 * Computes the clock vector that happens before propagates from this write.
1020 * @param rf The action that might be part of a release sequence. Must be a
1022 * @return ClockVector of happens before relation.
1025 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1026 SnapVector<ModelAction *> * processset = NULL;
1027 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1028 ASSERT(rf->is_write());
1029 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1031 if (processset == NULL)
1032 processset = new SnapVector<ModelAction *>();
1033 processset->push_back(rf);
1036 int i = (processset == NULL) ? 0 : processset->size();
1038 ClockVector * vec = NULL;
1040 if (rf->get_rfcv() != NULL) {
1041 vec = rf->get_rfcv();
1042 } else if (rf->is_acquire() && rf->is_release()) {
1044 } else if (rf->is_release() && !rf->is_rmw()) {
1046 } else if (rf->is_release()) {
1047 //have rmw that is release and doesn't have a rfcv
1048 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1051 //operation that isn't release
1052 if (rf->get_last_fence_release()) {
1054 vec = rf->get_last_fence_release()->get_cv();
1056 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1062 rf = (*processset)[i];
1066 if (processset != NULL)
1072 * Performs various bookkeeping operations for the current ModelAction. For
1073 * instance, adds action to the per-object, per-thread action vector and to the
1074 * action trace list of all thread actions.
1076 * @param act is the ModelAction to add.
1078 void ModelExecution::add_action_to_lists(ModelAction *act)
1080 int tid = id_to_int(act->get_tid());
1081 ModelAction *uninit = NULL;
1083 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1084 if (list->empty() && act->is_atomic_var()) {
1085 uninit = get_uninitialized_action(act);
1086 uninit_id = id_to_int(uninit->get_tid());
1087 list->push_front(uninit);
1088 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1089 if (uninit_id >= (int)vec->size())
1090 vec->resize(uninit_id + 1);
1091 (*vec)[uninit_id].push_front(uninit);
1093 list->push_back(act);
1095 // Update action trace, a total order of all actions
1096 action_trace.push_back(act);
1098 action_trace.push_front(uninit);
1100 // Update obj_thrd_map, a per location, per thread, order of actions
1101 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1102 if (tid >= (int)vec->size())
1103 vec->resize(priv->next_thread_id);
1104 (*vec)[tid].push_back(act);
1106 (*vec)[uninit_id].push_front(uninit);
1108 // Update thrd_last_action, the last action taken by each thrad
1109 if ((int)thrd_last_action.size() <= tid)
1110 thrd_last_action.resize(get_num_threads());
1111 thrd_last_action[tid] = act;
1113 thrd_last_action[uninit_id] = uninit;
1115 // Update thrd_last_fence_release, the last release fence taken by each thread
1116 if (act->is_fence() && act->is_release()) {
1117 if ((int)thrd_last_fence_release.size() <= tid)
1118 thrd_last_fence_release.resize(get_num_threads());
1119 thrd_last_fence_release[tid] = act;
1122 if (act->is_wait()) {
1123 void *mutex_loc = (void *) act->get_value();
1124 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1126 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1127 if (tid >= (int)vec->size())
1128 vec->resize(priv->next_thread_id);
1129 (*vec)[tid].push_back(act);
1133 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1134 action_list_t::reverse_iterator rit = list->rbegin();
1135 modelclock_t next_seq = act->get_seq_number();
1136 if (rit == list->rend() || (*rit)->get_seq_number() == next_seq)
1137 list->push_back(act);
1139 for(;rit != list->rend();rit++) {
1140 if ((*rit)->get_seq_number() == next_seq) {
1141 action_list_t::iterator it = rit.base();
1142 list->insert(it, act);
1149 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1150 action_list_t::reverse_iterator rit = list->rbegin();
1151 modelclock_t next_seq = act->get_seq_number();
1152 if (rit == list->rend()) {
1153 act->create_cv(NULL);
1154 } else if ((*rit)->get_seq_number() == next_seq) {
1155 act->create_cv((*rit));
1156 list->push_back(act);
1158 for(;rit != list->rend();rit++) {
1159 if ((*rit)->get_seq_number() == next_seq) {
1160 act->create_cv((*rit));
1161 action_list_t::iterator it = rit.base();
1162 list->insert(it, act);
1170 * Performs various bookkeeping operations for a normal write. The
1171 * complication is that we are typically inserting a normal write
1172 * lazily, so we need to insert it into the middle of lists.
1174 * @param act is the ModelAction to add.
1177 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1179 int tid = id_to_int(act->get_tid());
1180 insertIntoActionListAndSetCV(&action_trace, act);
1182 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1183 insertIntoActionList(list, act);
1185 // Update obj_thrd_map, a per location, per thread, order of actions
1186 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1187 if (tid >= (int)vec->size())
1188 vec->resize(priv->next_thread_id);
1189 insertIntoActionList(&(*vec)[tid],act);
1191 // Update thrd_last_action, the last action taken by each thrad
1192 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1193 thrd_last_action[tid] = act;
1197 void ModelExecution::add_write_to_lists(ModelAction *write) {
1198 // Update seq_cst map
1199 if (write->is_seqcst())
1200 obj_last_sc_map.put(write->get_location(), write);
1202 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1203 int tid = id_to_int(write->get_tid());
1204 if (tid >= (int)vec->size())
1205 vec->resize(priv->next_thread_id);
1206 (*vec)[tid].push_back(write);
1210 * @brief Get the last action performed by a particular Thread
1211 * @param tid The thread ID of the Thread in question
1212 * @return The last action in the thread
1214 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1216 int threadid = id_to_int(tid);
1217 if (threadid < (int)thrd_last_action.size())
1218 return thrd_last_action[id_to_int(tid)];
1224 * @brief Get the last fence release performed by a particular Thread
1225 * @param tid The thread ID of the Thread in question
1226 * @return The last fence release in the thread, if one exists; NULL otherwise
1228 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1230 int threadid = id_to_int(tid);
1231 if (threadid < (int)thrd_last_fence_release.size())
1232 return thrd_last_fence_release[id_to_int(tid)];
1238 * Gets the last memory_order_seq_cst write (in the total global sequence)
1239 * performed on a particular object (i.e., memory location), not including the
1241 * @param curr The current ModelAction; also denotes the object location to
1243 * @return The last seq_cst write
1245 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1247 void *location = curr->get_location();
1248 return obj_last_sc_map.get(location);
1252 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1253 * performed in a particular thread, prior to a particular fence.
1254 * @param tid The ID of the thread to check
1255 * @param before_fence The fence from which to begin the search; if NULL, then
1256 * search for the most recent fence in the thread.
1257 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1259 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1261 /* All fences should have location FENCE_LOCATION */
1262 action_list_t *list = obj_map.get(FENCE_LOCATION);
1267 action_list_t::reverse_iterator rit = list->rbegin();
1270 for (;rit != list->rend();rit++)
1271 if (*rit == before_fence)
1274 ASSERT(*rit == before_fence);
1278 for (;rit != list->rend();rit++)
1279 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1285 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1286 * location). This function identifies the mutex according to the current
1287 * action, which is presumed to perform on the same mutex.
1288 * @param curr The current ModelAction; also denotes the object location to
1290 * @return The last unlock operation
1292 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1294 void *location = curr->get_location();
1296 action_list_t *list = obj_map.get(location);
1297 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1298 action_list_t::reverse_iterator rit;
1299 for (rit = list->rbegin();rit != list->rend();rit++)
1300 if ((*rit)->is_unlock() || (*rit)->is_wait())
1305 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1307 ModelAction *parent = get_last_action(tid);
1309 parent = get_thread(tid)->get_creation();
1314 * Returns the clock vector for a given thread.
1315 * @param tid The thread whose clock vector we want
1316 * @return Desired clock vector
1318 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1320 ModelAction *firstaction=get_parent_action(tid);
1321 return firstaction != NULL ? firstaction->get_cv() : NULL;
1324 bool valequals(uint64_t val1, uint64_t val2, int size) {
1327 return ((uint8_t)val1) == ((uint8_t)val2);
1329 return ((uint16_t)val1) == ((uint16_t)val2);
1331 return ((uint32_t)val1) == ((uint32_t)val2);
1341 * Build up an initial set of all past writes that this 'read' action may read
1342 * from, as well as any previously-observed future values that must still be valid.
1344 * @param curr is the current ModelAction that we are exploring; it must be a
1347 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1349 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1351 ASSERT(curr->is_read());
1353 ModelAction *last_sc_write = NULL;
1355 if (curr->is_seqcst())
1356 last_sc_write = get_last_seq_cst_write(curr);
1358 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1360 /* Iterate over all threads */
1361 for (i = 0;i < thrd_lists->size();i++) {
1362 /* Iterate over actions in thread, starting from most recent */
1363 action_list_t *list = &(*thrd_lists)[i];
1364 action_list_t::reverse_iterator rit;
1365 for (rit = list->rbegin();rit != list->rend();rit++) {
1366 ModelAction *act = *rit;
1371 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1372 bool allow_read = true;
1374 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1377 /* Need to check whether we will have two RMW reading from the same value */
1378 if (curr->is_rmwr()) {
1379 /* It is okay if we have a failing CAS */
1380 if (!curr->is_rmwrcas() ||
1381 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1382 //Need to make sure we aren't the second RMW
1383 CycleNode * node = mo_graph->getNode_noCreate(act);
1384 if (node != NULL && node->getRMW() != NULL) {
1385 //we are the second RMW
1392 /* Only add feasible reads */
1393 rf_set->push_back(act);
1396 /* Include at most one act per-thread that "happens before" curr */
1397 if (act->happens_before(curr))
1402 if (DBG_ENABLED()) {
1403 model_print("Reached read action:\n");
1405 model_print("End printing read_from_past\n");
1411 * @brief Get an action representing an uninitialized atomic
1413 * This function may create a new one.
1415 * @param curr The current action, which prompts the creation of an UNINIT action
1416 * @return A pointer to the UNINIT ModelAction
1418 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1420 ModelAction *act = curr->get_uninit_action();
1422 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1423 curr->set_uninit_action(act);
1425 act->create_cv(NULL);
1429 static void print_list(const action_list_t *list)
1431 action_list_t::const_iterator it;
1433 model_print("------------------------------------------------------------------------------------\n");
1434 model_print("# t Action type MO Location Value Rf CV\n");
1435 model_print("------------------------------------------------------------------------------------\n");
1437 unsigned int hash = 0;
1439 for (it = list->begin();it != list->end();it++) {
1440 const ModelAction *act = *it;
1441 if (act->get_seq_number() > 0)
1443 hash = hash^(hash<<3)^((*it)->hash());
1445 model_print("HASH %u\n", hash);
1446 model_print("------------------------------------------------------------------------------------\n");
1449 #if SUPPORT_MOD_ORDER_DUMP
1450 void ModelExecution::dumpGraph(char *filename) const
1453 sprintf(buffer, "%s.dot", filename);
1454 FILE *file = fopen(buffer, "w");
1455 fprintf(file, "digraph %s {\n", filename);
1456 mo_graph->dumpNodes(file);
1457 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1459 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1460 ModelAction *act = *it;
1461 if (act->is_read()) {
1462 mo_graph->dot_print_node(file, act);
1463 mo_graph->dot_print_edge(file,
1464 act->get_reads_from(),
1466 "label=\"rf\", color=red, weight=2");
1468 if (thread_array[act->get_tid()]) {
1469 mo_graph->dot_print_edge(file,
1470 thread_array[id_to_int(act->get_tid())],
1472 "label=\"sb\", color=blue, weight=400");
1475 thread_array[act->get_tid()] = act;
1477 fprintf(file, "}\n");
1478 model_free(thread_array);
1483 /** @brief Prints an execution trace summary. */
1484 void ModelExecution::print_summary() const
1486 #if SUPPORT_MOD_ORDER_DUMP
1487 char buffername[100];
1488 sprintf(buffername, "exec%04u", get_execution_number());
1489 mo_graph->dumpGraphToFile(buffername);
1490 sprintf(buffername, "graph%04u", get_execution_number());
1491 dumpGraph(buffername);
1494 model_print("Execution trace %d:", get_execution_number());
1495 if (isfeasibleprefix()) {
1496 if (scheduler->all_threads_sleeping())
1497 model_print(" SLEEP-SET REDUNDANT");
1498 if (have_bug_reports())
1499 model_print(" DETECTED BUG(S)");
1501 print_infeasibility(" INFEASIBLE");
1504 print_list(&action_trace);
1510 * Add a Thread to the system for the first time. Should only be called once
1512 * @param t The Thread to add
1514 void ModelExecution::add_thread(Thread *t)
1516 unsigned int i = id_to_int(t->get_id());
1517 if (i >= thread_map.size())
1518 thread_map.resize(i + 1);
1520 if (!t->is_model_thread())
1521 scheduler->add_thread(t);
1525 * @brief Get a Thread reference by its ID
1526 * @param tid The Thread's ID
1527 * @return A Thread reference
1529 Thread * ModelExecution::get_thread(thread_id_t tid) const
1531 unsigned int i = id_to_int(tid);
1532 if (i < thread_map.size())
1533 return thread_map[i];
1538 * @brief Get a reference to the Thread in which a ModelAction was executed
1539 * @param act The ModelAction
1540 * @return A Thread reference
1542 Thread * ModelExecution::get_thread(const ModelAction *act) const
1544 return get_thread(act->get_tid());
1548 * @brief Get a Thread reference by its pthread ID
1549 * @param index The pthread's ID
1550 * @return A Thread reference
1552 Thread * ModelExecution::get_pthread(pthread_t pid) {
1558 uint32_t thread_id = x.v;
1559 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1564 * @brief Check if a Thread is currently enabled
1565 * @param t The Thread to check
1566 * @return True if the Thread is currently enabled
1568 bool ModelExecution::is_enabled(Thread *t) const
1570 return scheduler->is_enabled(t);
1574 * @brief Check if a Thread is currently enabled
1575 * @param tid The ID of the Thread to check
1576 * @return True if the Thread is currently enabled
1578 bool ModelExecution::is_enabled(thread_id_t tid) const
1580 return scheduler->is_enabled(tid);
1584 * @brief Select the next thread to execute based on the curren action
1586 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1587 * actions should be followed by the execution of their child thread. In either
1588 * case, the current action should determine the next thread schedule.
1590 * @param curr The current action
1591 * @return The next thread to run, if the current action will determine this
1592 * selection; otherwise NULL
1594 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1596 /* Do not split atomic RMW */
1597 if (curr->is_rmwr())
1598 return get_thread(curr);
1599 /* Follow CREATE with the created thread */
1600 /* which is not needed, because model.cc takes care of this */
1601 if (curr->get_type() == THREAD_CREATE)
1602 return curr->get_thread_operand();
1603 if (curr->get_type() == PTHREAD_CREATE) {
1604 return curr->get_thread_operand();
1610 * Takes the next step in the execution, if possible.
1611 * @param curr The current step to take
1612 * @return Returns the next Thread to run, if any; NULL if this execution
1615 Thread * ModelExecution::take_step(ModelAction *curr)
1617 Thread *curr_thrd = get_thread(curr);
1618 ASSERT(curr_thrd->get_state() == THREAD_READY);
1620 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1621 curr = check_current_action(curr);
1624 // model_print("poitner loc: %p, thread: %d, type: %d, order: %d, position: %s\n", curr, curr->get_tid(), curr->get_type(), curr->get_mo(), curr->get_position() );
1625 model->get_history()->add_func_atomic( curr, curr_thrd->get_id() );
1627 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1628 scheduler->remove_thread(curr_thrd);
1630 return action_select_next_thread(curr);
1633 Fuzzer * ModelExecution::getFuzzer() {