towards freeing actions

diff --git a/clockvector.cc b/clockvector.cc
index 2336df2f4720f6bea613891859591ddf47488fc3..5e25e00f1ac625fc0c116b563dd83ffd4040d296 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -62,6 +62,32 @@ bool ClockVector::merge(const ClockVector *cv)
        return changed;
 }
 
+/**
+ * Merge a clock vector into this vector, using a pairwise comparison. The
+ * resulting vector length will be the maximum length of the two being merged.
+ * @param cv is the ClockVector being merged into this vector.
+ */
+bool ClockVector::minmerge(const ClockVector *cv)
+{
+       ASSERT(cv != NULL);
+       bool changed = false;
+       if (cv->num_threads > num_threads) {
+               clock = (modelclock_t *)snapshot_realloc(clock, cv->num_threads * sizeof(modelclock_t));
+               for (int i = num_threads;i < cv->num_threads;i++)
+                       clock[i] = 0;
+               num_threads = cv->num_threads;
+       }
+
+       /* Element-wise maximum */
+       for (int i = 0;i < cv->num_threads;i++)
+               if (cv->clock[i] < clock[i]) {
+                       clock[i] = cv->clock[i];
+                       changed = true;
+               }
+
+       return changed;
+}
+
 /**
  * Check whether this vector's thread has synchronized with another action's
  * thread. This effectively checks the happens-before relation (or actually,

diff --git a/clockvector.h b/clockvector.h
index 962e9ec4844995c811638030d5a7c11a983ea36e..1a36a39dc040838f2c37b8166a8faf9b9a6a80fd 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -14,6 +14,7 @@ public:
        ClockVector(ClockVector *parent = NULL, const ModelAction *act = NULL);
        ~ClockVector();
        bool merge(const ClockVector *cv);
+       bool minmerge(const ClockVector *cv);
        bool synchronized_since(const ModelAction *act) const;
 
        void print() const;

diff --git a/cyclegraph.cc b/cyclegraph.cc
index f8d3b85297b981b98ceff9930b726f854d9a6f42..849c00d9cbc586a0a8ff2b2d3edf274432e0ff95 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -131,7 +131,7 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
                if (tonode != rmwnode) {
                        rmwnode->addEdge(tonode);
                }
-               tonode->refcount--;
+               tonode->removeInEdge(fromnode);
        }
        fromnode->edges.clear();
 
@@ -291,6 +291,15 @@ bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to)
        return checkReachable(fromnode, tonode);
 }
 
+void CycleGraph::freeAction(const ModelAction * act) {
+       CycleNode *cn = actionToNode.remove(act);
+       for(unsigned int i=0;i<cn->edges.size();i++) {
+               CycleNode *dst = cn->edges[i];
+               dst->removeInEdge(cn);
+       }
+       delete cn;
+}
+
 /**
  * @brief Constructor for a CycleNode
  * @param act The ModelAction for this node
@@ -298,11 +307,24 @@ bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to)
 CycleNode::CycleNode(const ModelAction *act) :
        action(act),
        hasRMW(NULL),
-       cv(new ClockVector(NULL, act)),
-       refcount(0)
+       cv(new ClockVector(NULL, act))
 {
 }
 
+CycleNode::~CycleNode() {
+       delete cv;
+}
+
+void CycleNode::removeInEdge(CycleNode *src) {
+       for(unsigned int i=0;i < edges.size();i++) {
+               if (edges[i] == src) {
+                       edges[i] = edges[edges.size()-1];
+                       edges.pop_back();
+                       break;
+               }
+       }
+}
+
 /**
  * @param i The index of the edge to return
  * @returns The CycleNode edge indexed by i
@@ -329,7 +351,7 @@ void CycleNode::addEdge(CycleNode *node)
                if (edges[i] == node)
                        return;
        edges.push_back(node);
-       node->refcount++;
+       node->inedges.push_back(this);
 }
 
 /** @returns the RMW CycleNode that reads from the current CycleNode */

diff --git a/cyclegraph.h b/cyclegraph.h
index c9481b788caf00fd939670e45a99c7b8256ae445..bbf7aaf16f71233a19b77d67073909bf9dbf267a 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -28,7 +28,7 @@ public:
        void addEdge(const ModelAction *from, const ModelAction *to, bool forceedge);
        void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
        bool checkReachable(const ModelAction *from, const ModelAction *to) const;
-
+       void freeAction(const ModelAction * act);
 #if SUPPORT_MOD_ORDER_DUMP
        void dumpNodes(FILE *file) const;
        void dumpGraphToFile(const char *filename) const;
@@ -67,6 +67,8 @@ public:
        CycleNode * getRMW() const;
        void clearRMW() { hasRMW = NULL; }
        const ModelAction * getAction() const { return action; }
+       void removeInEdge(CycleNode *src);
+       ~CycleNode();
 
        SNAPSHOTALLOC
 private:
@@ -76,6 +78,9 @@ private:
        /** @brief The edges leading out from this node */
        SnapVector<CycleNode *> edges;
 
+       /** @brief The edges leading in from this node */
+       SnapVector<CycleNode *> inedges;
+
        /** Pointer to a RMW node that reads from this node, or NULL, if none
         * exists */
        CycleNode *hasRMW;
@@ -83,9 +88,6 @@ private:
        /** ClockVector for this Node. */
        ClockVector *cv;
        friend class CycleGraph;
-
-       /** @brief Reference count to node. */
-       int refcount;
 };
 
 #endif /* __CYCLEGRAPH_H__ */

diff --git a/execution.cc b/execution.cc
index d6988edf3096008288213af4ff20f8b096d1409b..e4c05cfcf1764ad7d62a2b7a90524282f9e01908 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1672,8 +1672,42 @@ void ModelExecution::removeAction(ModelAction *act) {
                        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
                        (*vec)[act->get_tid()].erase(listref);
                }
+               //Remove from Cyclegraph
+               mo_graph->freeAction(act);
        }
+}
+
+ClockVector * ModelExecution::computeMinimalCV() {
+       ClockVector *cvmin = NULL;
+       for(unsigned int i = 0;i < thread_map.size();i++) {
+               Thread * t = thread_map[i];
+               if (t->get_state() == THREAD_COMPLETED)
+                       continue;
+               thread_id_t tid = int_to_id(i);
+               ClockVector * cv = get_cv(tid);
+               if (cvmin == NULL)
+                       cvmin = new ClockVector(cv, NULL);
+               else
+                       cvmin->minmerge(cv);
+       }
+       return cvmin;
+}
+
+void ModelExecution::collectActions() {
+       //Compute minimal clock vector for all live threads
+       ClockVector *cvmin = computeMinimalCV();
+
+       //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();
+
+       }
+
 
+       delete cvmin;
 }
 
 Fuzzer * ModelExecution::getFuzzer() {

diff --git a/execution.h b/execution.h
index 854513cd4b16cc4c6bc74ad0916fe6d108ea6a78..abec71269bb79a8448393be9691b1ac0c0526a36 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -87,8 +87,9 @@ public:
 
        bool isFinished() {return isfinished;}
        void setFinished() {isfinished = true;}
-
        void restore_last_seq_num();
+       void collectActions();
+
 #ifdef TLS
        pthread_key_t getPthreadKey() {return pthreadkey;}
 #endif
@@ -121,6 +122,7 @@ private:
        void w_modification_order(ModelAction *curr);
        ClockVector * get_hb_from_write(ModelAction *rf) const;
        ModelAction * convertNonAtomicStore(void*);
+       ClockVector * computeMinimalCV();
        void removeAction(ModelAction *act);
 
 #ifdef TLS

diff --git a/main.cc b/main.cc
index 8fa1e9dd99a52076043b821653836f916bbb489d..17bc71c86a87783614ffe5200e68d54ff0fc12c1 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -21,6 +21,7 @@ void param_defaults(struct model_params *params)
 {
        params->verbose = !!DBG_ENABLED();
        params->maxexecutions = 10;
+       params->tracebound = 0;
        params->nofork = false;
 }
 

diff --git a/params.h b/params.h
index b4bfc7e7b7921b62c80ccf82ba2c0b2bdd30f925..2c007c631a4926ef5e5690e4ea39115c0bf87237 100644 (file)
--- a/params.h
+++ b/params.h
@@ -8,6 +8,7 @@
 struct model_params {
        int maxexecutions;
        bool nofork;
+       unsigned int tracebound;
 
        /** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
        int verbose;