cyclegraph: map Promises to Promise nodes
[model-checker.git] / cyclegraph.cc
1 #include "cyclegraph.h"
2 #include "action.h"
3 #include "common.h"
4 #include "promise.h"
5 #include "model.h"
6
7 /** Initializes a CycleGraph object. */
8 CycleGraph::CycleGraph() :
9         discovered(new HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
10         hasCycles(false),
11         oldCycles(false)
12 {
13 }
14
15 /** CycleGraph destructor */
16 CycleGraph::~CycleGraph()
17 {
18         delete discovered;
19 }
20
21 /**
22  * Add a CycleNode to the graph, corresponding to a store ModelAction
23  * @param act The write action that should be added
24  * @param node The CycleNode that corresponds to the store
25  */
26 void CycleGraph::putNode(const ModelAction *act, CycleNode *node)
27 {
28         actionToNode.put(act, node);
29 #if SUPPORT_MOD_ORDER_DUMP
30         nodeList.push_back(node);
31 #endif
32 }
33
34 /**
35  * @brief Returns the CycleNode corresponding to a given ModelAction
36  * @param action The ModelAction to find a node for
37  * @return The CycleNode paired with this action
38  */
39 CycleNode * CycleGraph::getNode(const ModelAction *action)
40 {
41         CycleNode *node = actionToNode.get(action);
42         if (node == NULL) {
43                 node = new CycleNode(action);
44                 putNode(action, node);
45         }
46         return node;
47 }
48
49 /**
50  * @brief Returns a CycleNode corresponding to a promise
51  *
52  * Gets (or creates, if none exist) a CycleNode corresponding to a promised
53  * value.
54  *
55  * @param promise The Promise generated by a reader
56  * @return The CycleNode corresponding to the Promise
57  */
58 CycleNode * CycleGraph::getNode(const Promise *promise)
59 {
60         const ModelAction *reader = promise->get_action();
61         CycleNode *node = readerToPromiseNode.get(reader);
62         if (node == NULL) {
63                 node = new CycleNode(promise);
64                 readerToPromiseNode.put(reader, node);
65         }
66         return node;
67 }
68
69 /*
70  * @brief Adds an edge between objects
71  *
72  * This function will add an edge between any two objects which can be
73  * associated with a CycleNode. That is, if they have a CycleGraph::getNode
74  * implementation.
75  *
76  * The object to is ordered after the object from.
77  *
78  * @param to The edge points to this object, of type T
79  * @param from The edge comes from this object, of type U
80  */
81 template <typename T, typename U>
82 void CycleGraph::addEdge(const T from, const U to)
83 {
84         ASSERT(from);
85         ASSERT(to);
86
87         CycleNode *fromnode = getNode(from);
88         CycleNode *tonode = getNode(to);
89
90         addNodeEdge(fromnode, tonode);
91 }
92
93 /**
94  * Adds an edge between two CycleNodes.
95  * @param fromnode The edge comes from this CycleNode
96  * @param tonode The edge points to this CycleNode
97  */
98 void CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
99 {
100         if (!hasCycles)
101                 hasCycles = checkReachable(tonode, fromnode);
102
103         if (fromnode->addEdge(tonode))
104                 rollbackvector.push_back(fromnode);
105
106         /*
107          * If the fromnode has a rmwnode that is not the tonode, we should add
108          * an edge between its rmwnode and the tonode
109          */
110         CycleNode *rmwnode = fromnode->getRMW();
111         if (rmwnode && rmwnode != tonode) {
112                 if (!hasCycles)
113                         hasCycles = checkReachable(tonode, rmwnode);
114
115                 if (rmwnode->addEdge(tonode))
116                         rollbackvector.push_back(rmwnode);
117         }
118 }
119
120 /**
121  * @brief Add an edge between a write and the RMW which reads from it
122  *
123  * Handles special case of a RMW action, where the ModelAction rmw reads from
124  * the ModelAction from. The key differences are:
125  * (1) no write can occur in between the rmw and the from action.
126  * (2) Only one RMW action can read from a given write.
127  *
128  * @param from The edge comes from this ModelAction
129  * @param rmw The edge points to this ModelAction; this action must read from
130  * ModelAction from
131  */
132 void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
133 {
134         ASSERT(from);
135         ASSERT(rmw);
136
137         CycleNode *fromnode = getNode(from);
138         CycleNode *rmwnode = getNode(rmw);
139
140         /* Two RMW actions cannot read from the same write. */
141         if (fromnode->setRMW(rmwnode))
142                 hasCycles = true;
143         else
144                 rmwrollbackvector.push_back(fromnode);
145
146         /* Transfer all outgoing edges from the from node to the rmw node */
147         /* This process should not add a cycle because either:
148          * (1) The rmw should not have any incoming edges yet if it is the
149          * new node or
150          * (2) the fromnode is the new node and therefore it should not
151          * have any outgoing edges.
152          */
153         for (unsigned int i = 0; i < fromnode->getNumEdges(); i++) {
154                 CycleNode *tonode = fromnode->getEdge(i);
155                 if (tonode != rmwnode) {
156                         if (rmwnode->addEdge(tonode))
157                                 rollbackvector.push_back(rmwnode);
158                 }
159         }
160
161         addNodeEdge(fromnode, rmwnode);
162 }
163
164 #if SUPPORT_MOD_ORDER_DUMP
165 void CycleGraph::dumpNodes(FILE *file) const
166 {
167         for (unsigned int i = 0; i < nodeList.size(); i++) {
168                 CycleNode *cn = nodeList[i];
169                 const ModelAction *action = cn->getAction();
170                 fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
171                 if (cn->getRMW() != NULL) {
172                         fprintf(file, "N%u -> N%u[style=dotted];\n", action->get_seq_number(), cn->getRMW()->getAction()->get_seq_number());
173                 }
174                 for (unsigned int j = 0; j < cn->getNumEdges(); j++) {
175                         CycleNode *dst = cn->getEdge(j);
176                         const ModelAction *dstaction = dst->getAction();
177                         fprintf(file, "N%u -> N%u;\n", action->get_seq_number(), dstaction->get_seq_number());
178                 }
179         }
180 }
181
182 void CycleGraph::dumpGraphToFile(const char *filename) const
183 {
184         char buffer[200];
185         sprintf(buffer, "%s.dot", filename);
186         FILE *file = fopen(buffer, "w");
187         fprintf(file, "digraph %s {\n", filename);
188         dumpNodes(file);
189         fprintf(file, "}\n");
190         fclose(file);
191 }
192 #endif
193
194 /**
195  * Checks whether one ModelAction can reach another.
196  * @param from The ModelAction from which to begin exploration
197  * @param to The ModelAction to reach
198  * @return True, @a from can reach @a to; otherwise, false
199  */
200 bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) const
201 {
202         CycleNode *fromnode = actionToNode.get(from);
203         CycleNode *tonode = actionToNode.get(to);
204
205         if (!fromnode || !tonode)
206                 return false;
207
208         return checkReachable(fromnode, tonode);
209 }
210
211 /**
212  * Checks whether one CycleNode can reach another.
213  * @param from The CycleNode from which to begin exploration
214  * @param to The CycleNode to reach
215  * @return True, @a from can reach @a to; otherwise, false
216  */
217 bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) const
218 {
219         std::vector< const CycleNode *, ModelAlloc<const CycleNode *> > queue;
220         discovered->reset();
221
222         queue.push_back(from);
223         discovered->put(from, from);
224         while (!queue.empty()) {
225                 const CycleNode *node = queue.back();
226                 queue.pop_back();
227                 if (node == to)
228                         return true;
229
230                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
231                         CycleNode *next = node->getEdge(i);
232                         if (!discovered->contains(next)) {
233                                 discovered->put(next, next);
234                                 queue.push_back(next);
235                         }
236                 }
237         }
238         return false;
239 }
240
241 bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
242 {
243         std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
244         discovered->reset();
245         CycleNode *from = actionToNode.get(fromact);
246
247         queue.push_back(from);
248         discovered->put(from, from);
249         while (!queue.empty()) {
250                 CycleNode *node = queue.back();
251                 queue.pop_back();
252
253                 if (promise->eliminate_thread(node->getAction()->get_tid())) {
254                         return true;
255                 }
256
257                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
258                         CycleNode *next = node->getEdge(i);
259                         if (!discovered->contains(next)) {
260                                 discovered->put(next, next);
261                                 queue.push_back(next);
262                         }
263                 }
264         }
265         return false;
266 }
267
268 void CycleGraph::startChanges()
269 {
270         ASSERT(rollbackvector.empty());
271         ASSERT(rmwrollbackvector.empty());
272         ASSERT(oldCycles == hasCycles);
273 }
274
275 /** Commit changes to the cyclegraph. */
276 void CycleGraph::commitChanges()
277 {
278         rollbackvector.clear();
279         rmwrollbackvector.clear();
280         oldCycles = hasCycles;
281 }
282
283 /** Rollback changes to the previous commit. */
284 void CycleGraph::rollbackChanges()
285 {
286         for (unsigned int i = 0; i < rollbackvector.size(); i++)
287                 rollbackvector[i]->popEdge();
288
289         for (unsigned int i = 0; i < rmwrollbackvector.size(); i++)
290                 rmwrollbackvector[i]->clearRMW();
291
292         hasCycles = oldCycles;
293         rollbackvector.clear();
294         rmwrollbackvector.clear();
295 }
296
297 /** @returns whether a CycleGraph contains cycles. */
298 bool CycleGraph::checkForCycles() const
299 {
300         return hasCycles;
301 }
302
303 /**
304  * @brief Constructor for a CycleNode
305  * @param act The ModelAction for this node
306  */
307 CycleNode::CycleNode(const ModelAction *act) :
308         action(act),
309         promise(NULL),
310         hasRMW(NULL)
311 {
312 }
313
314 /**
315  * @brief Constructor for a Promise CycleNode
316  * @param promise The Promise which was generated
317  */
318 CycleNode::CycleNode(const Promise *promise) :
319         action(NULL),
320         promise(promise),
321         hasRMW(NULL)
322 {
323 }
324
325 /**
326  * @param i The index of the edge to return
327  * @returns The a CycleNode edge indexed by i
328  */
329 CycleNode * CycleNode::getEdge(unsigned int i) const
330 {
331         return edges[i];
332 }
333
334 /** @returns The number of edges leaving this CycleNode */
335 unsigned int CycleNode::getNumEdges() const
336 {
337         return edges.size();
338 }
339
340 CycleNode * CycleNode::getBackEdge(unsigned int i) const
341 {
342         return back_edges[i];
343 }
344
345 unsigned int CycleNode::getNumBackEdges() const
346 {
347         return back_edges.size();
348 }
349
350 /**
351  * @brief Remove an element from a vector
352  * @param v The vector
353  * @param n The element to remove
354  * @return True if the element was found; false otherwise
355  */
356 template <typename T>
357 static bool vector_remove_node(std::vector<T, SnapshotAlloc<T> >& v, const T n)
358 {
359         for (unsigned int i = 0; i < v.size(); i++) {
360                 if (v[i] == n) {
361                         v.erase(v.begin() + i);
362                         return true;
363                 }
364         }
365         return false;
366 }
367
368 /**
369  * @brief Remove a (forward) edge from this CycleNode
370  * @return The CycleNode which was popped, if one exists; otherwise NULL
371  */
372 CycleNode * CycleNode::removeEdge()
373 {
374         if (edges.empty())
375                 return NULL;
376
377         CycleNode *ret = edges.back();
378         edges.pop_back();
379         vector_remove_node(ret->back_edges, this);
380         return ret;
381 }
382
383 /**
384  * @brief Remove a (back) edge from this CycleNode
385  * @return The CycleNode which was popped, if one exists; otherwise NULL
386  */
387 CycleNode * CycleNode::removeBackEdge()
388 {
389         if (back_edges.empty())
390                 return NULL;
391
392         CycleNode *ret = back_edges.back();
393         back_edges.pop_back();
394         vector_remove_node(ret->edges, this);
395         return ret;
396 }
397
398 /**
399  * Adds an edge from this CycleNode to another CycleNode.
400  * @param node The node to which we add a directed edge
401  * @return True if this edge is a new edge; false otherwise
402  */
403 bool CycleNode::addEdge(CycleNode *node)
404 {
405         for (unsigned int i = 0; i < edges.size(); i++)
406                 if (edges[i] == node)
407                         return false;
408         edges.push_back(node);
409         node->back_edges.push_back(this);
410         return true;
411 }
412
413 /** @returns the RMW CycleNode that reads from the current CycleNode */
414 CycleNode * CycleNode::getRMW() const
415 {
416         return hasRMW;
417 }
418
419 /**
420  * Set a RMW action node that reads from the current CycleNode.
421  * @param node The RMW that reads from the current node
422  * @return True, if this node already was read by another RMW; false otherwise
423  * @see CycleGraph::addRMWEdge
424  */
425 bool CycleNode::setRMW(CycleNode *node)
426 {
427         if (hasRMW != NULL)
428                 return true;
429         hasRMW = node;
430         return false;
431 }