11 #include "clockvector.h"
12 #include "cyclegraph.h"
14 #include "threads-model.h"
15 #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) :
56 thread_map(2), /* We'll always need at least 2 threads */
60 condvar_waiters_map(),
64 thrd_last_fence_release(),
65 priv(new struct model_snapshot_members ()),
66 mo_graph(new CycleGraph()),
69 thrd_func_inst_lists()
71 /* Initialize a model-checker thread, for special ModelActions */
72 model_thread = new Thread(get_next_id());
73 add_thread(model_thread);
74 scheduler->register_engine(this);
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<const 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 /** @return a thread ID for a new Thread */
113 thread_id_t ModelExecution::get_next_id()
115 return priv->next_thread_id++;
118 /** @return the number of user threads created during this execution */
119 unsigned int ModelExecution::get_num_threads() const
121 return priv->next_thread_id;
124 /** @return a sequence number for a new ModelAction */
125 modelclock_t ModelExecution::get_next_seq_num()
127 return ++priv->used_sequence_numbers;
131 * @brief Should the current action wake up a given thread?
133 * @param curr The current action
134 * @param thread The thread that we might wake up
135 * @return True, if we should wake up the sleeping thread; false otherwise
137 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
139 const ModelAction *asleep = thread->get_pending();
140 /* Don't allow partial RMW to wake anyone up */
143 /* Synchronizing actions may have been backtracked */
144 if (asleep->could_synchronize_with(curr))
146 /* All acquire/release fences and fence-acquire/store-release */
147 if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
149 /* Fence-release + store can awake load-acquire on the same location */
150 if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
151 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
152 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
158 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
160 for (unsigned int i = 0;i < get_num_threads();i++) {
161 Thread *thr = get_thread(int_to_id(i));
162 if (scheduler->is_sleep_set(thr)) {
163 if (should_wake_up(curr, thr))
164 /* Remove this thread from sleep set */
165 scheduler->remove_sleep(thr);
170 /** @brief Alert the model-checker that an incorrectly-ordered
171 * synchronization was made */
172 void ModelExecution::set_bad_synchronization()
174 priv->bad_synchronization = true;
177 bool ModelExecution::assert_bug(const char *msg)
179 priv->bugs.push_back(new bug_message(msg));
181 if (isfeasibleprefix()) {
188 /** @return True, if any bugs have been reported for this execution */
189 bool ModelExecution::have_bug_reports() const
191 return priv->bugs.size() != 0;
194 /** @return True, if any fatal bugs have been reported for this execution.
195 * Any bug other than a data race is considered a fatal bug. Data races
196 * are not considered fatal unless the number of races is exceeds
197 * a threshold (temporarily set as 15).
199 bool ModelExecution::have_fatal_bug_reports() const
201 return priv->bugs.size() != 0;
204 SnapVector<bug_message *> * ModelExecution::get_bugs() const
210 * Check whether the current trace has triggered an assertion which should halt
213 * @return True, if the execution should be aborted; false otherwise
215 bool ModelExecution::has_asserted() const
217 return priv->asserted;
221 * Trigger a trace assertion which should cause this execution to be halted.
222 * This can be due to a detected bug or due to an infeasibility that should
225 void ModelExecution::set_assert()
227 priv->asserted = true;
231 * Check if we are in a deadlock. Should only be called at the end of an
232 * execution, although it should not give false positives in the middle of an
233 * execution (there should be some ENABLED thread).
235 * @return True if program is in a deadlock; false otherwise
237 bool ModelExecution::is_deadlocked() const
239 bool blocking_threads = false;
240 for (unsigned int i = 0;i < get_num_threads();i++) {
241 thread_id_t tid = int_to_id(i);
244 Thread *t = get_thread(tid);
245 if (!t->is_model_thread() && t->get_pending())
246 blocking_threads = true;
248 return blocking_threads;
252 * Check if this is a complete execution. That is, have all thread completed
253 * execution (rather than exiting because sleep sets have forced a redundant
256 * @return True if the execution is complete.
258 bool ModelExecution::is_complete_execution() const
260 for (unsigned int i = 0;i < get_num_threads();i++)
261 if (is_enabled(int_to_id(i)))
266 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
267 uint64_t value = *((const uint64_t *) location);
268 modelclock_t storeclock;
269 thread_id_t storethread;
270 getStoreThreadAndClock(location, &storethread, &storeclock);
271 setAtomicStoreFlag(location);
272 ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
273 act->set_seq_number(storeclock);
274 add_normal_write_to_lists(act);
275 add_write_to_lists(act);
276 w_modification_order(act);
281 * Processes a read model action.
282 * @param curr is the read model action to process.
283 * @param rf_set is the set of model actions we can possibly read from
284 * @return True if processing this read updates the mo_graph.
286 void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
288 SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
289 bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
290 if (hasnonatomicstore) {
291 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
292 rf_set->push_back(nonatomicstore);
296 int index = fuzzer->selectWrite(curr, rf_set);
297 ModelAction *rf = (*rf_set)[index];
301 bool canprune = false;
302 if (r_modification_order(curr, rf, priorset, &canprune)) {
303 for(unsigned int i=0;i<priorset->size();i++) {
304 mo_graph->addEdge((*priorset)[i], rf);
307 get_thread(curr)->set_return_value(curr->get_return_value());
309 if (canprune && curr->get_type() == ATOMIC_READ) {
310 int tid = id_to_int(curr->get_tid());
311 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
316 (*rf_set)[index] = rf_set->back();
322 * Processes a lock, trylock, or unlock model action. @param curr is
323 * the read model action to process.
325 * The try lock operation checks whether the lock is taken. If not,
326 * it falls to the normal lock operation case. If so, it returns
329 * The lock operation has already been checked that it is enabled, so
330 * it just grabs the lock and synchronizes with the previous unlock.
332 * The unlock operation has to re-enable all of the threads that are
333 * waiting on the lock.
335 * @return True if synchronization was updated; false otherwise
337 bool ModelExecution::process_mutex(ModelAction *curr)
339 cdsc::mutex *mutex = curr->get_mutex();
340 struct cdsc::mutex_state *state = NULL;
343 state = mutex->get_state();
345 switch (curr->get_type()) {
346 case ATOMIC_TRYLOCK: {
347 bool success = !state->locked;
348 curr->set_try_lock(success);
350 get_thread(curr)->set_return_value(0);
353 get_thread(curr)->set_return_value(1);
355 //otherwise fall into the lock case
357 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
358 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
359 // assert_bug("Lock access before initialization");
360 state->locked = get_thread(curr);
361 ModelAction *unlock = get_last_unlock(curr);
362 //synchronize with the previous unlock statement
363 if (unlock != NULL) {
364 synchronize(unlock, curr);
370 case ATOMIC_UNLOCK: {
371 //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...
373 /* wake up the other threads */
374 for (unsigned int i = 0;i < get_num_threads();i++) {
375 Thread *t = get_thread(int_to_id(i));
376 Thread *curr_thrd = get_thread(curr);
377 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
381 /* unlock the lock - after checking who was waiting on it */
382 state->locked = NULL;
384 if (!curr->is_wait())
385 break;/* The rest is only for ATOMIC_WAIT */
389 case ATOMIC_NOTIFY_ALL: {
390 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
391 //activate all the waiting threads
392 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
393 scheduler->wake(get_thread(*rit));
398 case ATOMIC_NOTIFY_ONE: {
399 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
400 if (waiters->size() != 0) {
401 Thread * thread = fuzzer->selectNotify(waiters);
402 scheduler->wake(thread);
414 * Process a write ModelAction
415 * @param curr The ModelAction to process
416 * @return True if the mo_graph was updated or promises were resolved
418 void ModelExecution::process_write(ModelAction *curr)
420 w_modification_order(curr);
421 get_thread(curr)->set_return_value(VALUE_NONE);
425 * Process a fence ModelAction
426 * @param curr The ModelAction to process
427 * @return True if synchronization was updated
429 bool ModelExecution::process_fence(ModelAction *curr)
432 * fence-relaxed: no-op
433 * fence-release: only log the occurence (not in this function), for
434 * use in later synchronization
435 * fence-acquire (this function): search for hypothetical release
437 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
439 bool updated = false;
440 if (curr->is_acquire()) {
441 action_list_t *list = &action_trace;
442 action_list_t::reverse_iterator rit;
443 /* Find X : is_read(X) && X --sb-> curr */
444 for (rit = list->rbegin();rit != list->rend();rit++) {
445 ModelAction *act = *rit;
448 if (act->get_tid() != curr->get_tid())
450 /* Stop at the beginning of the thread */
451 if (act->is_thread_start())
453 /* Stop once we reach a prior fence-acquire */
454 if (act->is_fence() && act->is_acquire())
458 /* read-acquire will find its own release sequences */
459 if (act->is_acquire())
462 /* Establish hypothetical release sequences */
463 ClockVector *cv = get_hb_from_write(act);
464 if (curr->get_cv()->merge(cv))
472 * @brief Process the current action for thread-related activity
474 * Performs current-action processing for a THREAD_* ModelAction. Proccesses
475 * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
476 * synchronization, etc. This function is a no-op for non-THREAD actions
477 * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
479 * @param curr The current action
480 * @return True if synchronization was updated or a thread completed
482 bool ModelExecution::process_thread_action(ModelAction *curr)
484 bool updated = false;
486 switch (curr->get_type()) {
487 case THREAD_CREATE: {
488 thrd_t *thrd = (thrd_t *)curr->get_location();
489 struct thread_params *params = (struct thread_params *)curr->get_value();
490 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
491 curr->set_thread_operand(th);
493 th->set_creation(curr);
496 case PTHREAD_CREATE: {
497 (*(uint32_t *)curr->get_location()) = pthread_counter++;
499 struct pthread_params *params = (struct pthread_params *)curr->get_value();
500 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
501 curr->set_thread_operand(th);
503 th->set_creation(curr);
505 if ( pthread_map.size() < pthread_counter )
506 pthread_map.resize( pthread_counter );
507 pthread_map[ pthread_counter-1 ] = th;
512 Thread *blocking = curr->get_thread_operand();
513 ModelAction *act = get_last_action(blocking->get_id());
514 synchronize(act, curr);
515 updated = true; /* trigger rel-seq checks */
519 Thread *blocking = curr->get_thread_operand();
520 ModelAction *act = get_last_action(blocking->get_id());
521 synchronize(act, curr);
522 updated = true; /* trigger rel-seq checks */
523 break; // WL: to be add (modified)
526 case THREAD_FINISH: {
527 Thread *th = get_thread(curr);
528 /* Wake up any joining threads */
529 for (unsigned int i = 0;i < get_num_threads();i++) {
530 Thread *waiting = get_thread(int_to_id(i));
531 if (waiting->waiting_on() == th &&
532 waiting->get_pending()->is_thread_join())
533 scheduler->wake(waiting);
536 updated = true; /* trigger rel-seq checks */
550 * Initialize the current action by performing one or more of the following
551 * actions, as appropriate: merging RMWR and RMWC/RMW actions,
552 * manipulating backtracking sets, allocating and
553 * initializing clock vectors, and computing the promises to fulfill.
555 * @param curr The current action, as passed from the user context; may be
556 * freed/invalidated after the execution of this function, with a different
557 * action "returned" its place (pass-by-reference)
558 * @return True if curr is a newly-explored action; false otherwise
560 bool ModelExecution::initialize_curr_action(ModelAction **curr)
562 if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
563 ModelAction *newcurr = process_rmw(*curr);
569 ModelAction *newcurr = *curr;
571 newcurr->set_seq_number(get_next_seq_num());
572 /* Always compute new clock vector */
573 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
575 /* Assign most recent release fence */
576 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
578 return true; /* This was a new ModelAction */
583 * @brief Establish reads-from relation between two actions
585 * Perform basic operations involved with establishing a concrete rf relation,
586 * including setting the ModelAction data and checking for release sequences.
588 * @param act The action that is reading (must be a read)
589 * @param rf The action from which we are reading (must be a write)
591 * @return True if this read established synchronization
594 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
597 ASSERT(rf->is_write());
599 act->set_read_from(rf);
600 if (act->is_acquire()) {
601 ClockVector *cv = get_hb_from_write(rf);
604 act->get_cv()->merge(cv);
609 * @brief Synchronizes two actions
611 * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
612 * This function performs the synchronization as well as providing other hooks
613 * for other checks along with synchronization.
615 * @param first The left-hand side of the synchronizes-with relation
616 * @param second The right-hand side of the synchronizes-with relation
617 * @return True if the synchronization was successful (i.e., was consistent
618 * with the execution order); false otherwise
620 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
622 if (*second < *first) {
623 set_bad_synchronization();
626 return second->synchronize_with(first);
630 * @brief Check whether a model action is enabled.
632 * Checks whether an operation would be successful (i.e., is a lock already
633 * locked, or is the joined thread already complete).
635 * For yield-blocking, yields are never enabled.
637 * @param curr is the ModelAction to check whether it is enabled.
638 * @return a bool that indicates whether the action is enabled.
640 bool ModelExecution::check_action_enabled(ModelAction *curr) {
641 if (curr->is_lock()) {
642 cdsc::mutex *lock = curr->get_mutex();
643 struct cdsc::mutex_state *state = lock->get_state();
646 } else if (curr->is_thread_join()) {
647 Thread *blocking = curr->get_thread_operand();
648 if (!blocking->is_complete()) {
657 * This is the heart of the model checker routine. It performs model-checking
658 * actions corresponding to a given "current action." Among other processes, it
659 * calculates reads-from relationships, updates synchronization clock vectors,
660 * forms a memory_order constraints graph, and handles replay/backtrack
661 * execution when running permutations of previously-observed executions.
663 * @param curr The current action to process
664 * @return The ModelAction that is actually executed; may be different than
667 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
670 bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
671 bool newly_explored = initialize_curr_action(&curr);
675 wake_up_sleeping_actions(curr);
677 /* Add the action to lists before any other model-checking tasks */
678 if (!second_part_of_rmw && curr->get_type() != NOOP)
679 add_action_to_lists(curr);
681 if (curr->is_write())
682 add_write_to_lists(curr);
684 SnapVector<ModelAction *> * rf_set = NULL;
685 /* Build may_read_from set for newly-created actions */
686 if (newly_explored && curr->is_read())
687 rf_set = build_may_read_from(curr);
689 process_thread_action(curr);
691 if (curr->is_read() && !second_part_of_rmw) {
692 process_read(curr, rf_set);
695 ASSERT(rf_set == NULL);
698 if (curr->is_write())
701 if (curr->is_fence())
704 if (curr->is_mutex_op())
711 * This is the strongest feasibility check available.
712 * @return whether the current trace (partial or complete) must be a prefix of
715 bool ModelExecution::isfeasibleprefix() const
717 return !is_infeasible();
721 * Print disagnostic information about an infeasible execution
722 * @param prefix A string to prefix the output with; if NULL, then a default
723 * message prefix will be provided
725 void ModelExecution::print_infeasibility(const char *prefix) const
729 if (priv->bad_synchronization)
730 ptr += sprintf(ptr, "[bad sw ordering]");
732 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
736 * Check if the current partial trace is infeasible. Does not check any
737 * end-of-execution flags, which might rule out the execution. Thus, this is
738 * useful only for ruling an execution as infeasible.
739 * @return whether the current partial trace is infeasible.
741 bool ModelExecution::is_infeasible() const
743 return priv->bad_synchronization;
746 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
747 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
748 ModelAction *lastread = get_last_action(act->get_tid());
749 lastread->process_rmw(act);
751 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
757 * @brief Updates the mo_graph with the constraints imposed from the current
760 * Basic idea is the following: Go through each other thread and find
761 * the last action that happened before our read. Two cases:
763 * -# The action is a write: that write must either occur before
764 * the write we read from or be the write we read from.
765 * -# The action is a read: the write that that action read from
766 * must occur before the write we read from or be the same write.
768 * @param curr The current action. Must be a read.
769 * @param rf The ModelAction or Promise that curr reads from. Must be a write.
770 * @return True if modification order edges were added; false otherwise
773 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
775 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
777 ASSERT(curr->is_read());
779 /* Last SC fence in the current thread */
780 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
782 int tid = curr->get_tid();
783 ModelAction *prev_same_thread = NULL;
784 /* Iterate over all threads */
785 for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
786 /* Last SC fence in thread tid */
787 ModelAction *last_sc_fence_thread_local = NULL;
789 last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
791 /* Last SC fence in thread tid, before last SC fence in current thread */
792 ModelAction *last_sc_fence_thread_before = NULL;
793 if (last_sc_fence_local)
794 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
796 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
797 if (prev_same_thread != NULL &&
798 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
799 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
803 /* Iterate over actions in thread, starting from most recent */
804 action_list_t *list = &(*thrd_lists)[tid];
805 action_list_t::reverse_iterator rit;
806 for (rit = list->rbegin();rit != list->rend();rit++) {
807 ModelAction *act = *rit;
812 /* Don't want to add reflexive edges on 'rf' */
813 if (act->equals(rf)) {
814 if (act->happens_before(curr))
820 if (act->is_write()) {
821 /* C++, Section 29.3 statement 5 */
822 if (curr->is_seqcst() && last_sc_fence_thread_local &&
823 *act < *last_sc_fence_thread_local) {
824 if (mo_graph->checkReachable(rf, act))
826 priorset->push_back(act);
829 /* C++, Section 29.3 statement 4 */
830 else if (act->is_seqcst() && last_sc_fence_local &&
831 *act < *last_sc_fence_local) {
832 if (mo_graph->checkReachable(rf, act))
834 priorset->push_back(act);
837 /* C++, Section 29.3 statement 6 */
838 else if (last_sc_fence_thread_before &&
839 *act < *last_sc_fence_thread_before) {
840 if (mo_graph->checkReachable(rf, act))
842 priorset->push_back(act);
848 * Include at most one act per-thread that "happens
851 if (act->happens_before(curr)) {
853 if (last_sc_fence_local == NULL ||
854 (*last_sc_fence_local < *prev_same_thread)) {
855 prev_same_thread = act;
858 if (act->is_write()) {
859 if (mo_graph->checkReachable(rf, act))
861 priorset->push_back(act);
863 const ModelAction *prevrf = act->get_reads_from();
864 if (!prevrf->equals(rf)) {
865 if (mo_graph->checkReachable(rf, prevrf))
867 priorset->push_back(prevrf);
869 if (act->get_tid() == curr->get_tid()) {
870 //Can prune curr from obj list
883 * Updates the mo_graph with the constraints imposed from the current write.
885 * Basic idea is the following: Go through each other thread and find
886 * the lastest action that happened before our write. Two cases:
888 * (1) The action is a write => that write must occur before
891 * (2) The action is a read => the write that that action read from
892 * must occur before the current write.
894 * This method also handles two other issues:
896 * (I) Sequential Consistency: Making sure that if the current write is
897 * seq_cst, that it occurs after the previous seq_cst write.
899 * (II) Sending the write back to non-synchronizing reads.
901 * @param curr The current action. Must be a write.
902 * @param send_fv A vector for stashing reads to which we may pass our future
903 * value. If NULL, then don't record any future values.
904 * @return True if modification order edges were added; false otherwise
906 void ModelExecution::w_modification_order(ModelAction *curr)
908 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
910 ASSERT(curr->is_write());
912 if (curr->is_seqcst()) {
913 /* We have to at least see the last sequentially consistent write,
914 so we are initialized. */
915 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
916 if (last_seq_cst != NULL) {
917 mo_graph->addEdge(last_seq_cst, curr);
921 /* Last SC fence in the current thread */
922 ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
924 /* Iterate over all threads */
925 for (i = 0;i < thrd_lists->size();i++) {
926 /* Last SC fence in thread i, before last SC fence in current thread */
927 ModelAction *last_sc_fence_thread_before = NULL;
928 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
929 last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
931 /* Iterate over actions in thread, starting from most recent */
932 action_list_t *list = &(*thrd_lists)[i];
933 action_list_t::reverse_iterator rit;
934 bool force_edge = false;
935 for (rit = list->rbegin();rit != list->rend();rit++) {
936 ModelAction *act = *rit;
939 * 1) If RMW and it actually read from something, then we
940 * already have all relevant edges, so just skip to next
943 * 2) If RMW and it didn't read from anything, we should
944 * whatever edge we can get to speed up convergence.
946 * 3) If normal write, we need to look at earlier actions, so
947 * continue processing list.
950 if (curr->is_rmw()) {
951 if (curr->get_reads_from() != NULL)
959 /* C++, Section 29.3 statement 7 */
960 if (last_sc_fence_thread_before && act->is_write() &&
961 *act < *last_sc_fence_thread_before) {
962 mo_graph->addEdge(act, curr, force_edge);
967 * Include at most one act per-thread that "happens
970 if (act->happens_before(curr)) {
972 * Note: if act is RMW, just add edge:
974 * The following edge should be handled elsewhere:
975 * readfrom(act) --mo--> act
978 mo_graph->addEdge(act, curr, force_edge);
979 else if (act->is_read()) {
980 //if previous read accessed a null, just keep going
981 mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
990 * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
991 * some constraints. This method checks one the following constraint (others
992 * require compiler support):
994 * If X --hb-> Y --mo-> Z, then X should not read from Z.
995 * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
997 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
999 SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1001 /* Iterate over all threads */
1002 for (i = 0;i < thrd_lists->size();i++) {
1003 const ModelAction *write_after_read = NULL;
1005 /* Iterate over actions in thread, starting from most recent */
1006 action_list_t *list = &(*thrd_lists)[i];
1007 action_list_t::reverse_iterator rit;
1008 for (rit = list->rbegin();rit != list->rend();rit++) {
1009 ModelAction *act = *rit;
1011 /* Don't disallow due to act == reader */
1012 if (!reader->happens_before(act) || reader == act)
1014 else if (act->is_write())
1015 write_after_read = act;
1016 else if (act->is_read() && act->get_reads_from() != NULL)
1017 write_after_read = act->get_reads_from();
1020 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1027 * Computes the clock vector that happens before propagates from this write.
1029 * @param rf The action that might be part of a release sequence. Must be a
1031 * @return ClockVector of happens before relation.
1034 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1035 SnapVector<ModelAction *> * processset = NULL;
1036 for ( ;rf != NULL;rf = rf->get_reads_from()) {
1037 ASSERT(rf->is_write());
1038 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1040 if (processset == NULL)
1041 processset = new SnapVector<ModelAction *>();
1042 processset->push_back(rf);
1045 int i = (processset == NULL) ? 0 : processset->size();
1047 ClockVector * vec = NULL;
1049 if (rf->get_rfcv() != NULL) {
1050 vec = rf->get_rfcv();
1051 } else if (rf->is_acquire() && rf->is_release()) {
1053 } else if (rf->is_release() && !rf->is_rmw()) {
1055 } else if (rf->is_release()) {
1056 //have rmw that is release and doesn't have a rfcv
1057 (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1060 //operation that isn't release
1061 if (rf->get_last_fence_release()) {
1063 vec = rf->get_last_fence_release()->get_cv();
1065 (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1071 rf = (*processset)[i];
1075 if (processset != NULL)
1081 * Performs various bookkeeping operations for the current ModelAction. For
1082 * instance, adds action to the per-object, per-thread action vector and to the
1083 * action trace list of all thread actions.
1085 * @param act is the ModelAction to add.
1087 void ModelExecution::add_action_to_lists(ModelAction *act)
1089 int tid = id_to_int(act->get_tid());
1090 ModelAction *uninit = NULL;
1092 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1093 if (list->empty() && act->is_atomic_var()) {
1094 uninit = get_uninitialized_action(act);
1095 uninit_id = id_to_int(uninit->get_tid());
1096 list->push_front(uninit);
1097 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1098 if (uninit_id >= (int)vec->size())
1099 vec->resize(uninit_id + 1);
1100 (*vec)[uninit_id].push_front(uninit);
1102 list->push_back(act);
1104 // Update action trace, a total order of all actions
1105 action_trace.push_back(act);
1107 action_trace.push_front(uninit);
1109 // Update obj_thrd_map, a per location, per thread, order of actions
1110 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1111 if (tid >= (int)vec->size())
1112 vec->resize(priv->next_thread_id);
1113 (*vec)[tid].push_back(act);
1115 (*vec)[uninit_id].push_front(uninit);
1117 // Update thrd_last_action, the last action taken by each thrad
1118 if ((int)thrd_last_action.size() <= tid)
1119 thrd_last_action.resize(get_num_threads());
1120 thrd_last_action[tid] = act;
1122 thrd_last_action[uninit_id] = uninit;
1124 // Update thrd_last_fence_release, the last release fence taken by each thread
1125 if (act->is_fence() && act->is_release()) {
1126 if ((int)thrd_last_fence_release.size() <= tid)
1127 thrd_last_fence_release.resize(get_num_threads());
1128 thrd_last_fence_release[tid] = act;
1131 if (act->is_wait()) {
1132 void *mutex_loc = (void *) act->get_value();
1133 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1135 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1136 if (tid >= (int)vec->size())
1137 vec->resize(priv->next_thread_id);
1138 (*vec)[tid].push_back(act);
1142 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1143 action_list_t::reverse_iterator rit = list->rbegin();
1144 modelclock_t next_seq = act->get_seq_number();
1145 if (rit == list->rend() || (*rit)->get_seq_number() == next_seq)
1146 list->push_back(act);
1148 for(;rit != list->rend();rit++) {
1149 if ((*rit)->get_seq_number() == next_seq) {
1150 action_list_t::iterator it = rit.base();
1151 list->insert(it, act);
1158 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1159 action_list_t::reverse_iterator rit = list->rbegin();
1160 modelclock_t next_seq = act->get_seq_number();
1161 if (rit == list->rend()) {
1162 act->create_cv(NULL);
1163 } else if ((*rit)->get_seq_number() == next_seq) {
1164 act->create_cv((*rit));
1165 list->push_back(act);
1167 for(;rit != list->rend();rit++) {
1168 if ((*rit)->get_seq_number() == next_seq) {
1169 act->create_cv((*rit));
1170 action_list_t::iterator it = rit.base();
1171 list->insert(it, act);
1179 * Performs various bookkeeping operations for a normal write. The
1180 * complication is that we are typically inserting a normal write
1181 * lazily, so we need to insert it into the middle of lists.
1183 * @param act is the ModelAction to add.
1186 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1188 int tid = id_to_int(act->get_tid());
1189 insertIntoActionListAndSetCV(&action_trace, act);
1191 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1192 insertIntoActionList(list, act);
1194 // Update obj_thrd_map, a per location, per thread, order of actions
1195 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1196 if (tid >= (int)vec->size())
1197 vec->resize(priv->next_thread_id);
1198 insertIntoActionList(&(*vec)[tid],act);
1200 // Update thrd_last_action, the last action taken by each thrad
1201 if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1202 thrd_last_action[tid] = act;
1206 void ModelExecution::add_write_to_lists(ModelAction *write) {
1207 // Update seq_cst map
1208 if (write->is_seqcst())
1209 obj_last_sc_map.put(write->get_location(), write);
1211 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1212 int tid = id_to_int(write->get_tid());
1213 if (tid >= (int)vec->size())
1214 vec->resize(priv->next_thread_id);
1215 (*vec)[tid].push_back(write);
1219 * @brief Get the last action performed by a particular Thread
1220 * @param tid The thread ID of the Thread in question
1221 * @return The last action in the thread
1223 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1225 int threadid = id_to_int(tid);
1226 if (threadid < (int)thrd_last_action.size())
1227 return thrd_last_action[id_to_int(tid)];
1233 * @brief Get the last fence release performed by a particular Thread
1234 * @param tid The thread ID of the Thread in question
1235 * @return The last fence release in the thread, if one exists; NULL otherwise
1237 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1239 int threadid = id_to_int(tid);
1240 if (threadid < (int)thrd_last_fence_release.size())
1241 return thrd_last_fence_release[id_to_int(tid)];
1247 * Gets the last memory_order_seq_cst write (in the total global sequence)
1248 * performed on a particular object (i.e., memory location), not including the
1250 * @param curr The current ModelAction; also denotes the object location to
1252 * @return The last seq_cst write
1254 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1256 void *location = curr->get_location();
1257 return obj_last_sc_map.get(location);
1261 * Gets the last memory_order_seq_cst fence (in the total global sequence)
1262 * performed in a particular thread, prior to a particular fence.
1263 * @param tid The ID of the thread to check
1264 * @param before_fence The fence from which to begin the search; if NULL, then
1265 * search for the most recent fence in the thread.
1266 * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1268 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1270 /* All fences should have location FENCE_LOCATION */
1271 action_list_t *list = obj_map.get(FENCE_LOCATION);
1276 action_list_t::reverse_iterator rit = list->rbegin();
1279 for (;rit != list->rend();rit++)
1280 if (*rit == before_fence)
1283 ASSERT(*rit == before_fence);
1287 for (;rit != list->rend();rit++)
1288 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1294 * Gets the last unlock operation performed on a particular mutex (i.e., memory
1295 * location). This function identifies the mutex according to the current
1296 * action, which is presumed to perform on the same mutex.
1297 * @param curr The current ModelAction; also denotes the object location to
1299 * @return The last unlock operation
1301 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1303 void *location = curr->get_location();
1305 action_list_t *list = obj_map.get(location);
1306 /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1307 action_list_t::reverse_iterator rit;
1308 for (rit = list->rbegin();rit != list->rend();rit++)
1309 if ((*rit)->is_unlock() || (*rit)->is_wait())
1314 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1316 ModelAction *parent = get_last_action(tid);
1318 parent = get_thread(tid)->get_creation();
1323 * Returns the clock vector for a given thread.
1324 * @param tid The thread whose clock vector we want
1325 * @return Desired clock vector
1327 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1329 ModelAction *firstaction=get_parent_action(tid);
1330 return firstaction != NULL ? firstaction->get_cv() : NULL;
1333 bool valequals(uint64_t val1, uint64_t val2, int size) {
1336 return ((uint8_t)val1) == ((uint8_t)val2);
1338 return ((uint16_t)val1) == ((uint16_t)val2);
1340 return ((uint32_t)val1) == ((uint32_t)val2);
1350 * Build up an initial set of all past writes that this 'read' action may read
1351 * from, as well as any previously-observed future values that must still be valid.
1353 * @param curr is the current ModelAction that we are exploring; it must be a
1356 SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
1358 SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1360 ASSERT(curr->is_read());
1362 ModelAction *last_sc_write = NULL;
1364 if (curr->is_seqcst())
1365 last_sc_write = get_last_seq_cst_write(curr);
1367 SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1369 /* Iterate over all threads */
1370 for (i = 0;i < thrd_lists->size();i++) {
1371 /* Iterate over actions in thread, starting from most recent */
1372 action_list_t *list = &(*thrd_lists)[i];
1373 action_list_t::reverse_iterator rit;
1374 for (rit = list->rbegin();rit != list->rend();rit++) {
1375 ModelAction *act = *rit;
1380 /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1381 bool allow_read = true;
1383 if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1386 /* Need to check whether we will have two RMW reading from the same value */
1387 if (curr->is_rmwr()) {
1388 /* It is okay if we have a failing CAS */
1389 if (!curr->is_rmwrcas() ||
1390 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1391 //Need to make sure we aren't the second RMW
1392 CycleNode * node = mo_graph->getNode_noCreate(act);
1393 if (node != NULL && node->getRMW() != NULL) {
1394 //we are the second RMW
1401 /* Only add feasible reads */
1402 rf_set->push_back(act);
1405 /* Include at most one act per-thread that "happens before" curr */
1406 if (act->happens_before(curr))
1411 if (DBG_ENABLED()) {
1412 model_print("Reached read action:\n");
1414 model_print("End printing read_from_past\n");
1420 * @brief Get an action representing an uninitialized atomic
1422 * This function may create a new one.
1424 * @param curr The current action, which prompts the creation of an UNINIT action
1425 * @return A pointer to the UNINIT ModelAction
1427 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1429 ModelAction *act = curr->get_uninit_action();
1431 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1432 curr->set_uninit_action(act);
1434 act->create_cv(NULL);
1438 static void print_list(const action_list_t *list)
1440 action_list_t::const_iterator it;
1442 model_print("------------------------------------------------------------------------------------\n");
1443 model_print("# t Action type MO Location Value Rf CV\n");
1444 model_print("------------------------------------------------------------------------------------\n");
1446 unsigned int hash = 0;
1448 for (it = list->begin();it != list->end();it++) {
1449 const ModelAction *act = *it;
1450 if (act->get_seq_number() > 0)
1452 hash = hash^(hash<<3)^((*it)->hash());
1454 model_print("HASH %u\n", hash);
1455 model_print("------------------------------------------------------------------------------------\n");
1458 #if SUPPORT_MOD_ORDER_DUMP
1459 void ModelExecution::dumpGraph(char *filename) const
1462 sprintf(buffer, "%s.dot", filename);
1463 FILE *file = fopen(buffer, "w");
1464 fprintf(file, "digraph %s {\n", filename);
1465 mo_graph->dumpNodes(file);
1466 ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1468 for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1469 ModelAction *act = *it;
1470 if (act->is_read()) {
1471 mo_graph->dot_print_node(file, act);
1472 mo_graph->dot_print_edge(file,
1473 act->get_reads_from(),
1475 "label=\"rf\", color=red, weight=2");
1477 if (thread_array[act->get_tid()]) {
1478 mo_graph->dot_print_edge(file,
1479 thread_array[id_to_int(act->get_tid())],
1481 "label=\"sb\", color=blue, weight=400");
1484 thread_array[act->get_tid()] = act;
1486 fprintf(file, "}\n");
1487 model_free(thread_array);
1492 /** @brief Prints an execution trace summary. */
1493 void ModelExecution::print_summary() const
1495 #if SUPPORT_MOD_ORDER_DUMP
1496 char buffername[100];
1497 sprintf(buffername, "exec%04u", get_execution_number());
1498 mo_graph->dumpGraphToFile(buffername);
1499 sprintf(buffername, "graph%04u", get_execution_number());
1500 dumpGraph(buffername);
1503 model_print("Execution trace %d:", get_execution_number());
1504 if (isfeasibleprefix()) {
1505 if (scheduler->all_threads_sleeping())
1506 model_print(" SLEEP-SET REDUNDANT");
1507 if (have_bug_reports())
1508 model_print(" DETECTED BUG(S)");
1510 print_infeasibility(" INFEASIBLE");
1513 print_list(&action_trace);
1519 * Add a Thread to the system for the first time. Should only be called once
1521 * @param t The Thread to add
1523 void ModelExecution::add_thread(Thread *t)
1525 unsigned int i = id_to_int(t->get_id());
1526 if (i >= thread_map.size())
1527 thread_map.resize(i + 1);
1529 if (!t->is_model_thread())
1530 scheduler->add_thread(t);
1534 * @brief Get a Thread reference by its ID
1535 * @param tid The Thread's ID
1536 * @return A Thread reference
1538 Thread * ModelExecution::get_thread(thread_id_t tid) const
1540 unsigned int i = id_to_int(tid);
1541 if (i < thread_map.size())
1542 return thread_map[i];
1547 * @brief Get a reference to the Thread in which a ModelAction was executed
1548 * @param act The ModelAction
1549 * @return A Thread reference
1551 Thread * ModelExecution::get_thread(const ModelAction *act) const
1553 return get_thread(act->get_tid());
1557 * @brief Get a Thread reference by its pthread ID
1558 * @param index The pthread's ID
1559 * @return A Thread reference
1561 Thread * ModelExecution::get_pthread(pthread_t pid) {
1567 uint32_t thread_id = x.v;
1568 if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1573 * @brief Check if a Thread is currently enabled
1574 * @param t The Thread to check
1575 * @return True if the Thread is currently enabled
1577 bool ModelExecution::is_enabled(Thread *t) const
1579 return scheduler->is_enabled(t);
1583 * @brief Check if a Thread is currently enabled
1584 * @param tid The ID of the Thread to check
1585 * @return True if the Thread is currently enabled
1587 bool ModelExecution::is_enabled(thread_id_t tid) const
1589 return scheduler->is_enabled(tid);
1593 * @brief Select the next thread to execute based on the curren action
1595 * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1596 * actions should be followed by the execution of their child thread. In either
1597 * case, the current action should determine the next thread schedule.
1599 * @param curr The current action
1600 * @return The next thread to run, if the current action will determine this
1601 * selection; otherwise NULL
1603 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1605 /* Do not split atomic RMW */
1606 if (curr->is_rmwr())
1607 return get_thread(curr);
1608 /* Follow CREATE with the created thread */
1609 /* which is not needed, because model.cc takes care of this */
1610 if (curr->get_type() == THREAD_CREATE)
1611 return curr->get_thread_operand();
1612 if (curr->get_type() == PTHREAD_CREATE) {
1613 return curr->get_thread_operand();
1619 * Takes the next step in the execution, if possible.
1620 * @param curr The current step to take
1621 * @return Returns the next Thread to run, if any; NULL if this execution
1624 Thread * ModelExecution::take_step(ModelAction *curr)
1626 Thread *curr_thrd = get_thread(curr);
1627 ASSERT(curr_thrd->get_state() == THREAD_READY);
1629 ASSERT(check_action_enabled(curr)); /* May have side effects? */
1630 curr = check_current_action(curr);
1633 /* Process this action in ModelHistory for records*/
1634 model->get_history()->process_action( curr, curr->get_tid() );
1636 if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1637 scheduler->remove_thread(curr_thrd);
1639 return action_select_next_thread(curr);
1642 Fuzzer * ModelExecution::getFuzzer() {