model: add 'add_future_value()' wrapper

Encapsulate a little logic in a function here, so we can reuse this in
other places.

diff --git a/model.cc b/model.cc
index bc17a882c56f38c7bab1a71064f584ca285e6171..88d5e710a18e2dbdb2978e6ca9b5856a41ff1c34 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -853,6 +853,15 @@ bool ModelChecker::process_mutex(ModelAction *curr)
        return false;
 }
 
+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->get_value(),
+                               writer->get_seq_number() + params.maxfuturedelay))
+               set_latest_backtrack(reader);
+}
+
 /**
  * Process a write ModelAction
  * @param curr The ModelAction to process
@@ -866,10 +875,7 @@ bool ModelChecker::process_write(ModelAction *curr)
        if (promises->size() == 0) {
                for (unsigned int i = 0; i < futurevalues->size(); i++) {
                        struct PendingFutureValue pfv = (*futurevalues)[i];
-                       //Do more ambitious checks now that mo is more complete
-                       if (mo_may_allow(pfv.writer, pfv.act) &&
-                                       pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
-                               set_latest_backtrack(pfv.act);
+                       add_future_value(pfv.writer, pfv.act);
                }
                futurevalues->clear();
        }

diff --git a/model.h b/model.h
index 414cf9337c4ba638198688a8586e4eb6681fb953..4fd2667753f4b3ae85698c6422921a1cf18163f7 100644 (file)
--- a/model.h
+++ b/model.h
@@ -188,6 +188,7 @@ private:
        void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
        bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
+       void add_future_value(const ModelAction *writer, ModelAction *reader);
 
        ModelAction * new_uninitialized_action(void *location) const;