cyclegraph.h

   1 /** @file cyclegraph.h @brief Data structure to track ordering
   2  *  constraints on modification order.  The idea is to see whether a
   3  *  total order exists that satisfies the ordering constriants.*/
   4
   5 #ifndef CYCLEGRAPH_H
   6 #define CYCLEGRAPH_H
   7
   8 #include "hashtable.h"
   9 #include <vector>
  10 #include <inttypes.h>
  11 #include "config.h"
  12 #include "mymemory.h"
  13
  14 class Promise;
  15 class CycleNode;
  16 class ModelAction;
  17
  18 /** @brief A graph of Model Actions for tracking cycles. */
  19 class CycleGraph {
  20  public:
  21         CycleGraph();
  22         ~CycleGraph();
  23         void addEdge(const ModelAction *from, const ModelAction *to);
  24         bool checkForCycles();
  25         bool checkForRMWViolation();
  26         void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
  27         bool checkPromise(const ModelAction *from, Promise *p);
  28         bool checkReachable(const ModelAction *from, const ModelAction *to);
  29         void startChanges();
  30         void commitChanges();
  31         void rollbackChanges();
  32 #if SUPPORT_MOD_ORDER_DUMP
  33         void dumpNodes(FILE *file);
  34         void dumpGraphToFile(const char *filename);
  35 #endif
  36
  37         SNAPSHOTALLOC
  38  private:
  39         CycleNode * getNode(const ModelAction *);
  40         HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> *discovered;
  41
  42         /** @brief A table for mapping ModelActions to CycleNodes */
  43         HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
  44 #if SUPPORT_MOD_ORDER_DUMP
  45         std::vector<CycleNode *> nodeList;
  46 #endif
  47
  48         bool checkReachable(CycleNode *from, CycleNode *to);
  49
  50         /** @brief A flag: true if this graph contains cycles */
  51         bool hasCycles;
  52         bool oldCycles;
  53
  54         bool hasRMWViolation;
  55         bool oldRMWViolation;
  56
  57         std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > rollbackvector;
  58         std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > rmwrollbackvector;
  59 };
  60
  61 /** @brief A node within a CycleGraph; corresponds to one ModelAction */
  62 class CycleNode {
  63  public:
  64         CycleNode(const ModelAction *action);
  65         bool addEdge(CycleNode *node);
  66         CycleNode * getEdge(unsigned int i) const;
  67         unsigned int getNumEdges() const;
  68         bool setRMW(CycleNode *);
  69         CycleNode * getRMW() const;
  70         const ModelAction * getAction() const { return action; }
  71
  72         void popEdge() {
  73                 edges.pop_back();
  74         }
  75         void clearRMW() {
  76                 hasRMW = NULL;
  77         }
  78
  79         SNAPSHOTALLOC
  80  private:
  81         /** @brief The ModelAction that this node represents */
  82         const ModelAction *action;
  83
  84         /** @brief The edges leading out from this node */
  85         std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > edges;
  86
  87         /** Pointer to a RMW node that reads from this node, or NULL, if none
  88          * exists */
  89         CycleNode *hasRMW;
  90 };
  91
  92 #endif