From 0cb05db166b91ab2820fd8c58b6903ca3a455e04 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 12 Sep 2012 20:35:47 -0700 Subject: [PATCH] separate out rmw actions make sure we don't insert promises twice for a node --- Makefile | 2 +- cyclegraph.cc | 13 +++++++++++-- cyclegraph.h | 5 ++++- model.cc | 44 +++++++++++++++++++++++++++++++++++++++----- model.h | 5 +++-- 5 files changed, 58 insertions(+), 11 deletions(-) diff --git a/Makefile b/Makefile index 2acdbc7d..67b6e6df 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,7 @@ include $(DEPS) debug: CPPFLAGS += -DCONFIG_DEBUG debug: all -mac: CPPFLAGS += -D_XOPEN_SOURCE -DMAC +mac: CPPFLAGS += -D_XOPEN_SOURCE -DMAC -DCONFIG_DEBUG mac: LDFLAGS=-ldl mac: SHARED=-Wl,-undefined,dynamic_lookup -dynamiclib mac: all diff --git a/cyclegraph.cc b/cyclegraph.cc index f519dac9..2bac4de7 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -5,7 +5,9 @@ /** Initializes a CycleGraph object. */ CycleGraph::CycleGraph() : hasCycles(false), - oldCycles(false) + oldCycles(false), + hasRMWViolation(false), + oldRMWViolation(false) { } @@ -77,7 +79,7 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) { /* Two RMW actions cannot read from the same write. */ if (fromnode->setRMW(rmwnode)) { - hasCycles=true; + hasRMWViolation=true; } else { rmwrollbackvector.push_back(fromnode); } @@ -144,6 +146,7 @@ void CycleGraph::startChanges() { ASSERT(rollbackvector.size()==0); ASSERT(rmwrollbackvector.size()==0); ASSERT(oldCycles==hasCycles); + ASSERT(oldRMWViolation==hasRMWViolation); } /** Commit changes to the cyclegraph. */ @@ -151,6 +154,7 @@ void CycleGraph::commitChanges() { rollbackvector.resize(0); rmwrollbackvector.resize(0); oldCycles=hasCycles; + oldRMWViolation=hasRMWViolation; } /** Rollback changes to the previous commit. */ @@ -164,6 +168,7 @@ void CycleGraph::rollbackChanges() { } hasCycles = oldCycles; + hasRMWViolation = oldRMWViolation; rollbackvector.resize(0); rmwrollbackvector.resize(0); } @@ -173,6 +178,10 @@ bool CycleGraph::checkForCycles() { return hasCycles; } +bool CycleGraph::checkForRMWViolation() { + return hasRMWViolation; +} + /** * Constructor for a CycleNode. * @param modelaction The ModelAction for this node diff --git a/cyclegraph.h b/cyclegraph.h index 8a9bf7c9..013a11a7 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -19,6 +19,7 @@ class CycleGraph { ~CycleGraph(); void addEdge(const ModelAction *from, const ModelAction *to); bool checkForCycles(); + bool checkForRMWViolation(); void addRMWEdge(const ModelAction *from, const ModelAction *rmw); bool checkReachable(const ModelAction *from, const ModelAction *to); @@ -36,9 +37,11 @@ class CycleGraph { /** @brief A flag: true if this graph contains cycles */ bool hasCycles; - bool oldCycles; + bool hasRMWViolation; + bool oldRMWViolation; + std::vector rollbackvector; std::vector rmwrollbackvector; }; diff --git a/model.cc b/model.cc index cc464a2b..bd4ade23 100644 --- a/model.cc +++ b/model.cc @@ -291,7 +291,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part mo_graph->commitChanges(); updated |= r_status; - } else { + } else if (!second_part_of_rmw) { /* Read from future value */ value = curr->get_node()->get_future_value(); modelclock_t expiration = curr->get_node()->get_future_value_expiration(); @@ -454,6 +454,11 @@ bool ModelChecker::isfeasibleprefix() { /** @returns whether the current partial trace is feasible. */ bool ModelChecker::isfeasible() { + return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW(); +} + +/** @returns whether the current partial trace is feasible. */ +bool ModelChecker::isfeasibleotherthanRMW() { return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired(); } @@ -704,9 +709,14 @@ 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(), curr->get_seq_number()+params.maxfuturedelay) && - (!priv->next_backtrack || *act > *priv->next_backtrack)) - priv->next_backtrack = act; + if (thin_air_constraint_may_allow(curr, act)) { + if (isfeasible() || + (curr->is_rmw() && act->is_rmw() && curr->get_reads_from()==act->get_reads_from() && isfeasibleotherthanRMW())) { + if (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; + } + } } } } @@ -714,6 +724,29 @@ bool ModelChecker::w_modification_order(ModelAction *curr) return added; } +/** 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) { + if (!writer->is_rmw()) + return true; + + if (!reader->is_rmw()) + return true; + + for(const ModelAction *search=writer->get_reads_from();search!=NULL;search=search->get_reads_from()) { + if (search==reader) + return false; + if (search->get_tid()==reader->get_tid()&& + search->happens_before(reader)) + break; + } + + return true; +} + + /** * Finds the head(s) of the release sequence(s) containing a given ModelAction. * The ModelAction under consideration is expected to be taking part in @@ -988,6 +1021,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) bool ModelChecker::resolve_promises(ModelAction *write) { bool resolved = false; + for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; if (write->get_node()->get_promise(i)) { @@ -1003,7 +1037,6 @@ bool ModelChecker::resolve_promises(ModelAction *write) } else promise_index++; } - return resolved; } @@ -1193,6 +1226,7 @@ bool ModelChecker::take_step() { if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); + priv->nextThread = check_current_action(priv->current_action); priv->current_action = NULL; if (!curr->is_blocked() && !curr->is_complete()) diff --git a/model.h b/model.h index bcb9d61a..fec8d1f1 100644 --- a/model.h +++ b/model.h @@ -75,11 +75,11 @@ public: ModelAction * get_parent_action(thread_id_t tid); bool next_execution(); bool isfeasible(); + bool isfeasibleotherthanRMW(); bool isfinalfeasible(); void check_promises(ClockVector *old_cv, ClockVector * merge_cv); void get_release_seq_heads(ModelAction *act, std::vector *release_heads); - void finish_execution(); bool isfeasibleprefix(); void set_assert() {asserted=true;} @@ -88,7 +88,8 @@ public: private: /** The scheduler to use: tracks the running/ready Threads */ Scheduler *scheduler; - + + bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader); bool has_asserted() {return asserted;} void reset_asserted() {asserted=false;} int num_executions; -- 2.34.1