From 75fd45bf45d7ec1ac8db7cb6209106ea4e3fc5ab Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 23 Jan 2013 18:05:28 -0800 Subject: [PATCH] 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. --- action.h | 1 + model.cc | 1 + 2 files changed, 2 insertions(+) diff --git a/action.h b/action.h index f742ddc..d0f02a3 100644 --- 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 d1496e8..c707ff8 100644 --- 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)); } -- 2.34.1