From 9cfaad02da50095ae169b8fd30ee3148bf88b282 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 21 Mar 2013 16:24:47 -0700 Subject: [PATCH] model: refactor add_future_value, add documentation --- model.cc | 42 ++++++++++++++++++++++++++---------------- 1 file changed, 26 insertions(+), 16 deletions(-) diff --git a/model.cc b/model.cc index 7ce959e..32be053 100644 --- a/model.cc +++ b/model.cc @@ -1051,25 +1051,35 @@ bool ModelChecker::process_mutex(ModelAction *curr) return false; } +/** + * @brief Add a future value to a reader + * + * This function performs a few additional checks to ensure that the future + * value can be feasibly observed by the reader + * + * @param writer The operation whose value is sent. Must be a write. + * @param reader The read operation which may read the future value. Must be a read. + */ 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)) { - Node *node = reader->get_node(); - - /* Find an ancestor thread which exists at the time of the reader */ - Thread *write_thread = get_thread(writer); - while (id_to_int(write_thread->get_id()) >= node->get_num_threads()) - write_thread = write_thread->get_parent(); - - struct future_value fv = { - writer->get_write_value(), - writer->get_seq_number() + params.maxfuturedelay, - write_thread->get_id(), - }; - if (node->add_future_value(fv)) - set_latest_backtrack(reader); - } + if (!mo_may_allow(writer, reader)) + return; + + Node *node = reader->get_node(); + + /* Find an ancestor thread which exists at the time of the reader */ + Thread *write_thread = get_thread(writer); + while (id_to_int(write_thread->get_id()) >= node->get_num_threads()) + write_thread = write_thread->get_parent(); + + struct future_value fv = { + writer->get_write_value(), + writer->get_seq_number() + params.maxfuturedelay, + write_thread->get_id(), + }; + if (node->add_future_value(fv)) + set_latest_backtrack(reader); } /** -- 2.34.1