+/**
+ * @brief Find the last backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking. This primary includes pairs of
+ * synchronizing actions which should be explored in the opposite execution
+ * order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act
+ */
+ModelAction * ModelChecker::get_last_conflict(ModelAction *act) const
+{
+ switch (act->get_type()) {
+ /* case ATOMIC_FENCE: fences don't directly cause backtracking */
+ case ATOMIC_READ:
+ case ATOMIC_WRITE:
+ case ATOMIC_RMW: {
+ ModelAction *ret = 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)) {
+ ret = prev;
+ break;
+ }
+ }
+
+ ModelAction *ret2 = get_last_fence_conflict(act);
+ if (!ret2)
+ return ret;
+ if (!ret)
+ return ret2;
+ if (*ret < *ret2)
+ return ret2;
+ return ret;
+ }
+ 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();
+
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
+ 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;
+
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
+ /* 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;
+ }
+
+ /* See if CHESS-like yield fairness allows */
+ if (model->params.yieldon) {
+ 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_over(tid, 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 model action.
+ * @param curr is the read model action to process.
+ * @return True if processing this read updates the mo_graph.
+ */
+bool ModelChecker::process_read(ModelAction *curr)
+{
+ Node *node = curr->get_node();
+ while (true) {
+ bool updated = false;
+ switch (node->get_read_from_status()) {
+ case READ_FROM_PAST: {
+ const ModelAction *rf = node->get_read_from_past();
+ ASSERT(rf);
+
+ mo_graph->startChanges();
+
+ ASSERT(!is_infeasible());
+ if (!check_recency(curr, rf)) {
+ if (node->increment_read_from()) {
+ mo_graph->rollbackChanges();
+ continue;
+ } else {
+ priv->too_many_reads = true;
+ }
+ }
+
+ updated = r_modification_order(curr, rf);
+ read_from(curr, rf);
+ mo_graph->commitChanges();
+ mo_check_promises(curr, true);
+ break;
+ }
+ case READ_FROM_PROMISE: {
+ Promise *promise = curr->get_node()->get_read_from_promise();
+ if (promise->add_reader(curr))
+ priv->failed_promise = true;
+ curr->set_read_from_promise(promise);
+ mo_graph->startChanges();
+ if (!check_recency(curr, promise))
+ priv->too_many_reads = true;
+ updated = r_modification_order(curr, promise);
+ mo_graph->commitChanges();
+ break;
+ }
+ case READ_FROM_FUTURE: {
+ /* Read from future value */
+ struct future_value fv = node->get_future_value();
+ Promise *promise = new Promise(curr, fv);
+ curr->set_read_from_promise(promise);
+ promises->push_back(promise);
+ mo_graph->startChanges();
+ updated = r_modification_order(curr, promise);
+ mo_graph->commitChanges();
+ break;
+ }
+ default:
+ ASSERT(false);
+ }
+ get_thread(curr)->set_return_value(curr->get_return_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 = curr->get_mutex();
+ struct std::mutex_state *state = NULL;
+
+ if (mutex)
+ state = mutex->get_state();
+
+ switch (curr->get_type()) {
+ case ATOMIC_TRYLOCK: {
+ bool success = !state->locked;
+ 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->locked = get_thread(curr);
+ ModelAction *unlock = get_last_unlock(curr);
+ //synchronize with the previous unlock statement
+ if (unlock != NULL) {
+ curr->synchronize_with(unlock);
+ return true;
+ }
+ break;
+ }
+ case ATOMIC_WAIT:
+ case ATOMIC_UNLOCK: {
+ /* wake up the other threads */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *t = get_thread(int_to_id(i));
+ Thread *curr_thrd = get_thread(curr);
+ if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+ scheduler->wake(t);
+ }
+
+ /* unlock the lock - after checking who was waiting on it */
+ state->locked = NULL;
+
+ if (!curr->is_wait())
+ break; /* The rest is only for ATOMIC_WAIT */
+
+ /* Should we go to sleep? (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;
+}
+
+/**
+ * @brief Check if the current pending promises allow a future value to be sent
+ *
+ * If one of the following is true:
+ * (a) there are no pending promises
+ * (b) the reader and writer do not cross any promises
+ * Then, it is safe to pass a future value back now.
+ *
+ * Otherwise, we must save the pending future value until (a) or (b) is true
+ *
+ * @param writer The operation which sends the future value. Must be a write.
+ * @param reader The operation which will observe the value. Must be a read.
+ * @return True if the future value can be sent now; false if it must wait.
+ */
+bool ModelChecker::promises_may_allow(const ModelAction *writer,
+ const ModelAction *reader) const
+{
+ if (promises->empty())
+ return true;
+ for(int i=promises->size()-1;i>=0;i--) {
+ ModelAction *pr=(*promises)[i]->get_reader(0);
+ //reader is after promise...doesn't cross any promise
+ if (*reader > *pr)
+ return true;
+ //writer is after promise, reader before...bad...
+ if (*writer > *pr)
+ return false;
+ }
+ return true;
+}
+
+/**
+ * @brief Add a future value to a reader
+ *
+ * This function performs a few additional checks to ensure that the future
+ * value can be feasibly observed by the reader
+ *
+ * @param writer The operation whose value is sent. Must be a write.
+ * @param reader The read operation which may read the future value. Must be a read.
+ */
+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))
+ return;
+
+ 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_write_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)
+{
+ /* Readers to which we may send our future value */
+ ModelVector<ModelAction *> send_fv;
+
+ const ModelAction *earliest_promise_reader;
+ bool updated_promises = false;
+
+ bool updated_mod_order = w_modification_order(curr, &send_fv);
+ Promise *promise = pop_promise_to_resolve(curr);
+
+ if (promise) {
+ earliest_promise_reader = promise->get_reader(0);
+ updated_promises = resolve_promise(curr, promise);
+ } else
+ earliest_promise_reader = NULL;
+
+ for (unsigned int i = 0; i < send_fv.size(); i++) {
+ ModelAction *read = send_fv[i];
+
+ /* Don't send future values to reads after the Promise we resolve */
+ if (!earliest_promise_reader || *read < *earliest_promise_reader) {
+ /* Check if future value can be sent immediately */
+ if (promises_may_allow(curr, read)) {
+ add_future_value(curr, read);
+ } else {
+ futurevalues->push_back(PendingFutureValue(curr, read));
+ }
+ }
+ }
+
+ /* Check the pending future values */
+ for (int i = (int)futurevalues->size() - 1; i >= 0; i--) {
+ struct PendingFutureValue pfv = (*futurevalues)[i];
+ if (promises_may_allow(pfv.writer, pfv.reader)) {
+ add_future_value(pfv.writer, pfv.reader);
+ futurevalues->erase(futurevalues->begin() + i);
+ }
+ }
+
+ mo_graph->commitChanges();
+ mo_check_promises(curr, false);
+
+ 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
+ * fence-seq-cst: MO constraints formed in {r,w}_modification_order
+ */
+ 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: {
+ thrd_t *thrd = (thrd_t *)curr->get_location();
+ struct thread_params *params = (struct thread_params *)curr->get_value();
+ Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr));
+ add_thread(th);
+ 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);
+ /* Wake up any joining threads */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *waiting = get_thread(int_to_id(i));
+ if (waiting->waiting_on() == th &&
+ waiting->get_pending()->is_thread_join())
+ scheduler->wake(waiting);
+ }
+ 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));
+ }
+ }
+ } else {
+ /* Break release sequence with new edges:
+ * release --mo--> write --mo--> rf */
+ mo_graph->addEdge(release, write);
+ mo_graph->addEdge(write, rf);
+ }
+
+ /* See if we have realized a data race */
+ checkDataRaces();
+}
+
+/**
+ * Initialize the current action by performing one or more of the following
+ * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
+ * in the NodeStack, manipulating backtracking sets, allocating and
+ * initializing clock vectors, and computing the promises to fulfill.
+ *
+ * @param curr The current action, as passed from the user context; may be
+ * freed/invalidated after the execution of this function, with a different
+ * action "returned" its place (pass-by-reference)
+ * @return True if curr is a newly-explored action; false otherwise
+ */
+bool ModelChecker::initialize_curr_action(ModelAction **curr)
+{
+ ModelAction *newcurr;
+
+ if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
+ newcurr = process_rmw(*curr);
+ delete *curr;
+
+ if (newcurr->is_rmw())
+ compute_promises(newcurr);
+
+ *curr = newcurr;
+ return false;
+ }
+
+ (*curr)->set_seq_number(get_next_seq_num());
+
+ newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
+ if (newcurr) {
+ /* First restore type and order in case of RMW operation */
+ if ((*curr)->is_rmwr())
+ newcurr->copy_typeandorder(*curr);
+
+ ASSERT((*curr)->get_location() == newcurr->get_location());
+ newcurr->copy_from_new(*curr);
+
+ /* Discard duplicate ModelAction; use action from NodeStack */
+ delete *curr;
+
+ /* Always compute new clock vector */
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ *curr = newcurr;
+ return false; /* Action was explored previously */
+ } else {
+ newcurr = *curr;
+
+ /* Always compute new clock vector */
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ /* Assign most recent release fence */
+ newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
+
+ /*
+ * Perform one-time actions when pushing new ModelAction onto
+ * NodeStack
+ */
+ if (newcurr->is_write())
+ compute_promises(newcurr);
+ else if (newcurr->is_relseq_fixup())
+ compute_relseq_breakwrites(newcurr);
+ else if (newcurr->is_wait())
+ newcurr->get_node()->set_misc_max(2);
+ else if (newcurr->is_notify_one()) {
+ newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
+ }
+ return true; /* This was a new ModelAction */
+ }
+}
+
+/**
+ * @brief Establish reads-from relation between two actions
+ *
+ * Perform basic operations involved with establishing a concrete rf relation,
+ * including setting the ModelAction data and checking for release sequences.
+ *
+ * @param act The action that is reading (must be a read)
+ * @param rf The action from which we are reading (must be a write)
+ *
+ * @return True if this read established synchronization
+ */
+bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
+{
+ ASSERT(rf);
+ ASSERT(rf->is_write());
+
+ act->set_read_from(rf);
+ if (act->is_acquire()) {
+ rel_heads_list_t release_heads;
+ get_release_seq_heads(act, act, &release_heads);
+ int num_heads = release_heads.size();
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ if (!act->synchronize_with(release_heads[i])) {
+ set_bad_synchronization();
+ num_heads--;