From ffb2033ac6b31407810703b65ae0fbaeb9c0da59 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 23 Jan 2013 17:24:11 -0800 Subject: [PATCH] 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. --- model.cc | 12 ++++++++---- nodestack.cc | 8 ++++---- nodestack.h | 2 +- 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/model.cc b/model.cc index ede2bcc..40b25d0 100644 --- 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 404339b..7d703bb 100644 --- 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 7e88912..47c7267 100644 --- 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; -- 2.34.1