model: remove unnecessary DEBUG()
[c11tester.git] / 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 *> rollbackvector;
58         std::vector<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         std::vector<CycleNode *> * getEdges();
67         bool setRMW(CycleNode *);
68         CycleNode* getRMW();
69         const ModelAction * getAction() {return action;};
70
71         void popEdge() {
72                 edges.pop_back();
73         };
74         void clearRMW() {
75                 hasRMW=NULL;
76         }
77
78         SNAPSHOTALLOC
79  private:
80         /** @brief The ModelAction that this node represents */
81         const ModelAction *action;
82
83         /** @brief The edges leading out from this node */
84         std::vector<CycleNode *> edges;
85
86         /** Pointer to a RMW node that reads from this node, or NULL, if none
87          * exists */
88         CycleNode * hasRMW;
89 };
90
91 #endif