11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #include "bugmessage.h"
18 #include "newfuzzer.h"
20 #define INITIAL_THREAD_ID 0
23 * Structure for holding small ModelChecker members that should be snapshotted
25 struct model_snapshot_members {
26 model_snapshot_members() :
27 /* First thread created will have id INITIAL_THREAD_ID */
28 next_thread_id(INITIAL_THREAD_ID),
29 used_sequence_numbers(0),
31 bad_synchronization(false),
35 ~model_snapshot_members() {
36 for (unsigned int i = 0;i < bugs.size();i++)
41 unsigned int next_thread_id;
42 modelclock_t used_sequence_numbers;
43 SnapVector<bug_message *> bugs;
44 /** @brief Incorrectly-ordered synchronization was made */
45 bool bad_synchronization;
51 /** @brief Constructor */
52 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
57 thread_map(2), /* We'll always need at least 2 threads */
61 condvar_waiters_map(),
65 thrd_last_fence_release(),
66 priv(new struct model_snapshot_members ()),
67 mo_graph(new CycleGraph()),
68 fuzzer(new NewFuzzer()),
70 thrd_func_act_lists(),
73 /* Initialize a model-checker thread, for special ModelActions */
74 model_thread = new Thread(get_next_id());
75 add_thread(model_thread);
76 scheduler->register_engine(this);
77 fuzzer->register_engine(m->get_history(), this);
80 /** @brief Destructor */
81 ModelExecution::~ModelExecution()
83 for (unsigned int i = 0;i < get_num_threads();i++)
84 delete get_thread(int_to_id(i));
90 int ModelExecution::get_execution_number() const
92 return model->get_execution_number();
95 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
97 action_list_t *tmp = hash->get(ptr);
99 tmp = new action_list_t();
105 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
107 SnapVector<action_list_t> *tmp = hash->get(ptr);
109 tmp = new SnapVector<action_list_t>();
115 /** @return a thread ID for a new Thread */
116 thread_id_t ModelExecution::get_next_id()
118 return priv->next_thread_id++;
121 /** @return the number of user threads created during this execution */
122 unsigned int ModelExecution::get_num_threads() const
124 return priv->next_thread_id;
127 /** @return a sequence number for a new ModelAction */
128 modelclock_t ModelExecution::get_next_seq_num()
130 return ++priv->used_sequence_numbers;
134 * @brief Should the current action wake up a given thread?
136 * @param curr The current action
137 * @param thread The thread that we might wake up
138 * @return True, if we should wake up the sleeping thread; false otherwise
140 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
142 const ModelAction *asleep = thread->get_pending();
143 /* Don't allow partial RMW to wake anyone up */
146 /* Synchronizing actions may have been backtracked */
147 if (asleep->could_synchronize_with(curr))
149 /* All acquire/release fences and fence-acquire/store-release */
150 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
152 /* Fence-release + store can awake load-acquire on the same location */
153 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
154 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
155 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
158 if (asleep->is_sleep()) {
159 if (fuzzer->shouldWake(asleep))
166 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
168 for (unsigned int i = 0;i < get_num_threads();i++) {
169 Thread *thr = get_thread(int_to_id(i));
170 if (scheduler->is_sleep_set(thr)) {
171 if (should_wake_up(curr, thr))
172 /* Remove this thread from sleep set */
173 scheduler->remove_sleep(thr);
178 /** @brief Alert the model-checker that an incorrectly-ordered
179 * synchronization was made */
180 void ModelExecution::set_bad_synchronization()
182 priv->bad_synchronization = true;
185 bool ModelExecution::assert_bug(const char *msg)
187 priv->bugs.push_back(new bug_message(msg));
189 if (isfeasibleprefix()) {
196 /** @return True, if any bugs have been reported for this execution */
197 bool ModelExecution::have_bug_reports() const
199 return priv->bugs.size() != 0;
202 /** @return True, if any fatal bugs have been reported for this execution.
203 * Any bug other than a data race is considered a fatal bug. Data races
204 * are not considered fatal unless the number of races is exceeds
205 * a threshold (temporarily set as 15).
207 bool ModelExecution::have_fatal_bug_reports() const
209 return priv->bugs.size() != 0;
212 SnapVector<bug_message *> * ModelExecution::get_bugs() const
218 * Check whether the current trace has triggered an assertion which should halt
221 * @return True, if the execution should be aborted; false otherwise
223 bool ModelExecution::has_asserted() const
225 return priv->asserted;
229 * Trigger a trace assertion which should cause this execution to be halted.
230 * This can be due to a detected bug or due to an infeasibility that should
233 void ModelExecution::set_assert()
235 priv->asserted = true;
239 * Check if we are in a deadlock. Should only be called at the end of an
240 * execution, although it should not give false positives in the middle of an
241 * execution (there should be some ENABLED thread).
243 * @return True if program is in a deadlock; false otherwise
245 bool ModelExecution::is_deadlocked() const
247 bool blocking_threads = false;
248 for (unsigned int i = 0;i < get_num_threads();i++) {
249 thread_id_t tid = int_to_id(i);
252 Thread *t = get_thread(tid);
253 if (!t->is_model_thread() && t->get_pending())
254 blocking_threads = true;
256 return blocking_threads;
260 * Check if this is a complete execution. That is, have all thread completed
261 * execution (rather than exiting because sleep sets have forced a redundant
264 * @return True if the execution is complete.
266 bool ModelExecution::is_complete_execution() const
268 for (unsigned int i = 0;i < get_num_threads();i++)
269 if (is_enabled(int_to_id(i)))
274 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
275 uint64_t value = *((const uint64_t *) location);
276 modelclock_t storeclock;
277 thread_id_t storethread;
278 getStoreThreadAndClock(location, &storethread, &storeclock);
279 setAtomicStoreFlag(location);
280 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
281 act->set_seq_number(storeclock);
282 add_normal_write_to_lists(act);
283 add_write_to_lists(act);
284 w_modification_order(act);
285 model->get_history()->process_action(act, act->get_tid());
290 * Processes a read model action.
291 * @param curr is the read model action to process.
292 * @param rf_set is the set of model actions we can possibly read from
293 * @return True if processing this read updates the mo_graph.
295 void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
297 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
298 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
299 if (hasnonatomicstore) {
300 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
301 rf_set->push_back(nonatomicstore);
305 int index = fuzzer->selectWrite(curr, rf_set);
306 ModelAction *rf = (*rf_set)[index];
309 bool canprune = false;
310 if (r_modification_order(curr, rf, priorset, &canprune)) {
311 for(unsigned int i=0;i<priorset->size();i++) {
312 mo_graph->addEdge((*priorset)[i], rf);
315 get_thread(curr)->set_return_value(curr->get_return_value());
317 if (canprune && curr->get_type() == ATOMIC_READ) {
318 int tid = id_to_int(curr->get_tid());
319 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
324 (*rf_set)[index] = rf_set->back();
330 * Processes a lock, trylock, or unlock model action. @param curr is
331 * the read model action to process.
333 * The try lock operation checks whether the lock is taken. If not,
334 * it falls to the normal lock operation case. If so, it returns
337 * The lock operation has already been checked that it is enabled, so
338 * it just grabs the lock and synchronizes with the previous unlock.
340 * The unlock operation has to re-enable all of the threads that are
341 * waiting on the lock.
343 * @return True if synchronization was updated; false otherwise
345 bool ModelExecution::process_mutex(ModelAction *curr)
347 cdsc::mutex *mutex = curr->get_mutex();
348 struct cdsc::mutex_state *state = NULL;
351 state = mutex->get_state();
353 switch (curr->get_type()) {
354 case ATOMIC_TRYLOCK: {
355 bool success = !state->locked;
356 curr->set_try_lock(success);
358 get_thread(curr)->set_return_value(0);
361 get_thread(curr)->set_return_value(1);
363 //otherwise fall into the lock case
365 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
366 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
367 // assert_bug("Lock access before initialization");
368 state->locked = get_thread(curr);
369 ModelAction *unlock = get_last_unlock(curr);
370 //synchronize with the previous unlock statement
371 if (unlock != NULL) {
372 synchronize(unlock, curr);
378 case ATOMIC_UNLOCK: {
379 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
381 /* wake up the other threads */
382 for (unsigned int i = 0;i < get_num_threads();i++) {
383 Thread *t = get_thread(int_to_id(i));
384 Thread *curr_thrd = get_thread(curr);
385 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
389 /* unlock the lock - after checking who was waiting on it */
390 state->locked = NULL;
392 if (!curr->is_wait())
393 break;/* The rest is only for ATOMIC_WAIT */
397 case ATOMIC_NOTIFY_ALL: {
398 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
399 //activate all the waiting threads
400 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
401 scheduler->wake(get_thread(rit->getVal()));
406 case ATOMIC_NOTIFY_ONE: {
407 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
408 if (waiters->size() != 0) {
409 Thread * thread = fuzzer->selectNotify(waiters);
410 scheduler->wake(thread);
422 * Process a write ModelAction
423 * @param curr The ModelAction to process
424 * @return True if the mo_graph was updated or promises were resolved
426 void ModelExecution::process_write(ModelAction *curr)
428 w_modification_order(curr);
429 get_thread(curr)->set_return_value(VALUE_NONE);
433 * Process a fence ModelAction
434 * @param curr The ModelAction to process
435 * @return True if synchronization was updated
437 bool ModelExecution::process_fence(ModelAction *curr)
440 * fence-relaxed: no-op
441 * fence-release: only log the occurence (not in this function), for
442 * use in later synchronization
443 * fence-acquire (this function): search for hypothetical release
445 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
447 bool updated = false;
448 if (curr->is_acquire()) {
449 action_list_t *list = &action_trace;
450 sllnode<ModelAction *> * rit;
451 /* Find X : is_read(X) && X --sb-> curr */
452 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
453 ModelAction *act = rit->getVal();
456 if (act->get_tid() != curr->get_tid())
458 /* Stop at the beginning of the thread */
459 if (act->is_thread_start())
461 /* Stop once we reach a prior fence-acquire */
462 if (act->is_fence() && act->is_acquire())
466 /* read-acquire will find its own release sequences */
467 if (act->is_acquire())
470 /* Establish hypothetical release sequences */
471 ClockVector *cv = get_hb_from_write(act->get_reads_from());
472 if (cv != NULL && curr->get_cv()->merge(cv))
480 * @brief Process the current action for thread-related activity
482 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
483 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
484 * synchronization, etc. This function is a no-op for non-THREAD actions
485 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
487 * @param curr The current action
488 * @return True if synchronization was updated or a thread completed
490 void ModelExecution::process_thread_action(ModelAction *curr)
492 switch (curr->get_type()) {
493 case THREAD_CREATE: {
494 thrd_t *thrd = (thrd_t *)curr->get_location();
495 struct thread_params *params = (struct thread_params *)curr->get_value();
496 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
497 curr->set_thread_operand(th);
499 th->set_creation(curr);
502 case PTHREAD_CREATE: {
503 (*(uint32_t *)curr->get_location()) = pthread_counter++;
505 struct pthread_params *params = (struct pthread_params *)curr->get_value();
506 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
507 curr->set_thread_operand(th);
509 th->set_creation(curr);
511 if ( pthread_map.size() < pthread_counter )
512 pthread_map.resize( pthread_counter );
513 pthread_map[ pthread_counter-1 ] = th;
518 Thread *blocking = curr->get_thread_operand();
519 ModelAction *act = get_last_action(blocking->get_id());
520 synchronize(act, curr);
524 Thread *blocking = curr->get_thread_operand();
525 ModelAction *act = get_last_action(blocking->get_id());
526 synchronize(act, curr);
527 break; // WL: to be add (modified)
530 case THREADONLY_FINISH:
531 case THREAD_FINISH: {
532 Thread *th = get_thread(curr);
533 if (curr->get_type() == THREAD_FINISH &&
534 th == model->getInitThread()) {
540 /* Wake up any joining threads */
541 for (unsigned int i = 0;i < get_num_threads();i++) {
542 Thread *waiting = get_thread(int_to_id(i));
543 if (waiting->waiting_on() == th &&
544 waiting->get_pending()->is_thread_join())
545 scheduler->wake(waiting);
559 * Initialize the current action by performing one or more of the following
560 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
561 * manipulating backtracking sets, allocating and
562 * initializing clock vectors, and computing the promises to fulfill.
564 * @param curr The current action, as passed from the user context; may be
565 * freed/invalidated after the execution of this function, with a different
566 * action "returned" its place (pass-by-reference)
567 * @return True if curr is a newly-explored action; false otherwise
569 bool ModelExecution::initialize_curr_action(ModelAction **curr)
571 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
572 ModelAction *newcurr = process_rmw(*curr);
578 ModelAction *newcurr = *curr;
580 newcurr->set_seq_number(get_next_seq_num());
581 /* Always compute new clock vector */
582 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
584 /* Assign most recent release fence */
585 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
587 return true; /* This was a new ModelAction */
592 * @brief Establish reads-from relation between two actions
594 * Perform basic operations involved with establishing a concrete rf relation,
595 * including setting the ModelAction data and checking for release sequences.
597 * @param act The action that is reading (must be a read)
598 * @param rf The action from which we are reading (must be a write)
600 * @return True if this read established synchronization
603 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
606 ASSERT(rf->is_write());
608 act->set_read_from(rf);
609 if (act->is_acquire()) {
610 ClockVector *cv = get_hb_from_write(rf);
613 act->get_cv()->merge(cv);
618 * @brief Synchronizes two actions
620 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
621 * This function performs the synchronization as well as providing other hooks
622 * for other checks along with synchronization.
624 * @param first The left-hand side of the synchronizes-with relation
625 * @param second The right-hand side of the synchronizes-with relation
626 * @return True if the synchronization was successful (i.e., was consistent
627 * with the execution order); false otherwise
629 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
631 if (*second < *first) {
632 set_bad_synchronization();
635 return second->synchronize_with(first);
639 * @brief Check whether a model action is enabled.
641 * Checks whether an operation would be successful (i.e., is a lock already
642 * locked, or is the joined thread already complete).
644 * For yield-blocking, yields are never enabled.
646 * @param curr is the ModelAction to check whether it is enabled.
647 * @return a bool that indicates whether the action is enabled.
649 bool ModelExecution::check_action_enabled(ModelAction *curr) {
650 if (curr->is_lock()) {
651 cdsc::mutex *lock = curr->get_mutex();
652 struct cdsc::mutex_state *state = lock->get_state();
655 } else if (curr->is_thread_join()) {
656 Thread *blocking = curr->get_thread_operand();
657 if (!blocking->is_complete()) {
660 } else if (curr->is_sleep()) {
661 if (!fuzzer->shouldSleep(curr))
669 * This is the heart of the model checker routine. It performs model-checking
670 * actions corresponding to a given "current action." Among other processes, it
671 * calculates reads-from relationships, updates synchronization clock vectors,
672 * forms a memory_order constraints graph, and handles replay/backtrack
673 * execution when running permutations of previously-observed executions.
675 * @param curr The current action to process
676 * @return The ModelAction that is actually executed; may be different than
679 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
682 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
683 bool newly_explored = initialize_curr_action(&curr);
687 wake_up_sleeping_actions(curr);
689 /* Add the action to lists before any other model-checking tasks */
690 if (!second_part_of_rmw && curr->get_type() != NOOP)
691 add_action_to_lists(curr);
693 if (curr->is_write())
694 add_write_to_lists(curr);
696 SnapVector<ModelAction *> * rf_set = NULL;
697 /* Build may_read_from set for newly-created actions */
698 if (newly_explored && curr->is_read())
699 rf_set = build_may_read_from(curr);
701 process_thread_action(curr);
703 if (curr->is_read() && !second_part_of_rmw) {
704 process_read(curr, rf_set);
707 ASSERT(rf_set == NULL);
710 if (curr->is_write())
713 if (curr->is_fence())
716 if (curr->is_mutex_op())
723 * This is the strongest feasibility check available.
724 * @return whether the current trace (partial or complete) must be a prefix of
727 bool ModelExecution::isfeasibleprefix() const
729 return !is_infeasible();
733 * Print disagnostic information about an infeasible execution
734 * @param prefix A string to prefix the output with; if NULL, then a default
735 * message prefix will be provided
737 void ModelExecution::print_infeasibility(const char *prefix) const
741 if (priv->bad_synchronization)
742 ptr += sprintf(ptr, "[bad sw ordering]");
744 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
748 * Check if the current partial trace is infeasible. Does not check any
749 * end-of-execution flags, which might rule out the execution. Thus, this is
750 * useful only for ruling an execution as infeasible.
751 * @return whether the current partial trace is infeasible.
753 bool ModelExecution::is_infeasible() const
755 return priv->bad_synchronization;
758 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
759 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
760 ModelAction *lastread = get_last_action(act->get_tid());
761 lastread->process_rmw(act);
763 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
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
785 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
787 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
789 ASSERT(curr->is_read());
791 /* Last SC fence in the current thread */
792 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
794 int tid = curr->get_tid();
795 ModelAction *prev_same_thread = NULL;
796 /* Iterate over all threads */
797 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
798 /* Last SC fence in thread tid */
799 ModelAction *last_sc_fence_thread_local = NULL;
801 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
803 /* Last SC fence in thread tid, before last SC fence in current thread */
804 ModelAction *last_sc_fence_thread_before = NULL;
805 if (last_sc_fence_local)
806 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
808 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
809 if (prev_same_thread != NULL &&
810 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
811 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
815 /* Iterate over actions in thread, starting from most recent */
816 action_list_t *list = &(*thrd_lists)[tid];
817 sllnode<ModelAction *> * rit;
818 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
819 ModelAction *act = rit->getVal();
824 /* Don't want to add reflexive edges on 'rf' */
825 if (act->equals(rf)) {
826 if (act->happens_before(curr))
832 if (act->is_write()) {
833 /* C++, Section 29.3 statement 5 */
834 if (curr->is_seqcst() && last_sc_fence_thread_local &&
835 *act < *last_sc_fence_thread_local) {
836 if (mo_graph->checkReachable(rf, act))
838 priorset->push_back(act);
841 /* C++, Section 29.3 statement 4 */
842 else if (act->is_seqcst() && last_sc_fence_local &&
843 *act < *last_sc_fence_local) {
844 if (mo_graph->checkReachable(rf, act))
846 priorset->push_back(act);
849 /* C++, Section 29.3 statement 6 */
850 else if (last_sc_fence_thread_before &&
851 *act < *last_sc_fence_thread_before) {
852 if (mo_graph->checkReachable(rf, act))
854 priorset->push_back(act);
860 * Include at most one act per-thread that "happens
863 if (act->happens_before(curr)) {
865 if (last_sc_fence_local == NULL ||
866 (*last_sc_fence_local < *act)) {
867 prev_same_thread = act;
870 if (act->is_write()) {
871 if (mo_graph->checkReachable(rf, act))
873 priorset->push_back(act);
875 const ModelAction *prevrf = act->get_reads_from();
876 if (!prevrf->equals(rf)) {
877 if (mo_graph->checkReachable(rf, prevrf))
879 priorset->push_back(prevrf);
881 if (act->get_tid() == curr->get_tid()) {
882 //Can prune curr from obj list
895 * Updates the mo_graph with the constraints imposed from the current write.
897 * Basic idea is the following: Go through each other thread and find
898 * the lastest action that happened before our write. Two cases:
900 * (1) The action is a write => that write must occur before
903 * (2) The action is a read => the write that that action read from
904 * must occur before the current write.
906 * This method also handles two other issues:
908 * (I) Sequential Consistency: Making sure that if the current write is
909 * seq_cst, that it occurs after the previous seq_cst write.
911 * (II) Sending the write back to non-synchronizing reads.
913 * @param curr The current action. Must be a write.
914 * @param send_fv A vector for stashing reads to which we may pass our future
915 * value. If NULL, then don't record any future values.
916 * @return True if modification order edges were added; false otherwise
918 void ModelExecution::w_modification_order(ModelAction *curr)
920 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
922 ASSERT(curr->is_write());
924 SnapList<ModelAction *> edgeset;
926 if (curr->is_seqcst()) {
927 /* We have to at least see the last sequentially consistent write,
928 so we are initialized. */
929 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
930 if (last_seq_cst != NULL) {
931 edgeset.push_back(last_seq_cst);
933 //update map for next query
934 obj_last_sc_map.put(curr->get_location(), curr);
937 /* Last SC fence in the current thread */
938 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
940 /* Iterate over all threads */
941 for (i = 0;i < thrd_lists->size();i++) {
942 /* Last SC fence in thread i, before last SC fence in current thread */
943 ModelAction *last_sc_fence_thread_before = NULL;
944 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
945 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
947 /* Iterate over actions in thread, starting from most recent */
948 action_list_t *list = &(*thrd_lists)[i];
949 sllnode<ModelAction*>* rit;
950 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
951 ModelAction *act = rit->getVal();
954 * 1) If RMW and it actually read from something, then we
955 * already have all relevant edges, so just skip to next
958 * 2) If RMW and it didn't read from anything, we should
959 * whatever edge we can get to speed up convergence.
961 * 3) If normal write, we need to look at earlier actions, so
962 * continue processing list.
964 if (curr->is_rmw()) {
965 if (curr->get_reads_from() != NULL)
973 /* C++, Section 29.3 statement 7 */
974 if (last_sc_fence_thread_before && act->is_write() &&
975 *act < *last_sc_fence_thread_before) {
976 edgeset.push_back(act);
981 * Include at most one act per-thread that "happens
984 if (act->happens_before(curr)) {
986 * Note: if act is RMW, just add edge:
988 * The following edge should be handled elsewhere:
989 * readfrom(act) --mo--> act
992 edgeset.push_back(act);
993 else if (act->is_read()) {
994 //if previous read accessed a null, just keep going
995 edgeset.push_back(act->get_reads_from());
1001 mo_graph->addEdges(&edgeset, curr);
1006 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1007 * some constraints. This method checks one the following constraint (others
1008 * require compiler support):
1010 * If X --hb-> Y --mo-> Z, then X should not read from Z.
1011 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1013 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1015 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1017 /* Iterate over all threads */
1018 for (i = 0;i < thrd_lists->size();i++) {
1019 const ModelAction *write_after_read = NULL;
1021 /* Iterate over actions in thread, starting from most recent */
1022 action_list_t *list = &(*thrd_lists)[i];
1023 sllnode<ModelAction *>* rit;
1024 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1025 ModelAction *act = rit->getVal();
1027 /* Don't disallow due to act == reader */
1028 if (!reader->happens_before(act) || reader == act)
1030 else if (act->is_write())
1031 write_after_read = act;
1032 else if (act->is_read() && act->get_reads_from() != NULL)
1033 write_after_read = act->get_reads_from();
1036 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1043 * Computes the clock vector that happens before propagates from this write.
1045 * @param rf The action that might be part of a release sequence. Must be a
1047 * @return ClockVector of happens before relation.
1050 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1051 SnapVector<ModelAction *> * processset = NULL;
1052 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1053 ASSERT(rf->is_write());
1054 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1056 if (processset == NULL)
1057 processset = new SnapVector<ModelAction *>();
1058 processset->push_back(rf);
1061 int i = (processset == NULL) ? 0 : processset->size();
1063 ClockVector * vec = NULL;
1065 if (rf->get_rfcv() != NULL) {
1066 vec = rf->get_rfcv();
1067 } else if (rf->is_acquire() && rf->is_release()) {
1069 } else if (rf->is_release() && !rf->is_rmw()) {
1071 } else if (rf->is_release()) {
1072 //have rmw that is release and doesn't have a rfcv
1073 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1076 //operation that isn't release
1077 if (rf->get_last_fence_release()) {
1079 vec = rf->get_last_fence_release()->get_cv();
1081 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1087 rf = (*processset)[i];
1091 if (processset != NULL)
1097 * Performs various bookkeeping operations for the current ModelAction. For
1098 * instance, adds action to the per-object, per-thread action vector and to the
1099 * action trace list of all thread actions.
1101 * @param act is the ModelAction to add.
1103 void ModelExecution::add_action_to_lists(ModelAction *act)
1105 int tid = id_to_int(act->get_tid());
1106 ModelAction *uninit = NULL;
1108 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1109 if (list->empty() && act->is_atomic_var()) {
1110 uninit = get_uninitialized_action(act);
1111 uninit_id = id_to_int(uninit->get_tid());
1112 list->push_front(uninit);
1113 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1114 if (uninit_id >= (int)vec->size()) {
1115 int oldsize = (int) vec->size();
1116 vec->resize(uninit_id + 1);
1117 for(int i=oldsize;i<uninit_id+1;i++) {
1118 new(&(*vec)[i]) action_list_t();
1121 (*vec)[uninit_id].push_front(uninit);
1123 list->push_back(act);
1125 // Update action trace, a total order of all actions
1126 action_trace.push_back(act);
1128 action_trace.push_front(uninit);
1130 // Update obj_thrd_map, a per location, per thread, order of actions
1131 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1132 if (tid >= (int)vec->size()) {
1133 uint oldsize =vec->size();
1134 vec->resize(priv->next_thread_id);
1135 for(uint i=oldsize;i<priv->next_thread_id;i++)
1136 new (&(*vec)[i]) action_list_t();
1138 (*vec)[tid].push_back(act);
1140 (*vec)[uninit_id].push_front(uninit);
1142 // Update thrd_last_action, the last action taken by each thrad
1143 if ((int)thrd_last_action.size() <= tid)
1144 thrd_last_action.resize(get_num_threads());
1145 thrd_last_action[tid] = act;
1147 thrd_last_action[uninit_id] = uninit;
1149 // Update thrd_last_fence_release, the last release fence taken by each thread
1150 if (act->is_fence() && act->is_release()) {
1151 if ((int)thrd_last_fence_release.size() <= tid)
1152 thrd_last_fence_release.resize(get_num_threads());
1153 thrd_last_fence_release[tid] = act;
1156 if (act->is_wait()) {
1157 void *mutex_loc = (void *) act->get_value();
1158 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1160 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1161 if (tid >= (int)vec->size()) {
1162 uint oldsize = vec->size();
1163 vec->resize(priv->next_thread_id);
1164 for(uint i=oldsize;i<priv->next_thread_id;i++)
1165 new (&(*vec)[i]) action_list_t();
1167 (*vec)[tid].push_back(act);
1171 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1172 sllnode<ModelAction*> * rit = list->end();
1173 modelclock_t next_seq = act->get_seq_number();
1174 if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1175 list->push_back(act);
1177 for(;rit != NULL;rit=rit->getPrev()) {
1178 if (rit->getVal()->get_seq_number() == next_seq) {
1179 list->insertAfter(rit, act);
1186 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1187 sllnode<ModelAction*> * rit = list->end();
1188 modelclock_t next_seq = act->get_seq_number();
1190 act->create_cv(NULL);
1191 } else if (rit->getVal()->get_seq_number() == next_seq) {
1192 act->create_cv(rit->getVal());
1193 list->push_back(act);
1195 for(;rit != NULL;rit=rit->getPrev()) {
1196 if (rit->getVal()->get_seq_number() == next_seq) {
1197 act->create_cv(rit->getVal());
1198 list->insertAfter(rit, act);
1206 * Performs various bookkeeping operations for a normal write. The
1207 * complication is that we are typically inserting a normal write
1208 * lazily, so we need to insert it into the middle of lists.
1210 * @param act is the ModelAction to add.
1213 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1215 int tid = id_to_int(act->get_tid());
1216 insertIntoActionListAndSetCV(&action_trace, act);
1218 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1219 insertIntoActionList(list, act);
1221 // Update obj_thrd_map, a per location, per thread, order of actions
1222 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1223 if (tid >= (int)vec->size()) {
1224 uint oldsize =vec->size();
1225 vec->resize(priv->next_thread_id);
1226 for(uint i=oldsize;i<priv->next_thread_id;i++)
1227 new (&(*vec)[i]) action_list_t();
1229 insertIntoActionList(&(*vec)[tid],act);
1231 // Update thrd_last_action, the last action taken by each thrad
1232 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1233 thrd_last_action[tid] = act;
1237 void ModelExecution::add_write_to_lists(ModelAction *write) {
1238 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1239 int tid = id_to_int(write->get_tid());
1240 if (tid >= (int)vec->size()) {
1241 uint oldsize =vec->size();
1242 vec->resize(priv->next_thread_id);
1243 for(uint i=oldsize;i<priv->next_thread_id;i++)
1244 new (&(*vec)[i]) action_list_t();
1246 (*vec)[tid].push_back(write);
1250 * @brief Get the last action performed by a particular Thread
1251 * @param tid The thread ID of the Thread in question
1252 * @return The last action in the thread
1254 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1256 int threadid = id_to_int(tid);
1257 if (threadid < (int)thrd_last_action.size())
1258 return thrd_last_action[id_to_int(tid)];
1264 * @brief Get the last fence release performed by a particular Thread
1265 * @param tid The thread ID of the Thread in question
1266 * @return The last fence release in the thread, if one exists; NULL otherwise
1268 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1270 int threadid = id_to_int(tid);
1271 if (threadid < (int)thrd_last_fence_release.size())
1272 return thrd_last_fence_release[id_to_int(tid)];
1278 * Gets the last memory_order_seq_cst write (in the total global sequence)
1279 * performed on a particular object (i.e., memory location), not including the
1281 * @param curr The current ModelAction; also denotes the object location to
1283 * @return The last seq_cst write
1285 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1287 void *location = curr->get_location();
1288 return obj_last_sc_map.get(location);
1292 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1293 * performed in a particular thread, prior to a particular fence.
1294 * @param tid The ID of the thread to check
1295 * @param before_fence The fence from which to begin the search; if NULL, then
1296 * search for the most recent fence in the thread.
1297 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1299 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1301 /* All fences should have location FENCE_LOCATION */
1302 action_list_t *list = obj_map.get(FENCE_LOCATION);
1307 sllnode<ModelAction*>* rit = list->end();
1310 for (;rit != NULL;rit=rit->getPrev())
1311 if (rit->getVal() == before_fence)
1314 ASSERT(rit->getVal() == before_fence);
1318 for (;rit != NULL;rit=rit->getPrev()) {
1319 ModelAction *act = rit->getVal();
1320 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1327 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1328 * location). This function identifies the mutex according to the current
1329 * action, which is presumed to perform on the same mutex.
1330 * @param curr The current ModelAction; also denotes the object location to
1332 * @return The last unlock operation
1334 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1336 void *location = curr->get_location();
1338 action_list_t *list = obj_map.get(location);
1339 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1340 sllnode<ModelAction*>* rit;
1341 for (rit = list->end();rit != NULL;rit=rit->getPrev())
1342 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1343 return rit->getVal();
1347 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1349 ModelAction *parent = get_last_action(tid);
1351 parent = get_thread(tid)->get_creation();
1356 * Returns the clock vector for a given thread.
1357 * @param tid The thread whose clock vector we want
1358 * @return Desired clock vector
1360 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1362 ModelAction *firstaction=get_parent_action(tid);
1363 return firstaction != NULL ? firstaction->get_cv() : NULL;
1366 bool valequals(uint64_t val1, uint64_t val2, int size) {
1369 return ((uint8_t)val1) == ((uint8_t)val2);
1371 return ((uint16_t)val1) == ((uint16_t)val2);
1373 return ((uint32_t)val1) == ((uint32_t)val2);
1383 * Build up an initial set of all past writes that this 'read' action may read
1384 * from, as well as any previously-observed future values that must still be valid.
1386 * @param curr is the current ModelAction that we are exploring; it must be a
1389 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1391 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1393 ASSERT(curr->is_read());
1395 ModelAction *last_sc_write = NULL;
1397 if (curr->is_seqcst())
1398 last_sc_write = get_last_seq_cst_write(curr);
1400 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1402 /* Iterate over all threads */
1403 for (i = 0;i < thrd_lists->size();i++) {
1404 /* Iterate over actions in thread, starting from most recent */
1405 action_list_t *list = &(*thrd_lists)[i];
1406 sllnode<ModelAction *> * rit;
1407 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1408 ModelAction *act = rit->getVal();
1413 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1414 bool allow_read = true;
1416 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1419 /* Need to check whether we will have two RMW reading from the same value */
1420 if (curr->is_rmwr()) {
1421 /* It is okay if we have a failing CAS */
1422 if (!curr->is_rmwrcas() ||
1423 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1424 //Need to make sure we aren't the second RMW
1425 CycleNode * node = mo_graph->getNode_noCreate(act);
1426 if (node != NULL && node->getRMW() != NULL) {
1427 //we are the second RMW
1434 /* Only add feasible reads */
1435 rf_set->push_back(act);
1438 /* Include at most one act per-thread that "happens before" curr */
1439 if (act->happens_before(curr))
1444 if (DBG_ENABLED()) {
1445 model_print("Reached read action:\n");
1447 model_print("End printing read_from_past\n");
1453 * @brief Get an action representing an uninitialized atomic
1455 * This function may create a new one.
1457 * @param curr The current action, which prompts the creation of an UNINIT action
1458 * @return A pointer to the UNINIT ModelAction
1460 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1462 ModelAction *act = curr->get_uninit_action();
1464 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1465 curr->set_uninit_action(act);
1467 act->create_cv(NULL);
1471 static void print_list(action_list_t *list)
1473 sllnode<ModelAction*> *it;
1475 model_print("------------------------------------------------------------------------------------\n");
1476 model_print("# t Action type MO Location Value Rf CV\n");
1477 model_print("------------------------------------------------------------------------------------\n");
1479 unsigned int hash = 0;
1481 for (it = list->begin();it != NULL;it=it->getNext()) {
1482 const ModelAction *act = it->getVal();
1483 if (act->get_seq_number() > 0)
1485 hash = hash^(hash<<3)^(it->getVal()->hash());
1487 model_print("HASH %u\n", hash);
1488 model_print("------------------------------------------------------------------------------------\n");
1491 #if SUPPORT_MOD_ORDER_DUMP
1492 void ModelExecution::dumpGraph(char *filename)
1495 sprintf(buffer, "%s.dot", filename);
1496 FILE *file = fopen(buffer, "w");
1497 fprintf(file, "digraph %s {\n", filename);
1498 mo_graph->dumpNodes(file);
1499 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1501 for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1502 ModelAction *act = it->getVal();
1503 if (act->is_read()) {
1504 mo_graph->dot_print_node(file, act);
1505 mo_graph->dot_print_edge(file,
1506 act->get_reads_from(),
1508 "label=\"rf\", color=red, weight=2");
1510 if (thread_array[act->get_tid()]) {
1511 mo_graph->dot_print_edge(file,
1512 thread_array[id_to_int(act->get_tid())],
1514 "label=\"sb\", color=blue, weight=400");
1517 thread_array[act->get_tid()] = act;
1519 fprintf(file, "}\n");
1520 model_free(thread_array);
1525 /** @brief Prints an execution trace summary. */
1526 void ModelExecution::print_summary()
1528 #if SUPPORT_MOD_ORDER_DUMP
1529 char buffername[100];
1530 sprintf(buffername, "exec%04u", get_execution_number());
1531 mo_graph->dumpGraphToFile(buffername);
1532 sprintf(buffername, "graph%04u", get_execution_number());
1533 dumpGraph(buffername);
1536 model_print("Execution trace %d:", get_execution_number());
1537 if (isfeasibleprefix()) {
1538 if (scheduler->all_threads_sleeping())
1539 model_print(" SLEEP-SET REDUNDANT");
1540 if (have_bug_reports())
1541 model_print(" DETECTED BUG(S)");
1543 print_infeasibility(" INFEASIBLE");
1546 print_list(&action_trace);
1552 * Add a Thread to the system for the first time. Should only be called once
1554 * @param t The Thread to add
1556 void ModelExecution::add_thread(Thread *t)
1558 unsigned int i = id_to_int(t->get_id());
1559 if (i >= thread_map.size())
1560 thread_map.resize(i + 1);
1562 if (!t->is_model_thread())
1563 scheduler->add_thread(t);
1567 * @brief Get a Thread reference by its ID
1568 * @param tid The Thread's ID
1569 * @return A Thread reference
1571 Thread * ModelExecution::get_thread(thread_id_t tid) const
1573 unsigned int i = id_to_int(tid);
1574 if (i < thread_map.size())
1575 return thread_map[i];
1580 * @brief Get a reference to the Thread in which a ModelAction was executed
1581 * @param act The ModelAction
1582 * @return A Thread reference
1584 Thread * ModelExecution::get_thread(const ModelAction *act) const
1586 return get_thread(act->get_tid());
1590 * @brief Get a Thread reference by its pthread ID
1591 * @param index The pthread's ID
1592 * @return A Thread reference
1594 Thread * ModelExecution::get_pthread(pthread_t pid) {
1600 uint32_t thread_id = x.v;
1601 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1606 * @brief Check if a Thread is currently enabled
1607 * @param t The Thread to check
1608 * @return True if the Thread is currently enabled
1610 bool ModelExecution::is_enabled(Thread *t) const
1612 return scheduler->is_enabled(t);
1616 * @brief Check if a Thread is currently enabled
1617 * @param tid The ID of the Thread to check
1618 * @return True if the Thread is currently enabled
1620 bool ModelExecution::is_enabled(thread_id_t tid) const
1622 return scheduler->is_enabled(tid);
1626 * @brief Select the next thread to execute based on the curren action
1628 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1629 * actions should be followed by the execution of their child thread. In either
1630 * case, the current action should determine the next thread schedule.
1632 * @param curr The current action
1633 * @return The next thread to run, if the current action will determine this
1634 * selection; otherwise NULL
1636 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1638 /* Do not split atomic RMW */
1639 if (curr->is_rmwr())
1640 return get_thread(curr);
1641 /* Follow CREATE with the created thread */
1642 /* which is not needed, because model.cc takes care of this */
1643 if (curr->get_type() == THREAD_CREATE)
1644 return curr->get_thread_operand();
1645 if (curr->get_type() == PTHREAD_CREATE) {
1646 return curr->get_thread_operand();
1652 * Takes the next step in the execution, if possible.
1653 * @param curr The current step to take
1654 * @return Returns the next Thread to run, if any; NULL if this execution
1657 Thread * ModelExecution::take_step(ModelAction *curr)
1659 Thread *curr_thrd = get_thread(curr);
1660 ASSERT(curr_thrd->get_state() == THREAD_READY);
1662 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1663 curr = check_current_action(curr);
1666 /* Process this action in ModelHistory for records */
1667 model->get_history()->process_action( curr, curr->get_tid() );
1669 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1670 scheduler->remove_thread(curr_thrd);
1672 return action_select_next_thread(curr);
1675 Fuzzer * ModelExecution::getFuzzer() {