12 #include "clockvector.h"
13 #include "cyclegraph.h"
15 #include "threads-model.h"
16 #include "bugmessage.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
31 bad_synchronization(false),
35 ~model_snapshot_members() {
36 for (unsigned int i = 0;i < bugs.size();i++)
41 unsigned int next_thread_id;
42 modelclock_t used_sequence_numbers;
43 SnapVector<bug_message *> bugs;
44 /** @brief Incorrectly-ordered synchronization was made */
45 bool bad_synchronization;
51 /** @brief Constructor */
52 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) :
57 thread_map(2), /* We'll always need at least 2 threads */
61 condvar_waiters_map(),
65 thrd_last_fence_release(),
66 node_stack(node_stack),
67 priv(new struct model_snapshot_members ()),
68 mo_graph(new CycleGraph()),
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);
75 node_stack->register_engine(this);
78 /** @brief Destructor */
79 ModelExecution::~ModelExecution()
81 for (unsigned int i = 0;i < get_num_threads();i++)
82 delete get_thread(int_to_id(i));
88 int ModelExecution::get_execution_number() const
90 return model->get_execution_number();
93 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
95 action_list_t *tmp = hash->get(ptr);
97 tmp = new action_list_t();
103 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
105 SnapVector<action_list_t> *tmp = hash->get(ptr);
107 tmp = new SnapVector<action_list_t>();
113 /** @return a thread ID for a new Thread */
114 thread_id_t ModelExecution::get_next_id()
116 return priv->next_thread_id++;
119 /** @return the number of user threads created during this execution */
120 unsigned int ModelExecution::get_num_threads() const
122 return priv->next_thread_id;
125 /** @return a sequence number for a new ModelAction */
126 modelclock_t ModelExecution::get_next_seq_num()
128 return ++priv->used_sequence_numbers;
132 * @brief Should the current action wake up a given thread?
134 * @param curr The current action
135 * @param thread The thread that we might wake up
136 * @return True, if we should wake up the sleeping thread; false otherwise
138 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
140 const ModelAction *asleep = thread->get_pending();
141 /* Don't allow partial RMW to wake anyone up */
144 /* Synchronizing actions may have been backtracked */
145 if (asleep->could_synchronize_with(curr))
147 /* All acquire/release fences and fence-acquire/store-release */
148 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
150 /* Fence-release + store can awake load-acquire on the same location */
151 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
152 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
153 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
159 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
161 for (unsigned int i = 0;i < get_num_threads();i++) {
162 Thread *thr = get_thread(int_to_id(i));
163 if (scheduler->is_sleep_set(thr)) {
164 if (should_wake_up(curr, thr))
165 /* Remove this thread from sleep set */
166 scheduler->remove_sleep(thr);
171 /** @brief Alert the model-checker that an incorrectly-ordered
172 * synchronization was made */
173 void ModelExecution::set_bad_synchronization()
175 priv->bad_synchronization = true;
178 bool ModelExecution::assert_bug(const char *msg)
180 priv->bugs.push_back(new bug_message(msg));
182 if (isfeasibleprefix()) {
189 /** @return True, if any bugs have been reported for this execution */
190 bool ModelExecution::have_bug_reports() const
192 return priv->bugs.size() != 0;
195 SnapVector<bug_message *> * ModelExecution::get_bugs() const
201 * Check whether the current trace has triggered an assertion which should halt
204 * @return True, if the execution should be aborted; false otherwise
206 bool ModelExecution::has_asserted() const
208 return priv->asserted;
212 * Trigger a trace assertion which should cause this execution to be halted.
213 * This can be due to a detected bug or due to an infeasibility that should
216 void ModelExecution::set_assert()
218 priv->asserted = true;
222 * Check if we are in a deadlock. Should only be called at the end of an
223 * execution, although it should not give false positives in the middle of an
224 * execution (there should be some ENABLED thread).
226 * @return True if program is in a deadlock; false otherwise
228 bool ModelExecution::is_deadlocked() const
230 bool blocking_threads = false;
231 for (unsigned int i = 0;i < get_num_threads();i++) {
232 thread_id_t tid = int_to_id(i);
235 Thread *t = get_thread(tid);
236 if (!t->is_model_thread() && t->get_pending())
237 blocking_threads = true;
239 return blocking_threads;
243 * Check if this is a complete execution. That is, have all thread completed
244 * execution (rather than exiting because sleep sets have forced a redundant
247 * @return True if the execution is complete.
249 bool ModelExecution::is_complete_execution() const
251 for (unsigned int i = 0;i < get_num_threads();i++)
252 if (is_enabled(int_to_id(i)))
259 * Processes a read model action.
260 * @param curr is the read model action to process.
261 * @param rf_set is the set of model actions we can possibly read from
262 * @return True if processing this read updates the mo_graph.
264 void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set)
266 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
269 int index = fuzzer->selectWrite(curr, rf_set);
270 const ModelAction *rf = (*rf_set)[index];
274 bool canprune = false;
275 if (r_modification_order(curr, rf, priorset, &canprune)) {
276 for(unsigned int i=0;i<priorset->size();i++) {
277 mo_graph->addEdge((*priorset)[i], rf);
280 get_thread(curr)->set_return_value(curr->get_return_value());
282 if (canprune && curr->get_type() == ATOMIC_READ) {
283 int tid = id_to_int(curr->get_tid());
284 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
289 (*rf_set)[index] = rf_set->back();
295 * Processes a lock, trylock, or unlock model action. @param curr is
296 * the read model action to process.
298 * The try lock operation checks whether the lock is taken. If not,
299 * it falls to the normal lock operation case. If so, it returns
302 * The lock operation has already been checked that it is enabled, so
303 * it just grabs the lock and synchronizes with the previous unlock.
305 * The unlock operation has to re-enable all of the threads that are
306 * waiting on the lock.
308 * @return True if synchronization was updated; false otherwise
310 bool ModelExecution::process_mutex(ModelAction *curr)
312 cdsc::mutex *mutex = curr->get_mutex();
313 struct cdsc::mutex_state *state = NULL;
316 state = mutex->get_state();
318 switch (curr->get_type()) {
319 case ATOMIC_TRYLOCK: {
320 bool success = !state->locked;
321 curr->set_try_lock(success);
323 get_thread(curr)->set_return_value(0);
326 get_thread(curr)->set_return_value(1);
328 //otherwise fall into the lock case
330 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
331 assert_bug("Lock access before initialization");
332 state->locked = get_thread(curr);
333 ModelAction *unlock = get_last_unlock(curr);
334 //synchronize with the previous unlock statement
335 if (unlock != NULL) {
336 synchronize(unlock, curr);
342 case ATOMIC_UNLOCK: {
343 //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...
345 /* wake up the other threads */
346 for (unsigned int i = 0;i < get_num_threads();i++) {
347 Thread *t = get_thread(int_to_id(i));
348 Thread *curr_thrd = get_thread(curr);
349 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
353 /* unlock the lock - after checking who was waiting on it */
354 state->locked = NULL;
356 if (!curr->is_wait())
357 break;/* The rest is only for ATOMIC_WAIT */
361 case ATOMIC_NOTIFY_ALL: {
362 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
363 //activate all the waiting threads
364 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
365 scheduler->wake(get_thread(*rit));
370 case ATOMIC_NOTIFY_ONE: {
371 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
372 if (waiters->size() != 0) {
373 Thread * thread = fuzzer->selectNotify(waiters);
374 scheduler->wake(thread);
386 * Process a write ModelAction
387 * @param curr The ModelAction to process
388 * @return True if the mo_graph was updated or promises were resolved
390 void ModelExecution::process_write(ModelAction *curr)
392 w_modification_order(curr);
393 get_thread(curr)->set_return_value(VALUE_NONE);
397 * Process a fence ModelAction
398 * @param curr The ModelAction to process
399 * @return True if synchronization was updated
401 bool ModelExecution::process_fence(ModelAction *curr)
404 * fence-relaxed: no-op
405 * fence-release: only log the occurence (not in this function), for
406 * use in later synchronization
407 * fence-acquire (this function): search for hypothetical release
409 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
411 bool updated = false;
412 if (curr->is_acquire()) {
413 action_list_t *list = &action_trace;
414 action_list_t::reverse_iterator rit;
415 /* Find X : is_read(X) && X --sb-> curr */
416 for (rit = list->rbegin();rit != list->rend();rit++) {
417 ModelAction *act = *rit;
420 if (act->get_tid() != curr->get_tid())
422 /* Stop at the beginning of the thread */
423 if (act->is_thread_start())
425 /* Stop once we reach a prior fence-acquire */
426 if (act->is_fence() && act->is_acquire())
430 /* read-acquire will find its own release sequences */
431 if (act->is_acquire())
434 /* Establish hypothetical release sequences */
435 rel_heads_list_t release_heads;
436 get_release_seq_heads(curr, act, &release_heads);
437 for (unsigned int i = 0;i < release_heads.size();i++)
438 synchronize(release_heads[i], curr);
439 if (release_heads.size() != 0)
447 * @brief Process the current action for thread-related activity
449 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
450 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
451 * synchronization, etc. This function is a no-op for non-THREAD actions
452 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
454 * @param curr The current action
455 * @return True if synchronization was updated or a thread completed
457 bool ModelExecution::process_thread_action(ModelAction *curr)
459 bool updated = false;
461 switch (curr->get_type()) {
462 case THREAD_CREATE: {
463 thrd_t *thrd = (thrd_t *)curr->get_location();
464 struct thread_params *params = (struct thread_params *)curr->get_value();
465 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
466 curr->set_thread_operand(th);
468 th->set_creation(curr);
471 case PTHREAD_CREATE: {
472 (*(uint32_t *)curr->get_location()) = pthread_counter++;
474 struct pthread_params *params = (struct pthread_params *)curr->get_value();
475 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
476 curr->set_thread_operand(th);
478 th->set_creation(curr);
480 if ( pthread_map.size() < pthread_counter )
481 pthread_map.resize( pthread_counter );
482 pthread_map[ pthread_counter-1 ] = th;
487 Thread *blocking = curr->get_thread_operand();
488 ModelAction *act = get_last_action(blocking->get_id());
489 synchronize(act, curr);
490 updated = true; /* trigger rel-seq checks */
494 Thread *blocking = curr->get_thread_operand();
495 ModelAction *act = get_last_action(blocking->get_id());
496 synchronize(act, curr);
497 updated = true; /* trigger rel-seq checks */
498 break; // WL: to be add (modified)
501 case THREAD_FINISH: {
502 Thread *th = get_thread(curr);
503 /* Wake up any joining threads */
504 for (unsigned int i = 0;i < get_num_threads();i++) {
505 Thread *waiting = get_thread(int_to_id(i));
506 if (waiting->waiting_on() == th &&
507 waiting->get_pending()->is_thread_join())
508 scheduler->wake(waiting);
511 updated = true; /* trigger rel-seq checks */
525 * Initialize the current action by performing one or more of the following
526 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
527 * in the NodeStack, manipulating backtracking sets, allocating and
528 * initializing clock vectors, and computing the promises to fulfill.
530 * @param curr The current action, as passed from the user context; may be
531 * freed/invalidated after the execution of this function, with a different
532 * action "returned" its place (pass-by-reference)
533 * @return True if curr is a newly-explored action; false otherwise
535 bool ModelExecution::initialize_curr_action(ModelAction **curr)
537 ModelAction *newcurr;
539 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
540 newcurr = process_rmw(*curr);
547 (*curr)->set_seq_number(get_next_seq_num());
549 newcurr = node_stack->explore_action(*curr);
551 /* First restore type and order in case of RMW operation */
552 if ((*curr)->is_rmwr())
553 newcurr->copy_typeandorder(*curr);
555 ASSERT((*curr)->get_location() == newcurr->get_location());
556 newcurr->copy_from_new(*curr);
558 /* Discard duplicate ModelAction; use action from NodeStack */
561 /* Always compute new clock vector */
562 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
565 return false; /* Action was explored previously */
569 /* Always compute new clock vector */
570 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
572 /* Assign most recent release fence */
573 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
575 return true; /* This was a new ModelAction */
580 * @brief Establish reads-from relation between two actions
582 * Perform basic operations involved with establishing a concrete rf relation,
583 * including setting the ModelAction data and checking for release sequences.
585 * @param act The action that is reading (must be a read)
586 * @param rf The action from which we are reading (must be a write)
588 * @return True if this read established synchronization
591 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
594 ASSERT(rf->is_write());
596 act->set_read_from(rf);
597 if (act->is_acquire()) {
598 rel_heads_list_t release_heads;
599 get_release_seq_heads(act, act, &release_heads);
600 int num_heads = release_heads.size();
601 for (unsigned int i = 0;i < release_heads.size();i++)
602 if (!synchronize(release_heads[i], act))
604 return num_heads > 0;
610 * @brief Synchronizes two actions
612 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
613 * This function performs the synchronization as well as providing other hooks
614 * for other checks along with synchronization.
616 * @param first The left-hand side of the synchronizes-with relation
617 * @param second The right-hand side of the synchronizes-with relation
618 * @return True if the synchronization was successful (i.e., was consistent
619 * with the execution order); false otherwise
621 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
623 if (*second < *first) {
624 set_bad_synchronization();
627 return second->synchronize_with(first);
631 * @brief Check whether a model action is enabled.
633 * Checks whether an operation would be successful (i.e., is a lock already
634 * locked, or is the joined thread already complete).
636 * For yield-blocking, yields are never enabled.
638 * @param curr is the ModelAction to check whether it is enabled.
639 * @return a bool that indicates whether the action is enabled.
641 bool ModelExecution::check_action_enabled(ModelAction *curr) {
642 if (curr->is_lock()) {
643 cdsc::mutex *lock = curr->get_mutex();
644 struct cdsc::mutex_state *state = lock->get_state();
647 } else if (curr->is_thread_join()) {
648 Thread *blocking = curr->get_thread_operand();
649 if (!blocking->is_complete()) {
658 * This is the heart of the model checker routine. It performs model-checking
659 * actions corresponding to a given "current action." Among other processes, it
660 * calculates reads-from relationships, updates synchronization clock vectors,
661 * forms a memory_order constraints graph, and handles replay/backtrack
662 * execution when running permutations of previously-observed executions.
664 * @param curr The current action to process
665 * @return The ModelAction that is actually executed; may be different than
668 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
671 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
672 bool newly_explored = initialize_curr_action(&curr);
676 wake_up_sleeping_actions(curr);
678 /* Add the action to lists before any other model-checking tasks */
679 if (!second_part_of_rmw && curr->get_type() != NOOP)
680 add_action_to_lists(curr);
682 SnapVector<const ModelAction *> * rf_set = NULL;
683 /* Build may_read_from set for newly-created actions */
684 if (newly_explored && curr->is_read())
685 rf_set = build_may_read_from(curr);
687 process_thread_action(curr);
689 if (curr->is_read() && !second_part_of_rmw) {
690 process_read(curr, rf_set);
693 ASSERT(rf_set == NULL);
696 if (curr->is_write())
699 if (curr->is_fence())
702 if (curr->is_mutex_op())
709 * This is the strongest feasibility check available.
710 * @return whether the current trace (partial or complete) must be a prefix of
713 bool ModelExecution::isfeasibleprefix() const
715 return !is_infeasible();
719 * Print disagnostic information about an infeasible execution
720 * @param prefix A string to prefix the output with; if NULL, then a default
721 * message prefix will be provided
723 void ModelExecution::print_infeasibility(const char *prefix) const
727 if (priv->bad_synchronization)
728 ptr += sprintf(ptr, "[bad sw ordering]");
730 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
734 * Check if the current partial trace is infeasible. Does not check any
735 * end-of-execution flags, which might rule out the execution. Thus, this is
736 * useful only for ruling an execution as infeasible.
737 * @return whether the current partial trace is infeasible.
739 bool ModelExecution::is_infeasible() const
741 return priv->bad_synchronization;
744 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
745 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
746 ModelAction *lastread = get_last_action(act->get_tid());
747 lastread->process_rmw(act);
749 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
755 * @brief Updates the mo_graph with the constraints imposed from the current
758 * Basic idea is the following: Go through each other thread and find
759 * the last action that happened before our read. Two cases:
761 * -# The action is a write: that write must either occur before
762 * the write we read from or be the write we read from.
763 * -# The action is a read: the write that that action read from
764 * must occur before the write we read from or be the same write.
766 * @param curr The current action. Must be a read.
767 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
768 * @return True if modification order edges were added; false otherwise
771 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
773 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
775 ASSERT(curr->is_read());
777 /* Last SC fence in the current thread */
778 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
780 int tid = curr->get_tid();
781 ModelAction *prev_same_thread = NULL;
782 /* Iterate over all threads */
783 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
784 /* Last SC fence in thread tid */
785 ModelAction *last_sc_fence_thread_local = NULL;
787 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
789 /* Last SC fence in thread tid, before last SC fence in current thread */
790 ModelAction *last_sc_fence_thread_before = NULL;
791 if (last_sc_fence_local)
792 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
794 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
795 if (prev_same_thread != NULL &&
796 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
797 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
801 /* Iterate over actions in thread, starting from most recent */
802 action_list_t *list = &(*thrd_lists)[tid];
803 action_list_t::reverse_iterator rit;
804 for (rit = list->rbegin();rit != list->rend();rit++) {
805 ModelAction *act = *rit;
810 /* Don't want to add reflexive edges on 'rf' */
811 if (act->equals(rf)) {
812 if (act->happens_before(curr))
818 if (act->is_write()) {
819 /* C++, Section 29.3 statement 5 */
820 if (curr->is_seqcst() && last_sc_fence_thread_local &&
821 *act < *last_sc_fence_thread_local) {
822 if (mo_graph->checkReachable(rf, act))
824 priorset->push_back(act);
827 /* C++, Section 29.3 statement 4 */
828 else if (act->is_seqcst() && last_sc_fence_local &&
829 *act < *last_sc_fence_local) {
830 if (mo_graph->checkReachable(rf, act))
832 priorset->push_back(act);
835 /* C++, Section 29.3 statement 6 */
836 else if (last_sc_fence_thread_before &&
837 *act < *last_sc_fence_thread_before) {
838 if (mo_graph->checkReachable(rf, act))
840 priorset->push_back(act);
846 * Include at most one act per-thread that "happens
849 if (act->happens_before(curr)) {
851 if (last_sc_fence_local == NULL ||
852 (*last_sc_fence_local < *prev_same_thread)) {
853 prev_same_thread = act;
856 if (act->is_write()) {
857 if (mo_graph->checkReachable(rf, act))
859 priorset->push_back(act);
861 const ModelAction *prevrf = act->get_reads_from();
862 if (!prevrf->equals(rf)) {
863 if (mo_graph->checkReachable(rf, prevrf))
865 priorset->push_back(prevrf);
867 if (act->get_tid() == curr->get_tid()) {
868 //Can prune curr from obj list
881 * Updates the mo_graph with the constraints imposed from the current write.
883 * Basic idea is the following: Go through each other thread and find
884 * the lastest action that happened before our write. Two cases:
886 * (1) The action is a write => that write must occur before
889 * (2) The action is a read => the write that that action read from
890 * must occur before the current write.
892 * This method also handles two other issues:
894 * (I) Sequential Consistency: Making sure that if the current write is
895 * seq_cst, that it occurs after the previous seq_cst write.
897 * (II) Sending the write back to non-synchronizing reads.
899 * @param curr The current action. Must be a write.
900 * @param send_fv A vector for stashing reads to which we may pass our future
901 * value. If NULL, then don't record any future values.
902 * @return True if modification order edges were added; false otherwise
904 void ModelExecution::w_modification_order(ModelAction *curr)
906 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
908 ASSERT(curr->is_write());
910 if (curr->is_seqcst()) {
911 /* We have to at least see the last sequentially consistent write,
912 so we are initialized. */
913 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
914 if (last_seq_cst != NULL) {
915 mo_graph->addEdge(last_seq_cst, curr);
919 /* Last SC fence in the current thread */
920 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
922 /* Iterate over all threads */
923 for (i = 0;i < thrd_lists->size();i++) {
924 /* Last SC fence in thread i, before last SC fence in current thread */
925 ModelAction *last_sc_fence_thread_before = NULL;
926 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
927 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
929 /* Iterate over actions in thread, starting from most recent */
930 action_list_t *list = &(*thrd_lists)[i];
931 action_list_t::reverse_iterator rit;
932 bool force_edge = false;
933 for (rit = list->rbegin();rit != list->rend();rit++) {
934 ModelAction *act = *rit;
937 * 1) If RMW and it actually read from something, then we
938 * already have all relevant edges, so just skip to next
941 * 2) If RMW and it didn't read from anything, we should
942 * whatever edge we can get to speed up convergence.
944 * 3) If normal write, we need to look at earlier actions, so
945 * continue processing list.
948 if (curr->is_rmw()) {
949 if (curr->get_reads_from() != NULL)
957 /* C++, Section 29.3 statement 7 */
958 if (last_sc_fence_thread_before && act->is_write() &&
959 *act < *last_sc_fence_thread_before) {
960 mo_graph->addEdge(act, curr, force_edge);
965 * Include at most one act per-thread that "happens
968 if (act->happens_before(curr)) {
970 * Note: if act is RMW, just add edge:
972 * The following edge should be handled elsewhere:
973 * readfrom(act) --mo--> act
976 mo_graph->addEdge(act, curr, force_edge);
977 else if (act->is_read()) {
978 //if previous read accessed a null, just keep going
979 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
982 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
983 !act->same_thread(curr)) {
984 /* We have an action that:
985 (1) did not happen before us
986 (2) is a read and we are a write
987 (3) cannot synchronize with us
988 (4) is in a different thread
990 that read could potentially read from our write. Note that
991 these checks are overly conservative at this point, we'll
992 do more checks before actually removing the
1003 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1004 * some constraints. This method checks one the following constraint (others
1005 * require compiler support):
1007 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1008 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1010 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1012 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1014 /* Iterate over all threads */
1015 for (i = 0;i < thrd_lists->size();i++) {
1016 const ModelAction *write_after_read = NULL;
1018 /* Iterate over actions in thread, starting from most recent */
1019 action_list_t *list = &(*thrd_lists)[i];
1020 action_list_t::reverse_iterator rit;
1021 for (rit = list->rbegin();rit != list->rend();rit++) {
1022 ModelAction *act = *rit;
1024 /* Don't disallow due to act == reader */
1025 if (!reader->happens_before(act) || reader == act)
1027 else if (act->is_write())
1028 write_after_read = act;
1029 else if (act->is_read() && act->get_reads_from() != NULL)
1030 write_after_read = act->get_reads_from();
1033 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1040 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1041 * The ModelAction under consideration is expected to be taking part in
1042 * release/acquire synchronization as an object of the "reads from" relation.
1043 * Note that this can only provide release sequence support for RMW chains
1044 * which do not read from the future, as those actions cannot be traced until
1045 * their "promise" is fulfilled. Similarly, we may not even establish the
1046 * presence of a release sequence with certainty, as some modification order
1047 * constraints may be decided further in the future. Thus, this function
1048 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1049 * and a boolean representing certainty.
1051 * @param rf The action that might be part of a release sequence. Must be a
1053 * @param release_heads A pass-by-reference style return parameter. After
1054 * execution of this function, release_heads will contain the heads of all the
1055 * relevant release sequences, if any exists with certainty
1056 * @return true, if the ModelExecution is certain that release_heads is complete;
1059 bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
1062 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1063 ASSERT(rf->is_write());
1065 if (rf->is_release())
1066 release_heads->push_back(rf);
1067 else if (rf->get_last_fence_release())
1068 release_heads->push_back(rf->get_last_fence_release());
1070 break;/* End of RMW chain */
1072 /** @todo Need to be smarter here... In the linux lock
1073 * example, this will run to the beginning of the program for
1075 /** @todo The way to be smarter here is to keep going until 1
1076 * thread has a release preceded by an acquire and you've seen
1079 /* acq_rel RMW is a sufficient stopping condition */
1080 if (rf->is_acquire() && rf->is_release())
1081 return true;/* complete */
1083 ASSERT(rf); // Needs to be real write
1085 if (rf->is_release())
1086 return true;/* complete */
1088 /* else relaxed write
1089 * - check for fence-release in the same thread (29.8, stmt. 3)
1090 * - check modification order for contiguous subsequence
1091 * -> rf must be same thread as release */
1093 const ModelAction *fence_release = rf->get_last_fence_release();
1094 /* Synchronize with a fence-release unconditionally; we don't need to
1095 * find any more "contiguous subsequence..." for it */
1097 release_heads->push_back(fence_release);
1099 return true; /* complete */
1103 * An interface for getting the release sequence head(s) with which a
1104 * given ModelAction must synchronize. This function only returns a non-empty
1105 * result when it can locate a release sequence head with certainty. Otherwise,
1106 * it may mark the internal state of the ModelExecution so that it will handle
1107 * the release sequence at a later time, causing @a acquire to update its
1108 * synchronization at some later point in execution.
1110 * @param acquire The 'acquire' action that may synchronize with a release
1112 * @param read The read action that may read from a release sequence; this may
1113 * be the same as acquire, or else an earlier action in the same thread (i.e.,
1114 * when 'acquire' is a fence-acquire)
1115 * @param release_heads A pass-by-reference return parameter. Will be filled
1116 * with the head(s) of the release sequence(s), if they exists with certainty.
1117 * @see ModelExecution::release_seq_heads
1119 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
1120 ModelAction *read, rel_heads_list_t *release_heads)
1122 const ModelAction *rf = read->get_reads_from();
1124 release_seq_heads(rf, release_heads);
1128 * Performs various bookkeeping operations for the current ModelAction. For
1129 * instance, adds action to the per-object, per-thread action vector and to the
1130 * action trace list of all thread actions.
1132 * @param act is the ModelAction to add.
1134 void ModelExecution::add_action_to_lists(ModelAction *act)
1136 int tid = id_to_int(act->get_tid());
1137 ModelAction *uninit = NULL;
1139 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1140 if (list->empty() && act->is_atomic_var()) {
1141 uninit = get_uninitialized_action(act);
1142 uninit_id = id_to_int(uninit->get_tid());
1143 list->push_front(uninit);
1145 list->push_back(act);
1147 action_trace.push_back(act);
1149 action_trace.push_front(uninit);
1151 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1152 if (tid >= (int)vec->size())
1153 vec->resize(priv->next_thread_id);
1154 (*vec)[tid].push_back(act);
1156 (*vec)[uninit_id].push_front(uninit);
1158 if ((int)thrd_last_action.size() <= tid)
1159 thrd_last_action.resize(get_num_threads());
1160 thrd_last_action[tid] = act;
1162 thrd_last_action[uninit_id] = uninit;
1164 if (act->is_fence() && act->is_release()) {
1165 if ((int)thrd_last_fence_release.size() <= tid)
1166 thrd_last_fence_release.resize(get_num_threads());
1167 thrd_last_fence_release[tid] = act;
1170 if (act->is_wait()) {
1171 void *mutex_loc = (void *) act->get_value();
1172 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1174 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1175 if (tid >= (int)vec->size())
1176 vec->resize(priv->next_thread_id);
1177 (*vec)[tid].push_back(act);
1182 * @brief Get the last action performed by a particular Thread
1183 * @param tid The thread ID of the Thread in question
1184 * @return The last action in the thread
1186 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1188 int threadid = id_to_int(tid);
1189 if (threadid < (int)thrd_last_action.size())
1190 return thrd_last_action[id_to_int(tid)];
1196 * @brief Get the last fence release performed by a particular Thread
1197 * @param tid The thread ID of the Thread in question
1198 * @return The last fence release in the thread, if one exists; NULL otherwise
1200 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1202 int threadid = id_to_int(tid);
1203 if (threadid < (int)thrd_last_fence_release.size())
1204 return thrd_last_fence_release[id_to_int(tid)];
1210 * Gets the last memory_order_seq_cst write (in the total global sequence)
1211 * performed on a particular object (i.e., memory location), not including the
1213 * @param curr The current ModelAction; also denotes the object location to
1215 * @return The last seq_cst write
1217 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1219 void *location = curr->get_location();
1220 action_list_t *list = obj_map.get(location);
1221 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1222 action_list_t::reverse_iterator rit;
1223 for (rit = list->rbegin();(*rit) != curr;rit++)
1225 rit++; /* Skip past curr */
1226 for ( ;rit != list->rend();rit++)
1227 if ((*rit)->is_write() && (*rit)->is_seqcst())
1233 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1234 * performed in a particular thread, prior to a particular fence.
1235 * @param tid The ID of the thread to check
1236 * @param before_fence The fence from which to begin the search; if NULL, then
1237 * search for the most recent fence in the thread.
1238 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1240 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1242 /* All fences should have location FENCE_LOCATION */
1243 action_list_t *list = obj_map.get(FENCE_LOCATION);
1248 action_list_t::reverse_iterator rit = list->rbegin();
1251 for (;rit != list->rend();rit++)
1252 if (*rit == before_fence)
1255 ASSERT(*rit == before_fence);
1259 for (;rit != list->rend();rit++)
1260 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1266 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1267 * location). This function identifies the mutex according to the current
1268 * action, which is presumed to perform on the same mutex.
1269 * @param curr The current ModelAction; also denotes the object location to
1271 * @return The last unlock operation
1273 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1275 void *location = curr->get_location();
1277 action_list_t *list = obj_map.get(location);
1278 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1279 action_list_t::reverse_iterator rit;
1280 for (rit = list->rbegin();rit != list->rend();rit++)
1281 if ((*rit)->is_unlock() || (*rit)->is_wait())
1286 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1288 ModelAction *parent = get_last_action(tid);
1290 parent = get_thread(tid)->get_creation();
1295 * Returns the clock vector for a given thread.
1296 * @param tid The thread whose clock vector we want
1297 * @return Desired clock vector
1299 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1301 ModelAction *firstaction=get_parent_action(tid);
1302 return firstaction != NULL ? firstaction->get_cv() : NULL;
1305 bool valequals(uint64_t val1, uint64_t val2, int size) {
1308 return ((uint8_t)val1) == ((uint8_t)val2);
1310 return ((uint16_t)val1) == ((uint16_t)val2);
1312 return ((uint32_t)val1) == ((uint32_t)val2);
1322 * Build up an initial set of all past writes that this 'read' action may read
1323 * from, as well as any previously-observed future values that must still be valid.
1325 * @param curr is the current ModelAction that we are exploring; it must be a
1328 SnapVector<const ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1330 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1332 ASSERT(curr->is_read());
1334 ModelAction *last_sc_write = NULL;
1336 if (curr->is_seqcst())
1337 last_sc_write = get_last_seq_cst_write(curr);
1339 SnapVector<const ModelAction *> * rf_set = new SnapVector<const ModelAction *>();
1341 /* Iterate over all threads */
1342 for (i = 0;i < thrd_lists->size();i++) {
1343 /* Iterate over actions in thread, starting from most recent */
1344 action_list_t *list = &(*thrd_lists)[i];
1345 action_list_t::reverse_iterator rit;
1346 for (rit = list->rbegin();rit != list->rend();rit++) {
1347 const ModelAction *act = *rit;
1349 /* Only consider 'write' actions */
1350 if (!act->is_write()) {
1351 if (act != curr && act->is_read() && act->happens_before(curr)) {
1352 const ModelAction *tmp = act->get_reads_from();
1353 if (((unsigned int) id_to_int(tmp->get_tid()))==i)
1364 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1365 bool allow_read = true;
1367 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1370 /* Need to check whether we will have two RMW reading from the same value */
1371 if (curr->is_rmwr()) {
1372 /* It is okay if we have a failing CAS */
1373 if (!curr->is_rmwrcas() ||
1374 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1375 //Need to make sure we aren't the second RMW
1376 CycleNode * node = mo_graph->getNode_noCreate(act);
1377 if (node != NULL && node->getRMW() != NULL) {
1378 //we are the second RMW
1385 /* Only add feasible reads */
1386 rf_set->push_back(act);
1389 /* Include at most one act per-thread that "happens before" curr */
1390 if (act->happens_before(curr))
1395 if (DBG_ENABLED()) {
1396 model_print("Reached read action:\n");
1398 model_print("End printing read_from_past\n");
1404 * @brief Get an action representing an uninitialized atomic
1406 * This function may create a new one or try to retrieve one from the NodeStack
1408 * @param curr The current action, which prompts the creation of an UNINIT action
1409 * @return A pointer to the UNINIT ModelAction
1411 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1413 Node *node = curr->get_node();
1414 ModelAction *act = node->get_uninit_action();
1416 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1417 node->set_uninit_action(act);
1419 act->create_cv(NULL);
1423 static void print_list(const action_list_t *list)
1425 action_list_t::const_iterator it;
1427 model_print("------------------------------------------------------------------------------------\n");
1428 model_print("# t Action type MO Location Value Rf CV\n");
1429 model_print("------------------------------------------------------------------------------------\n");
1431 unsigned int hash = 0;
1433 for (it = list->begin();it != list->end();it++) {
1434 const ModelAction *act = *it;
1435 if (act->get_seq_number() > 0)
1437 hash = hash^(hash<<3)^((*it)->hash());
1439 model_print("HASH %u\n", hash);
1440 model_print("------------------------------------------------------------------------------------\n");
1443 #if SUPPORT_MOD_ORDER_DUMP
1444 void ModelExecution::dumpGraph(char *filename) const
1447 sprintf(buffer, "%s.dot", filename);
1448 FILE *file = fopen(buffer, "w");
1449 fprintf(file, "digraph %s {\n", filename);
1450 mo_graph->dumpNodes(file);
1451 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1453 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1454 ModelAction *act = *it;
1455 if (act->is_read()) {
1456 mo_graph->dot_print_node(file, act);
1457 mo_graph->dot_print_edge(file,
1458 act->get_reads_from(),
1460 "label=\"rf\", color=red, weight=2");
1462 if (thread_array[act->get_tid()]) {
1463 mo_graph->dot_print_edge(file,
1464 thread_array[id_to_int(act->get_tid())],
1466 "label=\"sb\", color=blue, weight=400");
1469 thread_array[act->get_tid()] = act;
1471 fprintf(file, "}\n");
1472 model_free(thread_array);
1477 /** @brief Prints an execution trace summary. */
1478 void ModelExecution::print_summary() const
1480 #if SUPPORT_MOD_ORDER_DUMP
1481 char buffername[100];
1482 sprintf(buffername, "exec%04u", get_execution_number());
1483 mo_graph->dumpGraphToFile(buffername);
1484 sprintf(buffername, "graph%04u", get_execution_number());
1485 dumpGraph(buffername);
1488 model_print("Execution trace %d:", get_execution_number());
1489 if (isfeasibleprefix()) {
1490 if (scheduler->all_threads_sleeping())
1491 model_print(" SLEEP-SET REDUNDANT");
1492 if (have_bug_reports())
1493 model_print(" DETECTED BUG(S)");
1495 print_infeasibility(" INFEASIBLE");
1498 print_list(&action_trace);
1504 * Add a Thread to the system for the first time. Should only be called once
1506 * @param t The Thread to add
1508 void ModelExecution::add_thread(Thread *t)
1510 unsigned int i = id_to_int(t->get_id());
1511 if (i >= thread_map.size())
1512 thread_map.resize(i + 1);
1514 if (!t->is_model_thread())
1515 scheduler->add_thread(t);
1519 * @brief Get a Thread reference by its ID
1520 * @param tid The Thread's ID
1521 * @return A Thread reference
1523 Thread * ModelExecution::get_thread(thread_id_t tid) const
1525 unsigned int i = id_to_int(tid);
1526 if (i < thread_map.size())
1527 return thread_map[i];
1532 * @brief Get a reference to the Thread in which a ModelAction was executed
1533 * @param act The ModelAction
1534 * @return A Thread reference
1536 Thread * ModelExecution::get_thread(const ModelAction *act) const
1538 return get_thread(act->get_tid());
1542 * @brief Get a Thread reference by its pthread ID
1543 * @param index The pthread's ID
1544 * @return A Thread reference
1546 Thread * ModelExecution::get_pthread(pthread_t pid) {
1552 uint32_t thread_id = x.v;
1553 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1558 * @brief Check if a Thread is currently enabled
1559 * @param t The Thread to check
1560 * @return True if the Thread is currently enabled
1562 bool ModelExecution::is_enabled(Thread *t) const
1564 return scheduler->is_enabled(t);
1568 * @brief Check if a Thread is currently enabled
1569 * @param tid The ID of the Thread to check
1570 * @return True if the Thread is currently enabled
1572 bool ModelExecution::is_enabled(thread_id_t tid) const
1574 return scheduler->is_enabled(tid);
1578 * @brief Select the next thread to execute based on the curren action
1580 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1581 * actions should be followed by the execution of their child thread. In either
1582 * case, the current action should determine the next thread schedule.
1584 * @param curr The current action
1585 * @return The next thread to run, if the current action will determine this
1586 * selection; otherwise NULL
1588 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1590 /* Do not split atomic RMW */
1591 if (curr->is_rmwr())
1592 return get_thread(curr);
1593 /* Follow CREATE with the created thread */
1594 /* which is not needed, because model.cc takes care of this */
1595 if (curr->get_type() == THREAD_CREATE)
1596 return curr->get_thread_operand();
1597 if (curr->get_type() == PTHREAD_CREATE) {
1598 return curr->get_thread_operand();
1604 * Takes the next step in the execution, if possible.
1605 * @param curr The current step to take
1606 * @return Returns the next Thread to run, if any; NULL if this execution
1609 Thread * ModelExecution::take_step(ModelAction *curr)
1611 Thread *curr_thrd = get_thread(curr);
1612 ASSERT(curr_thrd->get_state() == THREAD_READY);
1614 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1615 curr = check_current_action(curr);
1618 // 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() );
1619 model->get_history()->add_func_atomic( curr, curr_thrd->get_id() );
1621 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1622 scheduler->remove_thread(curr_thrd);
1624 return action_select_next_thread(curr);
1627 Fuzzer * ModelExecution::getFuzzer() {