model: rename some 'isfeasible...' functions to 'is_infeasible...'

[c11tester.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index 22cc3784a1c75476b15c3e4378677158dc911e95..4da3cd60fd7db93c147fba60faf929d6fccb9a0f 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -91,7 +91,7 @@ void Node::print()
        if (action)
                action->print();
        else
-               printf("******** empty action ********\n");
+               model_print("******** empty action ********\n");
 }
 
 /** @brief Prints info about may_read_from set */
@@ -161,21 +161,14 @@ bool Node::increment_promise() {
  * @return true if we have explored all promise combinations.
  */
 bool Node::promise_empty() {
-       unsigned int rmw_count=0;
-       for (unsigned int i = 0; i < promises.size(); i++) {
-               if (promises[i]==(PROMISE_RMW|PROMISE_FULFILLED))
-                       rmw_count++;
-       }
-
-       for (unsigned int i = 0; i < promises.size();i++) {
-               if ((promises[i]& PROMISE_MASK) == PROMISE_UNFULFILLED) {
-                       //if this isn't a feasible option, keep going
-                       if ((rmw_count > 0)&&(promises[i] & PROMISE_RMW))
-                               continue;
+       bool fulfilledrmw=false;
+       for (int i = promises.size()-1 ; i>=0; i--) {
+               if (promises[i]==PROMISE_UNFULFILLED)
                        return false;
-               } else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
-                       rmw_count--;
-               }
+               if (!fulfilledrmw && ((promises[i]&PROMISE_MASK)==PROMISE_UNFULFILLED))
+                       return false;
+               if (promises[i]==(PROMISE_FULFILLED|PROMISE_RMW))
+                       fulfilledrmw=true;
        }
        return true;
 }
@@ -199,26 +192,39 @@ bool Node::misc_empty() {
 
 
 /**
- * Adds a value from a weakly ordered future write to backtrack to.
+ * 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
+ * sloppiness window of this expiration), or if the futurevalues set has
+ * reached its maximum.
+ * @see model_params.maxfuturevalues
+ *
  * @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) {
-       int suitableindex=-1;
+       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].expiration>=expiration)
+                       if (expiration <= future_values[i].expiration)
                                return false;
-                       if (future_index < ((int) i)) {
-                               suitableindex=i;
-                       }
+                       idx = i;
                }
        }
-
-       if (suitableindex!=-1) {
-               future_values[suitableindex].expiration=expiration;
+       if (idx > future_index) {
+               /* Future value hasn't been explored; update expiration */
+               future_values[idx].expiration = expiration;
                return true;
+       } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
+               /* Future value has been explored and is within the "sloppy" window */
+               return false;
        }
-       struct future_value newfv={value, expiration};
+
+       /* Limit the size of the future-values set */
+       if (model->params.maxfuturevalues > 0 &&
+                       (int)future_values.size() >= model->params.maxfuturevalues)
+               return false;
+
+       struct future_value newfv = {value, expiration};
        future_values.push_back(newfv);
        return true;
 }
@@ -489,14 +495,14 @@ NodeStack::~NodeStack()
 
 void NodeStack::print()
 {
-       printf("............................................\n");
-       printf("NodeStack printing node_list:\n");
+       model_print("............................................\n");
+       model_print("NodeStack printing node_list:\n");
        for (unsigned int it = 0; it < node_list.size(); it++) {
                if (it == this->iter)
-                       printf("vvv following action is the current iterator vvv\n");
+                       model_print("vvv following action is the current iterator vvv\n");
                node_list[it]->print();
        }
-       printf("............................................\n");
+       model_print("............................................\n");
 }
 
 /** Note: The is_enabled set contains what actions were enabled when