+#define __STDC_FORMAT_MACROS
+#include <inttypes.h>
+
#include <string.h>
#include "nodestack.h"
#include "common.h"
#include "model.h"
#include "threads-model.h"
+#include "modeltypes.h"
/**
* @brief Node constructor
}
/** 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");
return true;
}
-
void Node::set_misc_max(int i)
{
misc_max = i;
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
* @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;
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) {
(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;
}
}
/**
- * 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
-{
- ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
- return future_values[future_index].value;
-}
-
-modelclock_t Node::get_future_value_expiration() const
+struct future_value Node::get_future_value() const
{
ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
- return future_values[future_index].expiration;
+ return future_values[future_index];
}
-
int Node::get_read_from_size() const
{
return may_read_from.size();