More work towards freeing old ModelActions

diff --git a/action.h b/action.h
index 9486c9df7b39a4835ed345133b64fa73467c223b..b7e6f4797c7b8094ccee993ed0b58547ed772f9e 100644 (file)
--- a/action.h
+++ b/action.h
@@ -77,6 +77,7 @@ typedef enum action_type {
        ATOMIC_WAIT,    // < A wait action
        ATOMIC_TIMEDWAIT,       // < A timed wait action
        ATOMIC_ANNOTATION,      // < An annotation action to pass information to a trace analysis
+       READY_FREE
 } action_type_t;
 
 
@@ -100,6 +101,7 @@ public:
 
        thread_id_t get_tid() const { return tid; }
        action_type get_type() const { return type; }
+       void set_free() { type = READY_FREE; }
        memory_order get_mo() const { return order; }
        memory_order get_original_mo() const { return original_order; }
        void set_mo(memory_order order) { this->order = order; }

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 849c00d9cbc586a0a8ff2b2d3edf274432e0ff95..436464f9d361344de844e04da1cccdcbe15154db 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -43,7 +43,7 @@ CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
  * @param action The ModelAction to find a node for
  * @return The CycleNode paired with this action
  */
-CycleNode * CycleGraph::getNode(const ModelAction *action)
+CycleNode * CycleGraph::getNode(ModelAction *action)
 {
        CycleNode *node = getNode_noCreate(action);
        if (node == NULL) {
@@ -107,7 +107,7 @@ void CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode, bool forcee
  * @param rmw The edge points to this ModelAction; this action must read from
  * the ModelAction from
  */
-void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
+void CycleGraph::addRMWEdge(ModelAction *from, ModelAction *rmw)
 {
        ASSERT(from);
        ASSERT(rmw);
@@ -138,7 +138,7 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
        addNodeEdge(fromnode, rmwnode, true);
 }
 
-void CycleGraph::addEdges(SnapList<ModelAction *> * edgeset, const ModelAction *to) {
+void CycleGraph::addEdges(SnapList<ModelAction *> * edgeset, ModelAction *to) {
        for(sllnode<ModelAction*> * it = edgeset->begin();it!=NULL;) {
                ModelAction *act = it->getVal();
                CycleNode *node = getNode(act);
@@ -182,7 +182,7 @@ endouterloop:
  * @return True, if new edge(s) are added; otherwise false
  */
 
-void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
+void CycleGraph::addEdge(ModelAction *from, ModelAction *to)
 {
        ASSERT(from);
        ASSERT(to);
@@ -193,7 +193,7 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
        addNodeEdge(fromnode, tonode, false);
 }
 
-void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to, bool forceedge)
+void CycleGraph::addEdge(ModelAction *from, ModelAction *to, bool forceedge)
 {
        ASSERT(from);
        ASSERT(to);
@@ -304,7 +304,7 @@ void CycleGraph::freeAction(const ModelAction * act) {
  * @brief Constructor for a CycleNode
  * @param act The ModelAction for this node
  */
-CycleNode::CycleNode(const ModelAction *act) :
+CycleNode::CycleNode(ModelAction *act) :
        action(act),
        hasRMW(NULL),
        cv(new ClockVector(NULL, act))
@@ -340,6 +340,21 @@ unsigned int CycleNode::getNumEdges() const
        return edges.size();
 }
 
+/**
+ * @param i The index of the edge to return
+ * @returns The CycleNode edge indexed by i
+ */
+CycleNode * CycleNode::getInEdge(unsigned int i) const
+{
+       return inedges[i];
+}
+
+/** @returns The number of edges leaving this CycleNode */
+unsigned int CycleNode::getNumInEdges() const
+{
+       return inedges.size();
+}
+
 /**
  * Adds an edge from this CycleNode to another CycleNode.
  * @param node The node to which we add a directed edge

diff --git a/cyclegraph.h b/cyclegraph.h
index bbf7aaf16f71233a19b77d67073909bf9dbf267a..a7e2a115929066e03b5f0a018509f78e145d7c1f 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -23,10 +23,10 @@ class CycleGraph {
 public:
        CycleGraph();
        ~CycleGraph();
-       void addEdges(SnapList<ModelAction *> * edgeset, const ModelAction *to);
-       void addEdge(const ModelAction *from, const ModelAction *to);
-       void addEdge(const ModelAction *from, const ModelAction *to, bool forceedge);
-       void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
+       void addEdges(SnapList<ModelAction *> * edgeset, ModelAction *to);
+       void addEdge(ModelAction *from, ModelAction *to);
+       void addEdge(ModelAction *from, ModelAction *to, bool forceedge);
+       void addRMWEdge(ModelAction *from, ModelAction *rmw);
        bool checkReachable(const ModelAction *from, const ModelAction *to) const;
        void freeAction(const ModelAction * act);
 #if SUPPORT_MOD_ORDER_DUMP
@@ -41,7 +41,7 @@ public:
 private:
        void addNodeEdge(CycleNode *fromnode, CycleNode *tonode, bool forceedge);
        void putNode(const ModelAction *act, CycleNode *node);
-       CycleNode * getNode(const ModelAction *act);
+       CycleNode * getNode(ModelAction *act);
 
        /** @brief A table for mapping ModelActions to CycleNodes */
        HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
@@ -59,21 +59,23 @@ private:
  */
 class CycleNode {
 public:
-       CycleNode(const ModelAction *act);
+       CycleNode(ModelAction *act);
        void addEdge(CycleNode *node);
        CycleNode * getEdge(unsigned int i) const;
        unsigned int getNumEdges() const;
+       CycleNode * getInEdge(unsigned int i) const;
+       unsigned int getNumInEdges() const;
        bool setRMW(CycleNode *);
        CycleNode * getRMW() const;
        void clearRMW() { hasRMW = NULL; }
-       const ModelAction * getAction() const { return action; }
+       ModelAction * getAction() const { return action; }
        void removeInEdge(CycleNode *src);
        ~CycleNode();
 
        SNAPSHOTALLOC
 private:
        /** @brief The ModelAction that this node represents */
-       const ModelAction *action;
+       ModelAction *action;
 
        /** @brief The edges leading out from this node */
        SnapVector<CycleNode *> edges;

diff --git a/execution.cc b/execution.cc
index e4c05cfcf1764ad7d62a2b7a90524282f9e01908..1590d1c03f59131ad27c72668881d35d1edc9fc2 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -281,7 +281,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
  */
 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 {
-       SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
+       SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
        bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
        if (hasnonatomicstore) {
                ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
@@ -774,7 +774,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  */
 
 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
-                                                                                                                                                                       SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
+                                                                                                                                                                       SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;
@@ -868,7 +868,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                        if (!check_only)
                                                priorset->push_back(act);
                                } else {
-                                       const ModelAction *prevrf = act->get_reads_from();
+                                       ModelAction *prevrf = act->get_reads_from();
                                        if (!prevrf->equals(rf)) {
                                                if (mo_graph->checkReachable(rf, prevrf))
                                                        return false;
@@ -1696,20 +1696,48 @@ ClockVector * ModelExecution::computeMinimalCV() {
 void ModelExecution::collectActions() {
        //Compute minimal clock vector for all live threads
        ClockVector *cvmin = computeMinimalCV();
-
+       SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
        //walk action trace...  When we hit an action ,see if it is
        //invisible (e.g., earlier than the first before the minimum
        //clock for the thread...  if so erase it and all previous
        //actions in cyclegraph
        for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
                ModelAction *act = it->getVal();
+               modelclock_t actseq = act->get_seq_number();
+               thread_id_t act_tid = act->get_tid();
+               modelclock_t tid_clock = cvmin->getClock(act_tid);
+               if (actseq <= tid_clock) {
+                       ModelAction * write;
+                       if (act->is_write()) {
+                               write = act;
+                       } else if (act->is_read()) {
+                               write = act->get_reads_from();
+                       } else
+                               continue;
 
+                       //Mark everything earlier in MO graph to be freed
+                       queue->push_back(mo_graph->getNode_noCreate(write));
+                       while(!queue->empty()) {
+                               CycleNode * node = queue->back();
+                               queue->pop_back();
+                               for(unsigned int i=0;i<node->getNumInEdges();i++) {
+                                       CycleNode * prevnode = node->getInEdge(i);
+                                       ModelAction * prevact = prevnode->getAction();
+                                       if (prevact->get_type() != READY_FREE) {
+                                               prevact->set_free();
+                                               queue->push_back(prevnode);
+                                       }
+                               }
+                       }
+               }
        }
 
-
        delete cvmin;
+       delete queue;
 }
 
+
+
 Fuzzer * ModelExecution::getFuzzer() {
        return fuzzer;
 }

diff --git a/execution.h b/execution.h
index abec71269bb79a8448393be9691b1ac0c0526a36..1aaa9db3b79d7a280f689f935de3c27dcf334548 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -118,7 +118,7 @@ private:
        ModelAction * get_last_unlock(ModelAction *curr) const;
        SnapVector<ModelAction *> * build_may_read_from(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
-       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset, bool *canprune, bool check_only = false);
+       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<ModelAction *> *priorset, bool *canprune, bool check_only = false);
        void w_modification_order(ModelAction *curr);
        ClockVector * get_hb_from_write(ModelAction *rf) const;
        ModelAction * convertNonAtomicStore(void*);