X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=cyclegraph.h;h=83d3db21d77cdfc192f0bd286d21fee188de7fac;hp=8efd5d416ff05e2b372d2eae183d0686d704d36e;hb=ff29187c639cdb032debdb036d2c9062f77879b0;hpb=ca060d2744dd60d1ed37b7db12aa1814633f95e1 diff --git a/cyclegraph.h b/cyclegraph.h index 8efd5d41..83d3db21 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -19,16 +19,24 @@ class Promise; class CycleNode; class ModelAction; +typedef std::vector< const Promise *, ModelAlloc > promise_list_t; + /** @brief A graph of Model Actions for tracking cycles. */ class CycleGraph { public: CycleGraph(); ~CycleGraph(); - void addEdge(const ModelAction *from, const ModelAction *to); + + template + void addEdge(const T from, const U to); + bool checkForCycles() const; void addRMWEdge(const ModelAction *from, const ModelAction *rmw); bool checkPromise(const ModelAction *from, Promise *p) const; - bool checkReachable(const ModelAction *from, const ModelAction *to) const; + + template + bool checkReachable(const ModelAction *from, const T *to) const; + void startChanges(); void commitChanges(); void rollbackChanges(); @@ -37,15 +45,28 @@ class CycleGraph { void dumpGraphToFile(const char *filename) const; #endif + bool resolvePromise(ModelAction *reader, ModelAction *writer, + promise_list_t *mustResolve); + SNAPSHOTALLOC private: - void addEdge(CycleNode *fromnode, CycleNode *tonode); + void addNodeEdge(CycleNode *fromnode, CycleNode *tonode); void putNode(const ModelAction *act, CycleNode *node); - CycleNode * getNode(const ModelAction *); + CycleNode * getNode(const ModelAction *act); + CycleNode * getNode(const Promise *promise); + CycleNode * getNode_noCreate(const ModelAction *act) const; + CycleNode * getNode_noCreate(const Promise *promise) const; + bool mergeNodes(CycleNode *node1, CycleNode *node2, + promise_list_t *mustMerge); + HashTable *discovered; /** @brief A table for mapping ModelActions to CycleNodes */ HashTable actionToNode; + /** @brief A table for mapping reader ModelActions to Promise + * CycleNodes */ + HashTable readerToPromiseNode; + #if SUPPORT_MOD_ORDER_DUMP std::vector nodeList; #endif @@ -60,29 +81,44 @@ class CycleGraph { std::vector< CycleNode *, SnapshotAlloc > rmwrollbackvector; }; -/** @brief A node within a CycleGraph; corresponds to one ModelAction */ +/** + * @brief A node within a CycleGraph; corresponds either to one ModelAction or + * to a promised future value + */ class CycleNode { public: CycleNode(const ModelAction *act); + CycleNode(const Promise *promise); bool addEdge(CycleNode *node); CycleNode * getEdge(unsigned int i) const; unsigned int getNumEdges() const; CycleNode * getBackEdge(unsigned int i) const; unsigned int getNumBackEdges() const; + CycleNode * removeEdge(); + CycleNode * removeBackEdge(); + bool setRMW(CycleNode *); CycleNode * getRMW() const; void clearRMW() { hasRMW = NULL; } const ModelAction * getAction() const { return action; } + const Promise * getPromise() const { return promise; } void popEdge() { edges.pop_back(); } + bool is_promise() const { return !action; } + void resolvePromise(const ModelAction *writer); + SNAPSHOTALLOC private: /** @brief The ModelAction that this node represents */ const ModelAction *action; + /** @brief The promise represented by this node; only valid when action + * is NULL */ + const Promise *promise; + /** @brief The edges leading out from this node */ std::vector< CycleNode *, SnapshotAlloc > edges; @@ -94,4 +130,46 @@ class CycleNode { CycleNode *hasRMW; }; +/* + * @brief Adds an edge between objects + * + * This function will add an edge between any two objects which can be + * associated with a CycleNode. That is, if they have a CycleGraph::getNode + * implementation. + * + * The object to is ordered after the object from. + * + * @param to The edge points to this object, of type T + * @param from The edge comes from this object, of type U + */ +template +void CycleGraph::addEdge(const T from, const U to) +{ + ASSERT(from); + ASSERT(to); + + CycleNode *fromnode = getNode(from); + CycleNode *tonode = getNode(to); + + addNodeEdge(fromnode, tonode); +} + +/** + * Checks whether one ModelAction can reach another ModelAction/Promise + * @param from The ModelAction from which to begin exploration + * @param to The ModelAction or Promise to reach + * @return True, @a from can reach @a to; otherwise, false + */ +template +bool CycleGraph::checkReachable(const ModelAction *from, const T *to) const +{ + CycleNode *fromnode = getNode_noCreate(from); + CycleNode *tonode = getNode_noCreate(to); + + if (!fromnode || !tonode) + return false; + + return checkReachable(fromnode, tonode); +} + #endif /* __CYCLEGRAPH_H__ */