main: wrap help message
[model-checker.git] / cyclegraph.cc
1 #include "cyclegraph.h"
2 #include "action.h"
3 #include "common.h"
4
5 /** Initializes a CycleGraph object. */
6 CycleGraph::CycleGraph() :
7         hasCycles(false),
8         oldCycles(false),
9         hasRMWViolation(false),
10         oldRMWViolation(false)
11 {
12 }
13
14 /** CycleGraph destructor */
15 CycleGraph::~CycleGraph() {
16 }
17
18 /**
19  * @brief Returns the CycleNode corresponding to a given ModelAction
20  * @param action The ModelAction to find a node for
21  * @return The CycleNode paired with this action
22  */
23 CycleNode * CycleGraph::getNode(const ModelAction *action) {
24         CycleNode *node=actionToNode.get(action);
25         if (node==NULL) {
26                 node=new CycleNode(action);
27                 actionToNode.put(action, node);
28         }
29         return node;
30 }
31
32 /**
33  * Adds an edge between two ModelActions. The ModelAction @a to is ordered
34  * after the ModelAction @a from.
35  * @param to The edge points to this ModelAction
36  * @param from The edge comes from this ModelAction
37  */
38 void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
39         ASSERT(from);
40         ASSERT(to);
41
42         CycleNode *fromnode=getNode(from);
43         CycleNode *tonode=getNode(to);
44
45         if (!hasCycles) {
46                 // Check for Cycles
47                 hasCycles=checkReachable(tonode, fromnode);
48         }
49
50         rollbackvector.push_back(fromnode);
51         fromnode->addEdge(tonode);
52
53         CycleNode * rmwnode=fromnode->getRMW();
54
55         //If the fromnode has a rmwnode that is not the tonode, we
56         //should add an edge between its rmwnode and the tonode
57
58         //If tonode is also a rmw, don't do this check as the execution is
59         //doomed and we'll catch the problem elsewhere, but we want to allow
60         //for the possibility of sending to's write value to rmwnode
61
62         if (rmwnode!=NULL&&!to->is_rmw()) {
63                 if (!hasCycles) {
64                         // Check for Cycles
65                         hasCycles=checkReachable(tonode, rmwnode);
66                 }
67                 rollbackvector.push_back(rmwnode);
68                 rmwnode->addEdge(tonode);
69         }
70 }
71
72 /** Handles special case of a RMW action.  The ModelAction rmw reads
73  *  from the ModelAction from.  The key differences are: (1) no write
74  *  can occur in between the rmw and the from action.  Only one RMW
75  *  action can read from a given write.
76  */
77 void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
78         ASSERT(from);
79         ASSERT(rmw);
80
81         CycleNode *fromnode=getNode(from);
82         CycleNode *rmwnode=getNode(rmw);
83
84         /* Two RMW actions cannot read from the same write. */
85         if (fromnode->setRMW(rmwnode)) {
86                 hasRMWViolation=true;
87         } else {
88                 rmwrollbackvector.push_back(fromnode);
89         }
90
91         /* Transfer all outgoing edges from the from node to the rmw node */
92         /* This process should not add a cycle because either:
93          * (1) The rmw should not have any incoming edges yet if it is the
94          * new node or
95          * (2) the fromnode is the new node and therefore it should not
96          * have any outgoing edges.
97          */
98         std::vector<CycleNode *> * edges=fromnode->getEdges();
99         for(unsigned int i=0;i<edges->size();i++) {
100                 CycleNode * tonode=(*edges)[i];
101                 if (tonode!=rmwnode) {
102                         rollbackvector.push_back(rmwnode);
103                         rmwnode->addEdge(tonode);
104                 }
105         }
106         rollbackvector.push_back(fromnode);
107
108         if (!hasCycles) {
109                 // With promises we could be setting up a cycle here if we aren't
110                 // careful...avoid it..
111                 hasCycles=checkReachable(rmwnode, fromnode);
112         }
113         fromnode->addEdge(rmwnode);
114 }
115
116 /**
117  * Checks whether one ModelAction can reach another.
118  * @param from The ModelAction from which to begin exploration
119  * @param to The ModelAction to reach
120  * @return True, @a from can reach @a to; otherwise, false
121  */
122 bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) {
123         CycleNode *fromnode = actionToNode.get(from);
124         CycleNode *tonode = actionToNode.get(to);
125
126         if (!fromnode || !tonode)
127                 return false;
128
129         return checkReachable(fromnode, tonode);
130 }
131
132 /**
133  * Checks whether one CycleNode can reach another.
134  * @param from The CycleNode from which to begin exploration
135  * @param to The CycleNode to reach
136  * @return True, @a from can reach @a to; otherwise, false
137  */
138 bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
139         std::vector<CycleNode *> queue;
140         HashTable<CycleNode *, CycleNode *, uintptr_t, 4> discovered;
141
142         queue.push_back(from);
143         discovered.put(from, from);
144         while(!queue.empty()) {
145                 CycleNode * node=queue.back();
146                 queue.pop_back();
147                 if (node==to)
148                         return true;
149
150                 for(unsigned int i=0;i<node->getEdges()->size();i++) {
151                         CycleNode *next=(*node->getEdges())[i];
152                         if (!discovered.contains(next)) {
153                                 discovered.put(next,next);
154                                 queue.push_back(next);
155                         }
156                 }
157         }
158         return false;
159 }
160
161 void CycleGraph::startChanges() {
162         ASSERT(rollbackvector.size()==0);
163         ASSERT(rmwrollbackvector.size()==0);
164         ASSERT(oldCycles==hasCycles);
165         ASSERT(oldRMWViolation==hasRMWViolation);
166 }
167
168 /** Commit changes to the cyclegraph. */
169 void CycleGraph::commitChanges() {
170         rollbackvector.resize(0);
171         rmwrollbackvector.resize(0);
172         oldCycles=hasCycles;
173         oldRMWViolation=hasRMWViolation;
174 }
175
176 /** Rollback changes to the previous commit. */
177 void CycleGraph::rollbackChanges() {
178         for (unsigned int i = 0; i < rollbackvector.size(); i++) {
179                 rollbackvector[i]->popEdge();
180         }
181
182         for (unsigned int i = 0; i < rmwrollbackvector.size(); i++) {
183                 rmwrollbackvector[i]->clearRMW();
184         }
185
186         hasCycles = oldCycles;
187         hasRMWViolation = oldRMWViolation;
188         rollbackvector.resize(0);
189         rmwrollbackvector.resize(0);
190 }
191
192 /** @returns whether a CycleGraph contains cycles. */
193 bool CycleGraph::checkForCycles() {
194         return hasCycles;
195 }
196
197 bool CycleGraph::checkForRMWViolation() {
198         return hasRMWViolation;
199 }
200
201 /**
202  * Constructor for a CycleNode.
203  * @param modelaction The ModelAction for this node
204  */
205 CycleNode::CycleNode(const ModelAction *modelaction) :
206         action(modelaction),
207         hasRMW(NULL)
208 {
209 }
210
211 /** @returns a vector of the edges from a CycleNode. */
212 std::vector<CycleNode *> * CycleNode::getEdges() {
213         return &edges;
214 }
215
216 /**
217  * Adds an edge from this CycleNode to another CycleNode.
218  * @param node The node to which we add a directed edge
219  */
220 void CycleNode::addEdge(CycleNode *node) {
221         edges.push_back(node);
222 }
223
224 /** @returns the RMW CycleNode that reads from the current CycleNode */
225 CycleNode * CycleNode::getRMW() {
226         return hasRMW;
227 }
228
229 /**
230  * Set a RMW action node that reads from the current CycleNode.
231  * @param node The RMW that reads from the current node
232  * @return True, if this node already was read by another RMW; false otherwise
233  * @see CycleGraph::addRMWEdge
234  */
235 bool CycleNode::setRMW(CycleNode *node) {
236         if (hasRMW!=NULL)
237                 return true;
238         hasRMW=node;
239         return false;
240 }