cyclegraph: change Promise nodes map
[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         promiseToNode.put(promise, node);
42 #if SUPPORT_MOD_ORDER_DUMP
43         nodeList.push_back(node);
44 #endif
45 }
46
47 /**
48  * @brief Remove the Promise node from the graph
49  * @param promise The promise to remove from the graph
50  */
51 void CycleGraph::erasePromiseNode(const Promise *promise)
52 {
53         promiseToNode.put(promise, NULL);
54 #if SUPPORT_MOD_ORDER_DUMP
55         /* Remove the promise node from nodeList */
56         CycleNode *node = getNode_noCreate(promise);
57         for (unsigned int i = 0; i < nodeList.size(); )
58                 if (nodeList[i] == node)
59                         nodeList.erase(nodeList.begin() + i);
60                 else
61                         i++;
62 #endif
63 }
64
65 /** @return The corresponding CycleNode, if exists; otherwise NULL */
66 CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
67 {
68         return actionToNode.get(act);
69 }
70
71 /** @return The corresponding CycleNode, if exists; otherwise NULL */
72 CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const
73 {
74         return promiseToNode.get(promise);
75 }
76
77 /**
78  * @brief Returns the CycleNode corresponding to a given ModelAction
79  *
80  * Gets (or creates, if none exist) a CycleNode corresponding to a ModelAction
81  *
82  * @param action The ModelAction to find a node for
83  * @return The CycleNode paired with this action
84  */
85 CycleNode * CycleGraph::getNode(const ModelAction *action)
86 {
87         CycleNode *node = getNode_noCreate(action);
88         if (node == NULL) {
89                 node = new CycleNode(action);
90                 putNode(action, node);
91         }
92         return node;
93 }
94
95 /**
96  * @brief Returns a CycleNode corresponding to a promise
97  *
98  * Gets (or creates, if none exist) a CycleNode corresponding to a promised
99  * value.
100  *
101  * @param promise The Promise generated by a reader
102  * @return The CycleNode corresponding to the Promise
103  */
104 CycleNode * CycleGraph::getNode(const Promise *promise)
105 {
106         CycleNode *node = getNode_noCreate(promise);
107         if (node == NULL) {
108                 node = new CycleNode(promise);
109                 putNode(promise, node);
110         }
111         return node;
112 }
113
114 /**
115  * @return false if the resolution results in a cycle; true otherwise
116  */
117 bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer,
118                 promise_list_t *mustResolve)
119 {
120         CycleNode *promise_node = promiseToNode.get(promise);
121         CycleNode *w_node = actionToNode.get(writer);
122         ASSERT(promise_node);
123
124         if (w_node)
125                 return mergeNodes(w_node, promise_node, mustResolve);
126         /* No existing write-node; just convert the promise-node */
127         promise_node->resolvePromise(writer);
128         erasePromiseNode(promise_node->getPromise());
129         putNode(writer, promise_node);
130         return true;
131 }
132
133 /**
134  * @brief Merge two CycleNodes that represent the same write
135  *
136  * Note that this operation cannot be rolled back.
137  *
138  * @param w_node The write ModelAction node with which to merge
139  * @param p_node The Promise node to merge. Will be destroyed after this
140  * function.
141  * @param mustMerge Return (pass-by-reference) any additional Promises that
142  * must also be merged with w_node
143  *
144  * @return false if the merge results in a cycle; true otherwise
145  */
146 bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node,
147                 promise_list_t *mustMerge)
148 {
149         ASSERT(!w_node->is_promise());
150         ASSERT(p_node->is_promise());
151
152         const Promise *promise = p_node->getPromise();
153         if (!promise->is_compatible(w_node->getAction())) {
154                 hasCycles = true;
155                 return false;
156         }
157
158         /* Transfer the RMW */
159         CycleNode *promise_rmw = p_node->getRMW();
160         if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw)) {
161                 hasCycles = true;
162                 return false;
163         }
164
165         /* Transfer back edges to w_node */
166         while (p_node->getNumBackEdges() > 0) {
167                 CycleNode *back = p_node->removeBackEdge();
168                 if (back == w_node)
169                         continue;
170                 if (back->is_promise()) {
171                         if (checkReachable(w_node, back)) {
172                                 /* Edge would create cycle; merge instead */
173                                 mustMerge->push_back(back->getPromise());
174                                 if (!mergeNodes(w_node, back, mustMerge))
175                                         return false;
176                         } else
177                                 back->addEdge(w_node);
178                 } else
179                         addNodeEdge(back, w_node);
180         }
181
182         /* Transfer forward edges to w_node */
183         while (p_node->getNumEdges() > 0) {
184                 CycleNode *forward = p_node->removeEdge();
185                 if (forward == w_node)
186                         continue;
187                 if (forward->is_promise()) {
188                         if (checkReachable(forward, w_node)) {
189                                 mustMerge->push_back(forward->getPromise());
190                                 if (!mergeNodes(w_node, forward, mustMerge))
191                                         return false;
192                         } else
193                                 w_node->addEdge(forward);
194                 } else
195                         addNodeEdge(w_node, forward);
196         }
197
198         erasePromiseNode(promise);
199         /* Not deleting p_node, to maintain consistency if mergeNodes() fails */
200
201         return !hasCycles;
202 }
203
204 /**
205  * Adds an edge between two CycleNodes.
206  * @param fromnode The edge comes from this CycleNode
207  * @param tonode The edge points to this CycleNode
208  * @return True, if new edge(s) are added; otherwise false
209  */
210 bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
211 {
212         bool added;
213
214         if (!hasCycles)
215                 hasCycles = checkReachable(tonode, fromnode);
216
217         if ((added = fromnode->addEdge(tonode)))
218                 rollbackvector.push_back(fromnode);
219
220         /*
221          * If the fromnode has a rmwnode that is not the tonode, we should add
222          * an edge between its rmwnode and the tonode
223          */
224         CycleNode *rmwnode = fromnode->getRMW();
225         if (rmwnode && rmwnode != tonode) {
226                 if (!hasCycles)
227                         hasCycles = checkReachable(tonode, rmwnode);
228
229                 if (rmwnode->addEdge(tonode)) {
230                         rollbackvector.push_back(rmwnode);
231                         added = true;
232                 }
233         }
234         return added;
235 }
236
237 /**
238  * @brief Add an edge between a write and the RMW which reads from it
239  *
240  * Handles special case of a RMW action, where the ModelAction rmw reads from
241  * the ModelAction/Promise from. The key differences are:
242  * (1) no write can occur in between the rmw and the from action.
243  * (2) Only one RMW action can read from a given write.
244  *
245  * @param from The edge comes from this ModelAction/Promise
246  * @param rmw The edge points to this ModelAction; this action must read from
247  * the ModelAction/Promise from
248  */
249 template <typename T>
250 void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw)
251 {
252         ASSERT(from);
253         ASSERT(rmw);
254
255         CycleNode *fromnode = getNode(from);
256         CycleNode *rmwnode = getNode(rmw);
257
258         /* Two RMW actions cannot read from the same write. */
259         if (fromnode->setRMW(rmwnode))
260                 hasCycles = true;
261         else
262                 rmwrollbackvector.push_back(fromnode);
263
264         /* Transfer all outgoing edges from the from node to the rmw node */
265         /* This process should not add a cycle because either:
266          * (1) The rmw should not have any incoming edges yet if it is the
267          * new node or
268          * (2) the fromnode is the new node and therefore it should not
269          * have any outgoing edges.
270          */
271         for (unsigned int i = 0; i < fromnode->getNumEdges(); i++) {
272                 CycleNode *tonode = fromnode->getEdge(i);
273                 if (tonode != rmwnode) {
274                         if (rmwnode->addEdge(tonode))
275                                 rollbackvector.push_back(rmwnode);
276                 }
277         }
278
279         addNodeEdge(fromnode, rmwnode);
280 }
281 /* Instantiate two forms of CycleGraph::addRMWEdge */
282 template void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw);
283 template void CycleGraph::addRMWEdge(const Promise *from, const ModelAction *rmw);
284
285 /**
286  * @brief Adds an edge between objects
287  *
288  * This function will add an edge between any two objects which can be
289  * associated with a CycleNode. That is, if they have a CycleGraph::getNode
290  * implementation.
291  *
292  * The object to is ordered after the object from.
293  *
294  * @param to The edge points to this object, of type T
295  * @param from The edge comes from this object, of type U
296  * @return True, if new edge(s) are added; otherwise false
297  */
298 template <typename T, typename U>
299 bool CycleGraph::addEdge(const T *from, const U *to)
300 {
301         ASSERT(from);
302         ASSERT(to);
303
304         CycleNode *fromnode = getNode(from);
305         CycleNode *tonode = getNode(to);
306
307         return addNodeEdge(fromnode, tonode);
308 }
309 /* Instantiate four forms of CycleGraph::addEdge */
310 template bool CycleGraph::addEdge(const ModelAction *from, const ModelAction *to);
311 template bool CycleGraph::addEdge(const ModelAction *from, const Promise *to);
312 template bool CycleGraph::addEdge(const Promise *from, const ModelAction *to);
313 template bool CycleGraph::addEdge(const Promise *from, const Promise *to);
314
315 #if SUPPORT_MOD_ORDER_DUMP
316
317 static void print_node(const CycleNode *node, FILE *file, int label)
318 {
319         modelclock_t idx;
320         if (node->is_promise()) {
321                 const Promise *promise = node->getPromise();
322                 idx = promise->get_action()->get_seq_number();
323                 fprintf(file, "P%u", idx);
324                 if (label) {
325                         int first = 1;
326                         fprintf(file, " [label=\"P%u, T", idx);
327                         for (unsigned int i = 0 ; i < model->get_num_threads(); i++)
328                                 if (promise->thread_is_available(int_to_id(i))) {
329                                         fprintf(file, "%s%u", first ? "": ",", i);
330                                         first = 0;
331                                 }
332                         fprintf(file, "\"]");
333                 }
334         } else {
335                 const ModelAction *act = node->getAction();
336                 idx = act->get_seq_number();
337                 fprintf(file, "N%u", idx);
338                 if (label)
339                         fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid());
340         }
341 }
342
343 void CycleGraph::dumpNodes(FILE *file) const
344 {
345         for (unsigned int i = 0; i < nodeList.size(); i++) {
346                 CycleNode *n = nodeList[i];
347                 print_node(n, file, 1);
348                 fprintf(file, ";\n");
349                 if (n->getRMW() != NULL) {
350                         print_node(n, file, 0);
351                         fprintf(file, " -> ");
352                         print_node(n->getRMW(), file, 0);
353                         fprintf(file, "[style=dotted];\n");
354                 }
355                 for (unsigned int j = 0; j < n->getNumEdges(); j++) {
356                         print_node(n, file, 0);
357                         fprintf(file, " -> ");
358                         print_node(n->getEdge(j), file, 0);
359                         fprintf(file, ";\n");
360                 }
361         }
362 }
363
364 void CycleGraph::dumpGraphToFile(const char *filename) const
365 {
366         char buffer[200];
367         sprintf(buffer, "%s.dot", filename);
368         FILE *file = fopen(buffer, "w");
369         fprintf(file, "digraph %s {\n", filename);
370         dumpNodes(file);
371         fprintf(file, "}\n");
372         fclose(file);
373 }
374 #endif
375
376 /**
377  * Checks whether one CycleNode can reach another.
378  * @param from The CycleNode from which to begin exploration
379  * @param to The CycleNode to reach
380  * @return True, @a from can reach @a to; otherwise, false
381  */
382 bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) const
383 {
384         std::vector< const CycleNode *, ModelAlloc<const CycleNode *> > queue;
385         discovered->reset();
386
387         queue.push_back(from);
388         discovered->put(from, from);
389         while (!queue.empty()) {
390                 const CycleNode *node = queue.back();
391                 queue.pop_back();
392                 if (node == to)
393                         return true;
394
395                 for (unsigned int i = 0; i < node->getNumEdges(); i++) {
396                         CycleNode *next = node->getEdge(i);
397                         if (!discovered->contains(next)) {
398                                 discovered->put(next, next);
399                                 queue.push_back(next);
400                         }
401                 }
402         }
403         return false;
404 }
405
406 /**
407  * Checks whether one ModelAction/Promise can reach another ModelAction/Promise
408  * @param from The ModelAction or Promise from which to begin exploration
409  * @param to The ModelAction or Promise to reach
410  * @return True, @a from can reach @a to; otherwise, false
411  */
412 template <typename T, typename U>
413 bool CycleGraph::checkReachable(const T *from, const U *to) const
414 {
415         CycleNode *fromnode = getNode_noCreate(from);
416         CycleNode *tonode = getNode_noCreate(to);
417
418         if (!fromnode || !tonode)
419                 return false;
420
421         return checkReachable(fromnode, tonode);
422 }
423 /* Instantiate three forms of CycleGraph::checkReachable */
424 template bool CycleGraph::checkReachable(const ModelAction *from,
425                 const ModelAction *to) const;
426 template bool CycleGraph::checkReachable(const ModelAction *from,
427                 const Promise *to) const;
428 template bool CycleGraph::checkReachable(const Promise *from,
429                 const ModelAction *to) const;
430
431 /** @return True, if the promise has failed; false otherwise */
432 bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
433 {
434         std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
435         discovered->reset();
436         CycleNode *from = actionToNode.get(fromact);
437
438         queue.push_back(from);
439         discovered->put(from, from);
440         while (!queue.empty()) {
441                 CycleNode *node = queue.back();
442                 queue.pop_back();
443
444                 if (node->getPromise() == promise)
445                         return true;
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 }