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,
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;
if (tonode != rmwnode) {
rmwnode->addEdge(tonode);
}
- tonode->refcount--;
+ tonode->removeInEdge(fromnode);
}
fromnode->edges.clear();
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
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
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 */
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;
CycleNode * getRMW() const;
void clearRMW() { hasRMW = NULL; }
const ModelAction * getAction() const { return action; }
+ void removeInEdge(CycleNode *src);
+ ~CycleNode();
SNAPSHOTALLOC
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;
/** ClockVector for this Node. */
ClockVector *cv;
friend class CycleGraph;
-
- /** @brief Reference count to node. */
- int refcount;
};
#endif /* __CYCLEGRAPH_H__ */
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() {
bool isFinished() {return isfinished;}
void setFinished() {isfinished = true;}
-
void restore_last_seq_num();
+ void collectActions();
+
#ifdef TLS
pthread_key_t getPthreadKey() {return pthreadkey;}
#endif
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
{
params->verbose = !!DBG_ENABLED();
params->maxexecutions = 10;
+ params->tracebound = 0;
params->nofork = false;
}
struct model_params {
int maxexecutions;
bool nofork;
+ unsigned int tracebound;
/** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
int verbose;