nodestack: pass 'struct future_value' to add_future_value()

This makes more sense than passing individual parameters. This way, we
construct our future_value in ModelChecker, then simply pass it to the
NodeStack.

diff --git a/model.cc b/model.cc
index ede2bcc840d8710ae00e3d021accadb6ef8e0698..40b25d0d635a32a5fdd2832001c638c3ee1986fc 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -855,10 +855,14 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
 {
        /* Do more ambitious checks now that mo is more complete */
-       if (mo_may_allow(writer, reader) &&
-                       reader->get_node()->add_future_value(writer,
-                               writer->get_seq_number() + params.maxfuturedelay))
-               set_latest_backtrack(reader);
+       if (mo_may_allow(writer, reader)) {
+               struct future_value fv = {
+                       writer->get_value(),
+                       writer->get_seq_number() + params.maxfuturedelay,
+               };
+               if (reader->get_node()->add_future_value(fv))
+                       set_latest_backtrack(reader);
+       }
 }
 
 /**

diff --git a/nodestack.cc b/nodestack.cc
index 404339b6ebcf033b96b55f6b66aa4832c4dc1259..7d703bbff0860abb4cb7732b76a5780f0af0c13d 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -226,9 +226,10 @@ 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(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;
        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) {
@@ -251,8 +252,7 @@ bool Node::add_future_value(const ModelAction *writer, modelclock_t expiration)
                        (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;
 }
 

diff --git a/nodestack.h b/nodestack.h
index 7e88912e3e071de7f47e5a139e105a5a61d11869..47c72678aa13cffb9294e6a7d842860136e37baf 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -71,7 +71,7 @@ public:
         * occurred previously in the stack. */
        Node * get_parent() const { return parent; }
 
-       bool add_future_value(const ModelAction *writer, modelclock_t expiration);
+       bool add_future_value(struct future_value& fv);
        struct future_value get_future_value() const;
        bool increment_future_value();
        bool future_value_empty() const;