deal with looping due to bogus future value via promise expiration

fix promise bug

diff --git a/main.cc b/main.cc
index 215a2197d35e91fa29cf65b869a292165be4a9ad..b58599df76681bdae923157b84d47f16a42681e1 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -16,27 +16,32 @@
 
 static void param_defaults(struct model_params * params) {
        params->maxreads = 0;
+  params->maxfuturedelay = 100;
 }
 
-static void print_usage() {
+static void print_usage(struct model_params *params) {
        printf(
 "Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
 "\n"
 "Options:\n"
 "-h                    Display this help message and exit\n"
-"-m                    Maximum times a thread can read from the same write while other writes exist\n"
-"--                    Program arguments follow.\n\n");
+"-m                    Maximum times a thread can read from the same write while other writes exist. Default: %d\n"
+"-s                    Maximum actions that the model checker will wait for a write from the future past the expected number of actions.  Default: %d\n"
+"--                    Program arguments follow.\n\n", params->maxreads, params->maxfuturedelay);
        exit(EXIT_SUCCESS);
 }
 
 static void parse_options(struct model_params *params, int *argc, char ***argv) {
-       const char *shortopts = "hm:";
+       const char *shortopts = "hm:s:";
        int opt;
        bool error = false;
        while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
                switch (opt) {
                case 'h':
-                       print_usage();
+                       print_usage(params);
+                       break;
+               case 's':
+                       params->maxfuturedelay = atoi(optarg);
                        break;
                case 'm':
                        params->maxreads = atoi(optarg);
@@ -50,7 +55,7 @@ static void parse_options(struct model_params *params, int *argc, char ***argv)
        (*argv) += optind;
 
        if (error)
-               print_usage();
+               print_usage(params);
 }
 
 int main_argc;

diff --git a/model.cc b/model.cc
index 00982130b042f16add374761d180f717a51900a7..9611f2f615845c926485dd732ce26b026585c085 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -292,8 +292,9 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
                } else {
                        /* Read from future value */
                        value = curr->get_node()->get_future_value();
+                       modelclock_t expiration = curr->get_node()->get_future_value_expiration();
                        curr->read_from(NULL);
-                       Promise *valuepromise = new Promise(curr, value);
+                       Promise *valuepromise = new Promise(curr, value, expiration);
                        promises->push_back(valuepromise);
                }
                th->set_return_value(value);
@@ -428,6 +429,16 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        return get_next_thread(curr);
 }
 
+bool ModelChecker::promises_expired() {
+       for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
+               Promise *promise = (*promises)[promise_index];
+               if (promise->get_expiration()<priv->used_sequence_numbers) {
+                       return true;
+               }
+       }
+       return false;
+}
+
 /** @returns whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
@@ -436,7 +447,7 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
-       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads;
+       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -685,7 +696,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                   =>
                                   that read could potentially read from our write.
                                 */
-                               if (isfeasible() && act->get_node()->add_future_value(curr->get_value()) &&
+                               if (isfeasible() && act->get_node()->add_future_value(curr->get_value(), curr->get_seq_number()+params.maxfuturedelay) &&
                                                (!priv->next_backtrack || *act > *priv->next_backtrack))
                                        priv->next_backtrack = act;
                        }

diff --git a/model.h b/model.h
index 19143d36d4f433c5c734652fbd8fe7ae35a51853..1a2f6a145715fb7b8318eca7522048475ef9b436 100644 (file)
--- a/model.h
+++ b/model.h
@@ -29,6 +29,7 @@ class Promise;
  */
 struct model_params {
        int maxreads;
+       int maxfuturedelay;
 };
 
 /**
@@ -91,7 +92,7 @@ private:
        bool has_asserted() {return asserted;}
        void reset_asserted() {asserted=false;}
        int num_executions;
-
+       bool promises_expired();
        const model_params params;
 
        /**

diff --git a/nodestack.cc b/nodestack.cc
index a9399edbe9a35cd28328e438a8ce6e23c8cebeb3..431baafbdce9809a2cb49ebcea30837182c852cf 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -63,7 +63,8 @@ void Node::print_may_read_from()
 void Node::set_promise(unsigned int i) {
        if (i >= promises.size())
                promises.resize(i + 1, PROMISE_IGNORE);
-       promises[i] = PROMISE_UNFULFILLED;
+       if (promises[i] == PROMISE_IGNORE)
+               promises[i] = PROMISE_UNFULFILLED;
 }
 
 /**
@@ -109,12 +110,24 @@ bool Node::promise_empty() {
  * Adds a value from a weakly ordered future write to backtrack to.
  * @param value is the value to backtrack to.
  */
-bool Node::add_future_value(uint64_t value) {
-       for (unsigned int i = 0; i < future_values.size(); i++)
-               if (future_values[i] == value)
-                       return false;
+bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
+       int suitableindex=-1;
+       for (unsigned int i = 0; i < future_values.size(); i++) {
+               if (future_values[i].value == value) {
+                       if (future_values[i].expiration>=expiration)
+                               return false;
+                       if (future_index < i) {
+                               suitableindex=i;
+                       }
+               }
+       }
 
-       future_values.push_back(value);
+       if (suitableindex!=-1) {
+               future_values[suitableindex].expiration=expiration;
+               return true;
+       }
+       struct future_value newfv={value, expiration};
+       future_values.push_back(newfv);
        return true;
 }
 
@@ -218,9 +231,15 @@ void Node::add_read_from(const ModelAction *act)
  */
 uint64_t Node::get_future_value() {
        ASSERT(future_index<future_values.size());
-       return future_values[future_index];
+       return future_values[future_index].value;
 }
 
+modelclock_t Node::get_future_value_expiration() {
+       ASSERT(future_index<future_values.size());
+       return future_values[future_index].expiration;
+}
+
+
 int Node::get_read_from_size() {
        return may_read_from.size();
 }

diff --git a/nodestack.h b/nodestack.h
index b391645b3af7a458e9271fc1bd60d762c5935605..6c9779497e71f96e0621b37e762fbb199bd0556c 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -10,6 +10,7 @@
 #include <cstddef>
 #include "threads.h"
 #include "mymemory.h"
+#include "clockvector.h"
 
 class ModelAction;
 
@@ -26,6 +27,12 @@ typedef enum {
        PROMISE_FULFILLED /**< This promise is applicable and fulfilled */
 } promise_t;
 
+struct future_value {
+       uint64_t value;
+       modelclock_t expiration;
+};
+
+
 /**
  * @brief A single node in a NodeStack
  *
@@ -55,8 +62,9 @@ public:
         * occurred previously in the stack. */
        Node * get_parent() const { return parent; }
 
-       bool add_future_value(uint64_t value);
+       bool add_future_value(uint64_t value, modelclock_t expiration);
        uint64_t get_future_value();
+       modelclock_t get_future_value_expiration();
        bool increment_future_value();
        bool future_value_empty();
 
@@ -92,7 +100,7 @@ private:
 
        unsigned int read_from_index;
 
-       std::vector< uint64_t, MyAlloc< uint64_t > > future_values;
+       std::vector< struct future_value, MyAlloc<struct future_value> > future_values;
        std::vector< promise_t, MyAlloc<promise_t> > promises;
        unsigned int future_index;
 };

diff --git a/promise.h b/promise.h
index d729e0309868846425d0c439962187b7aa83de44..83198b27758ffffa4f783986f2f1125e7c654c48 100644 (file)
--- a/promise.h
+++ b/promise.h
@@ -13,15 +13,17 @@ class ModelAction;
 
 class Promise {
  public:
-       Promise(ModelAction *act, uint64_t value) :
-               value(value), read(act), numthreads(1)
+ Promise(ModelAction *act, uint64_t value, modelclock_t expiration) :
+       value(value), expiration(expiration), read(act), numthreads(1)
        { }
+       modelclock_t get_expiration() const {return expiration;}
        ModelAction * get_action() const { return read; }
        int increment_threads() { return ++numthreads; }
        uint64_t get_value() const { return value; }
 
  private:
        const uint64_t value;
+       const modelclock_t expiration;
        ModelAction * const read;
        unsigned int numthreads;
 };