From 9077381b71d4e95f5e25204480159decf16281a7 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Thu, 12 Dec 2019 23:31:57 -0800 Subject: [PATCH] towards freeing actions --- clockvector.cc | 26 ++++++++++++++++++++++++++ clockvector.h | 1 + cyclegraph.cc | 30 ++++++++++++++++++++++++++---- cyclegraph.h | 10 ++++++---- execution.cc | 34 ++++++++++++++++++++++++++++++++++ execution.h | 4 +++- main.cc | 1 + params.h | 1 + 8 files changed, 98 insertions(+), 9 deletions(-) diff --git a/clockvector.cc b/clockvector.cc index 2336df2f..5e25e00f 100644 --- 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 962e9ec4..1a36a39d 100644 --- 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 f8d3b852..849c00d9 100644 --- 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;iedges.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 c9481b78..bbf7aaf1 100644 --- 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 edges; + /** @brief The edges leading in from this node */ + SnapVector 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 d6988edf..e4c05cfc 100644 --- a/execution.cc +++ b/execution.cc @@ -1672,8 +1672,42 @@ void ModelExecution::removeAction(ModelAction *act) { SnapVector *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* 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 854513cd..abec7126 100644 --- 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 8fa1e9dd..17bc71c8 100644 --- 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 b4bfc7e7..2c007c63 100644 --- 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; -- 2.34.1