projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
promise: add const
[model-checker.git]
/
nodestack.cc
diff --git
a/nodestack.cc
b/nodestack.cc
index ccf79e40ea99b3726cbe092e6f0942b7659c61cb..addf93f67469f1cd7f96a15ffad8ec5551cb1c1b 100644
(file)
--- a/
nodestack.cc
+++ b/
nodestack.cc
@@
-8,6
+8,7
@@
#include "common.h"
#include "model.h"
#include "threads-model.h"
#include "common.h"
#include "model.h"
#include "threads-model.h"
+#include "modeltypes.h"
/**
* @brief Node constructor
/**
* @brief Node constructor
@@
-89,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 ");
@@
-163,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)
@@
-187,15
+188,14
@@
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;
}
-
void Node::set_misc_max(int i)
{
misc_max = i;
void Node::set_misc_max(int i)
{
misc_max = i;
@@
-216,7
+216,6
@@
bool Node::misc_empty() const
return (misc_index + 1) >= misc_max;
}
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
/**
* 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
@@
-227,11
+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(
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++) {
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(uint64_t value, 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;
}
@@
-383,23
+384,16
@@
void Node::add_read_from(const ModelAction *act)
}
/**
}
/**
- * Gets the next 'future_value'
value from this Node. Only valid for a nod
e
- *
where
this->action is a 'read'.
+ * Gets the next 'future_value'
from this Node. Only valid for a node wher
e
+ * this->action is a 'read'.
* @return The first element in future_values
*/
* @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()));
{
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();
int Node::get_read_from_size() const
{
return may_read_from.size();