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