+/**
+ * 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;
+ 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);
+ r_status = r_modification_order(curr, reads_from);
+ }
+
+
+ if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
+ mo_graph->rollbackChanges();
+ too_many_reads = false;
+ continue;
+ }
+
+ curr->read_from(reads_from);
+ mo_graph->commitChanges();
+ updated |= r_status;
+ } else if (!second_part_of_rmw) {
+ /* Read from future value */
+ value = curr->get_node()->get_future_value();
+ modelclock_t expiration = curr->get_node()->get_future_value_expiration();
+ curr->read_from(NULL);
+ Promise *valuepromise = new Promise(curr, value, expiration);
+ promises->push_back(valuepromise);
+ }
+ get_thread(curr)->set_return_value(value);
+ return updated;
+ }
+}
+
+/**
+ * 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];
+ if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
+ (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
+ priv->next_backtrack = pfv.act;
+ }
+ futurevalues->resize(0);
+ }
+
+ mo_graph->commitChanges();
+ get_thread(curr)->set_return_value(VALUE_NONE);
+ return updated_mod_order || updated_promises;
+}
+
+ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
+{
+ ModelAction *newcurr;
+
+ if (curr->is_rmwc() || curr->is_rmw()) {
+ newcurr = process_rmw(curr);
+ delete curr;
+ compute_promises(newcurr);
+ return newcurr;
+ }
+
+ newcurr = node_stack->explore_action(curr);
+ if (newcurr) {
+ /* First restore type and order in case of RMW operation */
+ if (curr->is_rmwr())
+ newcurr->copy_typeandorder(curr);
+
+ /* Discard duplicate ModelAction; use action from NodeStack */
+ delete curr;
+
+ /* If we have diverged, we need to reset the clock vector. */
+ if (diverge == NULL)
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+ } else {
+ newcurr = curr;
+ /*
+ * Perform one-time actions when pushing new ModelAction onto
+ * NodeStack
+ */
+ curr->create_cv(get_parent_action(curr->get_tid()));
+ if (curr->is_read())
+ build_reads_from_past(curr);
+ if (curr->is_write())
+ compute_promises(curr);
+ }
+ return newcurr;
+}
+