From 0b3c8355b0f1fdf7e4b983bef11472192405a9d9 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 22 Feb 2013 16:39:54 -0800 Subject: [PATCH 1/1] model: bugfix - inherit future values from previous loads Once a future value is observed once, it should be available for observation by other loads. Previously, we assume that a future value will be passed to each load that may observe it. However, as exemplified in the double-read-fv.c test, this may not be possible when there are no other feasible stores from which to read. Thus, when building an initial 'may-read-from' set, we should build a set of inherited future values as well. --- model.cc | 25 +++++++++++++++++++++---- model.h | 2 +- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/model.cc b/model.cc index 990f03c5..ae378894 100644 --- a/model.cc +++ b/model.cc @@ -1393,7 +1393,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr) /* Build may_read_from set for newly-created actions */ if (newly_explored && curr->is_read()) - build_reads_from_past(curr); + build_may_read_from(curr); /* Initialize work_queue with the "current action" work */ work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); @@ -2568,12 +2568,12 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) /** * Build up an initial set of all past writes that this 'read' action may read - * from. This set is determined by the clock vector's "happens before" - * relationship. + * from, as well as any previously-observed future values that must still be valid. + * * @param curr is the current ModelAction that we are exploring; it must be a * 'read' operation. */ -void ModelChecker::build_reads_from_past(ModelAction *curr) +void ModelChecker::build_may_read_from(ModelAction *curr) { std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; @@ -2618,6 +2618,23 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) break; } } + + /* Inherit existing, promised future values */ + for (i = 0; i < promises->size(); i++) { + const Promise *promise = (*promises)[i]; + const ModelAction *promise_read = promise->get_action(); + if (promise_read->same_var(curr)) { + /* Only add feasible future-values */ + mo_graph->startChanges(); + r_modification_order(curr, promise); + if (!is_infeasible()) { + const struct future_value fv = promise->get_fv(); + curr->get_node()->add_future_value(fv); + } + mo_graph->rollbackChanges(); + } + } + /* We may find no valid may-read-from only if the execution is doomed */ if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) { priv->no_valid_reads = true; diff --git a/model.h b/model.h index bb548c22..ee9d2c71 100644 --- a/model.h +++ b/model.h @@ -186,7 +186,7 @@ private: ModelAction * get_last_seq_cst_write(ModelAction *curr) const; ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const; ModelAction * get_last_unlock(ModelAction *curr) const; - void build_reads_from_past(ModelAction *curr); + void build_may_read_from(ModelAction *curr); ModelAction * process_rmw(ModelAction *curr); template -- 2.34.1