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.

diff --git a/model.cc b/model.cc
index 990f03c5d9ef38d856c9cec5a46c6e7ad94b6ecd..ae3788945c7756881178b1657bb215cf5a71901a 100644 (file)
--- 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<action_list_t> *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 bb548c22e85b3835da4d37f52364a231fd93a285..ee9d2c71280175e4dfe0380380b0839cfaa599f5 100644 (file)
--- 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 <typename rf_type>