+
+ /* Deal with new thread */
+ if (curr->get_type() == THREAD_START)
+ check_promises(NULL, curr->get_cv());
+
+ /* Assign reads_from values */
+ Thread *th = get_thread(curr->get_tid());
+ uint64_t value = VALUE_NONE;
+ bool updated = false;
+ if (curr->is_read()) {
+ while(true) {
+ const ModelAction *reads_from = curr->get_node()->get_read_from();
+ if (reads_from != NULL) {
+ value = reads_from->get_value();
+ /* Assign reads_from, perform release/acquire synchronization */
+ curr->read_from(reads_from);
+ if (!already_added)
+ check_recency(curr,false);
+
+ bool r_status=r_modification_order(curr,reads_from);
+
+ if (!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
+ mo_graph->rollbackChanges();
+ too_many_reads=false;
+ continue;
+ }
+
+ mo_graph->commitChanges();
+ updated |= r_status;
+ } else {
+ /* Read from future value */
+ value = curr->get_node()->get_future_value();
+ curr->read_from(NULL);
+ Promise *valuepromise = new Promise(curr, value);
+ promises->push_back(valuepromise);
+ }
+ break;
+ }
+ } else if (curr->is_write()) {
+ if (w_modification_order(curr))
+ updated = true;
+ if (resolve_promises(curr))
+ updated = true;
+ mo_graph->commitChanges();
+ }
+
+ if (updated)
+ resolve_release_sequences(curr->get_location());
+
+ th->set_return_value(value);
+
+ /* Add action to list. */
+ if (!already_added)
+ add_action_to_lists(curr);
+
+ Node *currnode = curr->get_node();
+ Node *parnode = currnode->get_parent();
+
+ if (!parnode->backtrack_empty() || !currnode->read_from_empty() ||
+ !currnode->future_value_empty() || !currnode->promise_empty())
+ if (!priv->next_backtrack || *curr > *priv->next_backtrack)
+ priv->next_backtrack = curr;
+
+ set_backtracking(curr);
+
+ /* Do not split atomic actions. */
+ if (curr->is_rmwr())
+ return thread_current();
+ /* The THREAD_CREATE action points to the created Thread */
+ else if (curr->get_type() == THREAD_CREATE)
+ return (Thread *)curr->get_location();
+ else
+ return get_next_replay_thread();
+}
+
+/** @returns whether the current partial trace must be a prefix of a
+ * feasible trace. */
+bool ModelChecker::isfeasibleprefix() {
+ return promises->size() == 0 && *lazy_sync_size == 0;
+}
+
+/** @returns whether the current partial trace is feasible. */
+bool ModelChecker::isfeasible() {
+ return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads;
+}
+
+/** Returns whether the current completed trace is feasible. */
+bool ModelChecker::isfinalfeasible() {
+ return isfeasible() && promises->size() == 0;