model: schedule appropriate fence backtracking points

[c11tester.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index e0800156f56178a0cfa5f69d4ad1026a316460f8..b2ef73cac30108fab56745f89b0542a186fc6410 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -90,7 +90,7 @@ 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 ");
@@ -164,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)
@@ -188,9 +188,9 @@ 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;
@@ -226,12 +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(const ModelAction *writer, modelclock_t expiration)
+bool Node::add_future_value(struct future_value& fv)
 {
-       uint64_t value = writer->get_value();
+       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;
@@ -251,8 +253,7 @@ bool Node::add_future_value(const ModelAction *writer, 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;
 }
 
@@ -555,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;