+ if (diverge == earliest_diverge) {
+ earliest_diverge = prevnode->get_action();
+ }
+ }
+ /* The correct sleep set is in the parent node. */
+ execute_sleep_set();
+
+ DEBUG("*** Divergence point ***\n");
+
+ diverge = NULL;
+ } else {
+ tid = next->get_tid();
+ }
+ DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
+ ASSERT(tid != THREAD_ID_T_NONE);
+ return thread_map->get(id_to_int(tid));
+}
+
+/**
+ * We need to know what the next actions of all threads in the sleep
+ * set will be. This method computes them and stores the actions at
+ * the corresponding thread object's pending action.
+ */
+
+void ModelChecker::execute_sleep_set()
+{
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ thread_id_t tid = int_to_id(i);
+ Thread *thr = get_thread(tid);
+ if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
+ thr->set_state(THREAD_RUNNING);
+ scheduler->next_thread(thr);
+ Thread::swap(&system_context, thr);
+ priv->current_action->set_sleep_flag();
+ thr->set_pending(priv->current_action);
+ }
+ }
+}
+
+void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
+{
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *thr = get_thread(int_to_id(i));
+ if (scheduler->is_sleep_set(thr)) {
+ ModelAction *pending_act = thr->get_pending();
+ if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
+ //Remove this thread from sleep set
+ scheduler->remove_sleep(thr);
+ }
+ }
+}
+
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelChecker::set_bad_synchronization()
+{
+ priv->bad_synchronization = true;
+}
+
+bool ModelChecker::has_asserted() const
+{
+ return priv->asserted;
+}
+
+void ModelChecker::set_assert()
+{
+ priv->asserted = true;
+}
+
+/**
+ * Check if we are in a deadlock. Should only be called at the end of an
+ * execution, although it should not give false positives in the middle of an
+ * execution (there should be some ENABLED thread).
+ *
+ * @return True if program is in a deadlock; false otherwise
+ */
+bool ModelChecker::is_deadlocked() const
+{
+ bool blocking_threads = false;
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ thread_id_t tid = int_to_id(i);
+ if (is_enabled(tid))
+ return false;
+ Thread *t = get_thread(tid);
+ if (!t->is_model_thread() && t->get_pending())
+ blocking_threads = true;
+ }
+ return blocking_threads;
+}
+
+/**
+ * Check if this is a complete execution. That is, have all thread completed
+ * execution (rather than exiting because sleep sets have forced a redundant
+ * execution).
+ *
+ * @return True if the execution is complete.
+ */
+bool ModelChecker::is_complete_execution() const
+{
+ for (unsigned int i = 0; i < get_num_threads(); i++)
+ if (is_enabled(int_to_id(i)))
+ return false;
+ return true;
+}
+
+/**
+ * @brief Assert a bug in the executing program.
+ *
+ * Use this function to assert any sort of bug in the user program. If the
+ * current trace is feasible (actually, a prefix of some feasible execution),
+ * then this execution will be aborted, printing the appropriate message. If
+ * the current trace is not yet feasible, the error message will be stashed and
+ * printed if the execution ever becomes feasible.
+ *
+ * @param msg Descriptive message for the bug (do not include newline char)
+ * @return True if bug is immediately-feasible
+ */
+bool ModelChecker::assert_bug(const char *msg)
+{
+ priv->bugs.push_back(new bug_message(msg));
+
+ if (isfeasibleprefix()) {
+ set_assert();
+ return true;
+ }
+ return false;
+}
+
+/**
+ * @brief Assert a bug in the executing program, asserted by a user thread
+ * @see ModelChecker::assert_bug
+ * @param msg Descriptive message for the bug (do not include newline char)
+ */
+void ModelChecker::assert_user_bug(const char *msg)
+{
+ /* If feasible bug, bail out now */
+ if (assert_bug(msg))
+ switch_to_master(NULL);
+}
+
+/** @return True, if any bugs have been reported for this execution */
+bool ModelChecker::have_bug_reports() const
+{
+ return priv->bugs.size() != 0;
+}
+
+/** @brief Print bug report listing for this execution (if any bugs exist) */
+void ModelChecker::print_bugs() const
+{
+ if (have_bug_reports()) {
+ model_print("Bug report: %zu bug%s detected\n",
+ priv->bugs.size(),
+ priv->bugs.size() > 1 ? "s" : "");
+ for (unsigned int i = 0; i < priv->bugs.size(); i++)
+ priv->bugs[i]->print();
+ }
+}
+
+/**
+ * @brief Record end-of-execution stats
+ *
+ * Must be run when exiting an execution. Records various stats.
+ * @see struct execution_stats
+ */
+void ModelChecker::record_stats()
+{
+ stats.num_total++;
+ if (!isfeasibleprefix())
+ stats.num_infeasible++;
+ else if (have_bug_reports())
+ stats.num_buggy_executions++;
+ else if (is_complete_execution())
+ stats.num_complete++;
+ else
+ stats.num_redundant++;
+}
+
+/** @brief Print execution stats */
+void ModelChecker::print_stats() const
+{
+ model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+ model_print("Number of redundant executions: %d\n", stats.num_redundant);
+ model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
+ model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
+ model_print("Total executions: %d\n", stats.num_total);
+ model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
+}
+
+/**
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
+ */
+void ModelChecker::print_execution(bool printbugs) const
+{
+ print_program_output();
+
+ if (DBG_ENABLED() || params.verbose) {
+ model_print("Earliest divergence point since last feasible execution:\n");
+ if (earliest_diverge)
+ earliest_diverge->print();
+ else
+ model_print("(Not set)\n");
+
+ model_print("\n");
+ print_stats();
+ }
+
+ /* Don't print invalid bugs */
+ if (printbugs)
+ print_bugs();
+
+ model_print("\n");
+ print_summary();
+}
+
+/**
+ * Queries the model-checker for more executions to explore and, if one
+ * exists, resets the model-checker state to execute a new execution.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
+bool ModelChecker::next_execution()
+{
+ DBG();
+ /* Is this execution a feasible execution that's worth bug-checking? */
+ bool complete = isfeasibleprefix() && (is_complete_execution() ||
+ have_bug_reports());
+
+ /* End-of-execution bug checks */
+ if (complete) {
+ if (is_deadlocked())
+ assert_bug("Deadlock detected");
+
+ checkDataRaces();
+ }
+
+ record_stats();
+
+ /* Output */
+ if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
+ print_execution(complete);
+ else
+ clear_program_output();
+
+ if (complete)
+ earliest_diverge = NULL;
+
+ if ((diverge = get_next_backtrack()) == NULL)
+ return false;
+
+ if (DBG_ENABLED()) {
+ model_print("Next execution will diverge at:\n");
+ diverge->print();
+ }
+
+ reset_to_initial_state();
+ return true;
+}
+
+ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
+{
+ switch (act->get_type()) {
+ case ATOMIC_FENCE:
+ case ATOMIC_READ:
+ case ATOMIC_WRITE:
+ case ATOMIC_RMW: {
+ /* Optimization: relaxed operations don't need backtracking */
+ if (act->is_relaxed())
+ return NULL;
+ /* linear search: from most recent to oldest */
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (prev->could_synchronize_with(act))
+ return prev;
+ }
+ break;
+ }
+ case ATOMIC_LOCK:
+ case ATOMIC_TRYLOCK: {
+ /* linear search: from most recent to oldest */
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (act->is_conflicting_lock(prev))
+ return prev;
+ }
+ break;
+ }
+ case ATOMIC_UNLOCK: {
+ /* linear search: from most recent to oldest */
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (!act->same_thread(prev) && prev->is_failed_trylock())
+ return prev;
+ }
+ break;
+ }
+ case ATOMIC_WAIT: {
+ /* linear search: from most recent to oldest */
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (!act->same_thread(prev) && prev->is_failed_trylock())
+ return prev;
+ if (!act->same_thread(prev) && prev->is_notify())
+ return prev;
+ }
+ break;
+ }
+
+ case ATOMIC_NOTIFY_ALL:
+ case ATOMIC_NOTIFY_ONE: {
+ /* linear search: from most recent to oldest */
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (!act->same_thread(prev) && prev->is_wait())
+ return prev;
+ }
+ break;
+ }
+ default:
+ break;
+ }
+ return NULL;
+}
+
+/** This method finds backtracking points where we should try to
+ * reorder the parameter ModelAction against.
+ *
+ * @param the ModelAction to find backtracking points for.
+ */
+void ModelChecker::set_backtracking(ModelAction *act)
+{
+ Thread *t = get_thread(act);
+ ModelAction *prev = get_last_conflict(act);
+ if (prev == NULL)
+ return;
+
+ Node *node = prev->get_node()->get_parent();
+
+ int low_tid, high_tid;
+ if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
+ low_tid = id_to_int(act->get_tid());
+ high_tid = low_tid + 1;
+ } else {
+ low_tid = 0;
+ high_tid = get_num_threads();
+ }
+
+ for (int i = low_tid; i < high_tid; i++) {
+ thread_id_t tid = int_to_id(i);
+
+ /* Make sure this thread can be enabled here. */
+ if (i >= node->get_num_threads())
+ break;
+
+ /* Don't backtrack into a point where the thread is disabled or sleeping. */
+ if (node->enabled_status(tid) != THREAD_ENABLED)
+ continue;
+
+ /* Check if this has been explored already */
+ if (node->has_been_explored(tid))
+ continue;
+
+ /* See if fairness allows */
+ if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
+ bool unfair = false;
+ for (int t = 0; t < node->get_num_threads(); t++) {
+ thread_id_t tother = int_to_id(t);
+ if (node->is_enabled(tother) && node->has_priority(tother)) {
+ unfair = true;
+ break;
+ }
+ }
+ if (unfair)
+ continue;
+ }
+ /* Cache the latest backtracking point */
+ set_latest_backtrack(prev);
+
+ /* If this is a new backtracking point, mark the tree */
+ if (!node->set_backtrack(tid))
+ continue;
+ DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
+ id_to_int(prev->get_tid()),
+ id_to_int(t->get_id()));
+ if (DBG_ENABLED()) {
+ prev->print();
+ act->print();
+ }
+ }
+}
+
+/**
+ * @brief Cache the a backtracking point as the "most recent", if eligible
+ *
+ * Note that this does not prepare the NodeStack for this backtracking
+ * operation, it only caches the action on a per-execution basis
+ *
+ * @param act The operation at which we should explore a different next action
+ * (i.e., backtracking point)
+ * @return True, if this action is now the most recent backtracking point;
+ * false otherwise
+ */
+bool ModelChecker::set_latest_backtrack(ModelAction *act)
+{
+ if (!priv->next_backtrack || *act > *priv->next_backtrack) {
+ priv->next_backtrack = act;
+ return true;
+ }
+ return false;
+}
+
+/**
+ * Returns last backtracking point. The model checker will explore a different
+ * path for this point in the next execution.
+ * @return The ModelAction at which the next execution should diverge.
+ */
+ModelAction * ModelChecker::get_next_backtrack()
+{
+ ModelAction *next = priv->next_backtrack;
+ priv->next_backtrack = NULL;
+ return next;
+}
+
+/**
+ * Processes a read or rmw model action.
+ * @param curr is the read model action to process.
+ * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
+ * @return True if processing this read updates the mo_graph.
+ */
+bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
+{
+ uint64_t value = VALUE_NONE;
+ bool updated = false;
+ while (true) {
+ const ModelAction *reads_from = curr->get_node()->get_read_from();
+ if (reads_from != NULL) {
+ mo_graph->startChanges();
+
+ value = reads_from->get_value();
+ bool r_status = false;
+
+ if (!second_part_of_rmw) {
+ check_recency(curr, reads_from);
+ r_status = r_modification_order(curr, reads_from);
+ }
+
+ if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
+ mo_graph->rollbackChanges();
+ priv->too_many_reads = false;
+ continue;
+ }
+
+ read_from(curr, reads_from);
+ mo_graph->commitChanges();
+ mo_check_promises(curr->get_tid(), reads_from, NULL);
+
+ updated |= r_status;
+ } else if (!second_part_of_rmw) {
+ /* Read from future value */
+ struct future_value fv = curr->get_node()->get_future_value();
+ Promise *promise = new Promise(curr, fv);
+ value = fv.value;
+ curr->set_read_from_promise(promise);
+ promises->push_back(promise);
+ mo_graph->startChanges();
+ updated = r_modification_order(curr, promise);
+ mo_graph->commitChanges();
+ }
+ get_thread(curr)->set_return_value(value);
+ return updated;
+ }
+}
+
+/**
+ * Processes a lock, trylock, or unlock model action. @param curr is
+ * the read model action to process.
+ *
+ * The try lock operation checks whether the lock is taken. If not,
+ * it falls to the normal lock operation case. If so, it returns
+ * fail.
+ *
+ * The lock operation has already been checked that it is enabled, so
+ * it just grabs the lock and synchronizes with the previous unlock.
+ *
+ * The unlock operation has to re-enable all of the threads that are
+ * waiting on the lock.
+ *
+ * @return True if synchronization was updated; false otherwise
+ */
+bool ModelChecker::process_mutex(ModelAction *curr)
+{
+ std::mutex *mutex = NULL;
+ struct std::mutex_state *state = NULL;
+
+ if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
+ mutex = (std::mutex *)curr->get_location();
+ state = mutex->get_state();
+ } else if (curr->is_wait()) {
+ mutex = (std::mutex *)curr->get_value();
+ state = mutex->get_state();
+ }
+
+ switch (curr->get_type()) {
+ case ATOMIC_TRYLOCK: {
+ bool success = !state->islocked;
+ curr->set_try_lock(success);
+ if (!success) {
+ get_thread(curr)->set_return_value(0);
+ break;
+ }
+ get_thread(curr)->set_return_value(1);
+ }
+ //otherwise fall into the lock case
+ case ATOMIC_LOCK: {
+ if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+ assert_bug("Lock access before initialization");
+ state->islocked = true;
+ ModelAction *unlock = get_last_unlock(curr);
+ //synchronize with the previous unlock statement
+ if (unlock != NULL) {
+ curr->synchronize_with(unlock);
+ return true;
+ }
+ break;
+ }
+ case ATOMIC_UNLOCK: {
+ //unlock the lock
+ state->islocked = false;
+ //wake up the other threads
+ action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
+ //activate all the waiting threads
+ for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+ scheduler->wake(get_thread(*rit));
+ }
+ waiters->clear();
+ break;
+ }
+ case ATOMIC_WAIT: {
+ //unlock the lock
+ state->islocked = false;
+ //wake up the other threads
+ action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
+ //activate all the waiting threads
+ for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+ scheduler->wake(get_thread(*rit));
+ }
+ waiters->clear();
+ //check whether we should go to sleep or not...simulate spurious failures
+ if (curr->get_node()->get_misc() == 0) {
+ get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
+ //disable us
+ scheduler->sleep(get_thread(curr));
+ }
+ break;
+ }
+ case ATOMIC_NOTIFY_ALL: {
+ action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
+ //activate all the waiting threads
+ for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+ scheduler->wake(get_thread(*rit));
+ }
+ waiters->clear();
+ break;
+ }
+ case ATOMIC_NOTIFY_ONE: {
+ action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
+ int wakeupthread = curr->get_node()->get_misc();
+ action_list_t::iterator it = waiters->begin();
+ advance(it, wakeupthread);
+ scheduler->wake(get_thread(*it));
+ waiters->erase(it);
+ break;
+ }
+
+ default:
+ ASSERT(0);
+ }
+ return false;
+}
+
+void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
+{
+ /* Do more ambitious checks now that mo is more complete */
+ if (mo_may_allow(writer, reader)) {
+ Node *node = reader->get_node();
+
+ /* Find an ancestor thread which exists at the time of the reader */
+ Thread *write_thread = get_thread(writer);
+ while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
+ write_thread = write_thread->get_parent();
+
+ struct future_value fv = {
+ writer->get_value(),
+ writer->get_seq_number() + params.maxfuturedelay,
+ write_thread->get_id(),
+ };
+ if (node->add_future_value(fv))
+ set_latest_backtrack(reader);
+ }
+}
+
+/**
+ * Process a write ModelAction
+ * @param curr The ModelAction to process
+ * @return True if the mo_graph was updated or promises were resolved
+ */
+bool ModelChecker::process_write(ModelAction *curr)
+{
+ bool updated_mod_order = w_modification_order(curr);
+ bool updated_promises = resolve_promises(curr);
+
+ if (promises->size() == 0) {
+ for (unsigned int i = 0; i < futurevalues->size(); i++) {
+ struct PendingFutureValue pfv = (*futurevalues)[i];
+ add_future_value(pfv.writer, pfv.act);
+ }
+ futurevalues->clear();
+ }
+
+ mo_graph->commitChanges();
+ mo_check_promises(curr->get_tid(), curr, NULL);
+
+ get_thread(curr)->set_return_value(VALUE_NONE);
+ return updated_mod_order || updated_promises;
+}
+
+/**
+ * Process a fence ModelAction
+ * @param curr The ModelAction to process
+ * @return True if synchronization was updated
+ */
+bool ModelChecker::process_fence(ModelAction *curr)
+{
+ /*
+ * fence-relaxed: no-op
+ * fence-release: only log the occurence (not in this function), for
+ * use in later synchronization
+ * fence-acquire (this function): search for hypothetical release
+ * sequences
+ */
+ bool updated = false;
+ if (curr->is_acquire()) {
+ action_list_t *list = action_trace;
+ action_list_t::reverse_iterator rit;
+ /* Find X : is_read(X) && X --sb-> curr */
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+ if (act == curr)
+ continue;
+ if (act->get_tid() != curr->get_tid())
+ continue;
+ /* Stop at the beginning of the thread */
+ if (act->is_thread_start())
+ break;
+ /* Stop once we reach a prior fence-acquire */
+ if (act->is_fence() && act->is_acquire())
+ break;
+ if (!act->is_read())
+ continue;
+ /* read-acquire will find its own release sequences */
+ if (act->is_acquire())
+ continue;
+
+ /* Establish hypothetical release sequences */
+ rel_heads_list_t release_heads;
+ get_release_seq_heads(curr, act, &release_heads);
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ if (!curr->synchronize_with(release_heads[i]))
+ set_bad_synchronization();
+ if (release_heads.size() != 0)
+ updated = true;
+ }
+ }
+ return updated;
+}
+
+/**
+ * @brief Process the current action for thread-related activity
+ *
+ * Performs current-action processing for a THREAD_* ModelAction. Proccesses
+ * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
+ * synchronization, etc. This function is a no-op for non-THREAD actions
+ * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
+ *
+ * @param curr The current action
+ * @return True if synchronization was updated or a thread completed
+ */
+bool ModelChecker::process_thread_action(ModelAction *curr)
+{
+ bool updated = false;
+
+ switch (curr->get_type()) {
+ case THREAD_CREATE: {
+ Thread *th = curr->get_thread_operand();
+ th->set_creation(curr);
+ /* Promises can be satisfied by children */
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ if (promise->thread_is_available(curr->get_tid()))
+ promise->add_thread(th->get_id());
+ }
+ break;
+ }
+ case THREAD_JOIN: {
+ Thread *blocking = curr->get_thread_operand();
+ ModelAction *act = get_last_action(blocking->get_id());
+ curr->synchronize_with(act);
+ updated = true; /* trigger rel-seq checks */
+ break;
+ }
+ case THREAD_FINISH: {
+ Thread *th = get_thread(curr);
+ while (!th->wait_list_empty()) {
+ ModelAction *act = th->pop_wait_list();
+ scheduler->wake(get_thread(act));
+ }
+ th->complete();
+ /* Completed thread can't satisfy promises */
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ if (promise->thread_is_available(th->get_id()))
+ if (promise->eliminate_thread(th->get_id()))
+ priv->failed_promise = true;
+ }
+ updated = true; /* trigger rel-seq checks */
+ break;
+ }
+ case THREAD_START: {
+ check_promises(curr->get_tid(), NULL, curr->get_cv());
+ break;
+ }
+ default:
+ break;
+ }
+
+ return updated;
+}
+
+/**
+ * @brief Process the current action for release sequence fixup activity
+ *
+ * Performs model-checker release sequence fixups for the current action,
+ * forcing a single pending release sequence to break (with a given, potential
+ * "loose" write) or to complete (i.e., synchronize). If a pending release
+ * sequence forms a complete release sequence, then we must perform the fixup
+ * synchronization, mo_graph additions, etc.
+ *
+ * @param curr The current action; must be a release sequence fixup action
+ * @param work_queue The work queue to which to add work items as they are
+ * generated
+ */
+void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
+{
+ const ModelAction *write = curr->get_node()->get_relseq_break();
+ struct release_seq *sequence = pending_rel_seqs->back();
+ pending_rel_seqs->pop_back();
+ ASSERT(sequence);
+ ModelAction *acquire = sequence->acquire;
+ const ModelAction *rf = sequence->rf;
+ const ModelAction *release = sequence->release;
+ ASSERT(acquire);
+ ASSERT(release);
+ ASSERT(rf);
+ ASSERT(release->same_thread(rf));
+
+ if (write == NULL) {
+ /**
+ * @todo Forcing a synchronization requires that we set
+ * modification order constraints. For instance, we can't allow
+ * a fixup sequence in which two separate read-acquire
+ * operations read from the same sequence, where the first one
+ * synchronizes and the other doesn't. Essentially, we can't
+ * allow any writes to insert themselves between 'release' and
+ * 'rf'
+ */
+
+ /* Must synchronize */
+ if (!acquire->synchronize_with(release)) {
+ set_bad_synchronization();
+ return;
+ }
+ /* Re-check all pending release sequences */
+ work_queue->push_back(CheckRelSeqWorkEntry(NULL));
+ /* Re-check act for mo_graph edges */
+ work_queue->push_back(MOEdgeWorkEntry(acquire));
+
+ /* propagate synchronization to later actions */
+ action_list_t::reverse_iterator rit = action_trace->rbegin();
+ for (; (*rit) != acquire; rit++) {
+ ModelAction *propagate = *rit;
+ if (acquire->happens_before(propagate)) {
+ propagate->synchronize_with(acquire);
+ /* Re-check 'propagate' for mo_graph edges */
+ work_queue->push_back(MOEdgeWorkEntry(propagate));
+ }