enabled_array(NULL),
read_from_past(),
read_from_past_idx(0),
+ read_from_promises(),
+ read_from_promise_idx(-1),
future_values(),
future_index(-1),
+ resolve_promise(),
+ resolve_promise_idx(-1),
relseq_break_writes(),
relseq_break_index(0),
misc_index(0),
model_print("[%d]", read_from_past[i]->get_seq_number());
model_print("\n");
+ model_print(" read-from promises: %s", read_from_promise_empty() ? "empty" : "non-empty ");
+ for (int i = read_from_promise_idx + 1; i < (int)read_from_promises.size(); i++)
+ model_print("[%d]", read_from_promises[i]->get_seq_number());
+ model_print("\n");
+
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(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
}
+/*********************************** promise **********************************/
+
/**
* Sets a promise to explore meeting with the given node.
* @param i is the promise index.
*/
-void Node::set_promise(unsigned int i, bool is_rmw)
-{
- if (i >= promises.size())
- promises.resize(i + 1, PROMISE_IGNORE);
- if (promises[i] == PROMISE_IGNORE) {
- promises[i] = PROMISE_UNFULFILLED;
- if (is_rmw)
- promises[i] |= PROMISE_RMW;
- }
+void Node::set_promise(unsigned int i)
+{
+ if (i >= resolve_promise.size())
+ resolve_promise.resize(i + 1, false);
+ resolve_promise[i] = true;
}
/**
* Looks up whether a given promise should be satisfied by this node.
* @param i The promise index.
- * @return true if the promise should be satisfied by the given model action.
+ * @return true if the promise should be satisfied by the given ModelAction.
*/
bool Node::get_promise(unsigned int i) const
{
- return (i < promises.size()) && ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED);
+ return (i < resolve_promise.size()) && (int)i == resolve_promise_idx;
}
/**
- * Increments to the next combination of promises.
+ * Increments to the next promise to resolve.
* @return true if we have a valid combination.
*/
bool Node::increment_promise()
{
DBG();
- 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 ((rmw_count > 0) && (promises[i] & PROMISE_RMW)) {
- //sending our value to two rmws... not going to work..try next combination
- continue;
- }
- promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_FULFILLED;
- while (i > 0) {
- i--;
- if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED)
- promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_UNFULFILLED;
- }
+ if (resolve_promise.empty())
+ return false;
+ int prev_idx = resolve_promise_idx;
+ resolve_promise_idx++;
+ for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++)
+ if (resolve_promise[resolve_promise_idx])
return true;
- } else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
- rmw_count--;
- }
- }
+ resolve_promise_idx = prev_idx;
return false;
}
*/
bool Node::promise_empty() const
{
- bool fulfilledrmw = false;
- for (int i = promises.size() - 1; i >= 0; i--) {
- if (promises[i] == PROMISE_UNFULFILLED)
+ for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++)
+ if (i >= 0 && resolve_promise[i])
return false;
- if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED))
- return false;
- if (promises[i] == (PROMISE_FULFILLED | PROMISE_RMW))
- fulfilledrmw = true;
- }
return true;
}
+/** @brief Clear any promise-resolution information for this Node */
+void Node::clear_promise_resolutions()
+{
+ resolve_promise.clear();
+ resolve_promise_idx = -1;
+}
+
+/******************************* end promise **********************************/
+
void Node::set_misc_max(int i)
{
misc_max = i;
backtrack[i] = false;
for (unsigned int i = 0; i < explored_children.size(); i++)
explored_children[i] = false;
+ numBacktracks = 0;
}
bool Node::is_enabled(Thread *t) const
*/
bool Node::increment_read_from()
{
- promises.clear();
+ clear_promise_resolutions();
if (increment_read_from_past()) {
read_from_status = READ_FROM_PAST;
return true;
+ } else if (increment_read_from_promise()) {
+ read_from_status = READ_FROM_PROMISE;
+ return true;
} else if (increment_future_value()) {
read_from_status = READ_FROM_FUTURE;
return true;
*/
bool Node::read_from_empty() const
{
- return read_from_past_empty() && future_value_empty();
+ return read_from_past_empty() &&
+ read_from_promise_empty() &&
+ future_value_empty();
}
/**
*/
unsigned int Node::read_from_size() const
{
- return read_from_past.size() + future_values.size();
+ return read_from_past.size() +
+ read_from_promises.size() +
+ future_values.size();
}
/******************************* end read from ********************************/
/************************** end read from past ********************************/
+/***************************** read_from_promises *****************************/
+
+/**
+ * Add an action to the read_from_promises set.
+ * @param reader The read which generated the Promise; we use the ModelAction
+ * instead of the Promise because the Promise does not last across executions
+ */
+void Node::add_read_from_promise(const ModelAction *reader)
+{
+ read_from_promises.push_back(reader);
+}
+
+/**
+ * Gets the next 'read-from-promise' from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @return The current element in read_from_promises
+ */
+Promise * Node::get_read_from_promise() const
+{
+ ASSERT(read_from_promise_idx >= 0 && read_from_promise_idx < ((int)read_from_promises.size()));
+ return read_from_promises[read_from_promise_idx]->get_reads_from_promise();
+}
+
+/**
+ * Checks whether the read_from_promises set for this node is empty.
+ * @return true if the read_from_promises set is empty.
+ */
+bool Node::read_from_promise_empty() const
+{
+ return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size()));
+}
+
+/**
+ * Increments the index into the read_from_promises set to explore the next item.
+ * @return Returns false if we have explored all promises.
+ */
+bool Node::increment_read_from_promise()
+{
+ DBG();
+ if (read_from_promise_idx < ((int)read_from_promises.size())) {
+ read_from_promise_idx++;
+ return (read_from_promise_idx < ((int)read_from_promises.size()));
+ }
+ return false;
+}
+
+/************************* end read_from_promises *****************************/
+
/****************************** future values *********************************/
/**
bool Node::increment_relseq_break()
{
DBG();
- promises.clear();
if (relseq_break_index < ((int)relseq_break_writes.size())) {
relseq_break_index++;
return (relseq_break_index < ((int)relseq_break_writes.size()));
projects / model-checker.git / blobdiff