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