12 #include "clockvector.h"
13 #include "cyclegraph.h"
15 #include "threads-model.h"
16 #include "bugmessage.h"
18 #define INITIAL_THREAD_ID 0
21 * Structure for holding small ModelChecker members that should be snapshotted
23 struct model_snapshot_members {
24 model_snapshot_members() :
25 /* First thread created will have id INITIAL_THREAD_ID */
26 next_thread_id(INITIAL_THREAD_ID),
27 used_sequence_numbers(0),
30 too_many_reads(false),
31 no_valid_reads(false),
32 bad_synchronization(false),
37 ~model_snapshot_members() {
38 for (unsigned int i = 0; i < bugs.size(); i++)
43 unsigned int next_thread_id;
44 modelclock_t used_sequence_numbers;
45 ModelAction *next_backtrack;
46 SnapVector<bug_message *> bugs;
49 /** @brief Incorrectly-ordered synchronization was made */
50 bool bad_synchronization;
57 /** @brief Constructor */
58 ModelExecution::ModelExecution(ModelChecker *m,
60 NodeStack *node_stack) :
65 thread_map(2), /* We'll always need at least 2 threads */
69 condvar_waiters_map(),
73 thrd_last_fence_release(),
74 node_stack(node_stack),
75 priv(new struct model_snapshot_members()),
76 mo_graph(new CycleGraph())
78 /* Initialize a model-checker thread, for special ModelActions */
79 model_thread = new Thread(get_next_id());
80 add_thread(model_thread);
81 scheduler->register_engine(this);
82 node_stack->register_engine(this);
85 /** @brief Destructor */
86 ModelExecution::~ModelExecution()
88 for (unsigned int i = 0; i < get_num_threads(); i++)
89 delete get_thread(int_to_id(i));
95 int ModelExecution::get_execution_number() const
97 return model->get_execution_number();
100 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
102 action_list_t *tmp = hash->get(ptr);
104 tmp = new action_list_t();
110 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
112 SnapVector<action_list_t> *tmp = hash->get(ptr);
114 tmp = new SnapVector<action_list_t>();
120 action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
122 SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
125 unsigned int thread=id_to_int(tid);
126 if (thread < wrv->size())
127 return &(*wrv)[thread];
132 /** @return a thread ID for a new Thread */
133 thread_id_t ModelExecution::get_next_id()
135 return priv->next_thread_id++;
138 /** @return the number of user threads created during this execution */
139 unsigned int ModelExecution::get_num_threads() const
141 return priv->next_thread_id;
144 /** @return a sequence number for a new ModelAction */
145 modelclock_t ModelExecution::get_next_seq_num()
147 return ++priv->used_sequence_numbers;
151 * @brief Should the current action wake up a given thread?
153 * @param curr The current action
154 * @param thread The thread that we might wake up
155 * @return True, if we should wake up the sleeping thread; false otherwise
157 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
159 const ModelAction *asleep = thread->get_pending();
160 /* Don't allow partial RMW to wake anyone up */
163 /* Synchronizing actions may have been backtracked */
164 if (asleep->could_synchronize_with(curr))
166 /* All acquire/release fences and fence-acquire/store-release */
167 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
169 /* Fence-release + store can awake load-acquire on the same location */
170 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
171 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
172 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
178 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
180 for (unsigned int i = 0; i < get_num_threads(); i++) {
181 Thread *thr = get_thread(int_to_id(i));
182 if (scheduler->is_sleep_set(thr)) {
183 if (should_wake_up(curr, thr))
184 /* Remove this thread from sleep set */
185 scheduler->remove_sleep(thr);
190 /** @brief Alert the model-checker that an incorrectly-ordered
191 * synchronization was made */
192 void ModelExecution::set_bad_synchronization()
194 priv->bad_synchronization = true;
197 /** @brief Alert the model-checker that an incorrectly-ordered
198 * synchronization was made */
199 void ModelExecution::set_bad_sc_read()
201 priv->bad_sc_read = true;
204 bool ModelExecution::assert_bug(const char *msg)
206 priv->bugs.push_back(new bug_message(msg));
208 if (isfeasibleprefix()) {
215 /** @return True, if any bugs have been reported for this execution */
216 bool ModelExecution::have_bug_reports() const
218 return priv->bugs.size() != 0;
221 SnapVector<bug_message *> * ModelExecution::get_bugs() const
227 * Check whether the current trace has triggered an assertion which should halt
230 * @return True, if the execution should be aborted; false otherwise
232 bool ModelExecution::has_asserted() const
234 return priv->asserted;
238 * Trigger a trace assertion which should cause this execution to be halted.
239 * This can be due to a detected bug or due to an infeasibility that should
242 void ModelExecution::set_assert()
244 priv->asserted = true;
248 * Check if we are in a deadlock. Should only be called at the end of an
249 * execution, although it should not give false positives in the middle of an
250 * execution (there should be some ENABLED thread).
252 * @return True if program is in a deadlock; false otherwise
254 bool ModelExecution::is_deadlocked() const
256 bool blocking_threads = false;
257 for (unsigned int i = 0; i < get_num_threads(); i++) {
258 thread_id_t tid = int_to_id(i);
261 Thread *t = get_thread(tid);
262 if (!t->is_model_thread() && t->get_pending())
263 blocking_threads = true;
265 return blocking_threads;
269 * Check if this is a complete execution. That is, have all thread completed
270 * execution (rather than exiting because sleep sets have forced a redundant
273 * @return True if the execution is complete.
275 bool ModelExecution::is_complete_execution() const
277 for (unsigned int i = 0; i < get_num_threads(); i++)
278 if (is_enabled(int_to_id(i)))
285 * Processes a read model action.
286 * @param curr is the read model action to process.
287 * @param rf_set is the set of model actions we can possibly read from
288 * @return True if processing this read updates the mo_graph.
290 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
292 int random_index = random() % rf_set->size();
293 bool updated = false;
295 const ModelAction *rf = (*rf_set)[random_index];
298 mo_graph->startChanges();
300 updated = r_modification_order(curr, rf);
302 mo_graph->commitChanges();
303 get_thread(curr)->set_return_value(curr->get_return_value());
308 * Processes a lock, trylock, or unlock model action. @param curr is
309 * the read model action to process.
311 * The try lock operation checks whether the lock is taken. If not,
312 * it falls to the normal lock operation case. If so, it returns
315 * The lock operation has already been checked that it is enabled, so
316 * it just grabs the lock and synchronizes with the previous unlock.
318 * The unlock operation has to re-enable all of the threads that are
319 * waiting on the lock.
321 * @return True if synchronization was updated; false otherwise
323 bool ModelExecution::process_mutex(ModelAction *curr)
325 cdsc::mutex *mutex = curr->get_mutex();
326 struct cdsc::mutex_state *state = NULL;
329 state = mutex->get_state();
331 switch (curr->get_type()) {
332 case ATOMIC_TRYLOCK: {
333 bool success = !state->locked;
334 curr->set_try_lock(success);
336 get_thread(curr)->set_return_value(0);
339 get_thread(curr)->set_return_value(1);
341 //otherwise fall into the lock case
343 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
344 assert_bug("Lock access before initialization");
345 state->locked = get_thread(curr);
346 ModelAction *unlock = get_last_unlock(curr);
347 //synchronize with the previous unlock statement
348 if (unlock != NULL) {
349 synchronize(unlock, curr);
355 case ATOMIC_UNLOCK: {
356 /* wake up the other threads */
357 for (unsigned int i = 0; i < get_num_threads(); i++) {
358 Thread *t = get_thread(int_to_id(i));
359 Thread *curr_thrd = get_thread(curr);
360 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
364 /* unlock the lock - after checking who was waiting on it */
365 state->locked = NULL;
367 if (!curr->is_wait())
368 break; /* The rest is only for ATOMIC_WAIT */
372 case ATOMIC_NOTIFY_ALL: {
373 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
374 //activate all the waiting threads
375 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
376 scheduler->wake(get_thread(*rit));
381 case ATOMIC_NOTIFY_ONE: {
382 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
384 //BCD -- TOFIX FUZZER
385 //THIS SHOULD BE A RANDOM CHOICE
386 // int wakeupthread = curr->get_node()->get_misc();
387 int wakeupthread = 0;
388 action_list_t::iterator it = waiters->begin();
391 if (it == waiters->end())
394 advance(it, wakeupthread);
395 scheduler->wake(get_thread(*it));
407 * Process a write ModelAction
408 * @param curr The ModelAction to process
409 * @return True if the mo_graph was updated or promises were resolved
411 bool ModelExecution::process_write(ModelAction *curr)
414 bool updated_mod_order = w_modification_order(curr);
416 mo_graph->commitChanges();
418 get_thread(curr)->set_return_value(VALUE_NONE);
419 return updated_mod_order;
423 * Process a fence ModelAction
424 * @param curr The ModelAction to process
425 * @return True if synchronization was updated
427 bool ModelExecution::process_fence(ModelAction *curr)
430 * fence-relaxed: no-op
431 * fence-release: only log the occurence (not in this function), for
432 * use in later synchronization
433 * fence-acquire (this function): search for hypothetical release
435 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
437 bool updated = false;
438 if (curr->is_acquire()) {
439 action_list_t *list = &action_trace;
440 action_list_t::reverse_iterator rit;
441 /* Find X : is_read(X) && X --sb-> curr */
442 for (rit = list->rbegin(); rit != list->rend(); rit++) {
443 ModelAction *act = *rit;
446 if (act->get_tid() != curr->get_tid())
448 /* Stop at the beginning of the thread */
449 if (act->is_thread_start())
451 /* Stop once we reach a prior fence-acquire */
452 if (act->is_fence() && act->is_acquire())
456 /* read-acquire will find its own release sequences */
457 if (act->is_acquire())
460 /* Establish hypothetical release sequences */
461 rel_heads_list_t release_heads;
462 get_release_seq_heads(curr, act, &release_heads);
463 for (unsigned int i = 0; i < release_heads.size(); i++)
464 synchronize(release_heads[i], curr);
465 if (release_heads.size() != 0)
473 * @brief Process the current action for thread-related activity
475 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
476 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
477 * synchronization, etc. This function is a no-op for non-THREAD actions
478 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
480 * @param curr The current action
481 * @return True if synchronization was updated or a thread completed
483 bool ModelExecution::process_thread_action(ModelAction *curr)
485 bool updated = false;
487 switch (curr->get_type()) {
488 case THREAD_CREATE: {
489 thrd_t *thrd = (thrd_t *)curr->get_location();
490 struct thread_params *params = (struct thread_params *)curr->get_value();
491 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
492 curr->set_thread_operand(th);
494 th->set_creation(curr);
497 case PTHREAD_CREATE: {
498 (*(pthread_t *)curr->get_location()) = pthread_counter++;
500 struct pthread_params *params = (struct pthread_params *)curr->get_value();
501 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
502 curr->set_thread_operand(th);
504 th->set_creation(curr);
506 if ( pthread_map.size() < pthread_counter )
507 pthread_map.resize( pthread_counter );
508 pthread_map[ pthread_counter-1 ] = th;
513 Thread *blocking = curr->get_thread_operand();
514 ModelAction *act = get_last_action(blocking->get_id());
515 synchronize(act, curr);
516 updated = true; /* trigger rel-seq checks */
520 Thread *blocking = curr->get_thread_operand();
521 ModelAction *act = get_last_action(blocking->get_id());
522 synchronize(act, curr);
523 updated = true; /* trigger rel-seq checks */
524 break; // WL: to be add (modified)
527 case THREAD_FINISH: {
528 Thread *th = get_thread(curr);
529 /* Wake up any joining threads */
530 for (unsigned int i = 0; i < get_num_threads(); i++) {
531 Thread *waiting = get_thread(int_to_id(i));
532 if (waiting->waiting_on() == th &&
533 waiting->get_pending()->is_thread_join())
534 scheduler->wake(waiting);
537 updated = true; /* trigger rel-seq checks */
551 * Initialize the current action by performing one or more of the following
552 * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
553 * in the NodeStack, manipulating backtracking sets, allocating and
554 * initializing clock vectors, and computing the promises to fulfill.
556 * @param curr The current action, as passed from the user context; may be
557 * freed/invalidated after the execution of this function, with a different
558 * action "returned" its place (pass-by-reference)
559 * @return True if curr is a newly-explored action; false otherwise
561 bool ModelExecution::initialize_curr_action(ModelAction **curr)
563 ModelAction *newcurr;
565 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
566 newcurr = process_rmw(*curr);
573 (*curr)->set_seq_number(get_next_seq_num());
575 newcurr = node_stack->explore_action(*curr);
577 /* First restore type and order in case of RMW operation */
578 if ((*curr)->is_rmwr())
579 newcurr->copy_typeandorder(*curr);
581 ASSERT((*curr)->get_location() == newcurr->get_location());
582 newcurr->copy_from_new(*curr);
584 /* Discard duplicate ModelAction; use action from NodeStack */
587 /* Always compute new clock vector */
588 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
591 return false; /* Action was explored previously */
595 /* Always compute new clock vector */
596 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
598 /* Assign most recent release fence */
599 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
601 return true; /* This was a new ModelAction */
606 * @brief Establish reads-from relation between two actions
608 * Perform basic operations involved with establishing a concrete rf relation,
609 * including setting the ModelAction data and checking for release sequences.
611 * @param act The action that is reading (must be a read)
612 * @param rf The action from which we are reading (must be a write)
614 * @return True if this read established synchronization
617 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
620 ASSERT(rf->is_write());
622 act->set_read_from(rf);
623 if (act->is_acquire()) {
624 rel_heads_list_t release_heads;
625 get_release_seq_heads(act, act, &release_heads);
626 int num_heads = release_heads.size();
627 for (unsigned int i = 0; i < release_heads.size(); i++)
628 if (!synchronize(release_heads[i], act))
630 return num_heads > 0;
636 * @brief Synchronizes two actions
638 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
639 * This function performs the synchronization as well as providing other hooks
640 * for other checks along with synchronization.
642 * @param first The left-hand side of the synchronizes-with relation
643 * @param second The right-hand side of the synchronizes-with relation
644 * @return True if the synchronization was successful (i.e., was consistent
645 * with the execution order); false otherwise
647 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
649 if (*second < *first) {
650 set_bad_synchronization();
653 return second->synchronize_with(first);
657 * @brief Check whether a model action is enabled.
659 * Checks whether an operation would be successful (i.e., is a lock already
660 * locked, or is the joined thread already complete).
662 * For yield-blocking, yields are never enabled.
664 * @param curr is the ModelAction to check whether it is enabled.
665 * @return a bool that indicates whether the action is enabled.
667 bool ModelExecution::check_action_enabled(ModelAction *curr) {
668 if (curr->is_lock()) {
669 cdsc::mutex *lock = curr->get_mutex();
670 struct cdsc::mutex_state *state = lock->get_state();
673 } else if (curr->is_thread_join()) {
674 Thread *blocking = curr->get_thread_operand();
675 if (!blocking->is_complete()) {
684 * This is the heart of the model checker routine. It performs model-checking
685 * actions corresponding to a given "current action." Among other processes, it
686 * calculates reads-from relationships, updates synchronization clock vectors,
687 * forms a memory_order constraints graph, and handles replay/backtrack
688 * execution when running permutations of previously-observed executions.
690 * @param curr The current action to process
691 * @return The ModelAction that is actually executed; may be different than
694 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
697 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
698 bool newly_explored = initialize_curr_action(&curr);
702 wake_up_sleeping_actions(curr);
704 /* Add the action to lists before any other model-checking tasks */
705 if (!second_part_of_rmw)
706 add_action_to_lists(curr);
708 ModelVector<ModelAction *> * rf_set = NULL;
709 /* Build may_read_from set for newly-created actions */
710 if (newly_explored && curr->is_read())
711 rf_set = build_may_read_from(curr);
713 process_thread_action(curr);
715 if (curr->is_read() && !second_part_of_rmw) {
716 process_read(curr, rf_set);
720 if (curr->is_write())
723 if (curr->is_fence())
726 if (curr->is_mutex_op())
733 * This is the strongest feasibility check available.
734 * @return whether the current trace (partial or complete) must be a prefix of
737 bool ModelExecution::isfeasibleprefix() const
739 return !is_infeasible();
743 * Print disagnostic information about an infeasible execution
744 * @param prefix A string to prefix the output with; if NULL, then a default
745 * message prefix will be provided
747 void ModelExecution::print_infeasibility(const char *prefix) const
751 if (mo_graph->checkForCycles())
752 ptr += sprintf(ptr, "[mo cycle]");
753 if (priv->too_many_reads)
754 ptr += sprintf(ptr, "[too many reads]");
755 if (priv->no_valid_reads)
756 ptr += sprintf(ptr, "[no valid reads-from]");
757 if (priv->bad_synchronization)
758 ptr += sprintf(ptr, "[bad sw ordering]");
759 if (priv->bad_sc_read)
760 ptr += sprintf(ptr, "[bad sc read]");
762 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
766 * Check if the current partial trace is infeasible. Does not check any
767 * end-of-execution flags, which might rule out the execution. Thus, this is
768 * useful only for ruling an execution as infeasible.
769 * @return whether the current partial trace is infeasible.
771 bool ModelExecution::is_infeasible() const
773 return mo_graph->checkForCycles() ||
774 priv->no_valid_reads ||
775 priv->too_many_reads ||
776 priv->bad_synchronization ||
780 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
781 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
782 ModelAction *lastread = get_last_action(act->get_tid());
783 lastread->process_rmw(act);
785 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
786 mo_graph->commitChanges();
792 * @brief Updates the mo_graph with the constraints imposed from the current
795 * Basic idea is the following: Go through each other thread and find
796 * the last action that happened before our read. Two cases:
798 * -# The action is a write: that write must either occur before
799 * the write we read from or be the write we read from.
800 * -# The action is a read: the write that that action read from
801 * must occur before the write we read from or be the same write.
803 * @param curr The current action. Must be a read.
804 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
805 * @return True if modification order edges were added; false otherwise
807 template <typename rf_type>
808 bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
810 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
813 ASSERT(curr->is_read());
815 /* Last SC fence in the current thread */
816 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
817 ModelAction *last_sc_write = NULL;
818 if (curr->is_seqcst())
819 last_sc_write = get_last_seq_cst_write(curr);
821 /* Iterate over all threads */
822 for (i = 0; i < thrd_lists->size(); i++) {
823 /* Last SC fence in thread i */
824 ModelAction *last_sc_fence_thread_local = NULL;
825 if (int_to_id((int)i) != curr->get_tid())
826 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
828 /* Last SC fence in thread i, before last SC fence in current thread */
829 ModelAction *last_sc_fence_thread_before = NULL;
830 if (last_sc_fence_local)
831 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
833 /* Iterate over actions in thread, starting from most recent */
834 action_list_t *list = &(*thrd_lists)[i];
835 action_list_t::reverse_iterator rit;
836 for (rit = list->rbegin(); rit != list->rend(); rit++) {
837 ModelAction *act = *rit;
842 /* Don't want to add reflexive edges on 'rf' */
843 if (act->equals(rf)) {
844 if (act->happens_before(curr))
850 if (act->is_write()) {
851 /* C++, Section 29.3 statement 5 */
852 if (curr->is_seqcst() && last_sc_fence_thread_local &&
853 *act < *last_sc_fence_thread_local) {
854 added = mo_graph->addEdge(act, rf) || added;
857 /* C++, Section 29.3 statement 4 */
858 else if (act->is_seqcst() && last_sc_fence_local &&
859 *act < *last_sc_fence_local) {
860 added = mo_graph->addEdge(act, rf) || added;
863 /* C++, Section 29.3 statement 6 */
864 else if (last_sc_fence_thread_before &&
865 *act < *last_sc_fence_thread_before) {
866 added = mo_graph->addEdge(act, rf) || added;
872 * Include at most one act per-thread that "happens
875 if (act->happens_before(curr)) {
876 if (act->is_write()) {
877 added = mo_graph->addEdge(act, rf) || added;
879 const ModelAction *prevrf = act->get_reads_from();
880 if (!prevrf->equals(rf))
881 added = mo_graph->addEdge(prevrf, rf) || added;
892 * Updates the mo_graph with the constraints imposed from the current write.
894 * Basic idea is the following: Go through each other thread and find
895 * the lastest action that happened before our write. Two cases:
897 * (1) The action is a write => that write must occur before
900 * (2) The action is a read => the write that that action read from
901 * must occur before the current write.
903 * This method also handles two other issues:
905 * (I) Sequential Consistency: Making sure that if the current write is
906 * seq_cst, that it occurs after the previous seq_cst write.
908 * (II) Sending the write back to non-synchronizing reads.
910 * @param curr The current action. Must be a write.
911 * @param send_fv A vector for stashing reads to which we may pass our future
912 * value. If NULL, then don't record any future values.
913 * @return True if modification order edges were added; false otherwise
915 bool ModelExecution::w_modification_order(ModelAction *curr)
917 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
920 ASSERT(curr->is_write());
922 if (curr->is_seqcst()) {
923 /* We have to at least see the last sequentially consistent write,
924 so we are initialized. */
925 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
926 if (last_seq_cst != NULL) {
927 added = mo_graph->addEdge(last_seq_cst, curr) || added;
931 /* Last SC fence in the current thread */
932 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
934 /* Iterate over all threads */
935 for (i = 0; i < thrd_lists->size(); i++) {
936 /* Last SC fence in thread i, before last SC fence in current thread */
937 ModelAction *last_sc_fence_thread_before = NULL;
938 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
939 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
941 /* Iterate over actions in thread, starting from most recent */
942 action_list_t *list = &(*thrd_lists)[i];
943 action_list_t::reverse_iterator rit;
944 for (rit = list->rbegin(); rit != list->rend(); rit++) {
945 ModelAction *act = *rit;
948 * 1) If RMW and it actually read from something, then we
949 * already have all relevant edges, so just skip to next
952 * 2) If RMW and it didn't read from anything, we should
953 * whatever edge we can get to speed up convergence.
955 * 3) If normal write, we need to look at earlier actions, so
956 * continue processing list.
958 if (curr->is_rmw()) {
959 if (curr->get_reads_from() != NULL)
967 /* C++, Section 29.3 statement 7 */
968 if (last_sc_fence_thread_before && act->is_write() &&
969 *act < *last_sc_fence_thread_before) {
970 added = mo_graph->addEdge(act, curr) || added;
975 * Include at most one act per-thread that "happens
978 if (act->happens_before(curr)) {
980 * Note: if act is RMW, just add edge:
982 * The following edge should be handled elsewhere:
983 * readfrom(act) --mo--> act
986 added = mo_graph->addEdge(act, curr) || added;
987 else if (act->is_read()) {
988 //if previous read accessed a null, just keep going
989 added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
992 } else if (act->is_read() && !act->could_synchronize_with(curr) &&
993 !act->same_thread(curr)) {
994 /* We have an action that:
995 (1) did not happen before us
996 (2) is a read and we are a write
997 (3) cannot synchronize with us
998 (4) is in a different thread
1000 that read could potentially read from our write. Note that
1001 these checks are overly conservative at this point, we'll
1002 do more checks before actually removing the
1015 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1016 * some constraints. This method checks one the following constraint (others
1017 * require compiler support):
1019 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1020 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1022 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1024 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1026 /* Iterate over all threads */
1027 for (i = 0; i < thrd_lists->size(); i++) {
1028 const ModelAction *write_after_read = NULL;
1030 /* Iterate over actions in thread, starting from most recent */
1031 action_list_t *list = &(*thrd_lists)[i];
1032 action_list_t::reverse_iterator rit;
1033 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1034 ModelAction *act = *rit;
1036 /* Don't disallow due to act == reader */
1037 if (!reader->happens_before(act) || reader == act)
1039 else if (act->is_write())
1040 write_after_read = act;
1041 else if (act->is_read() && act->get_reads_from() != NULL)
1042 write_after_read = act->get_reads_from();
1045 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1052 * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1053 * The ModelAction under consideration is expected to be taking part in
1054 * release/acquire synchronization as an object of the "reads from" relation.
1055 * Note that this can only provide release sequence support for RMW chains
1056 * which do not read from the future, as those actions cannot be traced until
1057 * their "promise" is fulfilled. Similarly, we may not even establish the
1058 * presence of a release sequence with certainty, as some modification order
1059 * constraints may be decided further in the future. Thus, this function
1060 * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1061 * and a boolean representing certainty.
1063 * @param rf The action that might be part of a release sequence. Must be a
1065 * @param release_heads A pass-by-reference style return parameter. After
1066 * execution of this function, release_heads will contain the heads of all the
1067 * relevant release sequences, if any exists with certainty
1068 * @return true, if the ModelExecution is certain that release_heads is complete;
1071 bool ModelExecution::release_seq_heads(const ModelAction *rf,
1072 rel_heads_list_t *release_heads) const
1074 /* Only check for release sequences if there are no cycles */
1075 if (mo_graph->checkForCycles())
1078 for ( ; rf != NULL; rf = rf->get_reads_from()) {
1079 ASSERT(rf->is_write());
1081 if (rf->is_release())
1082 release_heads->push_back(rf);
1083 else if (rf->get_last_fence_release())
1084 release_heads->push_back(rf->get_last_fence_release());
1086 break; /* End of RMW chain */
1088 /** @todo Need to be smarter here... In the linux lock
1089 * example, this will run to the beginning of the program for
1091 /** @todo The way to be smarter here is to keep going until 1
1092 * thread has a release preceded by an acquire and you've seen
1095 /* acq_rel RMW is a sufficient stopping condition */
1096 if (rf->is_acquire() && rf->is_release())
1097 return true; /* complete */
1099 ASSERT(rf); // Needs to be real write
1101 if (rf->is_release())
1102 return true; /* complete */
1104 /* else relaxed write
1105 * - check for fence-release in the same thread (29.8, stmt. 3)
1106 * - check modification order for contiguous subsequence
1107 * -> rf must be same thread as release */
1109 const ModelAction *fence_release = rf->get_last_fence_release();
1110 /* Synchronize with a fence-release unconditionally; we don't need to
1111 * find any more "contiguous subsequence..." for it */
1113 release_heads->push_back(fence_release);
1115 return true; /* complete */
1119 * An interface for getting the release sequence head(s) with which a
1120 * given ModelAction must synchronize. This function only returns a non-empty
1121 * result when it can locate a release sequence head with certainty. Otherwise,
1122 * it may mark the internal state of the ModelExecution so that it will handle
1123 * the release sequence at a later time, causing @a acquire to update its
1124 * synchronization at some later point in execution.
1126 * @param acquire The 'acquire' action that may synchronize with a release
1128 * @param read The read action that may read from a release sequence; this may
1129 * be the same as acquire, or else an earlier action in the same thread (i.e.,
1130 * when 'acquire' is a fence-acquire)
1131 * @param release_heads A pass-by-reference return parameter. Will be filled
1132 * with the head(s) of the release sequence(s), if they exists with certainty.
1133 * @see ModelExecution::release_seq_heads
1135 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
1136 ModelAction *read, rel_heads_list_t *release_heads)
1138 const ModelAction *rf = read->get_reads_from();
1140 release_seq_heads(rf, release_heads);
1144 * Performs various bookkeeping operations for the current ModelAction. For
1145 * instance, adds action to the per-object, per-thread action vector and to the
1146 * action trace list of all thread actions.
1148 * @param act is the ModelAction to add.
1150 void ModelExecution::add_action_to_lists(ModelAction *act)
1152 int tid = id_to_int(act->get_tid());
1153 ModelAction *uninit = NULL;
1155 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1156 if (list->empty() && act->is_atomic_var()) {
1157 uninit = get_uninitialized_action(act);
1158 uninit_id = id_to_int(uninit->get_tid());
1159 list->push_front(uninit);
1161 list->push_back(act);
1163 action_trace.push_back(act);
1165 action_trace.push_front(uninit);
1167 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1168 if (tid >= (int)vec->size())
1169 vec->resize(priv->next_thread_id);
1170 (*vec)[tid].push_back(act);
1172 (*vec)[uninit_id].push_front(uninit);
1174 if ((int)thrd_last_action.size() <= tid)
1175 thrd_last_action.resize(get_num_threads());
1176 thrd_last_action[tid] = act;
1178 thrd_last_action[uninit_id] = uninit;
1180 if (act->is_fence() && act->is_release()) {
1181 if ((int)thrd_last_fence_release.size() <= tid)
1182 thrd_last_fence_release.resize(get_num_threads());
1183 thrd_last_fence_release[tid] = act;
1186 if (act->is_wait()) {
1187 void *mutex_loc = (void *) act->get_value();
1188 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1190 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1191 if (tid >= (int)vec->size())
1192 vec->resize(priv->next_thread_id);
1193 (*vec)[tid].push_back(act);
1198 * @brief Get the last action performed by a particular Thread
1199 * @param tid The thread ID of the Thread in question
1200 * @return The last action in the thread
1202 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1204 int threadid = id_to_int(tid);
1205 if (threadid < (int)thrd_last_action.size())
1206 return thrd_last_action[id_to_int(tid)];
1212 * @brief Get the last fence release performed by a particular Thread
1213 * @param tid The thread ID of the Thread in question
1214 * @return The last fence release in the thread, if one exists; NULL otherwise
1216 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1218 int threadid = id_to_int(tid);
1219 if (threadid < (int)thrd_last_fence_release.size())
1220 return thrd_last_fence_release[id_to_int(tid)];
1226 * Gets the last memory_order_seq_cst write (in the total global sequence)
1227 * performed on a particular object (i.e., memory location), not including the
1229 * @param curr The current ModelAction; also denotes the object location to
1231 * @return The last seq_cst write
1233 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1235 void *location = curr->get_location();
1236 action_list_t *list = obj_map.get(location);
1237 /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1238 action_list_t::reverse_iterator rit;
1239 for (rit = list->rbegin(); (*rit) != curr; rit++)
1241 rit++; /* Skip past curr */
1242 for ( ; rit != list->rend(); rit++)
1243 if ((*rit)->is_write() && (*rit)->is_seqcst())
1249 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1250 * performed in a particular thread, prior to a particular fence.
1251 * @param tid The ID of the thread to check
1252 * @param before_fence The fence from which to begin the search; if NULL, then
1253 * search for the most recent fence in the thread.
1254 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1256 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1258 /* All fences should have location FENCE_LOCATION */
1259 action_list_t *list = obj_map.get(FENCE_LOCATION);
1264 action_list_t::reverse_iterator rit = list->rbegin();
1267 for (; rit != list->rend(); rit++)
1268 if (*rit == before_fence)
1271 ASSERT(*rit == before_fence);
1275 for (; rit != list->rend(); rit++)
1276 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1282 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1283 * location). This function identifies the mutex according to the current
1284 * action, which is presumed to perform on the same mutex.
1285 * @param curr The current ModelAction; also denotes the object location to
1287 * @return The last unlock operation
1289 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1291 void *location = curr->get_location();
1293 action_list_t *list = obj_map.get(location);
1294 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1295 action_list_t::reverse_iterator rit;
1296 for (rit = list->rbegin(); rit != list->rend(); rit++)
1297 if ((*rit)->is_unlock() || (*rit)->is_wait())
1302 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1304 ModelAction *parent = get_last_action(tid);
1306 parent = get_thread(tid)->get_creation();
1311 * Returns the clock vector for a given thread.
1312 * @param tid The thread whose clock vector we want
1313 * @return Desired clock vector
1315 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1317 return get_parent_action(tid)->get_cv();
1321 * Build up an initial set of all past writes that this 'read' action may read
1322 * from, as well as any previously-observed future values that must still be valid.
1324 * @param curr is the current ModelAction that we are exploring; it must be a
1327 ModelVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1329 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1331 ASSERT(curr->is_read());
1333 ModelAction *last_sc_write = NULL;
1335 if (curr->is_seqcst())
1336 last_sc_write = get_last_seq_cst_write(curr);
1338 ModelVector<ModelAction *> * rf_set = new ModelVector<ModelAction *>();
1340 /* Iterate over all threads */
1341 for (i = 0; i < thrd_lists->size(); i++) {
1342 /* Iterate over actions in thread, starting from most recent */
1343 action_list_t *list = &(*thrd_lists)[i];
1344 action_list_t::reverse_iterator rit;
1345 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1346 ModelAction *act = *rit;
1348 /* Only consider 'write' actions */
1349 if (!act->is_write() || act == curr)
1352 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1353 bool allow_read = true;
1355 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1359 /* Only add feasible reads */
1360 mo_graph->startChanges();
1361 r_modification_order(curr, act);
1362 if (!is_infeasible())
1363 rf_set->push_back(act);
1364 mo_graph->rollbackChanges();
1367 /* Include at most one act per-thread that "happens before" curr */
1368 if (act->happens_before(curr))
1373 if (DBG_ENABLED()) {
1374 model_print("Reached read action:\n");
1376 model_print("End printing read_from_past\n");
1382 * @brief Get an action representing an uninitialized atomic
1384 * This function may create a new one or try to retrieve one from the NodeStack
1386 * @param curr The current action, which prompts the creation of an UNINIT action
1387 * @return A pointer to the UNINIT ModelAction
1389 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1391 Node *node = curr->get_node();
1392 ModelAction *act = node->get_uninit_action();
1394 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1395 node->set_uninit_action(act);
1397 act->create_cv(NULL);
1401 static void print_list(const action_list_t *list)
1403 action_list_t::const_iterator it;
1405 model_print("------------------------------------------------------------------------------------\n");
1406 model_print("# t Action type MO Location Value Rf CV\n");
1407 model_print("------------------------------------------------------------------------------------\n");
1409 unsigned int hash = 0;
1411 for (it = list->begin(); it != list->end(); it++) {
1412 const ModelAction *act = *it;
1413 if (act->get_seq_number() > 0)
1415 hash = hash^(hash<<3)^((*it)->hash());
1417 model_print("HASH %u\n", hash);
1418 model_print("------------------------------------------------------------------------------------\n");
1421 #if SUPPORT_MOD_ORDER_DUMP
1422 void ModelExecution::dumpGraph(char *filename) const
1425 sprintf(buffer, "%s.dot", filename);
1426 FILE *file = fopen(buffer, "w");
1427 fprintf(file, "digraph %s {\n", filename);
1428 mo_graph->dumpNodes(file);
1429 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1431 for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) {
1432 ModelAction *act = *it;
1433 if (act->is_read()) {
1434 mo_graph->dot_print_node(file, act);
1435 mo_graph->dot_print_edge(file,
1436 act->get_reads_from(),
1438 "label=\"rf\", color=red, weight=2");
1440 if (thread_array[act->get_tid()]) {
1441 mo_graph->dot_print_edge(file,
1442 thread_array[id_to_int(act->get_tid())],
1444 "label=\"sb\", color=blue, weight=400");
1447 thread_array[act->get_tid()] = act;
1449 fprintf(file, "}\n");
1450 model_free(thread_array);
1455 /** @brief Prints an execution trace summary. */
1456 void ModelExecution::print_summary() const
1458 #if SUPPORT_MOD_ORDER_DUMP
1459 char buffername[100];
1460 sprintf(buffername, "exec%04u", get_execution_number());
1461 mo_graph->dumpGraphToFile(buffername);
1462 sprintf(buffername, "graph%04u", get_execution_number());
1463 dumpGraph(buffername);
1466 model_print("Execution trace %d:", get_execution_number());
1467 if (isfeasibleprefix()) {
1468 if (scheduler->all_threads_sleeping())
1469 model_print(" SLEEP-SET REDUNDANT");
1470 if (have_bug_reports())
1471 model_print(" DETECTED BUG(S)");
1473 print_infeasibility(" INFEASIBLE");
1476 print_list(&action_trace);
1482 * Add a Thread to the system for the first time. Should only be called once
1484 * @param t The Thread to add
1486 void ModelExecution::add_thread(Thread *t)
1488 unsigned int i = id_to_int(t->get_id());
1489 if (i >= thread_map.size())
1490 thread_map.resize(i + 1);
1492 if (!t->is_model_thread())
1493 scheduler->add_thread(t);
1497 * @brief Get a Thread reference by its ID
1498 * @param tid The Thread's ID
1499 * @return A Thread reference
1501 Thread * ModelExecution::get_thread(thread_id_t tid) const
1503 unsigned int i = id_to_int(tid);
1504 if (i < thread_map.size())
1505 return thread_map[i];
1510 * @brief Get a reference to the Thread in which a ModelAction was executed
1511 * @param act The ModelAction
1512 * @return A Thread reference
1514 Thread * ModelExecution::get_thread(const ModelAction *act) const
1516 return get_thread(act->get_tid());
1520 * @brief Get a Thread reference by its pthread ID
1521 * @param index The pthread's ID
1522 * @return A Thread reference
1524 Thread * ModelExecution::get_pthread(pthread_t pid) {
1525 if (pid < pthread_counter + 1) return pthread_map[pid];
1530 * @brief Check if a Thread is currently enabled
1531 * @param t The Thread to check
1532 * @return True if the Thread is currently enabled
1534 bool ModelExecution::is_enabled(Thread *t) const
1536 return scheduler->is_enabled(t);
1540 * @brief Check if a Thread is currently enabled
1541 * @param tid The ID of the Thread to check
1542 * @return True if the Thread is currently enabled
1544 bool ModelExecution::is_enabled(thread_id_t tid) const
1546 return scheduler->is_enabled(tid);
1550 * @brief Select the next thread to execute based on the curren action
1552 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1553 * actions should be followed by the execution of their child thread. In either
1554 * case, the current action should determine the next thread schedule.
1556 * @param curr The current action
1557 * @return The next thread to run, if the current action will determine this
1558 * selection; otherwise NULL
1560 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1562 /* Do not split atomic RMW */
1563 if (curr->is_rmwr())
1564 return get_thread(curr);
1565 if (curr->is_write()) {
1566 std::memory_order order = curr->get_mo();
1568 case std::memory_order_relaxed:
1569 return get_thread(curr);
1570 case std::memory_order_release:
1571 return get_thread(curr);
1577 /* Follow CREATE with the created thread */
1578 /* which is not needed, because model.cc takes care of this */
1579 if (curr->get_type() == THREAD_CREATE)
1580 return curr->get_thread_operand();
1581 if (curr->get_type() == PTHREAD_CREATE) {
1582 return curr->get_thread_operand();
1588 * Takes the next step in the execution, if possible.
1589 * @param curr The current step to take
1590 * @return Returns the next Thread to run, if any; NULL if this execution
1593 Thread * ModelExecution::take_step(ModelAction *curr)
1595 Thread *curr_thrd = get_thread(curr);
1596 ASSERT(curr_thrd->get_state() == THREAD_READY);
1598 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1599 curr = check_current_action(curr);
1602 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1603 scheduler->remove_thread(curr_thrd);
1605 return action_select_next_thread(curr);