action: record future value

Future values don't currently show up in ModelAction (e.g., when
printing). We should set the value when we choose to read from a future
value.

diff --git a/action.h b/action.h
index f742ddc62854a79fd2f2aff3721914781f115b36..d0f02a327e6d8373d35b2d56c3dd250a40aa948b 100644 (file)
--- a/action.h
+++ b/action.h
@@ -79,6 +79,7 @@ public:
        void * get_location() const { return location; }
        modelclock_t get_seq_number() const { return seq_number; }
        uint64_t get_value() const { return value; }
+       void set_value(uint64_t v) { value = v; }
        const ModelAction * get_reads_from() const { return reads_from; }
 
        Node * get_node() const;

diff --git a/model.cc b/model.cc
index d1496e8de55b69dd3f2526e9ba688df02913e5bf..c707ff8771b023d0f4b71b259e42dce77b7105e6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -737,6 +737,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                        /* Read from future value */
                        struct future_value fv = curr->get_node()->get_future_value();
                        value = fv.value;
+                       curr->set_value(fv.value);
                        curr->set_read_from(NULL);
                        promises->push_back(new Promise(curr, fv));
                }