cyclegraph/model: unify, clean up graph printing

This fixes several things:

1) The rf edges now are directed properly
2) Read-from-promises show up in the graph
3) ModelChecker uses the same code as CycleGraph for printing a
   CycleNode or graph edge
4) Graphs are more readable; I put a large weight on the
   sequenced-before edges, causing graphviz to try to make these edges
   "shorter, straighter and more vertical" [1]
5) Use the 'SnapshotAlloc' STL allocator for CycleGraph::nodeList

[1] http://www.graphviz.org/doc/info/attrs.html#d:weight

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 49ff00249fe9c49dbe9a1cda9fdad32af78c0f70..7e111b95a3a4bc43334d7037260fdc85ccbfc9c7 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -320,7 +320,7 @@ static void print_node(FILE *file, const CycleNode *node, int label)
        if (node->is_promise()) {
                const Promise *promise = node->getPromise();
                int idx = model->get_promise_number(promise);
-               fprintf(file, "P%d", idx);
+               fprintf(file, "P%u", idx);
                if (label) {
                        int first = 1;
                        fprintf(file, " [label=\"P%d, T", idx);
@@ -350,6 +350,23 @@ static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, c
        fprintf(file, ";\n");
 }
 
+void CycleGraph::dot_print_node(FILE *file, const ModelAction *act)
+{
+       print_node(file, getNode(act), 1);
+}
+
+template <typename T, typename U>
+void CycleGraph::dot_print_edge(FILE *file, const T *from, const U *to, const char *prop)
+{
+       CycleNode *fromnode = getNode(from);
+       CycleNode *tonode = getNode(to);
+
+       print_edge(file, fromnode, tonode, prop);
+}
+/* Instantiate two forms of CycleGraph::dot_print_edge */
+template void CycleGraph::dot_print_edge(FILE *file, const Promise *from, const ModelAction *to, const char *prop);
+template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, const ModelAction *to, const char *prop);
+
 void CycleGraph::dumpNodes(FILE *file) const
 {
        for (unsigned int i = 0; i < nodeList.size(); i++) {

diff --git a/cyclegraph.h b/cyclegraph.h
index 1af54c77818bde954d784eb925cc56adc2013fd4..a2cb93d7ca702217be5af879cbf0c2ba34f9a67e 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -9,9 +9,11 @@
 #ifndef __CYCLEGRAPH_H__
 #define __CYCLEGRAPH_H__
 
-#include "hashtable.h"
 #include <vector>
 #include <inttypes.h>
+#include <stdio.h>
+
+#include "hashtable.h"
 #include "config.h"
 #include "mymemory.h"
 
@@ -45,6 +47,10 @@ class CycleGraph {
 #if SUPPORT_MOD_ORDER_DUMP
        void dumpNodes(FILE *file) const;
        void dumpGraphToFile(const char *filename) const;
+
+       void dot_print_node(FILE *file, const ModelAction *act);
+       template <typename T, typename U>
+       void dot_print_edge(FILE *file, const T *from, const U *to, const char *prop);
 #endif
 
        bool resolvePromise(const Promise *promise, ModelAction *writer,
@@ -71,7 +77,7 @@ class CycleGraph {
        HashTable<const Promise *, CycleNode *, uintptr_t, 4> promiseToNode;
 
 #if SUPPORT_MOD_ORDER_DUMP
-       std::vector<CycleNode *> nodeList;
+       std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > nodeList;
 #endif
 
        bool checkReachable(const CycleNode *from, const CycleNode *to) const;

diff --git a/model.cc b/model.cc
index fa4dcc6fd3976281633317152bd4450d636fcc0c..9ebc85344cd8c4343349a4d7df21e9d034915edc 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2764,17 +2764,28 @@ void ModelChecker::dumpGraph(char *filename) const
        ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
 
        for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
-               ModelAction *action = *it;
-               if (action->is_read()) {
-                       fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
-                       if (action->get_reads_from() != NULL)
-                               fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+               ModelAction *act = *it;
+               if (act->is_read()) {
+                       mo_graph->dot_print_node(file, act);
+                       if (act->get_reads_from())
+                               mo_graph->dot_print_edge(file,
+                                               act->get_reads_from(),
+                                               act,
+                                               "label=\"rf\", color=red, weight=2");
+                       else
+                               mo_graph->dot_print_edge(file,
+                                               act->get_reads_from_promise(),
+                                               act,
+                                               "label=\"rf\", color=red");
                }
-               if (thread_array[action->get_tid()] != NULL) {
-                       fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
+               if (thread_array[act->get_tid()]) {
+                       mo_graph->dot_print_edge(file,
+                                       thread_array[id_to_int(act->get_tid())],
+                                       act,
+                                       "label=\"sb\", color=blue, weight=400");
                }
 
-               thread_array[action->get_tid()] = action;
+               thread_array[act->get_tid()] = act;
        }
        fprintf(file, "}\n");
        model_free(thread_array);