bugfix: straighten out STL vector allocation (snapshotted vs. persistent)
[model-checker.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
12 #include "mymemory.h"
13
14 class CycleNode;
15 class ModelAction;
16
17 /** @brief A graph of Model Actions for tracking cycles. */
18 class CycleGraph {
19  public:
20         CycleGraph();
21         ~CycleGraph();
22         void addEdge(const ModelAction *from, const ModelAction *to);
23         bool checkForCycles();
24         bool checkForRMWViolation();
25         void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
26
27         bool checkReachable(const ModelAction *from, const ModelAction *to);
28         void startChanges();
29         void commitChanges();
30         void rollbackChanges();
31
32         SNAPSHOTALLOC
33  private:
34         CycleNode * getNode(const ModelAction *);
35
36         /** @brief A table for mapping ModelActions to CycleNodes */
37         HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
38
39         bool checkReachable(CycleNode *from, CycleNode *to);
40
41         /** @brief A flag: true if this graph contains cycles */
42         bool hasCycles;
43         bool oldCycles;
44
45         bool hasRMWViolation;
46         bool oldRMWViolation;
47
48         std::vector<CycleNode *> rollbackvector;
49         std::vector<CycleNode *> rmwrollbackvector;
50 };
51
52 /** @brief A node within a CycleGraph; corresponds to one ModelAction */
53 class CycleNode {
54  public:
55         CycleNode(const ModelAction *action);
56         void addEdge(CycleNode * node);
57         std::vector<CycleNode *> * getEdges();
58         bool setRMW(CycleNode *);
59         CycleNode* getRMW();
60         void popEdge() {
61                 edges.pop_back();
62         };
63         void clearRMW() {
64                 hasRMW=NULL;
65         }
66
67         SNAPSHOTALLOC
68  private:
69         /** @brief The ModelAction that this node represents */
70         const ModelAction *action;
71
72         /** @brief The edges leading out from this node */
73         std::vector<CycleNode *> edges;
74
75         /** Pointer to a RMW node that reads from this node, or NULL, if none
76          * exists */
77         CycleNode * hasRMW;
78 };
79
80 #endif