nodestack: pass writer ModelAction to add_future_value()
authorBrian Norris <banorris@uci.edu>
Wed, 23 Jan 2013 18:43:48 +0000 (10:43 -0800)
committerBrian Norris <banorris@uci.edu>
Wed, 23 Jan 2013 18:43:48 +0000 (10:43 -0800)
NodeStack will have to know a little more about who wrote the future
value, so just pass the ModelAction as a parameter.

model.cc
nodestack.cc
nodestack.h

index 017455d24124c726ddd5164c508feaab3bd2b24f..97df9a2dbba274857e85e6be417489c776e82024 100644 (file)
--- 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);
 }
index 708ec3d0f5fa3da43a563228ef53c4b6e72475dd..46f7d12a007e6289aa384993d7e58fb29e1d5fed 100644 (file)
@@ -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) {
index 55991c3022a50dc67e51ca607f3ca33e3e638ce2..d2e6491b2edec5891943351e9891b358f2b05594 100644 (file)
@@ -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;