action: add <stdlib>
[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 #include "threads-model.h"
7
8 /** Initializes a CycleGraph object. */
9 CycleGraph::CycleGraph() :
10         discovered(new HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
11         queue(new ModelVector<const CycleNode *>()),
12         hasCycles(false),
13         oldCycles(false)
14 {
15 }
16
17 /** CycleGraph destructor */
18 CycleGraph::~CycleGraph()
19 {
20         delete queue;
21         delete discovered;
22 }
23
24 /**
25  * Add a CycleNode to the graph, corresponding to a store ModelAction
26  * @param act The write action that should be added
27  * @param node The CycleNode that corresponds to the store
28  */
29 void CycleGraph::putNode(const ModelAction *act, CycleNode *node)
30 {
31         actionToNode.put(act, node);
32 #if SUPPORT_MOD_ORDER_DUMP
33         nodeList.push_back(node);
34 #endif
35 }
36
37 /**
38  * Add a CycleNode to the graph, corresponding to a Promise
39  * @param promise The Promise that should be added
40  * @param node The CycleNode that corresponds to the Promise
41  */
42 void CycleGraph::putNode(const Promise *promise, CycleNode *node)
43 {
44         promiseToNode.put(promise, node);
45 #if SUPPORT_MOD_ORDER_DUMP
46         nodeList.push_back(node);
47 #endif
48 }
49
50 /**
51  * @brief Remove the Promise node from the graph
52  * @param promise The promise to remove from the graph
53  */
54 void CycleGraph::erasePromiseNode(const Promise *promise)
55 {
56         promiseToNode.put(promise, NULL);
57 #if SUPPORT_MOD_ORDER_DUMP
58         /* Remove the promise node from nodeList */
59         CycleNode *node = getNode_noCreate(promise);
60         for (unsigned int i = 0; i < nodeList.size(); )
61                 if (nodeList[i] == node)
62                         nodeList.erase(nodeList.begin() + i);
63                 else
64                         i++;
65 #endif
66 }
67
68 /** @return The corresponding CycleNode, if exists; otherwise NULL */
69 CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
70 {
71         return actionToNode.get(act);
72 }
73
74 /** @return The corresponding CycleNode, if exists; otherwise NULL */
75 CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const
76 {
77         return promiseToNode.get(promise);
78 }
79
80 /**
81  * @brief Returns the CycleNode corresponding to a given ModelAction
82  *
83  * Gets (or creates, if none exist) a CycleNode corresponding to a ModelAction
84  *
85  * @param action The ModelAction to find a node for
86  * @return The CycleNode paired with this action
87  */
88 CycleNode * CycleGraph::getNode(const ModelAction *action)
89 {
90         CycleNode *node = getNode_noCreate(action);
91         if (node == NULL) {
92                 node = new CycleNode(action);
93                 putNode(action, node);
94         }
95         return node;
96 }
97
98 /**
99  * @brief Returns a CycleNode corresponding to a promise
100  *
101  * Gets (or creates, if none exist) a CycleNode corresponding to a promised
102  * value.
103  *
104  * @param promise The Promise generated by a reader
105  * @return The CycleNode corresponding to the Promise
106  */
107 CycleNode * CycleGraph::getNode(const Promise *promise)
108 {
109         CycleNode *node = getNode_noCreate(promise);
110         if (node == NULL) {
111                 node = new CycleNode(promise);
112                 putNode(promise, node);
113         }
114         return node;
115 }
116
117 /**
118  * Resolve/satisfy a Promise with a particular store ModelAction, taking care
119  * of the CycleGraph cleanups, including merging any necessary CycleNodes.
120  *
121  * @param promise The Promise to resolve
122  * @param writer The store that will resolve this Promise
123  * @return false if the resolution results in a cycle (or fails in some other
124  * way); true otherwise
125  */
126 bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer)
127 {
128         CycleNode *promise_node = promiseToNode.get(promise);
129         CycleNode *w_node = actionToNode.get(writer);
130         ASSERT(promise_node);
131
132         if (w_node)
133                 return mergeNodes(w_node, promise_node);
134         /* No existing write-node; just convert the promise-node */
135         promise_node->resolvePromise(writer);
136         erasePromiseNode(promise_node->getPromise());
137         putNode(writer, promise_node);
138         return true;
139 }
140
141 /**
142  * @brief Merge two CycleNodes that represent the same write
143  *
144  * Note that this operation cannot be rolled back.
145  *
146  * @param w_node The write ModelAction node with which to merge
147  * @param p_node The Promise node to merge. Will be destroyed after this
148  * function.
149  *
150  * @return false if the merge cannot succeed; true otherwise
151  */
152 bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node)
153 {
154         ASSERT(!w_node->is_promise());
155         ASSERT(p_node->is_promise());
156
157         const Promise *promise = p_node->getPromise();
158         if (!promise->is_compatible(w_node->getAction()) ||
159                         !promise->same_value(w_node->getAction()))
160                 return false;
161
162         /* Transfer the RMW */
163         CycleNode *promise_rmw = p_node->getRMW();
164         if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw))
165                 return false;
166
167         /* Transfer back edges to w_node */
168         while (p_node->getNumBackEdges() > 0) {
169                 CycleNode *back = p_node->removeBackEdge();
170                 if (back == w_node)
171                         continue;
172                 addNodeEdge(back, w_node);
173                 if (hasCycles)
174                         return false;
175         }
176
177         /* Transfer forward edges to w_node */
178         while (p_node->getNumEdges() > 0) {
179                 CycleNode *forward = p_node->removeEdge();
180                 if (forward == w_node)
181                         continue;
182                 addNodeEdge(w_node, forward);
183                 if (hasCycles)
184                         return false;
185         }
186
187         erasePromiseNode(promise);
188         /* Not deleting p_node, to maintain consistency if mergeNodes() fails */
189
190         return !hasCycles;
191 }
192
193 /**
194  * Adds an edge between two CycleNodes.
195  * @param fromnode The edge comes from this CycleNode
196  * @param tonode The edge points to this CycleNode
197  * @return True, if new edge(s) are added; otherwise false
198  */
199 bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
200 {
201         if (fromnode->addEdge(tonode)) {
202                 rollbackvector.push_back(fromnode);
203                 if (!hasCycles)
204                         hasCycles = checkReachable(tonode, fromnode);
205         } else
206                 return false; /* No new edge */
207
208         /*
209          * If the fromnode has a rmwnode that is not the tonode, we should
210          * follow its RMW chain to add an edge at the end, unless we encounter
211          * tonode along the way
212          */
213         CycleNode *rmwnode = fromnode->getRMW();
214         if (rmwnode) {
215                 while (rmwnode != tonode && rmwnode->getRMW())
216                         rmwnode = rmwnode->getRMW();
217
218                 if (rmwnode != tonode) {
219                         if (rmwnode->addEdge(tonode)) {
220                                 if (!hasCycles)
221                                         hasCycles = checkReachable(tonode, rmwnode);
222
223                                 rollbackvector.push_back(rmwnode);
224                         }
225                 }
226         }
227         return true;
228 }
229
230 /**
231  * @brief Add an edge between a write and the RMW which reads from it
232  *
233  * Handles special case of a RMW action, where the ModelAction rmw reads from
234  * the ModelAction/Promise from. The key differences are:
235  *  -# No write can occur in between the @a rmw and @a from actions.
236  *  -# Only one RMW action can read from a given write.
237  *
238  * @param from The edge comes from this ModelAction/Promise
239  * @param rmw The edge points to this ModelAction; this action must read from
240  * the ModelAction/Promise from
241  */
242 template <typename T>
243 void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw)
244 {
245         ASSERT(from);
246         ASSERT(rmw);
247
248         CycleNode *fromnode = getNode(from);
249         CycleNode *rmwnode = getNode(rmw);
250
251         /* We assume that this RMW has no RMW reading from it yet */
252         ASSERT(!rmwnode->getRMW());
253
254         /* Two RMW actions cannot read from the same write. */
255         if (fromnode->setRMW(rmwnode))
256                 hasCycles = true;
257         else
258                 rmwrollbackvector.push_back(fromnode);
259
260         /* Transfer all outgoing edges from the from node to the rmw node */
261         /* This process should not add a cycle because either:
262          * (1) The rmw should not have any incoming edges yet if it is the
263          * new node or
264          * (2) the fromnode is the new node and therefore it should not
265          * have any outgoing edges.
266          */
267         for (unsigned int i = 0; i < fromnode->getNumEdges(); i++) {
268                 CycleNode *tonode = fromnode->getEdge(i);
269                 if (tonode != rmwnode) {
270                         if (rmwnode->addEdge(tonode))
271                                 rollbackvector.push_back(rmwnode);
272                 }
273         }
274
275         addNodeEdge(fromnode, rmwnode);
276 }
277 /* Instantiate two forms of CycleGraph::addRMWEdge */
278 template void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw);
279 template void CycleGraph::addRMWEdge(const Promise *from, const ModelAction *rmw);
280
281 /**
282  * @brief Adds an edge between objects
283  *
284  * This function will add an edge between any two objects which can be
285  * associated with a CycleNode. That is, if they have a CycleGraph::getNode
286  * implementation.
287  *
288  * The object to is ordered after the object from.
289  *
290  * @param to The edge points to this object, of type T
291  * @param from The edge comes from this object, of type U
292  * @return True, if new edge(s) are added; otherwise false
293  */
294 template <typename T, typename U>
295 bool CycleGraph::addEdge(const T *from, const U *to)
296 {
297         ASSERT(from);
298         ASSERT(to);
299
300         CycleNode *fromnode = getNode(from);
301         CycleNode *tonode = getNode(to);
302
303         return addNodeEdge(fromnode, tonode);
304 }
305 /* Instantiate four forms of CycleGraph::addEdge */
306 template bool CycleGraph::addEdge(const ModelAction *from, const ModelAction *to);
307 template bool CycleGraph::addEdge(const ModelAction *from, const Promise *to);
308 template bool CycleGraph::addEdge(const Promise *from, const ModelAction *to);
309 template bool CycleGraph::addEdge(const Promise *from, const Promise *to);
310
311 #if SUPPORT_MOD_ORDER_DUMP
312
313 static void print_node(FILE *file, const CycleNode *node, int label)
314 {
315         if (node->is_promise()) {
316                 const Promise *promise = node->getPromise();
317                 int idx = promise->get_index();
318                 fprintf(file, "P%u", idx);
319                 if (label) {
320                         int first = 1;
321                         fprintf(file, " [label=\"P%d, T", idx);
322                         for (unsigned int i = 0 ; i < model->get_num_threads(); i++)
323                                 if (promise->thread_is_available(int_to_id(i))) {
324                                         fprintf(file, "%s%u", first ? "": ",", i);
325                                         first = 0;
326                                 }
327                         fprintf(file, "\"]");
328                 }
329         } else {
330                 const ModelAction *act = node->getAction();
331                 modelclock_t idx = act->get_seq_number();
332                 fprintf(file, "N%u", idx);
333                 if (label)
334                         fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid());
335         }
336 }
337
338 static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, const char *prop)
339 {
340         print_node(file, from, 0);
341         fprintf(file, " -> ");
342         print_node(file, to, 0);
343         if (prop && strlen(prop))
344                 fprintf(file, " [%s]", prop);
345         fprintf(file, ";\n");
346 }
347
348 void CycleGraph::dot_print_node(FILE *file, const ModelAction *act)
349 {
350         print_node(file, getNode(act), 1);
351 }
352
353 template <typename T, typename U>
354 void CycleGraph::dot_print_edge(FILE *file, const T *from, const U *to, const char *prop)
355 {
356         CycleNode *fromnode = getNode(from);
357         CycleNode *tonode = getNode(to);
358
359         print_edge(file, fromnode, tonode, prop);
360 }
361 /* Instantiate two forms of CycleGraph::dot_print_edge */
362 template void CycleGraph::dot_print_edge(FILE *file, const Promise *from, const ModelAction *to, const char *prop);
363 template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, const ModelAction *to, const char *prop);
364
365 void CycleGraph::dumpNodes(FILE *file) const
366 {
367         for (unsigned int i = 0; i < nodeList.size(); i++) {
368                 CycleNode *n = nodeList[i];
369                 print_node(file, n, 1);
370                 fprintf(file, ";\n");
371                 if (n->getRMW())
372                         print_edge(file, n, n->getRMW(), "style=dotted");
373                 for (unsigned int j = 0; j < n->getNumEdges(); j++)
374                         print_edge(file, n, n->getEdge(j), NULL);
375         }
376 }
377
378 void CycleGraph::dumpGraphToFile(const char *filename) const
379 {
380         char buffer[200];
381         sprintf(buffer, "%s.dot", filename);
382         FILE *file = fopen(buffer, "w");
383         fprintf(file, "digraph %s {\n", filename);
384         dumpNodes(file);
385         fprintf(file, "}\n");
386         fclose(file);
387 }
388 #endif
389
390 /**
391  * Checks whether one CycleNode can reach another.
392  * @param from The CycleNode from which to begin exploration
393  * @param to The CycleNode to reach
394  * @return True, @a from can reach @a to; otherwise, false
395  */
396 bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) const
397 {
398         discovered->reset();
399         queue->clear();
400         queue->push_back(from);
401         discovered->put(from, from);
402         while (!queue->empty()) {
403                 const CycleNode *node = queue->back();
404                 queue->pop_back();
405                 if (node == to)
406                         return true;
407                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
408                         CycleNode *next = node->getEdge(i);
409                         if (!discovered->contains(next)) {
410                                 discovered->put(next, next);
411                                 queue->push_back(next);
412                         }
413                 }
414         }
415         return false;
416 }
417
418 /**
419  * Checks whether one ModelAction/Promise can reach another ModelAction/Promise
420  * @param from The ModelAction or Promise from which to begin exploration
421  * @param to The ModelAction or Promise to reach
422  * @return True, @a from can reach @a to; otherwise, false
423  */
424 template <typename T, typename U>
425 bool CycleGraph::checkReachable(const T *from, const U *to) const
426 {
427         CycleNode *fromnode = getNode_noCreate(from);
428         CycleNode *tonode = getNode_noCreate(to);
429
430         if (!fromnode || !tonode)
431                 return false;
432
433         return checkReachable(fromnode, tonode);
434 }
435 /* Instantiate four forms of CycleGraph::checkReachable */
436 template bool CycleGraph::checkReachable(const ModelAction *from,
437                 const ModelAction *to) const;
438 template bool CycleGraph::checkReachable(const ModelAction *from,
439                 const Promise *to) const;
440 template bool CycleGraph::checkReachable(const Promise *from,
441                 const ModelAction *to) const;
442 template bool CycleGraph::checkReachable(const Promise *from,
443                 const Promise *to) const;
444
445 /** @return True, if the promise has failed; false otherwise */
446 bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
447 {
448         discovered->reset();
449         queue->clear();
450         CycleNode *from = actionToNode.get(fromact);
451
452         queue->push_back(from);
453         discovered->put(from, from);
454         while (!queue->empty()) {
455                 const CycleNode *node = queue->back();
456                 queue->pop_back();
457
458                 if (node->getPromise() == promise)
459                         return true;
460                 if (!node->is_promise() &&
461                                 promise->eliminate_thread(node->getAction()->get_tid()))
462                         return true;
463
464                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
465                         CycleNode *next = node->getEdge(i);
466                         if (!discovered->contains(next)) {
467                                 discovered->put(next, next);
468                                 queue->push_back(next);
469                         }
470                 }
471         }
472         return false;
473 }
474
475 /** @brief Begin a new sequence of graph additions which can be rolled back */
476 void CycleGraph::startChanges()
477 {
478         ASSERT(rollbackvector.empty());
479         ASSERT(rmwrollbackvector.empty());
480         ASSERT(oldCycles == hasCycles);
481 }
482
483 /** Commit changes to the cyclegraph. */
484 void CycleGraph::commitChanges()
485 {
486         rollbackvector.clear();
487         rmwrollbackvector.clear();
488         oldCycles = hasCycles;
489 }
490
491 /** Rollback changes to the previous commit. */
492 void CycleGraph::rollbackChanges()
493 {
494         for (unsigned int i = 0; i < rollbackvector.size(); i++)
495                 rollbackvector[i]->removeEdge();
496
497         for (unsigned int i = 0; i < rmwrollbackvector.size(); i++)
498                 rmwrollbackvector[i]->clearRMW();
499
500         hasCycles = oldCycles;
501         rollbackvector.clear();
502         rmwrollbackvector.clear();
503 }
504
505 /** @returns whether a CycleGraph contains cycles. */
506 bool CycleGraph::checkForCycles() const
507 {
508         return hasCycles;
509 }
510
511 /**
512  * @brief Constructor for a CycleNode
513  * @param act The ModelAction for this node
514  */
515 CycleNode::CycleNode(const ModelAction *act) :
516         action(act),
517         promise(NULL),
518         hasRMW(NULL)
519 {
520 }
521
522 /**
523  * @brief Constructor for a Promise CycleNode
524  * @param promise The Promise which was generated
525  */
526 CycleNode::CycleNode(const Promise *promise) :
527         action(NULL),
528         promise(promise),
529         hasRMW(NULL)
530 {
531 }
532
533 /**
534  * @param i The index of the edge to return
535  * @returns The CycleNode edge indexed by i
536  */
537 CycleNode * CycleNode::getEdge(unsigned int i) const
538 {
539         return edges[i];
540 }
541
542 /** @returns The number of edges leaving this CycleNode */
543 unsigned int CycleNode::getNumEdges() const
544 {
545         return edges.size();
546 }
547
548 /**
549  * @param i The index of the back edge to return
550  * @returns The CycleNode back-edge indexed by i
551  */
552 CycleNode * CycleNode::getBackEdge(unsigned int i) const
553 {
554         return back_edges[i];
555 }
556
557 /** @returns The number of edges entering this CycleNode */
558 unsigned int CycleNode::getNumBackEdges() const
559 {
560         return back_edges.size();
561 }
562
563 /**
564  * @brief Remove an element from a vector
565  * @param v The vector
566  * @param n The element to remove
567  * @return True if the element was found; false otherwise
568  */
569 template <typename T>
570 static bool vector_remove_node(SnapVector<T>& v, const T n)
571 {
572         for (unsigned int i = 0; i < v.size(); i++) {
573                 if (v[i] == n) {
574                         v.erase(v.begin() + i);
575                         return true;
576                 }
577         }
578         return false;
579 }
580
581 /**
582  * @brief Remove a (forward) edge from this CycleNode
583  * @return The CycleNode which was popped, if one exists; otherwise NULL
584  */
585 CycleNode * CycleNode::removeEdge()
586 {
587         if (edges.empty())
588                 return NULL;
589
590         CycleNode *ret = edges.back();
591         edges.pop_back();
592         vector_remove_node(ret->back_edges, this);
593         return ret;
594 }
595
596 /**
597  * @brief Remove a (back) edge from this CycleNode
598  * @return The CycleNode which was popped, if one exists; otherwise NULL
599  */
600 CycleNode * CycleNode::removeBackEdge()
601 {
602         if (back_edges.empty())
603                 return NULL;
604
605         CycleNode *ret = back_edges.back();
606         back_edges.pop_back();
607         vector_remove_node(ret->edges, this);
608         return ret;
609 }
610
611 /**
612  * Adds an edge from this CycleNode to another CycleNode.
613  * @param node The node to which we add a directed edge
614  * @return True if this edge is a new edge; false otherwise
615  */
616 bool CycleNode::addEdge(CycleNode *node)
617 {
618         for (unsigned int i = 0; i < edges.size(); i++)
619                 if (edges[i] == node)
620                         return false;
621         edges.push_back(node);
622         node->back_edges.push_back(this);
623         return true;
624 }
625
626 /** @returns the RMW CycleNode that reads from the current CycleNode */
627 CycleNode * CycleNode::getRMW() const
628 {
629         return hasRMW;
630 }
631
632 /**
633  * Set a RMW action node that reads from the current CycleNode.
634  * @param node The RMW that reads from the current node
635  * @return True, if this node already was read by another RMW; false otherwise
636  * @see CycleGraph::addRMWEdge
637  */
638 bool CycleNode::setRMW(CycleNode *node)
639 {
640         if (hasRMW != NULL)
641                 return true;
642         hasRMW = node;
643         return false;
644 }
645
646 /**
647  * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be
648  * used when there's no existing ModelAction CycleNode for this write.
649  *
650  * @param writer The ModelAction which wrote the future value represented by
651  * this CycleNode
652  */
653 void CycleNode::resolvePromise(const ModelAction *writer)
654 {
655         ASSERT(is_promise());
656         ASSERT(promise->is_compatible(writer));
657         action = writer;
658         promise = NULL;
659         ASSERT(!is_promise());
660 }