From b410cb21b726638c0618e1a0b420374a707fb64b Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 7 Jan 2013 18:22:57 -0800 Subject: [PATCH] model: add 'add_future_value()' wrapper Encapsulate a little logic in a function here, so we can reuse this in other places. --- model.cc | 14 ++++++++++---- model.h | 1 + 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/model.cc b/model.cc index bc17a88..88d5e71 100644 --- 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 414cf93..4fd2667 100644 --- 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; -- 2.34.1