model: remove todo
[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
41         /** @brief A table for mapping ModelActions to CycleNodes */
42         HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
43 #if SUPPORT_MOD_ORDER_DUMP
44         std::vector<CycleNode *> nodeList;
45 #endif
46
47         bool checkReachable(CycleNode *from, CycleNode *to);
48
49         /** @brief A flag: true if this graph contains cycles */
50         bool hasCycles;
51         bool oldCycles;
52
53         bool hasRMWViolation;
54         bool oldRMWViolation;
55
56         std::vector<CycleNode *> rollbackvector;
57         std::vector<CycleNode *> rmwrollbackvector;
58 };
59
60 /** @brief A node within a CycleGraph; corresponds to one ModelAction */
61 class CycleNode {
62  public:
63         CycleNode(const ModelAction *action);
64         bool addEdge(CycleNode * node);
65         std::vector<CycleNode *> * getEdges();
66         bool setRMW(CycleNode *);
67         CycleNode* getRMW();
68         const ModelAction * getAction() {return action;};
69
70         void popEdge() {
71                 edges.pop_back();
72         };
73         void clearRMW() {
74                 hasRMW=NULL;
75         }
76
77         SNAPSHOTALLOC
78  private:
79         /** @brief The ModelAction that this node represents */
80         const ModelAction *action;
81
82         /** @brief The edges leading out from this node */
83         std::vector<CycleNode *> edges;
84
85         /** Pointer to a RMW node that reads from this node, or NULL, if none
86          * exists */
87         CycleNode * hasRMW;
88 };
89
90 #endif