X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.h;h=1cc0d069531e6499aed90a3972bfd1ff533c3c8f;hb=d96312573c237eb9648976be85de39261c9531c6;hp=8a9bf7c928186ec3b39c0efd5022ae1ccfd8c1d1;hpb=a0562e0739fd643fdb2108f784f4722482ea5a4f;p=c11tester.git diff --git a/cyclegraph.h b/cyclegraph.h index 8a9bf7c9..1cc0d069 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -8,7 +8,10 @@ #include "hashtable.h" #include #include +#include "config.h" +#include "mymemory.h" +class Promise; class CycleNode; class ModelAction; @@ -19,26 +22,37 @@ class CycleGraph { ~CycleGraph(); void addEdge(const ModelAction *from, const ModelAction *to); bool checkForCycles(); + bool checkForRMWViolation(); void addRMWEdge(const ModelAction *from, const ModelAction *rmw); - + bool checkPromise(const ModelAction *from, Promise *p); bool checkReachable(const ModelAction *from, const ModelAction *to); void startChanges(); void commitChanges(); void rollbackChanges(); +#if SUPPORT_MOD_ORDER_DUMP + void dumpNodes(FILE *file); + void dumpGraphToFile(const char * filename); +#endif + SNAPSHOTALLOC private: CycleNode * getNode(const ModelAction *); /** @brief A table for mapping ModelActions to CycleNodes */ HashTable actionToNode; +#if SUPPORT_MOD_ORDER_DUMP + std::vector nodeList; +#endif bool checkReachable(CycleNode *from, CycleNode *to); /** @brief A flag: true if this graph contains cycles */ bool hasCycles; - bool oldCycles; + bool hasRMWViolation; + bool oldRMWViolation; + std::vector rollbackvector; std::vector rmwrollbackvector; }; @@ -47,10 +61,12 @@ class CycleGraph { class CycleNode { public: CycleNode(const ModelAction *action); - void addEdge(CycleNode * node); + bool addEdge(CycleNode * node); std::vector * getEdges(); bool setRMW(CycleNode *); CycleNode* getRMW(); + const ModelAction * getAction() {return action;}; + void popEdge() { edges.pop_back(); }; @@ -58,6 +74,7 @@ class CycleNode { hasRMW=NULL; } + SNAPSHOTALLOC private: /** @brief The ModelAction that this node represents */ const ModelAction *action;