projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model: utilize CycleGraph 'addEdge()' status
[model-checker.git]
/
nodestack.cc
diff --git
a/nodestack.cc
b/nodestack.cc
index e0800156f56178a0cfa5f69d4ad1026a316460f8..addf93f67469f1cd7f96a15ffad8ec5551cb1c1b 100644
(file)
--- a/
nodestack.cc
+++ b/
nodestack.cc
@@
-90,7
+90,7
@@
Node::~Node()
}
/** Prints debugging info for the ModelAction associated with this Node */
}
/** 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 ");
{
action->print();
model_print(" backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
@@
-164,7
+164,7
@@
bool Node::increment_promise()
//sending our value to two rmws... not going to work..try next combination
continue;
}
//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)
while (i > 0) {
i--;
if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED)
@@
-188,9
+188,9
@@
bool Node::promise_empty() const
for (int i = promises.size() - 1; i >= 0; i--) {
if (promises[i] == PROMISE_UNFULFILLED)
return false;
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;
return false;
- if (promises[i] == (PROMISE_FULFILLED
|
PROMISE_RMW))
+ if (promises[i] == (PROMISE_FULFILLED
|
PROMISE_RMW))
fulfilledrmw = true;
}
return true;
fulfilledrmw = true;
}
return true;
@@
-226,12
+226,14
@@
bool Node::misc_empty() const
* @param value is the value to backtrack to.
* @return True if the future value was successully added; false otherwise
*/
* @param value is the value to backtrack to.
* @return True if the future value was successully added; false otherwise
*/
-bool Node::add_future_value(
const ModelAction *writer, modelclock_t expiration
)
+bool Node::add_future_value(
struct future_value& fv
)
{
{
- uint64_t value = writer->get_value();
+ 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++) {
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;
if (expiration <= future_values[i].expiration)
return false;
idx = i;
@@
-251,8
+253,7
@@
bool Node::add_future_value(const ModelAction *writer, modelclock_t expiration)
(int)future_values.size() >= model->params.maxfuturevalues)
return false;
(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;
}
return true;
}