separate out rmw actions

make sure we don't insert promises twice for a node

diff --git a/Makefile b/Makefile
index 2acdbc7dff8a7738c6f99349421aa66bc97b5d5b..67b6e6dfa5212438321639f5e4ef11bc8e2768e5 100644 (file)
--- 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 f519dac93b39975742887746f79a194e63dd12fe..2bac4de7cf0469c57818ceab835458a872bb7c29 100644 (file)
--- 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 8a9bf7c928186ec3b39c0efd5022ae1ccfd8c1d1..013a11a793bd9f20971a881af2c104a59e3085ec 100644 (file)
--- 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<CycleNode *> rollbackvector;
        std::vector<CycleNode *> rmwrollbackvector;
 };

diff --git a/model.cc b/model.cc
index cc464a2bcc5b76b933d8769ba450486b4804edbf..bd4ade23d540e371bb63ec7324ec933f7fb425db 100644 (file)
--- 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 bcb9d61a5e6d02e317a9428395b451b7e6285aec..fec8d1f1ea55bf331017f9817515cae7e0d93c34 100644 (file)
--- 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<const ModelAction *> *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;