From f10dc6ce67a97ab18423e7cedaa24961bf0d80dc Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 23 Jan 2013 10:43:48 -0800 Subject: [PATCH] nodestack: pass writer ModelAction to add_future_value() NodeStack will have to know a little more about who wrote the future value, so just pass the ModelAction as a parameter. --- model.cc | 2 +- nodestack.cc | 3 ++- nodestack.h | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/model.cc b/model.cc index 017455d..97df9a2 100644 --- a/model.cc +++ b/model.cc @@ -857,7 +857,7 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read { /* Do more ambitious checks now that mo is more complete */ if (mo_may_allow(writer, reader) && - reader->get_node()->add_future_value(writer->get_value(), + reader->get_node()->add_future_value(writer, writer->get_seq_number() + params.maxfuturedelay)) set_latest_backtrack(reader); } diff --git a/nodestack.cc b/nodestack.cc index 708ec3d..46f7d12 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -225,8 +225,9 @@ bool Node::misc_empty() const * @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(const ModelAction *writer, modelclock_t expiration) { + uint64_t value = writer->get_value(); 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) { diff --git a/nodestack.h b/nodestack.h index 55991c3..d2e6491 100644 --- a/nodestack.h +++ b/nodestack.h @@ -76,7 +76,7 @@ public: * occurred previously in the stack. */ Node * get_parent() const { return parent; } - bool add_future_value(uint64_t value, modelclock_t expiration); + bool add_future_value(const ModelAction *writer, modelclock_t expiration); struct future_value get_future_value() const; bool increment_future_value(); bool future_value_empty() const; -- 2.34.1