+#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
fairness(num_threads),
numBacktracks(0),
enabled_array(NULL),
- may_read_from(),
- read_from_index(0),
+ read_from_past(),
+ read_from_past_idx(0),
future_values(),
future_index(-1),
relseq_break_writes(),
}
/** 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_past_empty() ? "empty" : "non-empty ");
+ for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++)
+ model_print("[%d]", read_from_past[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");
}
-/** @brief Prints info about may_read_from set */
-void Node::print_may_read_from()
+/** @brief Prints info about read_from_past set */
+void Node::print_read_from_past()
{
- for (unsigned int i = 0; i < may_read_from.size(); i++)
- may_read_from[i]->print();
+ for (unsigned int i = 0; i < read_from_past.size(); i++)
+ read_from_past[i]->print();
}
/**
//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)
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;
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;
+ 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;
(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;
}
* Checks whether the readsfrom set for this node is empty.
* @return true if the readsfrom set is empty.
*/
-bool Node::read_from_empty() const
+bool Node::read_from_past_empty() const
{
- return ((read_from_index + 1) >= may_read_from.size());
+ return ((read_from_past_idx + 1) >= read_from_past.size());
}
/**
return int_to_id(i);
}
+void Node::clear_backtracking()
+{
+ for (unsigned int i = 0; i < backtrack.size(); i++)
+ backtrack[i] = false;
+ for (unsigned int i = 0; i < explored_children.size(); i++)
+ explored_children[i] = false;
+}
+
bool Node::is_enabled(Thread *t) const
{
int thread_id = id_to_int(t->get_id());
}
/**
- * Add an action to the may_read_from set.
+ * Add an action to the read_from_past set.
* @param act is the action to add
*/
-void Node::add_read_from(const ModelAction *act)
+void Node::add_read_from_past(const ModelAction *act)
{
- may_read_from.push_back(act);
+ read_from_past.push_back(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
+int Node::get_read_from_past_size() const
{
- ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
- return future_values[future_index].expiration;
+ return read_from_past.size();
}
-
-int Node::get_read_from_size() const
+const ModelAction * Node::get_read_from_past(int i) const
{
- return may_read_from.size();
-}
-
-const ModelAction * Node::get_read_from_at(int i) const
-{
- return may_read_from[i];
+ return read_from_past[i];
}
/**
- * Gets the next 'may_read_from' action from this Node. Only valid for a node
+ * Gets the next 'read_from_past' action from this Node. Only valid for a node
* where this->action is a 'read'.
- * @return The first element in may_read_from
+ * @return The first element in read_from_past
*/
-const ModelAction * Node::get_read_from() const
+const ModelAction * Node::get_read_from_past() const
{
- if (read_from_index < may_read_from.size())
- return may_read_from[read_from_index];
+ if (read_from_past_idx < read_from_past.size())
+ return read_from_past[read_from_past_idx];
else
return NULL;
}
* Increments the index into the readsfrom set to explore the next item.
* @return Returns false if we have explored all items.
*/
-bool Node::increment_read_from()
+bool Node::increment_read_from_past()
{
DBG();
promises.clear();
- if (read_from_index < may_read_from.size()) {
- read_from_index++;
- return read_from_index < may_read_from.size();
+ if (read_from_past_idx < read_from_past.size()) {
+ read_from_past_idx++;
+ return read_from_past_idx < read_from_past.size();
}
return false;
}
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;
for (unsigned int i = it; i < node_list.size(); i++)
delete node_list[i];
node_list.resize(it);
+ node_list.back()->clear_backtracking();
}
Node * NodeStack::get_head() const
projects / model-checker.git / blobdiff