From 6ec6d90066682d8849af174e531e4e0d547ebab3 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Thu, 26 Jul 2012 16:20:02 -0700 Subject: [PATCH] more changes towards keeping track of promises resolved by a given write statement --- model.cc | 22 ++++++++++++++++++++-- model.h | 1 + nodestack.cc | 50 ++++++++++++++++++++++++++++++++++++++++++-------- nodestack.h | 17 +++++++++++++---- promise.h | 1 + 5 files changed, 77 insertions(+), 14 deletions(-) diff --git a/model.cc b/model.cc index 29e16aa..de56873 100644 --- a/model.cc +++ b/model.cc @@ -22,7 +22,6 @@ ModelChecker::ModelChecker() /* First thread created will have id INITIAL_THREAD_ID */ next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), - num_executions(0), current_action(NULL), diverge(NULL), @@ -320,6 +319,7 @@ void ModelChecker::check_current_action(void) } } else if (curr->is_write()) { w_modification_order(curr); + resolve_promises(curr); } th->set_return_value(value); @@ -515,6 +515,24 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) { return get_parent_action(tid)->get_cv(); } + +/** Resolve promises. */ + +void ModelChecker::resolve_promises(ModelAction *curr) { + for(unsigned int i=0;isize();i++) { + Promise * promise=(*promises)[i]; + const ModelAction * act=promise->get_action(); + if (!act->happens_before(curr)&& + act->is_read()&& + !act->is_synchronizing(curr)&& + !act->same_thread(curr)&& + promise->get_value()==curr->get_value()) { + + + } + } +} + /** Checks promises in response to change in ClockVector Threads. */ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) { @@ -567,7 +585,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - + /* Only consider 'write' actions */ if (!act->is_write()) continue; diff --git a/model.h b/model.h index e6dc06d..3c22555 100644 --- a/model.h +++ b/model.h @@ -78,6 +78,7 @@ private: thread_id_t get_next_replay_thread(); ModelAction * get_next_backtrack(); void reset_to_initial_state(); + void resolve_promises(ModelAction *curr); void add_action_to_lists(ModelAction *act); ModelAction * get_last_action(thread_id_t tid); diff --git a/nodestack.cc b/nodestack.cc index 0828358..6eb71dc 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -57,19 +57,60 @@ void Node::print_may_read_from() (*it)->print(); } +void Node::set_promise(uint32_t i) { + if (i>=promises.size()) + promises.resize(i+1,0); + promises[i]=1; +} + +bool Node::get_promise(uint32_t i) { + return (promises[i]==2); +} + +bool Node::increment_promises() { + for (unsigned int i=0;i0); + return true; + } + } + return false; +} + +bool Node::promises_empty() { + for (unsigned int i=0;i=future_values.size()); +} + /** * Checks if the Thread associated with this thread ID has been explored from @@ -102,14 +143,7 @@ bool Node::readsfrom_empty() { return ((read_from_index+1)>=may_read_from.size()); } -/** - * Checks whether the future_values set for this node is empty. - * @return true if the future_values set is empty. - */ -bool Node::futurevalues_empty() { - return ((future_index+1)>=future_values.size()); -} /** * Mark the appropriate backtracking information for exploring a thread choice. diff --git a/nodestack.h b/nodestack.h index 9ccde8d..4162ff7 100644 --- a/nodestack.h +++ b/nodestack.h @@ -15,6 +15,7 @@ class ModelAction; typedef std::vector< const ModelAction *, MyAlloc< const ModelAction * > > readfrom_set_t; typedef std::vector< uint64_t, MyAlloc< uint64_t > > futurevalues_t; +typedef std::vector< uint32_t, MyAlloc< uint32_t > > promises_t; /** * @brief A single node in a NodeStack @@ -33,8 +34,7 @@ public: bool has_been_explored(thread_id_t tid); /* return true = backtrack set is empty */ bool backtrack_empty(); - bool readsfrom_empty(); - bool futurevalues_empty(); + void explore_child(ModelAction *act); /* return false = thread was already in backtrack */ bool set_backtrack(thread_id_t id); @@ -47,11 +47,19 @@ public: Node * get_parent() const { return parent; } bool add_future_value(uint64_t value); + uint64_t get_future_value(); + bool increment_future_values(); + bool futurevalues_empty(); + void add_read_from(const ModelAction *act); const ModelAction * get_read_from(); - uint64_t get_future_value(); bool increment_read_from(); - bool increment_future_values(); + bool readsfrom_empty(); + + void set_promise(uint32_t i); + bool get_promise(uint32_t i); + bool increment_promises(); + bool promises_empty(); void print(); void print_may_read_from(); @@ -73,6 +81,7 @@ private: unsigned int read_from_index; futurevalues_t future_values; + promises_t promises; unsigned int future_index; }; diff --git a/promise.h b/promise.h index 180d9b0..0bf62d6 100644 --- a/promise.h +++ b/promise.h @@ -16,6 +16,7 @@ class Promise { Promise(ModelAction * act, uint64_t value); const ModelAction * get_action() { return read; } int increment_threads() { return ++numthreads; } + uint64_t get_value() { return value; } private: uint64_t value; -- 2.34.1