action: add <stdlib>
[model-checker.git] / cyclegraph.h
1 /**
2  * @file cyclegraph.h
3  * @brief Data structure to track ordering constraints on modification order
4  *
5  * Used to determine whether a total order exists that satisfies the ordering
6  * constraints.
7  */
8
9 #ifndef __CYCLEGRAPH_H__
10 #define __CYCLEGRAPH_H__
11
12 #include <inttypes.h>
13 #include <stdio.h>
14
15 #include "hashtable.h"
16 #include "config.h"
17 #include "mymemory.h"
18 #include "stl-model.h"
19
20 class Promise;
21 class CycleNode;
22 class ModelAction;
23
24 /** @brief A graph of Model Actions for tracking cycles. */
25 class CycleGraph {
26  public:
27         CycleGraph();
28         ~CycleGraph();
29
30         template <typename T, typename U>
31         bool addEdge(const T *from, const U *to);
32
33         template <typename T>
34         void addRMWEdge(const T *from, const ModelAction *rmw);
35
36         bool checkForCycles() const;
37         bool checkPromise(const ModelAction *from, Promise *p) const;
38
39         template <typename T, typename U>
40         bool checkReachable(const T *from, const U *to) const;
41
42         void startChanges();
43         void commitChanges();
44         void rollbackChanges();
45 #if SUPPORT_MOD_ORDER_DUMP
46         void dumpNodes(FILE *file) const;
47         void dumpGraphToFile(const char *filename) const;
48
49         void dot_print_node(FILE *file, const ModelAction *act);
50         template <typename T, typename U>
51         void dot_print_edge(FILE *file, const T *from, const U *to, const char *prop);
52 #endif
53
54         bool resolvePromise(const Promise *promise, ModelAction *writer);
55
56         SNAPSHOTALLOC
57  private:
58         bool addNodeEdge(CycleNode *fromnode, CycleNode *tonode);
59         void putNode(const ModelAction *act, CycleNode *node);
60         void putNode(const Promise *promise, CycleNode *node);
61         void erasePromiseNode(const Promise *promise);
62         CycleNode * getNode(const ModelAction *act);
63         CycleNode * getNode(const Promise *promise);
64         CycleNode * getNode_noCreate(const ModelAction *act) const;
65         CycleNode * getNode_noCreate(const Promise *promise) const;
66         bool mergeNodes(CycleNode *node1, CycleNode *node2);
67
68         HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> *discovered;
69         ModelVector<const CycleNode *> * queue;
70
71
72         /** @brief A table for mapping ModelActions to CycleNodes */
73         HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
74         /** @brief A table for mapping Promises to CycleNodes */
75         HashTable<const Promise *, CycleNode *, uintptr_t, 4> promiseToNode;
76
77 #if SUPPORT_MOD_ORDER_DUMP
78         SnapVector<CycleNode *> nodeList;
79 #endif
80
81         bool checkReachable(const CycleNode *from, const CycleNode *to) const;
82
83         /** @brief A flag: true if this graph contains cycles */
84         bool hasCycles;
85         /** @brief The previous value of CycleGraph::hasCycles, for rollback */
86         bool oldCycles;
87
88         SnapVector<CycleNode *> rollbackvector;
89         SnapVector<CycleNode *> rmwrollbackvector;
90 };
91
92 /**
93  * @brief A node within a CycleGraph; corresponds either to one ModelAction or
94  * to a promised future value
95  */
96 class CycleNode {
97  public:
98         CycleNode(const ModelAction *act);
99         CycleNode(const Promise *promise);
100         bool addEdge(CycleNode *node);
101         CycleNode * getEdge(unsigned int i) const;
102         unsigned int getNumEdges() const;
103         CycleNode * getBackEdge(unsigned int i) const;
104         unsigned int getNumBackEdges() const;
105         CycleNode * removeEdge();
106         CycleNode * removeBackEdge();
107
108         bool setRMW(CycleNode *);
109         CycleNode * getRMW() const;
110         void clearRMW() { hasRMW = NULL; }
111         const ModelAction * getAction() const { return action; }
112         const Promise * getPromise() const { return promise; }
113         bool is_promise() const { return !action; }
114         void resolvePromise(const ModelAction *writer);
115
116         SNAPSHOTALLOC
117  private:
118         /** @brief The ModelAction that this node represents */
119         const ModelAction *action;
120
121         /** @brief The promise represented by this node; only valid when action
122          * is NULL */
123         const Promise *promise;
124
125         /** @brief The edges leading out from this node */
126         SnapVector<CycleNode *> edges;
127
128         /** @brief The edges leading into this node */
129         SnapVector<CycleNode *> back_edges;
130
131         /** Pointer to a RMW node that reads from this node, or NULL, if none
132          * exists */
133         CycleNode *hasRMW;
134 };
135
136 #endif /* __CYCLEGRAPH_H__ */