model: wire up rest of release seq. resolution backtracking

I still need to actually initiate the special ModelAction fixups.

diff --git a/model.cc b/model.cc
index 6eaf65606b6fbfb96f79946836bfae5da2db7b2c..e46a18cb8e2f6132706e52a8f9312abd82e672be 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -163,6 +163,10 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        /* The next node will try to read from a different future value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
+               } else if (nextnode->increment_relseq_break()) {
+                       /* The next node will try to resolve a release sequence differently */
+                       tid = next->get_tid();
+                       node_stack->pop_restofstack(2);
                } else {
                        /* Make a different thread execute for next step */
                        Node *node = nextnode->get_parent();
@@ -591,6 +595,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                 */
                if (newcurr->is_write())
                        compute_promises(newcurr);
+               else if (newcurr->is_relseq_fixup())
+                       compute_relseq_breakwrites(newcurr);
        }
        return newcurr;
 }
@@ -740,7 +746,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        if ((!parnode->backtrack_empty() ||
                         !currnode->read_from_empty() ||
                         !currnode->future_value_empty() ||
-                        !currnode->promise_empty())
+                        !currnode->promise_empty() ||
+                        !currnode->relseq_break_empty())
                        && (!priv->next_backtrack ||
                                        *curr > *priv->next_backtrack)) {
                priv->next_backtrack = curr;
@@ -1652,6 +1659,29 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
        }
 }
 
+/**
+ * Compute the set of writes that may break the current pending release
+ * sequence. This information is extracted from previou release sequence
+ * calculations.
+ *
+ * @param curr The current ModelAction. Must be a release sequence fixup
+ * action.
+ */
+void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
+{
+       if (pending_rel_seqs->empty())
+               return;
+
+       struct release_seq *pending = pending_rel_seqs->back();
+       for (unsigned int i = 0; i < pending->writes.size(); i++) {
+               const ModelAction *write = pending->writes[i];
+               curr->get_node()->add_relseq_break(write);
+       }
+
+       /* NULL means don't break the sequence; just synchronize */
+       curr->get_node()->add_relseq_break(NULL);
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from. This set is determined by the clock vector's "happens before"

diff --git a/model.h b/model.h
index d5dc42266769004d542d72f472f6e1029c1a7e5c..a8268cf8740c05fe32c86fe213b9f1d4d095f178 100644 (file)
--- a/model.h
+++ b/model.h
@@ -152,6 +152,7 @@ private:
        void reset_to_initial_state();
        bool resolve_promises(ModelAction *curr);
        void compute_promises(ModelAction *curr);
+       void compute_relseq_breakwrites(ModelAction *curr);
 
        void check_curr_backtracking(ModelAction * curr);
        void add_action_to_lists(ModelAction *act);