46b0d4ac4eb803df74d57e53148d0d463f343e26
[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  * @return false if the resolution results in a cycle; true otherwise
95  */
96 bool CycleGraph::resolvePromise(ModelAction *reader, ModelAction *writer,
97                 promise_list_t *mustResolve)
98 {
99         CycleNode *promise_node = readerToPromiseNode.get(reader);
100         CycleNode *w_node = actionToNode.get(writer);
101         ASSERT(promise_node);
102
103         if (w_node)
104                 return mergeNodes(w_node, promise_node, mustResolve);
105         /* No existing write-node; just convert the promise-node */
106         promise_node->resolvePromise(writer);
107         readerToPromiseNode.put(reader, NULL); /* erase promise_node */
108         putNode(writer, promise_node);
109         return true;
110 }
111
112 /**
113  * @brief Merge two CycleNodes that represent the same write
114  *
115  * Note that this operation cannot be rolled back.
116  *
117  * @param w_node The write ModelAction node with which to merge
118  * @param p_node The Promise node to merge. Will be destroyed after this
119  * function.
120  * @param mustMerge Return (pass-by-reference) any additional Promises that
121  * must also be merged with w_node
122  *
123  * @return false if the merge results in a cycle; true otherwise
124  */
125 bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node,
126                 promise_list_t *mustMerge)
127 {
128         ASSERT(!w_node->is_promise());
129         ASSERT(p_node->is_promise());
130         const Promise *promise = p_node->getPromise();
131         if (!promise->is_compatible(w_node->getAction())) {
132                 hasCycles = true;
133                 return false;
134         }
135
136         /* Transfer back edges to w_node */
137         while (p_node->getNumBackEdges() > 0) {
138                 CycleNode *back = p_node->removeBackEdge();
139                 if (back != w_node) {
140                         if (back->is_promise()) {
141                                 if (checkReachable(w_node, back)) {
142                                         /* Edge would create cycle; merge instead */
143                                         mustMerge->push_back(back->getPromise());
144                                         if (!mergeNodes(w_node, back, mustMerge))
145                                                 return false;
146                                 } else
147                                         back->addEdge(w_node);
148                         } else
149                                 addNodeEdge(back, w_node);
150                 }
151         }
152
153         /* Transfer forward edges to w_node */
154         while (p_node->getNumEdges() > 0) {
155                 CycleNode *forward = p_node->removeEdge();
156                 if (forward != w_node) {
157                         if (forward->is_promise()) {
158                                 if (checkReachable(forward, w_node)) {
159                                         mustMerge->push_back(forward->getPromise());
160                                         if (!mergeNodes(w_node, forward, mustMerge))
161                                                 return false;
162                                 } else
163                                         w_node->addEdge(forward);
164                         } else
165                                 addNodeEdge(w_node, forward);
166                 }
167         }
168
169         /* erase p_node */
170         readerToPromiseNode.put(promise->get_action(), NULL);
171         delete p_node;
172
173         return !hasCycles;
174 }
175
176 /**
177  * Adds an edge between two CycleNodes.
178  * @param fromnode The edge comes from this CycleNode
179  * @param tonode The edge points to this CycleNode
180  */
181 void CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
182 {
183         if (!hasCycles)
184                 hasCycles = checkReachable(tonode, fromnode);
185
186         if (fromnode->addEdge(tonode))
187                 rollbackvector.push_back(fromnode);
188
189         /*
190          * If the fromnode has a rmwnode that is not the tonode, we should add
191          * an edge between its rmwnode and the tonode
192          */
193         CycleNode *rmwnode = fromnode->getRMW();
194         if (rmwnode && rmwnode != tonode) {
195                 if (!hasCycles)
196                         hasCycles = checkReachable(tonode, rmwnode);
197
198                 if (rmwnode->addEdge(tonode))
199                         rollbackvector.push_back(rmwnode);
200         }
201 }
202
203 /**
204  * @brief Add an edge between a write and the RMW which reads from it
205  *
206  * Handles special case of a RMW action, where the ModelAction rmw reads from
207  * the ModelAction from. The key differences are:
208  * (1) no write can occur in between the rmw and the from action.
209  * (2) Only one RMW action can read from a given write.
210  *
211  * @param from The edge comes from this ModelAction
212  * @param rmw The edge points to this ModelAction; this action must read from
213  * ModelAction from
214  */
215 void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
216 {
217         ASSERT(from);
218         ASSERT(rmw);
219
220         CycleNode *fromnode = getNode(from);
221         CycleNode *rmwnode = getNode(rmw);
222
223         /* Two RMW actions cannot read from the same write. */
224         if (fromnode->setRMW(rmwnode))
225                 hasCycles = true;
226         else
227                 rmwrollbackvector.push_back(fromnode);
228
229         /* Transfer all outgoing edges from the from node to the rmw node */
230         /* This process should not add a cycle because either:
231          * (1) The rmw should not have any incoming edges yet if it is the
232          * new node or
233          * (2) the fromnode is the new node and therefore it should not
234          * have any outgoing edges.
235          */
236         for (unsigned int i = 0; i < fromnode->getNumEdges(); i++) {
237                 CycleNode *tonode = fromnode->getEdge(i);
238                 if (tonode != rmwnode) {
239                         if (rmwnode->addEdge(tonode))
240                                 rollbackvector.push_back(rmwnode);
241                 }
242         }
243
244         addNodeEdge(fromnode, rmwnode);
245 }
246
247 #if SUPPORT_MOD_ORDER_DUMP
248 void CycleGraph::dumpNodes(FILE *file) const
249 {
250         for (unsigned int i = 0; i < nodeList.size(); i++) {
251                 CycleNode *cn = nodeList[i];
252                 const ModelAction *action = cn->getAction();
253                 fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
254                 if (cn->getRMW() != NULL) {
255                         fprintf(file, "N%u -> N%u[style=dotted];\n", action->get_seq_number(), cn->getRMW()->getAction()->get_seq_number());
256                 }
257                 for (unsigned int j = 0; j < cn->getNumEdges(); j++) {
258                         CycleNode *dst = cn->getEdge(j);
259                         const ModelAction *dstaction = dst->getAction();
260                         fprintf(file, "N%u -> N%u;\n", action->get_seq_number(), dstaction->get_seq_number());
261                 }
262         }
263 }
264
265 void CycleGraph::dumpGraphToFile(const char *filename) const
266 {
267         char buffer[200];
268         sprintf(buffer, "%s.dot", filename);
269         FILE *file = fopen(buffer, "w");
270         fprintf(file, "digraph %s {\n", filename);
271         dumpNodes(file);
272         fprintf(file, "}\n");
273         fclose(file);
274 }
275 #endif
276
277 /**
278  * Checks whether one ModelAction can reach another.
279  * @param from The ModelAction from which to begin exploration
280  * @param to The ModelAction to reach
281  * @return True, @a from can reach @a to; otherwise, false
282  */
283 bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) const
284 {
285         CycleNode *fromnode = actionToNode.get(from);
286         CycleNode *tonode = actionToNode.get(to);
287
288         if (!fromnode || !tonode)
289                 return false;
290
291         return checkReachable(fromnode, tonode);
292 }
293
294 /**
295  * Checks whether one CycleNode can reach another.
296  * @param from The CycleNode from which to begin exploration
297  * @param to The CycleNode to reach
298  * @return True, @a from can reach @a to; otherwise, false
299  */
300 bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) const
301 {
302         std::vector< const CycleNode *, ModelAlloc<const CycleNode *> > queue;
303         discovered->reset();
304
305         queue.push_back(from);
306         discovered->put(from, from);
307         while (!queue.empty()) {
308                 const CycleNode *node = queue.back();
309                 queue.pop_back();
310                 if (node == to)
311                         return true;
312
313                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
314                         CycleNode *next = node->getEdge(i);
315                         if (!discovered->contains(next)) {
316                                 discovered->put(next, next);
317                                 queue.push_back(next);
318                         }
319                 }
320         }
321         return false;
322 }
323
324 bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
325 {
326         std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
327         discovered->reset();
328         CycleNode *from = actionToNode.get(fromact);
329
330         queue.push_back(from);
331         discovered->put(from, from);
332         while (!queue.empty()) {
333                 CycleNode *node = queue.back();
334                 queue.pop_back();
335
336                 if (promise->eliminate_thread(node->getAction()->get_tid())) {
337                         return true;
338                 }
339
340                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
341                         CycleNode *next = node->getEdge(i);
342                         if (!discovered->contains(next)) {
343                                 discovered->put(next, next);
344                                 queue.push_back(next);
345                         }
346                 }
347         }
348         return false;
349 }
350
351 void CycleGraph::startChanges()
352 {
353         ASSERT(rollbackvector.empty());
354         ASSERT(rmwrollbackvector.empty());
355         ASSERT(oldCycles == hasCycles);
356 }
357
358 /** Commit changes to the cyclegraph. */
359 void CycleGraph::commitChanges()
360 {
361         rollbackvector.clear();
362         rmwrollbackvector.clear();
363         oldCycles = hasCycles;
364 }
365
366 /** Rollback changes to the previous commit. */
367 void CycleGraph::rollbackChanges()
368 {
369         for (unsigned int i = 0; i < rollbackvector.size(); i++)
370                 rollbackvector[i]->popEdge();
371
372         for (unsigned int i = 0; i < rmwrollbackvector.size(); i++)
373                 rmwrollbackvector[i]->clearRMW();
374
375         hasCycles = oldCycles;
376         rollbackvector.clear();
377         rmwrollbackvector.clear();
378 }
379
380 /** @returns whether a CycleGraph contains cycles. */
381 bool CycleGraph::checkForCycles() const
382 {
383         return hasCycles;
384 }
385
386 /**
387  * @brief Constructor for a CycleNode
388  * @param act The ModelAction for this node
389  */
390 CycleNode::CycleNode(const ModelAction *act) :
391         action(act),
392         promise(NULL),
393         hasRMW(NULL)
394 {
395 }
396
397 /**
398  * @brief Constructor for a Promise CycleNode
399  * @param promise The Promise which was generated
400  */
401 CycleNode::CycleNode(const Promise *promise) :
402         action(NULL),
403         promise(promise),
404         hasRMW(NULL)
405 {
406 }
407
408 /**
409  * @param i The index of the edge to return
410  * @returns The a CycleNode edge indexed by i
411  */
412 CycleNode * CycleNode::getEdge(unsigned int i) const
413 {
414         return edges[i];
415 }
416
417 /** @returns The number of edges leaving this CycleNode */
418 unsigned int CycleNode::getNumEdges() const
419 {
420         return edges.size();
421 }
422
423 CycleNode * CycleNode::getBackEdge(unsigned int i) const
424 {
425         return back_edges[i];
426 }
427
428 unsigned int CycleNode::getNumBackEdges() const
429 {
430         return back_edges.size();
431 }
432
433 /**
434  * @brief Remove an element from a vector
435  * @param v The vector
436  * @param n The element to remove
437  * @return True if the element was found; false otherwise
438  */
439 template <typename T>
440 static bool vector_remove_node(std::vector<T, SnapshotAlloc<T> >& v, const T n)
441 {
442         for (unsigned int i = 0; i < v.size(); i++) {
443                 if (v[i] == n) {
444                         v.erase(v.begin() + i);
445                         return true;
446                 }
447         }
448         return false;
449 }
450
451 /**
452  * @brief Remove a (forward) edge from this CycleNode
453  * @return The CycleNode which was popped, if one exists; otherwise NULL
454  */
455 CycleNode * CycleNode::removeEdge()
456 {
457         if (edges.empty())
458                 return NULL;
459
460         CycleNode *ret = edges.back();
461         edges.pop_back();
462         vector_remove_node(ret->back_edges, this);
463         return ret;
464 }
465
466 /**
467  * @brief Remove a (back) edge from this CycleNode
468  * @return The CycleNode which was popped, if one exists; otherwise NULL
469  */
470 CycleNode * CycleNode::removeBackEdge()
471 {
472         if (back_edges.empty())
473                 return NULL;
474
475         CycleNode *ret = back_edges.back();
476         back_edges.pop_back();
477         vector_remove_node(ret->edges, this);
478         return ret;
479 }
480
481 /**
482  * Adds an edge from this CycleNode to another CycleNode.
483  * @param node The node to which we add a directed edge
484  * @return True if this edge is a new edge; false otherwise
485  */
486 bool CycleNode::addEdge(CycleNode *node)
487 {
488         for (unsigned int i = 0; i < edges.size(); i++)
489                 if (edges[i] == node)
490                         return false;
491         edges.push_back(node);
492         node->back_edges.push_back(this);
493         return true;
494 }
495
496 /** @returns the RMW CycleNode that reads from the current CycleNode */
497 CycleNode * CycleNode::getRMW() const
498 {
499         return hasRMW;
500 }
501
502 /**
503  * Set a RMW action node that reads from the current CycleNode.
504  * @param node The RMW that reads from the current node
505  * @return True, if this node already was read by another RMW; false otherwise
506  * @see CycleGraph::addRMWEdge
507  */
508 bool CycleNode::setRMW(CycleNode *node)
509 {
510         if (hasRMW != NULL)
511                 return true;
512         hasRMW = node;
513         return false;
514 }
515
516 /**
517  * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be
518  * used when there's no existing ModelAction CycleNode for this write.
519  *
520  * @param writer The ModelAction which wrote the future value represented by
521  * this CycleNode
522  */
523 void CycleNode::resolvePromise(const ModelAction *writer)
524 {
525         ASSERT(is_promise());
526         ASSERT(promise->is_compatible(writer));
527         action = writer;
528         promise = NULL;
529         ASSERT(!is_promise());
530 }