+/** @returns whether the current partial trace is feasible. */
+bool ModelChecker::isfeasible() {
+ return !cyclegraph->checkForCycles() && !failed_promise;
+}
+
+/** 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())
+ cyclegraph->addRMWEdge(lastread, lastread->get_reads_from());
+ return lastread;
+}
+
+/**
+ * Updates the cyclegraph with the constraints imposed from the current read.
+ * @param curr The current action. Must be a read.
+ * @param rf The action that curr reads from. Must be a write.
+ */
+void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+ unsigned int i;
+ ASSERT(curr->is_read());
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+
+ /* Include at most one act per-thread that "happens before" curr */
+ if (act->happens_before(curr)) {
+ if (act->is_read()) {
+ const ModelAction * prevreadfrom = act->get_reads_from();
+ if (prevreadfrom != NULL && rf != prevreadfrom)
+ cyclegraph->addEdge(rf, prevreadfrom);
+ } else if (rf != act) {
+ cyclegraph->addEdge(rf, act);
+ }
+ break;
+ }
+ }
+ }
+}
+
+/** Updates the cyclegraph with the constraints imposed from the
+ * current read. */
+void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelAction *rf) {
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+ unsigned int i;
+ ASSERT(curr->is_read());
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ ModelAction *lastact = NULL;
+
+ /* Find last action that happens after curr */
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+ if (curr->happens_before(act)) {
+ lastact = act;
+ } else
+ break;
+ }
+
+ /* Include at most one act per-thread that "happens before" curr */
+ if (lastact != NULL) {
+ if (lastact->is_read()) {
+ const ModelAction * postreadfrom = lastact->get_reads_from();
+ if (postreadfrom != NULL&&rf != postreadfrom)
+ cyclegraph->addEdge(postreadfrom, rf);
+ } else if (rf != lastact) {
+ cyclegraph->addEdge(lastact, rf);
+ }
+ break;
+ }
+ }
+}
+
+/**
+ * Updates the cyclegraph with the constraints imposed from the current write.
+ * @param curr The current action. Must be a write.
+ */
+void ModelChecker::w_modification_order(ModelAction * curr) {
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+ unsigned int i;
+ ASSERT(curr->is_write());
+
+ if (curr->is_seqcst()) {
+ /* We have to at least see the last sequentially consistent write,
+ so we are initialized. */
+ ModelAction * last_seq_cst = get_last_seq_cst(curr->get_location());
+ if (last_seq_cst != NULL)
+ cyclegraph->addEdge(curr, last_seq_cst);
+ }
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+
+ /* Include at most one act per-thread that "happens before" curr */
+ if (act->happens_before(curr)) {
+ if (act->is_read())
+ cyclegraph->addEdge(curr, act->get_reads_from());
+ else
+ cyclegraph->addEdge(curr, act);
+ break;
+ } else if (act->is_read() && !act->is_synchronizing(curr) &&
+ !act->same_thread(curr)) {
+ /* We have an action that:
+ (1) did not happen before us
+ (2) is a read and we are a write
+ (3) cannot synchronize with us
+ (4) is in a different thread
+ =>
+ that read could potentially read from our write.
+ */
+ if (act->get_node()->add_future_value(curr->get_value()) &&
+ (!next_backtrack || *act > *next_backtrack))
+ next_backtrack = act;
+ }
+ }
+ }
+}
+
+/**
+ * Performs various bookkeeping operations for the current ModelAction. For
+ * instance, adds action to the per-object, per-thread action vector and to the
+ * action trace list of all thread actions.
+ *
+ * @param act is the ModelAction to add.
+ */
+void ModelChecker::add_action_to_lists(ModelAction *act)