if (action)
action->print();
else
- printf("******** empty action ********\n");
+ model_print("******** empty action ********\n");
}
/** @brief Prints info about may_read_from set */
/**
- * 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;
}
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