model: pass current action as function argument
[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 #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