From: Brian Demsky Date: Wed, 12 Sep 2012 22:12:31 +0000 (-0700) Subject: deal with looping due to bogus future value via promise expiration X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=1bc8782b55cab0503f1b64529f993f0b9e3a1846;hp=0c61161a061c85189d4d1531a9ad00caf2f2588d deal with looping due to bogus future value via promise expiration fix promise bug --- diff --git a/main.cc b/main.cc index 215a2197..b58599df 100644 --- 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: [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 00982130..9611f2f6 100644 --- 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()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 19143d36..1a2f6a14 100644 --- 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 a9399edb..431baafb 100644 --- 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 #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 > future_values; std::vector< promise_t, MyAlloc > promises; unsigned int future_index; }; diff --git a/promise.h b/promise.h index d729e030..83198b27 100644 --- 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; };