+/**
+ * @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)
+{
+ act->set_read_from(rf);
+ if (rf != NULL && 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--;
+ }
+ return num_heads > 0;
+ }
+ return false;
+}
+
+/**
+ * @brief Check whether a model action is enabled.
+ *
+ * Checks whether a lock or join operation would be successful (i.e., is the
+ * lock already locked, or is the joined thread already complete). If not, put
+ * the action in a waiter list.
+ *
+ * @param curr is the ModelAction to check whether it is enabled.
+ * @return a bool that indicates whether the action is enabled.
+ */
+bool ModelChecker::check_action_enabled(ModelAction *curr) {
+ if (curr->is_lock()) {
+ std::mutex *lock = (std::mutex *)curr->get_location();
+ struct std::mutex_state *state = lock->get_state();
+ if (state->islocked) {
+ //Stick the action in the appropriate waiting queue
+ get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
+ return false;