12 #include "clockvector.h"
13 #include "cyclegraph.h"
15 #include "threads-model.h"
16 #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),
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;
52 /** @brief Constructor */
53 ModelExecution::ModelExecution(ModelChecker *m,
55 NodeStack *node_stack) :
60 thread_map(2), /* We'll always need at least 2 threads */
64 condvar_waiters_map(),
68 thrd_last_fence_release(),
69 node_stack(node_stack),
70 priv(new struct model_snapshot_members()),
71 mo_graph(new CycleGraph()),
74 /* Initialize a model-checker thread, for special ModelActions */
75 model_thread = new Thread(get_next_id());
76 add_thread(model_thread);
77 scheduler->register_engine(this);
78 node_stack->register_engine(this);
81 /** @brief Destructor */
82 ModelExecution::~ModelExecution()
84 for (unsigned int i = 0; i < get_num_threads(); i++)
85 delete get_thread(int_to_id(i));
91 int ModelExecution::get_execution_number() const
93 return model->get_execution_number();
96 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
98 action_list_t *tmp = hash->get(ptr);
100 tmp = new action_list_t();
106 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
108 SnapVector<action_list_t> *tmp = hash->get(ptr);
110 tmp = new SnapVector<action_list_t>();
116 action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
118 SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
121 unsigned int thread=id_to_int(tid);
122 if (thread < wrv->size())
123 return &(*wrv)[thread];
128 /** @return a thread ID for a new Thread */
129 thread_id_t ModelExecution::get_next_id()
131 return priv->next_thread_id++;
134 /** @return the number of user threads created during this execution */
135 unsigned int ModelExecution::get_num_threads() const
137 return priv->next_thread_id;
140 /** @return a sequence number for a new ModelAction */
141 modelclock_t ModelExecution::get_next_seq_num()
143 return ++priv->used_sequence_numbers;
147 * @brief Should the current action wake up a given thread?
149 * @param curr The current action
150 * @param thread The thread that we might wake up
151 * @return True, if we should wake up the sleeping thread; false otherwise
153 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
155 const ModelAction *asleep = thread->get_pending();
156 /* Don't allow partial RMW to wake anyone up */
159 /* Synchronizing actions may have been backtracked */
160 if (asleep->could_synchronize_with(curr))
162 /* All acquire/release fences and fence-acquire/store-release */
163 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
165 /* Fence-release + store can awake load-acquire on the same location */
166 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
167 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
168 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
174 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
176 for (unsigned int i = 0; i < get_num_threads(); i++) {
177 Thread *thr = get_thread(int_to_id(i));
178 if (scheduler->is_sleep_set(thr)) {
179 if (should_wake_up(curr, thr))
180 /* Remove this thread from sleep set */
181 scheduler->remove_sleep(thr);
186 /** @brief Alert the model-checker that an incorrectly-ordered
187 * synchronization was made */
188 void ModelExecution::set_bad_synchronization()
190 priv->bad_synchronization = true;
193 /** @brief Alert the model-checker that an incorrectly-ordered
194 * synchronization was made */
195 void ModelExecution::set_bad_sc_read()
197 priv->bad_sc_read = true;
200 bool ModelExecution::assert_bug(const char *msg)
202 priv->bugs.push_back(new bug_message(msg));
204 if (isfeasibleprefix()) {
211 /** @return True, if any bugs have been reported for this execution */
212 bool ModelExecution::have_bug_reports() const
214 return priv->bugs.size() != 0;
217 SnapVector<bug_message *> * ModelExecution::get_bugs() const
223 * Check whether the current trace has triggered an assertion which should halt
226 * @return True, if the execution should be aborted; false otherwise
228 bool ModelExecution::has_asserted() const
230 return priv->asserted;
234 * Trigger a trace assertion which should cause this execution to be halted.
235 * This can be due to a detected bug or due to an infeasibility that should
238 void ModelExecution::set_assert()
240 priv->asserted = true;
244 * Check if we are in a deadlock. Should only be called at the end of an
245 * execution, although it should not give false positives in the middle of an
246 * execution (there should be some ENABLED thread).
248 * @return True if program is in a deadlock; false otherwise
250 bool ModelExecution::is_deadlocked() const
252 bool blocking_threads = false;
253 for (unsigned int i = 0; i < get_num_threads(); i++) {
254 thread_id_t tid = int_to_id(i);
257 Thread *t = get_thread(tid);
258 if (!t->is_model_thread() && t->get_pending())
259 blocking_threads = true;
261 return blocking_threads;
265 * Check if this is a complete execution. That is, have all thread completed
266 * execution (rather than exiting because sleep sets have forced a redundant
269 * @return True if the execution is complete.
271 bool ModelExecution::is_complete_execution() const
273 for (unsigned int i = 0; i < get_num_threads(); i++)
274 if (is_enabled(int_to_id(i)))
281 * Processes a read model action.
282 * @param curr is the read model action to process.
283 * @param rf_set is the set of model actions we can possibly read from
284 * @return True if processing this read updates the mo_graph.
286 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
288 bool updated = false;
290 const ModelAction *rf = fuzzer->selectWrite(curr, rf_set);
294 mo_graph->startChanges();
295 updated = r_modification_order(curr, rf);
297 mo_graph->commitChanges();
298 get_thread(curr)->set_return_value(curr->get_return_value());
303 * Processes a lock, trylock, or unlock model action. @param curr is
304 * the read model action to process.
306 * The try lock operation checks whether the lock is taken. If not,
307 * it falls to the normal lock operation case. If so, it returns
310 * The lock operation has already been checked that it is enabled, so
311 * it just grabs the lock and synchronizes with the previous unlock.
313 * The unlock operation has to re-enable all of the threads that are
314 * waiting on the lock.
316 * @return True if synchronization was updated; false otherwise
318 bool ModelExecution::process_mutex(ModelAction *curr)
320 cdsc::mutex *mutex = curr->get_mutex();
321 struct cdsc::mutex_state *state = NULL;
324 state = mutex->get_state();
326 switch (curr->get_type()) {
327 case ATOMIC_TRYLOCK: {
328 bool success = !state->locked;
329 curr->set_try_lock(success);
331 get_thread(curr)->set_return_value(0);
334 get_thread(curr)->set_return_value(1);
336 //otherwise fall into the lock case
338 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
339 assert_bug("Lock access before initialization");
340 state->locked = get_thread(curr);
341 ModelAction *unlock = get_last_unlock(curr);
342 //synchronize with the previous unlock statement
343 if (unlock != NULL) {
344 synchronize(unlock, curr);
350 case ATOMIC_UNLOCK: {
351 /* wake up the other threads */
352 for (unsigned int i = 0; i < get_num_threads(); i++) {
353 Thread *t = get_thread(int_to_id(i));
354 Thread *curr_thrd = get_thread(curr);
355 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
359 /* unlock the lock - after checking who was waiting on it */
360 state->locked = NULL;
362 if (!curr->is_wait())
363 break; /* The rest is only for ATOMIC_WAIT */
367 case ATOMIC_NOTIFY_ALL: {
368 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
369 //activate all the waiting threads
370 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
371 scheduler->wake(get_thread(*rit));
376 case ATOMIC_NOTIFY_ONE: {
377 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
378 Thread * thread = fuzzer->selectNotify(waiters);
379 scheduler->wake(thread);
390 * Process a write ModelAction
391 * @param curr The ModelAction to process
392 * @return True if the mo_graph was updated or promises were resolved
394 bool ModelExecution::process_write(ModelAction *curr)
397 bool updated_mod_order = w_modification_order(curr);
399 mo_graph->commitChanges();
401 get_thread(curr)->set_return_value(VALUE_NONE);
402 return updated_mod_order;
406 * Process a fence ModelAction
407 * @param curr The ModelAction to process
408 * @return True if synchronization was updated
410 bool ModelExecution::process_fence(ModelAction *curr)
413 * fence-relaxed: no-op
414 * fence-release: only log the occurence (not in this function), for
415 * use in later synchronization
416 * fence-acquire (this function): search for hypothetical release
418 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
420 bool updated = false;
421 if (curr->is_acquire()) {
422 action_list_t *list = &action_trace;
423 action_list_t::reverse_iterator rit;
424 /* Find X : is_read(X) && X --sb-> curr */
425 for (rit = list->rbegin(); rit != list->rend(); rit++) {
426 ModelAction *act = *rit;
429 if (act->get_tid() != curr->get_tid())
431 /* Stop at the beginning of the thread */
432 if (act->is_thread_start())
434 /* Stop once we reach a prior fence-acquire */
435 if (act->is_fence() && act->is_acquire())
439 /* read-acquire will find its own release sequences */
440 if (act->is_acquire())
443 /* Establish hypothetical release sequences */
444 rel_heads_list_t release_heads;
445 get_release_seq_heads(curr, act, &release_heads);
446 for (unsigned int i = 0; i < release_heads.size(); i++)
447 synchronize(release_heads[i], curr);
448 if (release_heads.size() != 0)
456 * @brief Process the current action for thread-related activity
458 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
459 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
460 * synchronization, etc. This function is a no-op for non-THREAD actions
461 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
463 * @param curr The current action
464 * @return True if synchronization was updated or a thread completed
466 bool ModelExecution::process_thread_action(ModelAction *curr)
468 bool updated = false;
470 switch (curr->get_type()) {
471 case THREAD_CREATE: {
472 thrd_t *thrd = (thrd_t *)curr->get_location();
473 struct thread_params *params = (struct thread_params *)curr->get_value();
474 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
475 curr->set_thread_operand(th);
477 th->set_creation(curr);
480 case PTHREAD_CREATE: {
481 (*(uint32_t *)curr->get_location()) = pthread_counter++;
483 struct pthread_params *params = (struct pthread_params *)curr->get_value();
484 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
485 curr->set_thread_operand(th);
487 th->set_creation(curr);
489 if ( pthread_map.size() < pthread_counter )
490 pthread_map.resize( pthread_counter );
491 pthread_map[ pthread_counter-1 ] = th;
496 Thread *blocking = curr->get_thread_operand();
497 ModelAction *act = get_last_action(blocking->get_id());
498 synchronize(act, curr);
499 updated = true; /* trigger rel-seq checks */
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 */
507 break; // WL: to be add (modified)
510 case THREAD_FINISH: {
511 Thread *th = get_thread(curr);
512 /* Wake up any joining threads */
513 for (unsigned int i = 0; i < get_num_threads(); i++) {
514 Thread *waiting = get_thread(int_to_id(i));
515 if (waiting->waiting_on() == th &&
516 waiting->get_pending()->is_thread_join())
517 scheduler->wake(waiting);
520 updated = true; /* trigger rel-seq checks */
534 * Initialize the current action by performing one or more of the following
535 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
536 * in the NodeStack, manipulating backtracking sets, allocating and
537 * initializing clock vectors, and computing the promises to fulfill.
539 * @param curr The current action, as passed from the user context; may be
540 * freed/invalidated after the execution of this function, with a different
541 * action "returned" its place (pass-by-reference)
542 * @return True if curr is a newly-explored action; false otherwise
544 bool ModelExecution::initialize_curr_action(ModelAction **curr)
546 ModelAction *newcurr;
548 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
549 newcurr = process_rmw(*curr);
556 (*curr)->set_seq_number(get_next_seq_num());
558 newcurr = node_stack->explore_action(*curr);
560 /* First restore type and order in case of RMW operation */
561 if ((*curr)->is_rmwr())
562 newcurr->copy_typeandorder(*curr);
564 ASSERT((*curr)->get_location() == newcurr->get_location());
565 newcurr->copy_from_new(*curr);
567 /* Discard duplicate ModelAction; use action from NodeStack */
570 /* Always compute new clock vector */
571 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
574 return false; /* Action was explored previously */
578 /* Always compute new clock vector */
579 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
581 /* Assign most recent release fence */
582 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
584 return true; /* This was a new ModelAction */
589 * @brief Establish reads-from relation between two actions
591 * Perform basic operations involved with establishing a concrete rf relation,
592 * including setting the ModelAction data and checking for release sequences.
594 * @param act The action that is reading (must be a read)
595 * @param rf The action from which we are reading (must be a write)
597 * @return True if this read established synchronization
600 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
603 ASSERT(rf->is_write());
605 act->set_read_from(rf);
606 if (act->is_acquire()) {
607 rel_heads_list_t release_heads;
608 get_release_seq_heads(act, act, &release_heads);
609 int num_heads = release_heads.size();
610 for (unsigned int i = 0; i < release_heads.size(); i++)
611 if (!synchronize(release_heads[i], act))
613 return num_heads > 0;
619 * @brief Synchronizes two actions
621 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
622 * This function performs the synchronization as well as providing other hooks
623 * for other checks along with synchronization.
625 * @param first The left-hand side of the synchronizes-with relation
626 * @param second The right-hand side of the synchronizes-with relation
627 * @return True if the synchronization was successful (i.e., was consistent
628 * with the execution order); false otherwise
630 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
632 if (*second < *first) {
633 set_bad_synchronization();
636 return second->synchronize_with(first);
640 * @brief Check whether a model action is enabled.
642 * Checks whether an operation would be successful (i.e., is a lock already
643 * locked, or is the joined thread already complete).
645 * For yield-blocking, yields are never enabled.
647 * @param curr is the ModelAction to check whether it is enabled.
648 * @return a bool that indicates whether the action is enabled.
650 bool ModelExecution::check_action_enabled(ModelAction *curr) {
651 if (curr->is_lock()) {
652 cdsc::mutex *lock = curr->get_mutex();
653 struct cdsc::mutex_state *state = lock->get_state();
656 } else if (curr->is_thread_join()) {
657 Thread *blocking = curr->get_thread_operand();
658 if (!blocking->is_complete()) {
667 * This is the heart of the model checker routine. It performs model-checking
668 * actions corresponding to a given "current action." Among other processes, it
669 * calculates reads-from relationships, updates synchronization clock vectors,
670 * forms a memory_order constraints graph, and handles replay/backtrack
671 * execution when running permutations of previously-observed executions.
673 * @param curr The current action to process
674 * @return The ModelAction that is actually executed; may be different than
677 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
680 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
681 bool newly_explored = initialize_curr_action(&curr);
685 wake_up_sleeping_actions(curr);
687 /* Add the action to lists before any other model-checking tasks */
688 if (!second_part_of_rmw)
689 add_action_to_lists(curr);
691 ModelVector<ModelAction *> * rf_set = NULL;
692 /* Build may_read_from set for newly-created actions */
693 if (newly_explored && curr->is_read())
694 rf_set = build_may_read_from(curr);
696 process_thread_action(curr);
698 if (curr->is_read() && !second_part_of_rmw) {
699 process_read(curr, rf_set);
703 if (curr->is_write())
706 if (curr->is_fence())
709 if (curr->is_mutex_op())
716 * This is the strongest feasibility check available.
717 * @return whether the current trace (partial or complete) must be a prefix of
720 bool ModelExecution::isfeasibleprefix() const
722 return !is_infeasible();
726 * Print disagnostic information about an infeasible execution
727 * @param prefix A string to prefix the output with; if NULL, then a default
728 * message prefix will be provided
730 void ModelExecution::print_infeasibility(const char *prefix) const
734 if (mo_graph->checkForCycles())
735 ptr += sprintf(ptr, "[mo cycle]");
736 if (priv->bad_synchronization)
737 ptr += sprintf(ptr, "[bad sw ordering]");
738 if (priv->bad_sc_read)
739 ptr += sprintf(ptr, "[bad sc read]");
741 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
745 * Check if the current partial trace is infeasible. Does not check any
746 * end-of-execution flags, which might rule out the execution. Thus, this is
747 * useful only for ruling an execution as infeasible.
748 * @return whether the current partial trace is infeasible.
750 bool ModelExecution::is_infeasible() const
752 return mo_graph->checkForCycles() ||
753 priv->bad_synchronization ||
757 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
758 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
759 ModelAction *lastread = get_last_action(act->get_tid());
760 lastread->process_rmw(act);
762 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
763 mo_graph->commitChanges();
769 * @brief Updates the mo_graph with the constraints imposed from the current
772 * Basic idea is the following: Go through each other thread and find
773 * the last action that happened before our read. Two cases:
775 * -# The action is a write: that write must either occur before
776 * the write we read from or be the write we read from.
777 * -# The action is a read: the write that that action read from
778 * must occur before the write we read from or be the same write.
780 * @param curr The current action. Must be a read.
781 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
782 * @return True if modification order edges were added; false otherwise
784 template <typename rf_type>
785 bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
787 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
790 ASSERT(curr->is_read());
792 /* Last SC fence in the current thread */
793 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
794 ModelAction *last_sc_write = NULL;
795 if (curr->is_seqcst())
796 last_sc_write = get_last_seq_cst_write(curr);
798 /* Iterate over all threads */
799 for (i = 0; i < thrd_lists->size(); i++) {
800 /* Last SC fence in thread i */
801 ModelAction *last_sc_fence_thread_local = NULL;
802 if (int_to_id((int)i) != curr->get_tid())
803 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
805 /* Last SC fence in thread i, before last SC fence in current thread */
806 ModelAction *last_sc_fence_thread_before = NULL;
807 if (last_sc_fence_local)
808 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
810 /* Iterate over actions in thread, starting from most recent */
811 action_list_t *list = &(*thrd_lists)[i];
812 action_list_t::reverse_iterator rit;
813 for (rit = list->rbegin(); rit != list->rend(); rit++) {
814 ModelAction *act = *rit;
819 /* Don't want to add reflexive edges on 'rf' */
820 if (act->equals(rf)) {
821 if (act->happens_before(curr))
827 if (act->is_write()) {
828 /* C++, Section 29.3 statement 5 */
829 if (curr->is_seqcst() && last_sc_fence_thread_local &&
830 *act < *last_sc_fence_thread_local) {
831 added = mo_graph->addEdge(act, rf) || added;
834 /* C++, Section 29.3 statement 4 */
835 else if (act->is_seqcst() && last_sc_fence_local &&
836 *act < *last_sc_fence_local) {
837 added = mo_graph->addEdge(act, rf) || added;
840 /* C++, Section 29.3 statement 6 */
841 else if (last_sc_fence_thread_before &&
842 *act < *last_sc_fence_thread_before) {
843 added = mo_graph->addEdge(act, rf) || added;
849 * Include at most one act per-thread that "happens
852 if (act->happens_before(curr)) {
853 if (act->is_write()) {
854 added = mo_graph->addEdge(act, rf) || added;
856 const ModelAction *prevrf = act->get_reads_from();
857 if (!prevrf->equals(rf))
858 added = mo_graph->addEdge(prevrf, rf) || added;
869 * Updates the mo_graph with the constraints imposed from the current write.
871 * Basic idea is the following: Go through each other thread and find
872 * the lastest action that happened before our write. Two cases:
874 * (1) The action is a write => that write must occur before
877 * (2) The action is a read => the write that that action read from
878 * must occur before the current write.
880 * This method also handles two other issues:
882 * (I) Sequential Consistency: Making sure that if the current write is
883 * seq_cst, that it occurs after the previous seq_cst write.
885 * (II) Sending the write back to non-synchronizing reads.
887 * @param curr The current action. Must be a write.
888 * @param send_fv A vector for stashing reads to which we may pass our future
889 * value. If NULL, then don't record any future values.
890 * @return True if modification order edges were added; false otherwise
892 bool ModelExecution::w_modification_order(ModelAction *curr)
894 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
897 ASSERT(curr->is_write());
899 if (curr->is_seqcst()) {
900 /* We have to at least see the last sequentially consistent write,
901 so we are initialized. */
902 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
903 if (last_seq_cst != NULL) {
904 added = mo_graph->addEdge(last_seq_cst, curr) || added;
908 /* Last SC fence in the current thread */
909 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
911 /* Iterate over all threads */
912 for (i = 0; i < thrd_lists->size(); i++) {
913 /* Last SC fence in thread i, before last SC fence in current thread */
914 ModelAction *last_sc_fence_thread_before = NULL;
915 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
916 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
918 /* Iterate over actions in thread, starting from most recent */
919 action_list_t *list = &(*thrd_lists)[i];
920 action_list_t::reverse_iterator rit;
921 for (rit = list->rbegin(); rit != list->rend(); rit++) {
922 ModelAction *act = *rit;
925 * 1) If RMW and it actually read from something, then we
926 * already have all relevant edges, so just skip to next
929 * 2) If RMW and it didn't read from anything, we should
930 * whatever edge we can get to speed up convergence.
932 * 3) If normal write, we need to look at earlier actions, so
933 * continue processing list.
935 if (curr->is_rmw()) {
936 if (curr->get_reads_from() != NULL)
944 /* C++, Section 29.3 statement 7 */
945 if (last_sc_fence_thread_before && act->is_write() &&
946 *act < *last_sc_fence_thread_before) {
947 added = mo_graph->addEdge(act, curr) || added;
952 * Include at most one act per-thread that "happens
955 if (act->happens_before(curr)) {
957 * Note: if act is RMW, just add edge:
959 * The following edge should be handled elsewhere:
960 * readfrom(act) --mo--> act
963 added = mo_graph->addEdge(act, curr) || added;
964 else if (act->is_read()) {
965 //if previous read accessed a null, just keep going
966 added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
969 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
970 !act->same_thread(curr)) {
971 /* We have an action that:
972 (1) did not happen before us
973 (2) is a read and we are a write
974 (3) cannot synchronize with us
975 (4) is in a different thread
977 that read could potentially read from our write. Note that
978 these checks are overly conservative at this point, we'll
979 do more checks before actually removing the
992 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
993 * some constraints. This method checks one the following constraint (others
994 * require compiler support):
996 * If X --hb-> Y --mo-> Z, then X should not read from Z.
997 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
999 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1001 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1003 /* Iterate over all threads */
1004 for (i = 0; i < thrd_lists->size(); i++) {
1005 const ModelAction *write_after_read = NULL;
1007 /* Iterate over actions in thread, starting from most recent */
1008 action_list_t *list = &(*thrd_lists)[i];
1009 action_list_t::reverse_iterator rit;
1010 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1011 ModelAction *act = *rit;
1013 /* Don't disallow due to act == reader */
1014 if (!reader->happens_before(act) || reader == act)
1016 else if (act->is_write())
1017 write_after_read = act;
1018 else if (act->is_read() && act->get_reads_from() != NULL)
1019 write_after_read = act->get_reads_from();
1022 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1029 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1030 * The ModelAction under consideration is expected to be taking part in
1031 * release/acquire synchronization as an object of the "reads from" relation.
1032 * Note that this can only provide release sequence support for RMW chains
1033 * which do not read from the future, as those actions cannot be traced until
1034 * their "promise" is fulfilled. Similarly, we may not even establish the
1035 * presence of a release sequence with certainty, as some modification order
1036 * constraints may be decided further in the future. Thus, this function
1037 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1038 * and a boolean representing certainty.
1040 * @param rf The action that might be part of a release sequence. Must be a
1042 * @param release_heads A pass-by-reference style return parameter. After
1043 * execution of this function, release_heads will contain the heads of all the
1044 * relevant release sequences, if any exists with certainty
1045 * @return true, if the ModelExecution is certain that release_heads is complete;
1048 bool ModelExecution::release_seq_heads(const ModelAction *rf,
1049 rel_heads_list_t *release_heads) const
1051 /* Only check for release sequences if there are no cycles */
1052 if (mo_graph->checkForCycles())
1055 for ( ; rf != NULL; rf = rf->get_reads_from()) {
1056 ASSERT(rf->is_write());
1058 if (rf->is_release())
1059 release_heads->push_back(rf);
1060 else if (rf->get_last_fence_release())
1061 release_heads->push_back(rf->get_last_fence_release());
1063 break; /* End of RMW chain */
1065 /** @todo Need to be smarter here... In the linux lock
1066 * example, this will run to the beginning of the program for
1068 /** @todo The way to be smarter here is to keep going until 1
1069 * thread has a release preceded by an acquire and you've seen
1072 /* acq_rel RMW is a sufficient stopping condition */
1073 if (rf->is_acquire() && rf->is_release())
1074 return true; /* complete */
1076 ASSERT(rf); // Needs to be real write
1078 if (rf->is_release())
1079 return true; /* complete */
1081 /* else relaxed write
1082 * - check for fence-release in the same thread (29.8, stmt. 3)
1083 * - check modification order for contiguous subsequence
1084 * -> rf must be same thread as release */
1086 const ModelAction *fence_release = rf->get_last_fence_release();
1087 /* Synchronize with a fence-release unconditionally; we don't need to
1088 * find any more "contiguous subsequence..." for it */
1090 release_heads->push_back(fence_release);
1092 return true; /* complete */
1096 * An interface for getting the release sequence head(s) with which a
1097 * given ModelAction must synchronize. This function only returns a non-empty
1098 * result when it can locate a release sequence head with certainty. Otherwise,
1099 * it may mark the internal state of the ModelExecution so that it will handle
1100 * the release sequence at a later time, causing @a acquire to update its
1101 * synchronization at some later point in execution.
1103 * @param acquire The 'acquire' action that may synchronize with a release
1105 * @param read The read action that may read from a release sequence; this may
1106 * be the same as acquire, or else an earlier action in the same thread (i.e.,
1107 * when 'acquire' is a fence-acquire)
1108 * @param release_heads A pass-by-reference return parameter. Will be filled
1109 * with the head(s) of the release sequence(s), if they exists with certainty.
1110 * @see ModelExecution::release_seq_heads
1112 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
1113 ModelAction *read, rel_heads_list_t *release_heads)
1115 const ModelAction *rf = read->get_reads_from();
1117 release_seq_heads(rf, release_heads);
1121 * Performs various bookkeeping operations for the current ModelAction. For
1122 * instance, adds action to the per-object, per-thread action vector and to the
1123 * action trace list of all thread actions.
1125 * @param act is the ModelAction to add.
1127 void ModelExecution::add_action_to_lists(ModelAction *act)
1129 int tid = id_to_int(act->get_tid());
1130 ModelAction *uninit = NULL;
1132 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1133 if (list->empty() && act->is_atomic_var()) {
1134 uninit = get_uninitialized_action(act);
1135 uninit_id = id_to_int(uninit->get_tid());
1136 list->push_front(uninit);
1138 list->push_back(act);
1140 action_trace.push_back(act);
1142 action_trace.push_front(uninit);
1144 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1145 if (tid >= (int)vec->size())
1146 vec->resize(priv->next_thread_id);
1147 (*vec)[tid].push_back(act);
1149 (*vec)[uninit_id].push_front(uninit);
1151 if ((int)thrd_last_action.size() <= tid)
1152 thrd_last_action.resize(get_num_threads());
1153 thrd_last_action[tid] = act;
1155 thrd_last_action[uninit_id] = uninit;
1157 if (act->is_fence() && act->is_release()) {
1158 if ((int)thrd_last_fence_release.size() <= tid)
1159 thrd_last_fence_release.resize(get_num_threads());
1160 thrd_last_fence_release[tid] = act;
1163 if (act->is_wait()) {
1164 void *mutex_loc = (void *) act->get_value();
1165 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1167 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1168 if (tid >= (int)vec->size())
1169 vec->resize(priv->next_thread_id);
1170 (*vec)[tid].push_back(act);
1175 * @brief Get the last action performed by a particular Thread
1176 * @param tid The thread ID of the Thread in question
1177 * @return The last action in the thread
1179 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1181 int threadid = id_to_int(tid);
1182 if (threadid < (int)thrd_last_action.size())
1183 return thrd_last_action[id_to_int(tid)];
1189 * @brief Get the last fence release performed by a particular Thread
1190 * @param tid The thread ID of the Thread in question
1191 * @return The last fence release in the thread, if one exists; NULL otherwise
1193 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1195 int threadid = id_to_int(tid);
1196 if (threadid < (int)thrd_last_fence_release.size())
1197 return thrd_last_fence_release[id_to_int(tid)];
1203 * Gets the last memory_order_seq_cst write (in the total global sequence)
1204 * performed on a particular object (i.e., memory location), not including the
1206 * @param curr The current ModelAction; also denotes the object location to
1208 * @return The last seq_cst write
1210 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1212 void *location = curr->get_location();
1213 action_list_t *list = obj_map.get(location);
1214 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1215 action_list_t::reverse_iterator rit;
1216 for (rit = list->rbegin(); (*rit) != curr; rit++)
1218 rit++; /* Skip past curr */
1219 for ( ; rit != list->rend(); rit++)
1220 if ((*rit)->is_write() && (*rit)->is_seqcst())
1226 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1227 * performed in a particular thread, prior to a particular fence.
1228 * @param tid The ID of the thread to check
1229 * @param before_fence The fence from which to begin the search; if NULL, then
1230 * search for the most recent fence in the thread.
1231 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1233 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1235 /* All fences should have location FENCE_LOCATION */
1236 action_list_t *list = obj_map.get(FENCE_LOCATION);
1241 action_list_t::reverse_iterator rit = list->rbegin();
1244 for (; rit != list->rend(); rit++)
1245 if (*rit == before_fence)
1248 ASSERT(*rit == before_fence);
1252 for (; rit != list->rend(); rit++)
1253 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1259 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1260 * location). This function identifies the mutex according to the current
1261 * action, which is presumed to perform on the same mutex.
1262 * @param curr The current ModelAction; also denotes the object location to
1264 * @return The last unlock operation
1266 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1268 void *location = curr->get_location();
1270 action_list_t *list = obj_map.get(location);
1271 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1272 action_list_t::reverse_iterator rit;
1273 for (rit = list->rbegin(); rit != list->rend(); rit++)
1274 if ((*rit)->is_unlock() || (*rit)->is_wait())
1279 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1281 ModelAction *parent = get_last_action(tid);
1283 parent = get_thread(tid)->get_creation();
1288 * Returns the clock vector for a given thread.
1289 * @param tid The thread whose clock vector we want
1290 * @return Desired clock vector
1292 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1294 return get_parent_action(tid)->get_cv();
1297 bool valequals(uint64_t val1, uint64_t val2, int size) {
1300 return ((uint8_t)val1) == ((uint8_t)val2);
1302 return ((uint16_t)val1) == ((uint16_t)val2);
1304 return ((uint32_t)val1) == ((uint32_t)val2);
1314 * Build up an initial set of all past writes that this 'read' action may read
1315 * from, as well as any previously-observed future values that must still be valid.
1317 * @param curr is the current ModelAction that we are exploring; it must be a
1320 ModelVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1322 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1324 ASSERT(curr->is_read());
1326 ModelAction *last_sc_write = NULL;
1328 if (curr->is_seqcst())
1329 last_sc_write = get_last_seq_cst_write(curr);
1331 ModelVector<ModelAction *> * rf_set = new ModelVector<ModelAction *>();
1333 /* Iterate over all threads */
1334 for (i = 0; i < thrd_lists->size(); i++) {
1335 /* Iterate over actions in thread, starting from most recent */
1336 action_list_t *list = &(*thrd_lists)[i];
1337 action_list_t::reverse_iterator rit;
1338 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1339 ModelAction *act = *rit;
1341 /* Only consider 'write' actions */
1342 if (!act->is_write() || act == curr)
1345 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1346 bool allow_read = true;
1348 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1351 /* Need to check whether we will have two RMW reading from the same value */
1352 if (curr->is_rmwr()) {
1353 /* It is okay if we have a failing CAS */
1354 if (!curr->is_rmwrcas() ||
1355 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1356 //Need to make sure we aren't the second RMW
1357 CycleNode * node = mo_graph->getNode_noCreate(act);
1358 if (node != NULL && node->getRMW() != NULL) {
1359 //we are the second RMW
1366 /* Only add feasible reads */
1367 mo_graph->startChanges();
1368 r_modification_order(curr, act);
1369 if (!is_infeasible())
1370 rf_set->push_back(act);
1371 mo_graph->rollbackChanges();
1374 /* Include at most one act per-thread that "happens before" curr */
1375 if (act->happens_before(curr))
1380 if (DBG_ENABLED()) {
1381 model_print("Reached read action:\n");
1383 model_print("End printing read_from_past\n");
1389 * @brief Get an action representing an uninitialized atomic
1391 * This function may create a new one or try to retrieve one from the NodeStack
1393 * @param curr The current action, which prompts the creation of an UNINIT action
1394 * @return A pointer to the UNINIT ModelAction
1396 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1398 Node *node = curr->get_node();
1399 ModelAction *act = node->get_uninit_action();
1401 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1402 node->set_uninit_action(act);
1404 act->create_cv(NULL);
1408 static void print_list(const action_list_t *list)
1410 action_list_t::const_iterator it;
1412 model_print("------------------------------------------------------------------------------------\n");
1413 model_print("# t Action type MO Location Value Rf CV\n");
1414 model_print("------------------------------------------------------------------------------------\n");
1416 unsigned int hash = 0;
1418 for (it = list->begin(); it != list->end(); it++) {
1419 const ModelAction *act = *it;
1420 if (act->get_seq_number() > 0)
1422 hash = hash^(hash<<3)^((*it)->hash());
1424 model_print("HASH %u\n", hash);
1425 model_print("------------------------------------------------------------------------------------\n");
1428 #if SUPPORT_MOD_ORDER_DUMP
1429 void ModelExecution::dumpGraph(char *filename) const
1432 sprintf(buffer, "%s.dot", filename);
1433 FILE *file = fopen(buffer, "w");
1434 fprintf(file, "digraph %s {\n", filename);
1435 mo_graph->dumpNodes(file);
1436 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1438 for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) {
1439 ModelAction *act = *it;
1440 if (act->is_read()) {
1441 mo_graph->dot_print_node(file, act);
1442 mo_graph->dot_print_edge(file,
1443 act->get_reads_from(),
1445 "label=\"rf\", color=red, weight=2");
1447 if (thread_array[act->get_tid()]) {
1448 mo_graph->dot_print_edge(file,
1449 thread_array[id_to_int(act->get_tid())],
1451 "label=\"sb\", color=blue, weight=400");
1454 thread_array[act->get_tid()] = act;
1456 fprintf(file, "}\n");
1457 model_free(thread_array);
1462 /** @brief Prints an execution trace summary. */
1463 void ModelExecution::print_summary() const
1465 #if SUPPORT_MOD_ORDER_DUMP
1466 char buffername[100];
1467 sprintf(buffername, "exec%04u", get_execution_number());
1468 mo_graph->dumpGraphToFile(buffername);
1469 sprintf(buffername, "graph%04u", get_execution_number());
1470 dumpGraph(buffername);
1473 model_print("Execution trace %d:", get_execution_number());
1474 if (isfeasibleprefix()) {
1475 if (scheduler->all_threads_sleeping())
1476 model_print(" SLEEP-SET REDUNDANT");
1477 if (have_bug_reports())
1478 model_print(" DETECTED BUG(S)");
1480 print_infeasibility(" INFEASIBLE");
1483 print_list(&action_trace);
1489 * Add a Thread to the system for the first time. Should only be called once
1491 * @param t The Thread to add
1493 void ModelExecution::add_thread(Thread *t)
1495 unsigned int i = id_to_int(t->get_id());
1496 if (i >= thread_map.size())
1497 thread_map.resize(i + 1);
1499 if (!t->is_model_thread())
1500 scheduler->add_thread(t);
1504 * @brief Get a Thread reference by its ID
1505 * @param tid The Thread's ID
1506 * @return A Thread reference
1508 Thread * ModelExecution::get_thread(thread_id_t tid) const
1510 unsigned int i = id_to_int(tid);
1511 if (i < thread_map.size())
1512 return thread_map[i];
1517 * @brief Get a reference to the Thread in which a ModelAction was executed
1518 * @param act The ModelAction
1519 * @return A Thread reference
1521 Thread * ModelExecution::get_thread(const ModelAction *act) const
1523 return get_thread(act->get_tid());
1527 * @brief Get a Thread reference by its pthread ID
1528 * @param index The pthread's ID
1529 * @return A Thread reference
1531 Thread * ModelExecution::get_pthread(pthread_t pid) {
1537 uint32_t thread_id = x.v;
1538 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1543 * @brief Check if a Thread is currently enabled
1544 * @param t The Thread to check
1545 * @return True if the Thread is currently enabled
1547 bool ModelExecution::is_enabled(Thread *t) const
1549 return scheduler->is_enabled(t);
1553 * @brief Check if a Thread is currently enabled
1554 * @param tid The ID of the Thread to check
1555 * @return True if the Thread is currently enabled
1557 bool ModelExecution::is_enabled(thread_id_t tid) const
1559 return scheduler->is_enabled(tid);
1563 * @brief Select the next thread to execute based on the curren action
1565 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1566 * actions should be followed by the execution of their child thread. In either
1567 * case, the current action should determine the next thread schedule.
1569 * @param curr The current action
1570 * @return The next thread to run, if the current action will determine this
1571 * selection; otherwise NULL
1573 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1575 /* Do not split atomic RMW */
1576 if (curr->is_rmwr())
1577 return get_thread(curr);
1578 if (curr->is_write()) {
1579 std::memory_order order = curr->get_mo();
1581 case std::memory_order_relaxed:
1582 return get_thread(curr);
1583 case std::memory_order_release:
1584 return get_thread(curr);
1590 /* Follow CREATE with the created thread */
1591 /* which is not needed, because model.cc takes care of this */
1592 if (curr->get_type() == THREAD_CREATE)
1593 return curr->get_thread_operand();
1594 if (curr->get_type() == PTHREAD_CREATE) {
1595 return curr->get_thread_operand();
1601 * Takes the next step in the execution, if possible.
1602 * @param curr The current step to take
1603 * @return Returns the next Thread to run, if any; NULL if this execution
1606 Thread * ModelExecution::take_step(ModelAction *curr)
1608 Thread *curr_thrd = get_thread(curr);
1609 ASSERT(curr_thrd->get_state() == THREAD_READY);
1611 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1612 curr = check_current_action(curr);
1615 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1616 scheduler->remove_thread(curr_thrd);
1618 return action_select_next_thread(curr);
1621 Fuzzer * ModelExecution::getFuzzer() {