future_value: add thread ID parameter

This just records the parameter for now, and makes it a distinction
between future values. Shouldn't affect model-checker behavior, except
for the introduction of extra future values: one for each thread which
writes the same value.

We calculate whether the writing thread exists at the time of the future
value and if not, find an ancestor thread which does.

diff --git a/model.cc b/model.cc
index 40b25d0d635a32a5fdd2832001c638c3ee1986fc..d1496e8de55b69dd3f2526e9ba688df02913e5bf 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -856,11 +856,19 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
 {
        /* 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_value(),
                        writer->get_seq_number() + params.maxfuturedelay,
+                       write_thread->get_id(),
                };
-               if (reader->get_node()->add_future_value(fv))
+               if (node->add_future_value(fv))
                        set_latest_backtrack(reader);
        }
 }

diff --git a/nodestack.cc b/nodestack.cc
index 7d703bbff0860abb4cb7732b76a5780f0af0c13d..dd2dd855c658f7734b7024f76a973e2341ac522c 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -230,9 +230,10 @@ bool Node::add_future_value(struct future_value& fv)
 {
        uint64_t value = fv.value;
        modelclock_t expiration = fv.expiration;
+       thread_id_t tid = fv.tid;
        int idx = -1; /* Highest index where value is found */
        for (unsigned int i = 0; i < future_values.size(); i++) {
-               if (future_values[i].value == value) {
+               if (future_values[i].value == value && future_values[i].tid == tid) {
                        if (expiration <= future_values[i].expiration)
                                return false;
                        idx = i;

diff --git a/promise.h b/promise.h
index 7e6e396e15f9330e24ed7590e6abaefc9f3b1c38..3c0d5dddd7330e33f06bbc9c2a21320963e6fc4c 100644 (file)
--- a/promise.h
+++ b/promise.h
@@ -16,6 +16,7 @@
 struct future_value {
        uint64_t value;
        modelclock_t expiration;
+       thread_id_t tid;
 };
 
 class Promise {