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),
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, NodeStack *node_stack) :
56 thread_map(2), /* We'll always need at least 2 threads */
60 condvar_waiters_map(),
64 thrd_last_fence_release(),
65 node_stack(node_stack),
66 priv(new struct model_snapshot_members ()),
67 mo_graph(new CycleGraph()),
70 /* Initialize a model-checker thread, for special ModelActions */
71 model_thread = new Thread(get_next_id());
72 add_thread(model_thread);
73 scheduler->register_engine(this);
74 node_stack->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<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 action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
114 SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
117 unsigned int thread=id_to_int(tid);
118 if (thread < wrv->size())
119 return &(*wrv)[thread];
124 /** @return a thread ID for a new Thread */
125 thread_id_t ModelExecution::get_next_id()
127 return priv->next_thread_id++;
130 /** @return the number of user threads created during this execution */
131 unsigned int ModelExecution::get_num_threads() const
133 return priv->next_thread_id;
136 /** @return a sequence number for a new ModelAction */
137 modelclock_t ModelExecution::get_next_seq_num()
139 return ++priv->used_sequence_numbers;
143 * @brief Should the current action wake up a given thread?
145 * @param curr The current action
146 * @param thread The thread that we might wake up
147 * @return True, if we should wake up the sleeping thread; false otherwise
149 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
151 const ModelAction *asleep = thread->get_pending();
152 /* Don't allow partial RMW to wake anyone up */
155 /* Synchronizing actions may have been backtracked */
156 if (asleep->could_synchronize_with(curr))
158 /* All acquire/release fences and fence-acquire/store-release */
159 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
161 /* Fence-release + store can awake load-acquire on the same location */
162 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
163 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
164 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
170 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
172 for (unsigned int i = 0;i < get_num_threads();i++) {
173 Thread *thr = get_thread(int_to_id(i));
174 if (scheduler->is_sleep_set(thr)) {
175 if (should_wake_up(curr, thr))
176 /* Remove this thread from sleep set */
177 scheduler->remove_sleep(thr);
182 /** @brief Alert the model-checker that an incorrectly-ordered
183 * synchronization was made */
184 void ModelExecution::set_bad_synchronization()
186 priv->bad_synchronization = true;
189 bool ModelExecution::assert_bug(const char *msg)
191 priv->bugs.push_back(new bug_message(msg));
193 if (isfeasibleprefix()) {
200 /** @return True, if any bugs have been reported for this execution */
201 bool ModelExecution::have_bug_reports() const
203 return priv->bugs.size() != 0;
206 SnapVector<bug_message *> * ModelExecution::get_bugs() const
212 * Check whether the current trace has triggered an assertion which should halt
215 * @return True, if the execution should be aborted; false otherwise
217 bool ModelExecution::has_asserted() const
219 return priv->asserted;
223 * Trigger a trace assertion which should cause this execution to be halted.
224 * This can be due to a detected bug or due to an infeasibility that should
227 void ModelExecution::set_assert()
229 priv->asserted = true;
233 * Check if we are in a deadlock. Should only be called at the end of an
234 * execution, although it should not give false positives in the middle of an
235 * execution (there should be some ENABLED thread).
237 * @return True if program is in a deadlock; false otherwise
239 bool ModelExecution::is_deadlocked() const
241 bool blocking_threads = false;
242 for (unsigned int i = 0;i < get_num_threads();i++) {
243 thread_id_t tid = int_to_id(i);
246 Thread *t = get_thread(tid);
247 if (!t->is_model_thread() && t->get_pending())
248 blocking_threads = true;
250 return blocking_threads;
254 * Check if this is a complete execution. That is, have all thread completed
255 * execution (rather than exiting because sleep sets have forced a redundant
258 * @return True if the execution is complete.
260 bool ModelExecution::is_complete_execution() const
262 for (unsigned int i = 0;i < get_num_threads();i++)
263 if (is_enabled(int_to_id(i)))
270 * Processes a read model action.
271 * @param curr is the read model action to process.
272 * @param rf_set is the set of model actions we can possibly read from
273 * @return True if processing this read updates the mo_graph.
275 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
279 int index = fuzzer->selectWrite(curr, rf_set);
280 const ModelAction *rf = (*rf_set)[index];
285 mo_graph->startChanges();
286 r_modification_order(curr, rf);
287 if (!is_infeasible()) {
289 mo_graph->commitChanges();
290 get_thread(curr)->set_return_value(curr->get_return_value());
293 mo_graph->rollbackChanges();
294 (*rf_set)[index] = rf_set->back();
300 * Processes a lock, trylock, or unlock model action. @param curr is
301 * the read model action to process.
303 * The try lock operation checks whether the lock is taken. If not,
304 * it falls to the normal lock operation case. If so, it returns
307 * The lock operation has already been checked that it is enabled, so
308 * it just grabs the lock and synchronizes with the previous unlock.
310 * The unlock operation has to re-enable all of the threads that are
311 * waiting on the lock.
313 * @return True if synchronization was updated; false otherwise
315 bool ModelExecution::process_mutex(ModelAction *curr)
317 cdsc::mutex *mutex = curr->get_mutex();
318 struct cdsc::mutex_state *state = NULL;
321 state = mutex->get_state();
323 switch (curr->get_type()) {
324 case ATOMIC_TRYLOCK: {
325 bool success = !state->locked;
326 curr->set_try_lock(success);
328 get_thread(curr)->set_return_value(0);
331 get_thread(curr)->set_return_value(1);
333 //otherwise fall into the lock case
335 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
336 assert_bug("Lock access before initialization");
337 state->locked = get_thread(curr);
338 ModelAction *unlock = get_last_unlock(curr);
339 //synchronize with the previous unlock statement
340 if (unlock != NULL) {
341 synchronize(unlock, curr);
347 case ATOMIC_UNLOCK: {
348 /* wake up the other threads */
349 for (unsigned int i = 0;i < get_num_threads();i++) {
350 Thread *t = get_thread(int_to_id(i));
351 Thread *curr_thrd = get_thread(curr);
352 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
356 /* unlock the lock - after checking who was waiting on it */
357 state->locked = NULL;
359 if (!curr->is_wait())
360 break;/* The rest is only for ATOMIC_WAIT */
364 case ATOMIC_NOTIFY_ALL: {
365 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
366 //activate all the waiting threads
367 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
368 scheduler->wake(get_thread(*rit));
373 case ATOMIC_NOTIFY_ONE: {
374 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
375 Thread * thread = fuzzer->selectNotify(waiters);
376 scheduler->wake(thread);
387 * Process a write ModelAction
388 * @param curr The ModelAction to process
389 * @return True if the mo_graph was updated or promises were resolved
391 bool ModelExecution::process_write(ModelAction *curr)
394 bool updated_mod_order = w_modification_order(curr);
396 mo_graph->commitChanges();
398 get_thread(curr)->set_return_value(VALUE_NONE);
399 return updated_mod_order;
403 * Process a fence ModelAction
404 * @param curr The ModelAction to process
405 * @return True if synchronization was updated
407 bool ModelExecution::process_fence(ModelAction *curr)
410 * fence-relaxed: no-op
411 * fence-release: only log the occurence (not in this function), for
412 * use in later synchronization
413 * fence-acquire (this function): search for hypothetical release
415 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
417 bool updated = false;
418 if (curr->is_acquire()) {
419 action_list_t *list = &action_trace;
420 action_list_t::reverse_iterator rit;
421 /* Find X : is_read(X) && X --sb-> curr */
422 for (rit = list->rbegin();rit != list->rend();rit++) {
423 ModelAction *act = *rit;
426 if (act->get_tid() != curr->get_tid())
428 /* Stop at the beginning of the thread */
429 if (act->is_thread_start())
431 /* Stop once we reach a prior fence-acquire */
432 if (act->is_fence() && act->is_acquire())
436 /* read-acquire will find its own release sequences */
437 if (act->is_acquire())
440 /* Establish hypothetical release sequences */
441 rel_heads_list_t release_heads;
442 get_release_seq_heads(curr, act, &release_heads);
443 for (unsigned int i = 0;i < release_heads.size();i++)
444 synchronize(release_heads[i], curr);
445 if (release_heads.size() != 0)
453 * @brief Process the current action for thread-related activity
455 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
456 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
457 * synchronization, etc. This function is a no-op for non-THREAD actions
458 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
460 * @param curr The current action
461 * @return True if synchronization was updated or a thread completed
463 bool ModelExecution::process_thread_action(ModelAction *curr)
465 bool updated = false;
467 switch (curr->get_type()) {
468 case THREAD_CREATE: {
469 thrd_t *thrd = (thrd_t *)curr->get_location();
470 struct thread_params *params = (struct thread_params *)curr->get_value();
471 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
472 curr->set_thread_operand(th);
474 th->set_creation(curr);
477 case PTHREAD_CREATE: {
478 (*(uint32_t *)curr->get_location()) = pthread_counter++;
480 struct pthread_params *params = (struct pthread_params *)curr->get_value();
481 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
482 curr->set_thread_operand(th);
484 th->set_creation(curr);
486 if ( pthread_map.size() < pthread_counter )
487 pthread_map.resize( pthread_counter );
488 pthread_map[ pthread_counter-1 ] = th;
493 Thread *blocking = curr->get_thread_operand();
494 ModelAction *act = get_last_action(blocking->get_id());
495 synchronize(act, curr);
496 updated = true; /* trigger rel-seq checks */
500 Thread *blocking = curr->get_thread_operand();
501 ModelAction *act = get_last_action(blocking->get_id());
502 synchronize(act, curr);
503 updated = true; /* trigger rel-seq checks */
504 break; // WL: to be add (modified)
507 case THREAD_FINISH: {
508 Thread *th = get_thread(curr);
509 /* Wake up any joining threads */
510 for (unsigned int i = 0;i < get_num_threads();i++) {
511 Thread *waiting = get_thread(int_to_id(i));
512 if (waiting->waiting_on() == th &&
513 waiting->get_pending()->is_thread_join())
514 scheduler->wake(waiting);
517 updated = true; /* trigger rel-seq checks */
531 * Initialize the current action by performing one or more of the following
532 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
533 * in the NodeStack, manipulating backtracking sets, allocating and
534 * initializing clock vectors, and computing the promises to fulfill.
536 * @param curr The current action, as passed from the user context; may be
537 * freed/invalidated after the execution of this function, with a different
538 * action "returned" its place (pass-by-reference)
539 * @return True if curr is a newly-explored action; false otherwise
541 bool ModelExecution::initialize_curr_action(ModelAction **curr)
543 ModelAction *newcurr;
545 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
546 newcurr = process_rmw(*curr);
553 (*curr)->set_seq_number(get_next_seq_num());
555 newcurr = node_stack->explore_action(*curr);
557 /* First restore type and order in case of RMW operation */
558 if ((*curr)->is_rmwr())
559 newcurr->copy_typeandorder(*curr);
561 ASSERT((*curr)->get_location() == newcurr->get_location());
562 newcurr->copy_from_new(*curr);
564 /* Discard duplicate ModelAction; use action from NodeStack */
567 /* Always compute new clock vector */
568 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
571 return false; /* Action was explored previously */
575 /* Always compute new clock vector */
576 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
578 /* Assign most recent release fence */
579 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
581 return true; /* This was a new ModelAction */
586 * @brief Establish reads-from relation between two actions
588 * Perform basic operations involved with establishing a concrete rf relation,
589 * including setting the ModelAction data and checking for release sequences.
591 * @param act The action that is reading (must be a read)
592 * @param rf The action from which we are reading (must be a write)
594 * @return True if this read established synchronization
597 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
600 ASSERT(rf->is_write());
602 act->set_read_from(rf);
603 if (act->is_acquire()) {
604 rel_heads_list_t release_heads;
605 get_release_seq_heads(act, act, &release_heads);
606 int num_heads = release_heads.size();
607 for (unsigned int i = 0;i < release_heads.size();i++)
608 if (!synchronize(release_heads[i], act))
610 return num_heads > 0;
616 * @brief Synchronizes two actions
618 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
619 * This function performs the synchronization as well as providing other hooks
620 * for other checks along with synchronization.
622 * @param first The left-hand side of the synchronizes-with relation
623 * @param second The right-hand side of the synchronizes-with relation
624 * @return True if the synchronization was successful (i.e., was consistent
625 * with the execution order); false otherwise
627 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
629 if (*second < *first) {
630 set_bad_synchronization();
633 return second->synchronize_with(first);
637 * @brief Check whether a model action is enabled.
639 * Checks whether an operation would be successful (i.e., is a lock already
640 * locked, or is the joined thread already complete).
642 * For yield-blocking, yields are never enabled.
644 * @param curr is the ModelAction to check whether it is enabled.
645 * @return a bool that indicates whether the action is enabled.
647 bool ModelExecution::check_action_enabled(ModelAction *curr) {
648 if (curr->is_lock()) {
649 cdsc::mutex *lock = curr->get_mutex();
650 struct cdsc::mutex_state *state = lock->get_state();
653 } else if (curr->is_thread_join()) {
654 Thread *blocking = curr->get_thread_operand();
655 if (!blocking->is_complete()) {
664 * This is the heart of the model checker routine. It performs model-checking
665 * actions corresponding to a given "current action." Among other processes, it
666 * calculates reads-from relationships, updates synchronization clock vectors,
667 * forms a memory_order constraints graph, and handles replay/backtrack
668 * execution when running permutations of previously-observed executions.
670 * @param curr The current action to process
671 * @return The ModelAction that is actually executed; may be different than
674 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
677 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
678 bool newly_explored = initialize_curr_action(&curr);
682 wake_up_sleeping_actions(curr);
684 /* Add the action to lists before any other model-checking tasks */
685 if (!second_part_of_rmw)
686 add_action_to_lists(curr);
688 SnapVector<ModelAction *> * rf_set = NULL;
689 /* Build may_read_from set for newly-created actions */
690 if (newly_explored && curr->is_read())
691 rf_set = build_may_read_from(curr);
693 process_thread_action(curr);
695 if (curr->is_read() && !second_part_of_rmw) {
696 process_read(curr, rf_set);
699 ASSERT(rf_set == NULL);
702 if (curr->is_write())
705 if (curr->is_fence())
708 if (curr->is_mutex_op())
715 * This is the strongest feasibility check available.
716 * @return whether the current trace (partial or complete) must be a prefix of
719 bool ModelExecution::isfeasibleprefix() const
721 return !is_infeasible();
725 * Print disagnostic information about an infeasible execution
726 * @param prefix A string to prefix the output with; if NULL, then a default
727 * message prefix will be provided
729 void ModelExecution::print_infeasibility(const char *prefix) const
733 if (mo_graph->checkForCycles())
734 ptr += sprintf(ptr, "[mo cycle]");
735 if (priv->bad_synchronization)
736 ptr += sprintf(ptr, "[bad sw ordering]");
738 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
742 * Check if the current partial trace is infeasible. Does not check any
743 * end-of-execution flags, which might rule out the execution. Thus, this is
744 * useful only for ruling an execution as infeasible.
745 * @return whether the current partial trace is infeasible.
747 bool ModelExecution::is_infeasible() const
749 return mo_graph->checkForCycles() ||
750 priv->bad_synchronization;
753 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
754 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
755 ModelAction *lastread = get_last_action(act->get_tid());
756 lastread->process_rmw(act);
758 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
759 mo_graph->commitChanges();
765 * @brief Updates the mo_graph with the constraints imposed from the current
768 * Basic idea is the following: Go through each other thread and find
769 * the last action that happened before our read. Two cases:
771 * -# The action is a write: that write must either occur before
772 * the write we read from or be the write we read from.
773 * -# The action is a read: the write that that action read from
774 * must occur before the write we read from or be the same write.
776 * @param curr The current action. Must be a read.
777 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
778 * @return True if modification order edges were added; false otherwise
781 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<ModelAction *> * priorset)
783 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
785 ASSERT(curr->is_read());
787 /* Last SC fence in the current thread */
788 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
789 ModelAction *last_sc_write = NULL;
790 if (curr->is_seqcst())
791 last_sc_write = get_last_seq_cst_write(curr);
793 /* Iterate over all threads */
794 for (i = 0;i < thrd_lists->size();i++) {
795 /* Last SC fence in thread i */
796 ModelAction *last_sc_fence_thread_local = NULL;
797 if (int_to_id((int)i) != curr->get_tid())
798 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
800 /* Last SC fence in thread i, before last SC fence in current thread */
801 ModelAction *last_sc_fence_thread_before = NULL;
802 if (last_sc_fence_local)
803 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
805 /* Iterate over actions in thread, starting from most recent */
806 action_list_t *list = &(*thrd_lists)[i];
807 action_list_t::reverse_iterator rit;
808 for (rit = list->rbegin();rit != list->rend();rit++) {
809 ModelAction *act = *rit;
814 /* Don't want to add reflexive edges on 'rf' */
815 if (act->equals(rf)) {
816 if (act->happens_before(curr))
822 if (act->is_write()) {
823 /* C++, Section 29.3 statement 5 */
824 if (curr->is_seqcst() && last_sc_fence_thread_local &&
825 *act < *last_sc_fence_thread_local) {
826 if (mo_graph->checkReachable(rf, act))
831 /* C++, Section 29.3 statement 4 */
832 else if (act->is_seqcst() && last_sc_fence_local &&
833 *act < *last_sc_fence_local) {
834 if (mo_graph->checkReachable(rf, act))
839 /* C++, Section 29.3 statement 6 */
840 else if (last_sc_fence_thread_before &&
841 *act < *last_sc_fence_thread_before) {
842 if (mo_graph->checkReachable(rf, act))
850 * Include at most one act per-thread that "happens
853 if (act->happens_before(curr)) {
854 if (act->is_write()) {
855 if (mo_graph->checkReachable(rf, act))
859 const ModelAction *prevrf = act->get_reads_from();
860 if (!prevrf->equals(rf)) {
861 if (mo_graph->checkReachable(rf, prevrf))
863 priorset->add(prevrf);
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 for (rit = list->rbegin();rit != list->rend();rit++) {
926 ModelAction *act = *rit;
929 * 1) If RMW and it actually read from something, then we
930 * already have all relevant edges, so just skip to next
933 * 2) If RMW and it didn't read from anything, we should
934 * whatever edge we can get to speed up convergence.
936 * 3) If normal write, we need to look at earlier actions, so
937 * continue processing list.
939 if (curr->is_rmw()) {
940 if (curr->get_reads_from() != NULL)
948 /* C++, Section 29.3 statement 7 */
949 if (last_sc_fence_thread_before && act->is_write() &&
950 *act < *last_sc_fence_thread_before) {
951 mo_graph->addEdge(act, curr);
956 * Include at most one act per-thread that "happens
959 if (act->happens_before(curr)) {
961 * Note: if act is RMW, just add edge:
963 * The following edge should be handled elsewhere:
964 * readfrom(act) --mo--> act
967 mo_graph->addEdge(act, curr);
968 else if (act->is_read()) {
969 //if previous read accessed a null, just keep going
970 mo_graph->addEdge(act->get_reads_from(), curr);
973 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
974 !act->same_thread(curr)) {
975 /* We have an action that:
976 (1) did not happen before us
977 (2) is a read and we are a write
978 (3) cannot synchronize with us
979 (4) is in a different thread
981 that read could potentially read from our write. Note that
982 these checks are overly conservative at this point, we'll
983 do more checks before actually removing the
994 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
995 * some constraints. This method checks one the following constraint (others
996 * require compiler support):
998 * If X --hb-> Y --mo-> Z, then X should not read from Z.
999 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1001 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1003 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1005 /* Iterate over all threads */
1006 for (i = 0;i < thrd_lists->size();i++) {
1007 const ModelAction *write_after_read = NULL;
1009 /* Iterate over actions in thread, starting from most recent */
1010 action_list_t *list = &(*thrd_lists)[i];
1011 action_list_t::reverse_iterator rit;
1012 for (rit = list->rbegin();rit != list->rend();rit++) {
1013 ModelAction *act = *rit;
1015 /* Don't disallow due to act == reader */
1016 if (!reader->happens_before(act) || reader == act)
1018 else if (act->is_write())
1019 write_after_read = act;
1020 else if (act->is_read() && act->get_reads_from() != NULL)
1021 write_after_read = act->get_reads_from();
1024 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1031 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1032 * The ModelAction under consideration is expected to be taking part in
1033 * release/acquire synchronization as an object of the "reads from" relation.
1034 * Note that this can only provide release sequence support for RMW chains
1035 * which do not read from the future, as those actions cannot be traced until
1036 * their "promise" is fulfilled. Similarly, we may not even establish the
1037 * presence of a release sequence with certainty, as some modification order
1038 * constraints may be decided further in the future. Thus, this function
1039 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1040 * and a boolean representing certainty.
1042 * @param rf The action that might be part of a release sequence. Must be a
1044 * @param release_heads A pass-by-reference style return parameter. After
1045 * execution of this function, release_heads will contain the heads of all the
1046 * relevant release sequences, if any exists with certainty
1047 * @return true, if the ModelExecution is certain that release_heads is complete;
1050 bool ModelExecution::release_seq_heads(const ModelAction *rf,
1051 rel_heads_list_t *release_heads) const
1053 /* Only check for release sequences if there are no cycles */
1054 if (mo_graph->checkForCycles())
1057 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1058 ASSERT(rf->is_write());
1060 if (rf->is_release())
1061 release_heads->push_back(rf);
1062 else if (rf->get_last_fence_release())
1063 release_heads->push_back(rf->get_last_fence_release());
1065 break;/* End of RMW chain */
1067 /** @todo Need to be smarter here... In the linux lock
1068 * example, this will run to the beginning of the program for
1070 /** @todo The way to be smarter here is to keep going until 1
1071 * thread has a release preceded by an acquire and you've seen
1074 /* acq_rel RMW is a sufficient stopping condition */
1075 if (rf->is_acquire() && rf->is_release())
1076 return true;/* complete */
1078 ASSERT(rf); // Needs to be real write
1080 if (rf->is_release())
1081 return true;/* complete */
1083 /* else relaxed write
1084 * - check for fence-release in the same thread (29.8, stmt. 3)
1085 * - check modification order for contiguous subsequence
1086 * -> rf must be same thread as release */
1088 const ModelAction *fence_release = rf->get_last_fence_release();
1089 /* Synchronize with a fence-release unconditionally; we don't need to
1090 * find any more "contiguous subsequence..." for it */
1092 release_heads->push_back(fence_release);
1094 return true; /* complete */
1098 * An interface for getting the release sequence head(s) with which a
1099 * given ModelAction must synchronize. This function only returns a non-empty
1100 * result when it can locate a release sequence head with certainty. Otherwise,
1101 * it may mark the internal state of the ModelExecution so that it will handle
1102 * the release sequence at a later time, causing @a acquire to update its
1103 * synchronization at some later point in execution.
1105 * @param acquire The 'acquire' action that may synchronize with a release
1107 * @param read The read action that may read from a release sequence; this may
1108 * be the same as acquire, or else an earlier action in the same thread (i.e.,
1109 * when 'acquire' is a fence-acquire)
1110 * @param release_heads A pass-by-reference return parameter. Will be filled
1111 * with the head(s) of the release sequence(s), if they exists with certainty.
1112 * @see ModelExecution::release_seq_heads
1114 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
1115 ModelAction *read, rel_heads_list_t *release_heads)
1117 const ModelAction *rf = read->get_reads_from();
1119 release_seq_heads(rf, release_heads);
1123 * Performs various bookkeeping operations for the current ModelAction. For
1124 * instance, adds action to the per-object, per-thread action vector and to the
1125 * action trace list of all thread actions.
1127 * @param act is the ModelAction to add.
1129 void ModelExecution::add_action_to_lists(ModelAction *act)
1131 int tid = id_to_int(act->get_tid());
1132 ModelAction *uninit = NULL;
1134 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1135 if (list->empty() && act->is_atomic_var()) {
1136 uninit = get_uninitialized_action(act);
1137 uninit_id = id_to_int(uninit->get_tid());
1138 list->push_front(uninit);
1140 list->push_back(act);
1142 action_trace.push_back(act);
1144 action_trace.push_front(uninit);
1146 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1147 if (tid >= (int)vec->size())
1148 vec->resize(priv->next_thread_id);
1149 (*vec)[tid].push_back(act);
1151 (*vec)[uninit_id].push_front(uninit);
1153 if ((int)thrd_last_action.size() <= tid)
1154 thrd_last_action.resize(get_num_threads());
1155 thrd_last_action[tid] = act;
1157 thrd_last_action[uninit_id] = uninit;
1159 if (act->is_fence() && act->is_release()) {
1160 if ((int)thrd_last_fence_release.size() <= tid)
1161 thrd_last_fence_release.resize(get_num_threads());
1162 thrd_last_fence_release[tid] = act;
1165 if (act->is_wait()) {
1166 void *mutex_loc = (void *) act->get_value();
1167 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1169 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1170 if (tid >= (int)vec->size())
1171 vec->resize(priv->next_thread_id);
1172 (*vec)[tid].push_back(act);
1177 * @brief Get the last action performed by a particular Thread
1178 * @param tid The thread ID of the Thread in question
1179 * @return The last action in the thread
1181 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1183 int threadid = id_to_int(tid);
1184 if (threadid < (int)thrd_last_action.size())
1185 return thrd_last_action[id_to_int(tid)];
1191 * @brief Get the last fence release performed by a particular Thread
1192 * @param tid The thread ID of the Thread in question
1193 * @return The last fence release in the thread, if one exists; NULL otherwise
1195 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1197 int threadid = id_to_int(tid);
1198 if (threadid < (int)thrd_last_fence_release.size())
1199 return thrd_last_fence_release[id_to_int(tid)];
1205 * Gets the last memory_order_seq_cst write (in the total global sequence)
1206 * performed on a particular object (i.e., memory location), not including the
1208 * @param curr The current ModelAction; also denotes the object location to
1210 * @return The last seq_cst write
1212 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1214 void *location = curr->get_location();
1215 action_list_t *list = obj_map.get(location);
1216 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1217 action_list_t::reverse_iterator rit;
1218 for (rit = list->rbegin();(*rit) != curr;rit++)
1220 rit++; /* Skip past curr */
1221 for ( ;rit != list->rend();rit++)
1222 if ((*rit)->is_write() && (*rit)->is_seqcst())
1228 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1229 * performed in a particular thread, prior to a particular fence.
1230 * @param tid The ID of the thread to check
1231 * @param before_fence The fence from which to begin the search; if NULL, then
1232 * search for the most recent fence in the thread.
1233 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1235 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1237 /* All fences should have location FENCE_LOCATION */
1238 action_list_t *list = obj_map.get(FENCE_LOCATION);
1243 action_list_t::reverse_iterator rit = list->rbegin();
1246 for (;rit != list->rend();rit++)
1247 if (*rit == before_fence)
1250 ASSERT(*rit == before_fence);
1254 for (;rit != list->rend();rit++)
1255 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1261 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1262 * location). This function identifies the mutex according to the current
1263 * action, which is presumed to perform on the same mutex.
1264 * @param curr The current ModelAction; also denotes the object location to
1266 * @return The last unlock operation
1268 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1270 void *location = curr->get_location();
1272 action_list_t *list = obj_map.get(location);
1273 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1274 action_list_t::reverse_iterator rit;
1275 for (rit = list->rbegin();rit != list->rend();rit++)
1276 if ((*rit)->is_unlock() || (*rit)->is_wait())
1281 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1283 ModelAction *parent = get_last_action(tid);
1285 parent = get_thread(tid)->get_creation();
1290 * Returns the clock vector for a given thread.
1291 * @param tid The thread whose clock vector we want
1292 * @return Desired clock vector
1294 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1296 return get_parent_action(tid)->get_cv();
1299 bool valequals(uint64_t val1, uint64_t val2, int size) {
1302 return ((uint8_t)val1) == ((uint8_t)val2);
1304 return ((uint16_t)val1) == ((uint16_t)val2);
1306 return ((uint32_t)val1) == ((uint32_t)val2);
1316 * Build up an initial set of all past writes that this 'read' action may read
1317 * from, as well as any previously-observed future values that must still be valid.
1319 * @param curr is the current ModelAction that we are exploring; it must be a
1322 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1324 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1326 ASSERT(curr->is_read());
1328 ModelAction *last_sc_write = NULL;
1330 if (curr->is_seqcst())
1331 last_sc_write = get_last_seq_cst_write(curr);
1333 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1334 SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
1336 /* Iterate over all threads */
1337 for (i = 0;i < thrd_lists->size();i++) {
1338 /* Iterate over actions in thread, starting from most recent */
1339 action_list_t *list = &(*thrd_lists)[i];
1340 action_list_t::reverse_iterator rit;
1341 for (rit = list->rbegin();rit != list->rend();rit++) {
1342 ModelAction *act = *rit;
1344 /* Only consider 'write' actions */
1345 if (!act->is_write() || act == curr)
1348 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1349 bool allow_read = true;
1351 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1354 /* Need to check whether we will have two RMW reading from the same value */
1355 if (curr->is_rmwr()) {
1356 /* It is okay if we have a failing CAS */
1357 if (!curr->is_rmwrcas() ||
1358 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1359 //Need to make sure we aren't the second RMW
1360 CycleNode * node = mo_graph->getNode_noCreate(act);
1361 if (node != NULL && node->getRMW() != NULL) {
1362 //we are the second RMW
1369 /* Only add feasible reads */
1370 rf_set->push_back(act);
1373 /* Include at most one act per-thread that "happens before" curr */
1374 if (act->happens_before(curr))
1379 if (DBG_ENABLED()) {
1380 model_print("Reached read action:\n");
1382 model_print("End printing read_from_past\n");
1388 * @brief Get an action representing an uninitialized atomic
1390 * This function may create a new one or try to retrieve one from the NodeStack
1392 * @param curr The current action, which prompts the creation of an UNINIT action
1393 * @return A pointer to the UNINIT ModelAction
1395 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1397 Node *node = curr->get_node();
1398 ModelAction *act = node->get_uninit_action();
1400 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1401 node->set_uninit_action(act);
1403 act->create_cv(NULL);
1407 static void print_list(const action_list_t *list)
1409 action_list_t::const_iterator it;
1411 model_print("------------------------------------------------------------------------------------\n");
1412 model_print("# t Action type MO Location Value Rf CV\n");
1413 model_print("------------------------------------------------------------------------------------\n");
1415 unsigned int hash = 0;
1417 for (it = list->begin();it != list->end();it++) {
1418 const ModelAction *act = *it;
1419 if (act->get_seq_number() > 0)
1421 hash = hash^(hash<<3)^((*it)->hash());
1423 model_print("HASH %u\n", hash);
1424 model_print("------------------------------------------------------------------------------------\n");
1427 #if SUPPORT_MOD_ORDER_DUMP
1428 void ModelExecution::dumpGraph(char *filename) const
1431 sprintf(buffer, "%s.dot", filename);
1432 FILE *file = fopen(buffer, "w");
1433 fprintf(file, "digraph %s {\n", filename);
1434 mo_graph->dumpNodes(file);
1435 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1437 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1438 ModelAction *act = *it;
1439 if (act->is_read()) {
1440 mo_graph->dot_print_node(file, act);
1441 mo_graph->dot_print_edge(file,
1442 act->get_reads_from(),
1444 "label=\"rf\", color=red, weight=2");
1446 if (thread_array[act->get_tid()]) {
1447 mo_graph->dot_print_edge(file,
1448 thread_array[id_to_int(act->get_tid())],
1450 "label=\"sb\", color=blue, weight=400");
1453 thread_array[act->get_tid()] = act;
1455 fprintf(file, "}\n");
1456 model_free(thread_array);
1461 /** @brief Prints an execution trace summary. */
1462 void ModelExecution::print_summary() const
1464 #if SUPPORT_MOD_ORDER_DUMP
1465 char buffername[100];
1466 sprintf(buffername, "exec%04u", get_execution_number());
1467 mo_graph->dumpGraphToFile(buffername);
1468 sprintf(buffername, "graph%04u", get_execution_number());
1469 dumpGraph(buffername);
1472 model_print("Execution trace %d:", get_execution_number());
1473 if (isfeasibleprefix()) {
1474 if (scheduler->all_threads_sleeping())
1475 model_print(" SLEEP-SET REDUNDANT");
1476 if (have_bug_reports())
1477 model_print(" DETECTED BUG(S)");
1479 print_infeasibility(" INFEASIBLE");
1482 print_list(&action_trace);
1488 * Add a Thread to the system for the first time. Should only be called once
1490 * @param t The Thread to add
1492 void ModelExecution::add_thread(Thread *t)
1494 unsigned int i = id_to_int(t->get_id());
1495 if (i >= thread_map.size())
1496 thread_map.resize(i + 1);
1498 if (!t->is_model_thread())
1499 scheduler->add_thread(t);
1503 * @brief Get a Thread reference by its ID
1504 * @param tid The Thread's ID
1505 * @return A Thread reference
1507 Thread * ModelExecution::get_thread(thread_id_t tid) const
1509 unsigned int i = id_to_int(tid);
1510 if (i < thread_map.size())
1511 return thread_map[i];
1516 * @brief Get a reference to the Thread in which a ModelAction was executed
1517 * @param act The ModelAction
1518 * @return A Thread reference
1520 Thread * ModelExecution::get_thread(const ModelAction *act) const
1522 return get_thread(act->get_tid());
1526 * @brief Get a Thread reference by its pthread ID
1527 * @param index The pthread's ID
1528 * @return A Thread reference
1530 Thread * ModelExecution::get_pthread(pthread_t pid) {
1536 uint32_t thread_id = x.v;
1537 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1542 * @brief Check if a Thread is currently enabled
1543 * @param t The Thread to check
1544 * @return True if the Thread is currently enabled
1546 bool ModelExecution::is_enabled(Thread *t) const
1548 return scheduler->is_enabled(t);
1552 * @brief Check if a Thread is currently enabled
1553 * @param tid The ID of the Thread to check
1554 * @return True if the Thread is currently enabled
1556 bool ModelExecution::is_enabled(thread_id_t tid) const
1558 return scheduler->is_enabled(tid);
1562 * @brief Select the next thread to execute based on the curren action
1564 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1565 * actions should be followed by the execution of their child thread. In either
1566 * case, the current action should determine the next thread schedule.
1568 * @param curr The current action
1569 * @return The next thread to run, if the current action will determine this
1570 * selection; otherwise NULL
1572 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1574 /* Do not split atomic RMW */
1575 if (curr->is_rmwr())
1576 return get_thread(curr);
1577 if (curr->is_write()) {
1578 std::memory_order order = curr->get_mo();
1580 case std::memory_order_relaxed:
1581 return get_thread(curr);
1582 case std::memory_order_release:
1583 return get_thread(curr);
1589 /* Follow CREATE with the created thread */
1590 /* which is not needed, because model.cc takes care of this */
1591 if (curr->get_type() == THREAD_CREATE)
1592 return curr->get_thread_operand();
1593 if (curr->get_type() == PTHREAD_CREATE) {
1594 return curr->get_thread_operand();
1600 * Takes the next step in the execution, if possible.
1601 * @param curr The current step to take
1602 * @return Returns the next Thread to run, if any; NULL if this execution
1605 Thread * ModelExecution::take_step(ModelAction *curr)
1607 Thread *curr_thrd = get_thread(curr);
1608 ASSERT(curr_thrd->get_state() == THREAD_READY);
1610 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1611 curr = check_current_action(curr);
1614 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1615 scheduler->remove_thread(curr_thrd);
1617 return action_select_next_thread(curr);
1620 Fuzzer * ModelExecution::getFuzzer() {