Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

diff --git a/main.cc b/main.cc
index a10bec364c0633ee569306b89243b3f1283fc3d6..4f37390e163d9fdc80e5197a462bf2d8551601be 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -16,7 +16,7 @@
 static void param_defaults(struct model_params *params)
 {
        params->maxreads = 0;
-       params->maxfuturedelay = 100;
+       params->maxfuturedelay = 10;
        params->fairwindow = 0;
        params->yieldon = false;
        params->enabledcount = 1;

diff --git a/model.cc b/model.cc
index 3ed2fb24971b3c42908b1b59f243a54a8b786500..167ea947a79a020964ec13fc67d67077aae961f7 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1051,25 +1051,56 @@ bool ModelChecker::process_mutex(ModelAction *curr)
        return false;
 }
 
+/**
+ * @brief Check if the current pending promises allow a future value to be sent
+ *
+ * If one of the following is true:
+ *  (a) there are no pending promises
+ *  (b) the reader is ordered after the latest Promise creation
+ * Then, it is safe to pass a future value back now.
+ *
+ * Otherwise, we must save the pending future value until (a) or (b) is true
+ *
+ * @param writer The operation which sends the future value. Must be a write.
+ * @param reader The operation which will observe the value. Must be a read.
+ * @return True if the future value can be sent now; false if it must wait.
+ */
+bool ModelChecker::promises_may_allow(const ModelAction *writer,
+               const ModelAction *reader) const
+{
+       return promises->empty() ||
+               *(promises->back()->get_reader(0)) < *reader;
+}
+
+/**
+ * @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);
 }
 
 /**
@@ -1082,30 +1113,39 @@ bool ModelChecker::process_write(ModelAction *curr)
        /* Readers to which we may send our future value */
        ModelVector<ModelAction *> send_fv;
 
-       bool updated_mod_order = w_modification_order(curr, &send_fv);
-       int promise_idx = get_promise_to_resolve(curr);
        const ModelAction *earliest_promise_reader;
        bool updated_promises = false;
 
-       if (promise_idx >= 0) {
-               earliest_promise_reader = (*promises)[promise_idx]->get_reader(0);
-               updated_promises = resolve_promise(curr, promise_idx);
+       bool updated_mod_order = w_modification_order(curr, &send_fv);
+       Promise *promise = pop_promise_to_resolve(curr);
+
+       if (promise) {
+               earliest_promise_reader = promise->get_reader(0);
+               updated_promises = resolve_promise(curr, promise);
        } else
                earliest_promise_reader = NULL;
 
-       /* Don't send future values to reads after the Promise we resolve */
        for (unsigned int i = 0; i < send_fv.size(); i++) {
                ModelAction *read = send_fv[i];
-               if (!earliest_promise_reader || *read < *earliest_promise_reader)
-                       futurevalues->push_back(PendingFutureValue(curr, read));
+
+               /* Don't send future values to reads after the Promise we resolve */
+               if (!earliest_promise_reader || *read < *earliest_promise_reader) {
+                       /* Check if future value can be sent immediately */
+                       if (promises_may_allow(curr, read)) {
+                               add_future_value(curr, read);
+                       } else {
+                               futurevalues->push_back(PendingFutureValue(curr, read));
+                       }
+               }
        }
 
-       if (promises->size() == 0) {
-               for (unsigned int i = 0; i < futurevalues->size(); i++) {
-                       struct PendingFutureValue pfv = (*futurevalues)[i];
-                       add_future_value(pfv.writer, pfv.act);
+       /* Check the pending future values */
+       for (int i = (int)futurevalues->size() - 1; i >= 0; i--) {
+               struct PendingFutureValue pfv = (*futurevalues)[i];
+               if (promises_may_allow(pfv.writer, pfv.reader)) {
+                       add_future_value(pfv.writer, pfv.reader);
+                       futurevalues->erase(futurevalues->begin() + i);
                }
-               futurevalues->clear();
        }
 
        mo_graph->commitChanges();
@@ -2048,7 +2088,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr, ModelVector<ModelActi
 /** Arbitrary reads from the future are not allowed.  Section 29.3
  * part 9 places some constraints.  This method checks one result of constraint
  * constraint.  Others require compiler support. */
-bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
+bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const
 {
        if (!writer->is_rmw())
                return true;
@@ -2550,29 +2590,31 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const
 }
 
 /**
- * @brief Find the promise, if any to resolve for the current action
+ * @brief Find the promise (if any) to resolve for the current action and
+ * remove it from the pending promise vector
  * @param curr The current ModelAction. Should be a write.
- * @return The (non-negative) index for the Promise to resolve, if any;
- * otherwise -1
+ * @return The Promise to resolve, if any; otherwise NULL
  */
-int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
+Promise * ModelChecker::pop_promise_to_resolve(const ModelAction *curr)
 {
        for (unsigned int i = 0; i < promises->size(); i++)
-               if (curr->get_node()->get_promise(i))
-                       return i;
-       return -1;
+               if (curr->get_node()->get_promise(i)) {
+                       Promise *ret = (*promises)[i];
+                       promises->erase(promises->begin() + i);
+                       return ret;
+               }
+       return NULL;
 }
 
 /**
  * Resolve a Promise with a current write.
  * @param write The ModelAction that is fulfilling Promises
- * @param promise_idx The index corresponding to the promise
+ * @param promise The Promise to resolve
  * @return True if the Promise was successfully resolved; false otherwise
  */
-bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
+bool ModelChecker::resolve_promise(ModelAction *write, Promise *promise)
 {
        ModelVector<ModelAction *> actions_to_check;
-       Promise *promise = (*promises)[promise_idx];
 
        for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
                ModelAction *read = promise->get_reader(i);
@@ -2584,7 +2626,6 @@ bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
        if (!mo_graph->resolvePromise(promise, write))
                priv->failed_promise = true;
 
-       promises->erase(promises->begin() + promise_idx);
        /**
         * @todo  It is possible to end up in an inconsistent state, where a
         * "resolved" promise may still be referenced if

diff --git a/model.h b/model.h
index 4b87b04a48a00263b9377c8e3b82549228e329f9..355764b7c4d290cfb3de64f7f0c0086a0ba83c73 100644 (file)
--- a/model.h
+++ b/model.h
@@ -73,9 +73,11 @@ struct execution_stats {
 };
 
 struct PendingFutureValue {
-       PendingFutureValue(ModelAction *writer, ModelAction *act) : writer(writer), act(act) { }
+       PendingFutureValue(ModelAction *writer, ModelAction *reader) :
+               writer(writer), reader(reader)
+       { }
        const ModelAction *writer;
-       ModelAction *act;
+       ModelAction *reader;
 };
 
 /** @brief Records information regarding a single pending release sequence */
@@ -144,8 +146,9 @@ private:
        void add_thread(Thread *t);
 
        bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
-       bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader);
+       bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
+       bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        bool has_asserted() const;
        void set_assert();
        void set_bad_synchronization();
@@ -183,8 +186,8 @@ private:
        bool set_latest_backtrack(ModelAction *act);
        ModelAction * get_next_backtrack();
        void reset_to_initial_state();
-       int get_promise_to_resolve(const ModelAction *curr) const;
-       bool resolve_promise(ModelAction *curr, unsigned int promise_idx);
+       Promise * pop_promise_to_resolve(const ModelAction *curr);
+       bool resolve_promise(ModelAction *curr, Promise *promise);
        void compute_promises(ModelAction *curr);
        void compute_relseq_breakwrites(ModelAction *curr);