model: schedule appropriate fence backtracking points

[c11tester.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index ec72def002838b97429d3a27a99e0fd3825aecc0..b2ef73cac30108fab56745f89b0542a186fc6410 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -1,3 +1,6 @@
+#define __STDC_FORMAT_MACROS
+#include <inttypes.h>
+
 #include <string.h>
 
 #include "nodestack.h"
@@ -5,6 +8,7 @@
 #include "common.h"
 #include "model.h"
 #include "threads-model.h"
+#include "modeltypes.h"
 
 /**
  * @brief Node constructor
@@ -86,16 +90,24 @@ Node::~Node()
 }
 
 /** Prints debugging info for the ModelAction associated with this Node */
-void Node::print()
+void Node::print() const
 {
        action->print();
-       model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty");
+       model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
        for (int i = 0; i < (int)backtrack.size(); i++)
                if (backtrack[i] == true)
                        model_print("[%d]", i);
        model_print("\n");
-       model_print("          future values: %s\n", future_value_empty() ? "empty" : "non-empty");
-       model_print("          read-from: %s\n", read_from_empty() ? "empty" : "non-empty");
+       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);
+       model_print("\n");
+
+       model_print("          read-from: %s", read_from_empty() ? "empty" : "non-empty ");
+       for (int i = read_from_index + 1; i < (int)may_read_from.size(); i++)
+               model_print("[%d]", may_read_from[i]->get_seq_number());
+       model_print("\n");
+
        model_print("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
        model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
        model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
@@ -152,7 +164,7 @@ bool Node::increment_promise()
                                //sending our value to two rmws... not going to work..try next combination
                                continue;
                        }
-                       promises[i] = (promises[i] & PROMISE_RMW) |PROMISE_FULFILLED;
+                       promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_FULFILLED;
                        while (i > 0) {
                                i--;
                                if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED)
@@ -176,15 +188,14 @@ bool Node::promise_empty() const
        for (int i = promises.size() - 1; i >= 0; i--) {
                if (promises[i] == PROMISE_UNFULFILLED)
                        return false;
-               if (!fulfilledrmw && ((promises[i]&PROMISE_MASK) == PROMISE_UNFULFILLED))
+               if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED))
                        return false;
-               if (promises[i] == (PROMISE_FULFILLED|PROMISE_RMW))
+               if (promises[i] == (PROMISE_FULFILLED | PROMISE_RMW))
                        fulfilledrmw = true;
        }
        return true;
 }
 
-
 void Node::set_misc_max(int i)
 {
        misc_max = i;
@@ -205,7 +216,6 @@ bool Node::misc_empty() const
        return (misc_index + 1) >= misc_max;
 }
 
-
 /**
  * Adds a value from a weakly ordered future write to backtrack to. This
  * operation may "fail" if the future value has already been run (within some
@@ -216,11 +226,14 @@ bool Node::misc_empty() const
  * @param value is the value to backtrack to.
  * @return True if the future value was successully added; false otherwise
  */
-bool Node::add_future_value(uint64_t value, modelclock_t expiration)
+bool Node::add_future_value(struct future_value& fv)
 {
+       uint64_t value = fv.value;
+       modelclock_t expiration = fv.expiration;
+       thread_id_t tid = fv.tid;
        int idx = -1; /* Highest index where value is found */
        for (unsigned int i = 0; i < future_values.size(); i++) {
-               if (future_values[i].value == value) {
+               if (future_values[i].value == value && future_values[i].tid == tid) {
                        if (expiration <= future_values[i].expiration)
                                return false;
                        idx = i;
@@ -240,8 +253,7 @@ bool Node::add_future_value(uint64_t value, modelclock_t expiration)
                        (int)future_values.size() >= model->params.maxfuturevalues)
                return false;
 
-       struct future_value newfv = {value, expiration};
-       future_values.push_back(newfv);
+       future_values.push_back(fv);
        return true;
 }
 
@@ -372,23 +384,16 @@ void Node::add_read_from(const ModelAction *act)
 }
 
 /**
- * Gets the next 'future_value' value from this Node. Only valid for a node
- * where this->action is a 'read'.
+ * Gets the next 'future_value' from this Node. Only valid for a node where
+ * this->action is a 'read'.
  * @return The first element in future_values
  */
-uint64_t Node::get_future_value() const
+struct future_value Node::get_future_value() const
 {
        ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-       return future_values[future_index].value;
+       return future_values[future_index];
 }
 
-modelclock_t Node::get_future_value_expiration() const
-{
-       ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-       return future_values[future_index].expiration;
-}
-
-
 int Node::get_read_from_size() const
 {
        return may_read_from.size();
@@ -551,7 +556,11 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena
                if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow)
                        prevfairness = node_list[head_idx - model->params.fairwindow];
        }
-       node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness));
+
+       int next_threads = model->get_num_threads();
+       if (act->get_type() == THREAD_CREATE)
+               next_threads++;
+       node_list.push_back(new Node(act, head, next_threads, prevfairness));
        total_nodes++;
        head_idx++;
        return NULL;