promise: update comments/names to reflect usage
[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  * Add a CycleNode to the graph, corresponding to a Promise
36  * @param promise The Promise that should be added
37  * @param node The CycleNode that corresponds to the Promise
38  */
39 void CycleGraph::putNode(const Promise *promise, CycleNode *node)
40 {
41         const ModelAction *reader = promise->get_action();
42         readerToPromiseNode.put(reader, 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         const ModelAction *reader = promise->get_action();
55         readerToPromiseNode.put(reader, NULL);
56 #if SUPPORT_MOD_ORDER_DUMP
57         /* Remove the promise node from nodeList */
58         CycleNode *node = getNode_noCreate(promise);
59         for (unsigned int i = 0; i < nodeList.size(); )
60                 if (nodeList[i] == node)
61                         nodeList.erase(nodeList.begin() + i);
62                 else
63                         i++;
64 #endif
65 }
66
67 /** @return The corresponding CycleNode, if exists; otherwise NULL */
68 CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
69 {
70         return actionToNode.get(act);
71 }
72
73 /** @return The corresponding CycleNode, if exists; otherwise NULL */
74 CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const
75 {
76         return readerToPromiseNode.get(promise->get_action());
77 }
78
79 /**
80  * @brief Returns the CycleNode corresponding to a given ModelAction
81  *
82  * Gets (or creates, if none exist) a CycleNode corresponding to a ModelAction
83  *
84  * @param action The ModelAction to find a node for
85  * @return The CycleNode paired with this action
86  */
87 CycleNode * CycleGraph::getNode(const ModelAction *action)
88 {
89         CycleNode *node = getNode_noCreate(action);
90         if (node == NULL) {
91                 node = new CycleNode(action);
92                 putNode(action, node);
93         }
94         return node;
95 }
96
97 /**
98  * @brief Returns a CycleNode corresponding to a promise
99  *
100  * Gets (or creates, if none exist) a CycleNode corresponding to a promised
101  * value.
102  *
103  * @param promise The Promise generated by a reader
104  * @return The CycleNode corresponding to the Promise
105  */
106 CycleNode * CycleGraph::getNode(const Promise *promise)
107 {
108         CycleNode *node = getNode_noCreate(promise);
109         if (node == NULL) {
110                 node = new CycleNode(promise);
111                 putNode(promise, node);
112         }
113         return node;
114 }
115
116 /**
117  * @return false if the resolution results in a cycle; true otherwise
118  */
119 bool CycleGraph::resolvePromise(ModelAction *reader, ModelAction *writer,
120                 promise_list_t *mustResolve)
121 {
122         CycleNode *promise_node = readerToPromiseNode.get(reader);
123         CycleNode *w_node = actionToNode.get(writer);
124         ASSERT(promise_node);
125
126         if (w_node)
127                 return mergeNodes(w_node, promise_node, mustResolve);
128         /* No existing write-node; just convert the promise-node */
129         promise_node->resolvePromise(writer);
130         erasePromiseNode(promise_node->getPromise());
131         putNode(writer, promise_node);
132         return true;
133 }
134
135 /**
136  * @brief Merge two CycleNodes that represent the same write
137  *
138  * Note that this operation cannot be rolled back.
139  *
140  * @param w_node The write ModelAction node with which to merge
141  * @param p_node The Promise node to merge. Will be destroyed after this
142  * function.
143  * @param mustMerge Return (pass-by-reference) any additional Promises that
144  * must also be merged with w_node
145  *
146  * @return false if the merge results in a cycle; true otherwise
147  */
148 bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node,
149                 promise_list_t *mustMerge)
150 {
151         ASSERT(!w_node->is_promise());
152         ASSERT(p_node->is_promise());
153
154         const Promise *promise = p_node->getPromise();
155         if (!promise->is_compatible(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(const CycleNode *node, FILE *file, int label)
320 {
321         modelclock_t idx;
322         if (node->is_promise()) {
323                 const Promise *promise = node->getPromise();
324                 idx = promise->get_action()->get_seq_number();
325                 fprintf(file, "P%u", idx);
326                 if (label) {
327                         int first = 1;
328                         fprintf(file, " [label=\"P%u, T", idx);
329                         for (unsigned int i = 0 ; i < model->get_num_threads(); i++)
330                                 if (promise->thread_is_available(int_to_id(i))) {
331                                         fprintf(file, "%s%u", first ? "": ",", i);
332                                         first = 0;
333                                 }
334                         fprintf(file, "\"]");
335                 }
336         } else {
337                 const ModelAction *act = node->getAction();
338                 idx = act->get_seq_number();
339                 fprintf(file, "N%u", idx);
340                 if (label)
341                         fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid());
342         }
343 }
344
345 void CycleGraph::dumpNodes(FILE *file) const
346 {
347         for (unsigned int i = 0; i < nodeList.size(); i++) {
348                 CycleNode *n = nodeList[i];
349                 print_node(n, file, 1);
350                 fprintf(file, ";\n");
351                 if (n->getRMW() != NULL) {
352                         print_node(n, file, 0);
353                         fprintf(file, " -> ");
354                         print_node(n->getRMW(), file, 0);
355                         fprintf(file, "[style=dotted];\n");
356                 }
357                 for (unsigned int j = 0; j < n->getNumEdges(); j++) {
358                         print_node(n, file, 0);
359                         fprintf(file, " -> ");
360                         print_node(n->getEdge(j), file, 0);
361                         fprintf(file, ";\n");
362                 }
363         }
364 }
365
366 void CycleGraph::dumpGraphToFile(const char *filename) const
367 {
368         char buffer[200];
369         sprintf(buffer, "%s.dot", filename);
370         FILE *file = fopen(buffer, "w");
371         fprintf(file, "digraph %s {\n", filename);
372         dumpNodes(file);
373         fprintf(file, "}\n");
374         fclose(file);
375 }
376 #endif
377
378 /**
379  * Checks whether one CycleNode can reach another.
380  * @param from The CycleNode from which to begin exploration
381  * @param to The CycleNode to reach
382  * @return True, @a from can reach @a to; otherwise, false
383  */
384 bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) const
385 {
386         std::vector< const CycleNode *, ModelAlloc<const CycleNode *> > queue;
387         discovered->reset();
388
389         queue.push_back(from);
390         discovered->put(from, from);
391         while (!queue.empty()) {
392                 const CycleNode *node = queue.back();
393                 queue.pop_back();
394                 if (node == to)
395                         return true;
396
397                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
398                         CycleNode *next = node->getEdge(i);
399                         if (!discovered->contains(next)) {
400                                 discovered->put(next, next);
401                                 queue.push_back(next);
402                         }
403                 }
404         }
405         return false;
406 }
407
408 /**
409  * Checks whether one ModelAction/Promise can reach another ModelAction/Promise
410  * @param from The ModelAction or Promise from which to begin exploration
411  * @param to The ModelAction or Promise to reach
412  * @return True, @a from can reach @a to; otherwise, false
413  */
414 template <typename T, typename U>
415 bool CycleGraph::checkReachable(const T *from, const U *to) const
416 {
417         CycleNode *fromnode = getNode_noCreate(from);
418         CycleNode *tonode = getNode_noCreate(to);
419
420         if (!fromnode || !tonode)
421                 return false;
422
423         return checkReachable(fromnode, tonode);
424 }
425 /* Instantiate three forms of CycleGraph::checkReachable */
426 template bool CycleGraph::checkReachable(const ModelAction *from,
427                 const ModelAction *to) const;
428 template bool CycleGraph::checkReachable(const ModelAction *from,
429                 const Promise *to) const;
430 template bool CycleGraph::checkReachable(const Promise *from,
431                 const ModelAction *to) const;
432
433 /** @return True, if the promise has failed; false otherwise */
434 bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
435 {
436         std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
437         discovered->reset();
438         CycleNode *from = actionToNode.get(fromact);
439
440         queue.push_back(from);
441         discovered->put(from, from);
442         while (!queue.empty()) {
443                 CycleNode *node = queue.back();
444                 queue.pop_back();
445
446                 if (!node->is_promise() &&
447                                 promise->eliminate_thread(node->getAction()->get_tid()))
448                         return true;
449
450                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
451                         CycleNode *next = node->getEdge(i);
452                         if (!discovered->contains(next)) {
453                                 discovered->put(next, next);
454                                 queue.push_back(next);
455                         }
456                 }
457         }
458         return false;
459 }
460
461 void CycleGraph::startChanges()
462 {
463         ASSERT(rollbackvector.empty());
464         ASSERT(rmwrollbackvector.empty());
465         ASSERT(oldCycles == hasCycles);
466 }
467
468 /** Commit changes to the cyclegraph. */
469 void CycleGraph::commitChanges()
470 {
471         rollbackvector.clear();
472         rmwrollbackvector.clear();
473         oldCycles = hasCycles;
474 }
475
476 /** Rollback changes to the previous commit. */
477 void CycleGraph::rollbackChanges()
478 {
479         for (unsigned int i = 0; i < rollbackvector.size(); i++)
480                 rollbackvector[i]->removeEdge();
481
482         for (unsigned int i = 0; i < rmwrollbackvector.size(); i++)
483                 rmwrollbackvector[i]->clearRMW();
484
485         hasCycles = oldCycles;
486         rollbackvector.clear();
487         rmwrollbackvector.clear();
488 }
489
490 /** @returns whether a CycleGraph contains cycles. */
491 bool CycleGraph::checkForCycles() const
492 {
493         return hasCycles;
494 }
495
496 /**
497  * @brief Constructor for a CycleNode
498  * @param act The ModelAction for this node
499  */
500 CycleNode::CycleNode(const ModelAction *act) :
501         action(act),
502         promise(NULL),
503         hasRMW(NULL)
504 {
505 }
506
507 /**
508  * @brief Constructor for a Promise CycleNode
509  * @param promise The Promise which was generated
510  */
511 CycleNode::CycleNode(const Promise *promise) :
512         action(NULL),
513         promise(promise),
514         hasRMW(NULL)
515 {
516 }
517
518 /**
519  * @param i The index of the edge to return
520  * @returns The a CycleNode edge indexed by i
521  */
522 CycleNode * CycleNode::getEdge(unsigned int i) const
523 {
524         return edges[i];
525 }
526
527 /** @returns The number of edges leaving this CycleNode */
528 unsigned int CycleNode::getNumEdges() const
529 {
530         return edges.size();
531 }
532
533 CycleNode * CycleNode::getBackEdge(unsigned int i) const
534 {
535         return back_edges[i];
536 }
537
538 unsigned int CycleNode::getNumBackEdges() const
539 {
540         return back_edges.size();
541 }
542
543 /**
544  * @brief Remove an element from a vector
545  * @param v The vector
546  * @param n The element to remove
547  * @return True if the element was found; false otherwise
548  */
549 template <typename T>
550 static bool vector_remove_node(std::vector<T, SnapshotAlloc<T> >& v, const T n)
551 {
552         for (unsigned int i = 0; i < v.size(); i++) {
553                 if (v[i] == n) {
554                         v.erase(v.begin() + i);
555                         return true;
556                 }
557         }
558         return false;
559 }
560
561 /**
562  * @brief Remove a (forward) edge from this CycleNode
563  * @return The CycleNode which was popped, if one exists; otherwise NULL
564  */
565 CycleNode * CycleNode::removeEdge()
566 {
567         if (edges.empty())
568                 return NULL;
569
570         CycleNode *ret = edges.back();
571         edges.pop_back();
572         vector_remove_node(ret->back_edges, this);
573         return ret;
574 }
575
576 /**
577  * @brief Remove a (back) edge from this CycleNode
578  * @return The CycleNode which was popped, if one exists; otherwise NULL
579  */
580 CycleNode * CycleNode::removeBackEdge()
581 {
582         if (back_edges.empty())
583                 return NULL;
584
585         CycleNode *ret = back_edges.back();
586         back_edges.pop_back();
587         vector_remove_node(ret->edges, this);
588         return ret;
589 }
590
591 /**
592  * Adds an edge from this CycleNode to another CycleNode.
593  * @param node The node to which we add a directed edge
594  * @return True if this edge is a new edge; false otherwise
595  */
596 bool CycleNode::addEdge(CycleNode *node)
597 {
598         for (unsigned int i = 0; i < edges.size(); i++)
599                 if (edges[i] == node)
600                         return false;
601         edges.push_back(node);
602         node->back_edges.push_back(this);
603         return true;
604 }
605
606 /** @returns the RMW CycleNode that reads from the current CycleNode */
607 CycleNode * CycleNode::getRMW() const
608 {
609         return hasRMW;
610 }
611
612 /**
613  * Set a RMW action node that reads from the current CycleNode.
614  * @param node The RMW that reads from the current node
615  * @return True, if this node already was read by another RMW; false otherwise
616  * @see CycleGraph::addRMWEdge
617  */
618 bool CycleNode::setRMW(CycleNode *node)
619 {
620         if (hasRMW != NULL)
621                 return true;
622         hasRMW = node;
623         return false;
624 }
625
626 /**
627  * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be
628  * used when there's no existing ModelAction CycleNode for this write.
629  *
630  * @param writer The ModelAction which wrote the future value represented by
631  * this CycleNode
632  */
633 void CycleNode::resolvePromise(const ModelAction *writer)
634 {
635         ASSERT(is_promise());
636         ASSERT(promise->is_compatible(writer));
637         action = writer;
638         promise = NULL;
639         ASSERT(!is_promise());
640 }