+/** @returns whether the current partial trace is feasible. */
+bool ModelChecker::isfeasible() {
+ return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
+}
+
+/** @returns whether the current partial trace is feasible other than
+ * multiple RMW reading from the same store. */
+bool ModelChecker::isfeasibleotherthanRMW() {
+ return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
+}
+
+/** Returns whether the current completed trace is feasible. */
+bool ModelChecker::isfinalfeasible() {
+ return isfeasible() && promises->size() == 0;
+}
+
+/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
+ModelAction * ModelChecker::process_rmw(ModelAction *act) {
+ int tid = id_to_int(act->get_tid());
+ ModelAction *lastread = get_last_action(tid);
+ lastread->process_rmw(act);
+ if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
+ mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+ mo_graph->commitChanges();
+ }
+ return lastread;
+}
+
+/**
+ * Checks whether a thread has read from the same write for too many times
+ * without seeing the effects of a later write.
+ *
+ * Basic idea:
+ * 1) there must a different write that we could read from that would satisfy the modification order,
+ * 2) we must have read from the same value in excess of maxreads times, and
+ * 3) that other write must have been in the reads_from set for maxreads times.
+ *
+ * If so, we decide that the execution is no longer feasible.
+ */
+void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
+ if (params.maxreads != 0) {
+ if (curr->get_node()->get_read_from_size() <= 1)
+ return;
+
+ //Must make sure that execution is currently feasible... We could
+ //accidentally clear by rolling back
+ if (!isfeasible())
+ return;
+
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ int tid = id_to_int(curr->get_tid());
+
+ /* Skip checks */
+ if ((int)thrd_lists->size() <= tid)
+ return;
+
+ action_list_t *list = &(*thrd_lists)[tid];
+
+ action_list_t::reverse_iterator rit = list->rbegin();
+ /* Skip past curr */
+ if (already_added) {
+ for (; (*rit) != curr; rit++)
+ ;
+ /* go past curr now */
+ rit++;
+ }
+
+ action_list_t::reverse_iterator ritcopy = rit;
+ //See if we have enough reads from the same value
+ int count = 0;
+ for (; count < params.maxreads; rit++,count++) {
+ if (rit==list->rend())
+ return;
+ ModelAction *act = *rit;
+ if (!act->is_read())
+ return;
+ if (act->get_reads_from() != curr->get_reads_from())
+ return;
+ if (act->get_node()->get_read_from_size() <= 1)
+ return;
+ }
+
+ for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
+ //Get write
+ const ModelAction * write = curr->get_node()->get_read_from_at(i);
+ //Need a different write
+ if (write==curr->get_reads_from())
+ continue;
+
+ /* Test to see whether this is a feasible write to read from*/
+ mo_graph->startChanges();
+ r_modification_order(curr, write);
+ bool feasiblereadfrom = isfeasible();
+ mo_graph->rollbackChanges();
+
+ if (!feasiblereadfrom)
+ continue;
+ rit = ritcopy;
+
+ bool feasiblewrite = true;
+ //new we need to see if this write works for everyone
+
+ for (int loop = count; loop>0; loop--,rit++) {
+ ModelAction *act=*rit;
+ bool foundvalue = false;
+ for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
+ if (act->get_node()->get_read_from_at(i)==write) {
+ foundvalue = true;
+ break;
+ }
+ }
+ if (!foundvalue) {
+ feasiblewrite = false;
+ break;
+ }
+ }
+ if (feasiblewrite) {
+ too_many_reads = true;
+ return;
+ }
+ }
+ }
+}
+
+/**
+ * Updates the mo_graph with the constraints imposed from the current
+ * read.
+ *
+ * Basic idea is the following: Go through each other thread and find
+ * the lastest action that happened before our read. Two cases:
+ *
+ * (1) The action is a write => that write must either occur before
+ * the write we read from or be the write we read from.
+ *
+ * (2) The action is a read => the write that that action read from
+ * must occur before the write we read from or be the same write.
+ *
+ * @param curr The current action. Must be a read.
+ * @param rf The action that curr reads from. Must be a write.
+ * @return True if modification order edges were added; false otherwise
+ */
+bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)