model: add variable arguments for bug messages
[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  * (1) no write can occur in between the rmw and the from action.
236  * (2) 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 = model->get_promise_number(promise);
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 void CycleGraph::startChanges()
476 {
477         ASSERT(rollbackvector.empty());
478         ASSERT(rmwrollbackvector.empty());
479         ASSERT(oldCycles == hasCycles);
480 }
481
482 /** Commit changes to the cyclegraph. */
483 void CycleGraph::commitChanges()
484 {
485         rollbackvector.clear();
486         rmwrollbackvector.clear();
487         oldCycles = hasCycles;
488 }
489
490 /** Rollback changes to the previous commit. */
491 void CycleGraph::rollbackChanges()
492 {
493         for (unsigned int i = 0; i < rollbackvector.size(); i++)
494                 rollbackvector[i]->removeEdge();
495
496         for (unsigned int i = 0; i < rmwrollbackvector.size(); i++)
497                 rmwrollbackvector[i]->clearRMW();
498
499         hasCycles = oldCycles;
500         rollbackvector.clear();
501         rmwrollbackvector.clear();
502 }
503
504 /** @returns whether a CycleGraph contains cycles. */
505 bool CycleGraph::checkForCycles() const
506 {
507         return hasCycles;
508 }
509
510 /**
511  * @brief Constructor for a CycleNode
512  * @param act The ModelAction for this node
513  */
514 CycleNode::CycleNode(const ModelAction *act) :
515         action(act),
516         promise(NULL),
517         hasRMW(NULL)
518 {
519 }
520
521 /**
522  * @brief Constructor for a Promise CycleNode
523  * @param promise The Promise which was generated
524  */
525 CycleNode::CycleNode(const Promise *promise) :
526         action(NULL),
527         promise(promise),
528         hasRMW(NULL)
529 {
530 }
531
532 /**
533  * @param i The index of the edge to return
534  * @returns The a CycleNode edge indexed by i
535  */
536 CycleNode * CycleNode::getEdge(unsigned int i) const
537 {
538         return edges[i];
539 }
540
541 /** @returns The number of edges leaving this CycleNode */
542 unsigned int CycleNode::getNumEdges() const
543 {
544         return edges.size();
545 }
546
547 CycleNode * CycleNode::getBackEdge(unsigned int i) const
548 {
549         return back_edges[i];
550 }
551
552 unsigned int CycleNode::getNumBackEdges() const
553 {
554         return back_edges.size();
555 }
556
557 /**
558  * @brief Remove an element from a vector
559  * @param v The vector
560  * @param n The element to remove
561  * @return True if the element was found; false otherwise
562  */
563 template <typename T>
564 static bool vector_remove_node(SnapVector<T>& v, const T n)
565 {
566         for (unsigned int i = 0; i < v.size(); i++) {
567                 if (v[i] == n) {
568                         v.erase(v.begin() + i);
569                         return true;
570                 }
571         }
572         return false;
573 }
574
575 /**
576  * @brief Remove a (forward) edge from this CycleNode
577  * @return The CycleNode which was popped, if one exists; otherwise NULL
578  */
579 CycleNode * CycleNode::removeEdge()
580 {
581         if (edges.empty())
582                 return NULL;
583
584         CycleNode *ret = edges.back();
585         edges.pop_back();
586         vector_remove_node(ret->back_edges, this);
587         return ret;
588 }
589
590 /**
591  * @brief Remove a (back) edge from this CycleNode
592  * @return The CycleNode which was popped, if one exists; otherwise NULL
593  */
594 CycleNode * CycleNode::removeBackEdge()
595 {
596         if (back_edges.empty())
597                 return NULL;
598
599         CycleNode *ret = back_edges.back();
600         back_edges.pop_back();
601         vector_remove_node(ret->edges, this);
602         return ret;
603 }
604
605 /**
606  * Adds an edge from this CycleNode to another CycleNode.
607  * @param node The node to which we add a directed edge
608  * @return True if this edge is a new edge; false otherwise
609  */
610 bool CycleNode::addEdge(CycleNode *node)
611 {
612         for (unsigned int i = 0; i < edges.size(); i++)
613                 if (edges[i] == node)
614                         return false;
615         edges.push_back(node);
616         node->back_edges.push_back(this);
617         return true;
618 }
619
620 /** @returns the RMW CycleNode that reads from the current CycleNode */
621 CycleNode * CycleNode::getRMW() const
622 {
623         return hasRMW;
624 }
625
626 /**
627  * Set a RMW action node that reads from the current CycleNode.
628  * @param node The RMW that reads from the current node
629  * @return True, if this node already was read by another RMW; false otherwise
630  * @see CycleGraph::addRMWEdge
631  */
632 bool CycleNode::setRMW(CycleNode *node)
633 {
634         if (hasRMW != NULL)
635                 return true;
636         hasRMW = node;
637         return false;
638 }
639
640 /**
641  * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be
642  * used when there's no existing ModelAction CycleNode for this write.
643  *
644  * @param writer The ModelAction which wrote the future value represented by
645  * this CycleNode
646  */
647 void CycleNode::resolvePromise(const ModelAction *writer)
648 {
649         ASSERT(is_promise());
650         ASSERT(promise->is_compatible(writer));
651         action = writer;
652         promise = NULL;
653         ASSERT(!is_promise());
654 }