nodestack: add read_from_promises backtracking

This is just the basic framework for now. I still need to hook it up for
actual use in ModelChecker.

diff --git a/nodestack.cc b/nodestack.cc
index 730c702443e3f5a1e50e91606c314f3c76b8a66a..3cde3456bb9363bc08f2549035166b6f7fe3bd15 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -36,6 +36,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
        enabled_array(NULL),
        read_from_past(),
        read_from_past_idx(0),
+       read_from_promises(),
+       read_from_promise_idx(-1),
        future_values(),
        future_index(-1),
        relseq_break_writes(),
@@ -105,6 +107,11 @@ void Node::print() const
                model_print("[%d]", read_from_past[i]->get_seq_number());
        model_print("\n");
 
+       model_print("          read-from promises: %s", read_from_promise_empty() ? "empty" : "non-empty ");
+       for (int i = read_from_promise_idx + 1; i < (int)read_from_promises.size(); i++)
+               model_print("[%d]", read_from_promises[i]->get_seq_number());
+       model_print("\n");
+
        model_print("          future values: %s", future_value_empty() ? "empty" : "non-empty ");
        for (int i = future_index + 1; i < (int)future_values.size(); i++)
                model_print("[%#" PRIx64 "]", future_values[i].value);
@@ -342,6 +349,9 @@ bool Node::increment_read_from()
        if (increment_read_from_past()) {
               read_from_status = READ_FROM_PAST;
               return true;
+       } else if (increment_read_from_promise()) {
+               read_from_status = READ_FROM_PROMISE;
+               return true;
        } else if (increment_future_value()) {
                read_from_status = READ_FROM_FUTURE;
                return true;
@@ -436,6 +446,55 @@ bool Node::increment_read_from_past()
 
 /************************** end read from past ********************************/
 
+/***************************** read_from_promises *****************************/
+
+/**
+ * Add an action to the read_from_promises set.
+ * @param reader The read which generated the Promise; we use the ModelAction
+ * instead of the Promise because the Promise does not last across executions
+ */
+void Node::add_read_from_promise(const ModelAction *reader)
+{
+       read_from_promises.push_back(reader);
+}
+
+/**
+ * Gets the next 'read-from-promise' from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @return The current element in read_from_promises
+ */
+const Promise * Node::get_read_from_promise() const
+{
+       if (read_from_promise_idx < 0 || read_from_promise_idx >= ((int)read_from_promises.size()))
+               return NULL;
+       return read_from_promises[read_from_promise_idx]->get_reads_from_promise();
+}
+
+/**
+ * Checks whether the read_from_promises set for this node is empty.
+ * @return true if the read_from_promises set is empty.
+ */
+bool Node::read_from_promise_empty() const
+{
+       return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size()));
+}
+
+/**
+ * Increments the index into the read_from_promises set to explore the next item.
+ * @return Returns false if we have explored all promises.
+ */
+bool Node::increment_read_from_promise()
+{
+       DBG();
+       if (read_from_promise_idx < ((int)read_from_promises.size())) {
+               read_from_promise_idx++;
+               return (read_from_promise_idx < ((int)read_from_promises.size()));
+       }
+       return false;
+}
+
+/************************* end read_from_promises *****************************/
+
 /****************************** future values *********************************/
 
 /**

diff --git a/nodestack.h b/nodestack.h
index a857084ba1fe8676b0b2c5b8e57fc8a873a77bc0..8a20c45cb2c03e53bdeaf53ee8e80a89b3882014 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -40,6 +40,7 @@ struct fairness_info {
 
 typedef enum {
        READ_FROM_PAST,
+       READ_FROM_PROMISE,
        READ_FROM_FUTURE,
        READ_FROM_NONE,
 } read_from_type_t;
@@ -89,6 +90,9 @@ public:
        const ModelAction * get_read_from_past(int i) const;
        int get_read_from_past_size() const;
 
+       void add_read_from_promise(const ModelAction *reader);
+       const Promise * get_read_from_promise() const;
+
        bool add_future_value(struct future_value fv);
        struct future_value get_future_value() const;
 
@@ -116,6 +120,8 @@ private:
 
        bool read_from_past_empty() const;
        bool increment_read_from_past();
+       bool read_from_promise_empty() const;
+       bool increment_read_from_promise();
        bool future_value_empty() const;
        bool increment_future_value();
        read_from_type_t read_from_status;
@@ -136,6 +142,9 @@ private:
        std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > read_from_past;
        unsigned int read_from_past_idx;
 
+       std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > read_from_promises;
+       int read_from_promise_idx;
+
        std::vector< struct future_value, ModelAlloc<struct future_value> > future_values;
        std::vector< promise_t, ModelAlloc<promise_t> > promises;
        int future_index;