From: Brian Norris <banorris@uci.edu>
Date: Fri, 1 Mar 2013 07:24:20 +0000 (-0800)
Subject: cyclegraph/model: unify, clean up graph printing
X-Git-Tag: oopsla2013~198
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=e0f80c403452e544452f64687b3c489a869e4f77

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 49ff002..7e111b9 100644
--- 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 1af54c7..a2cb93d 100644
--- 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 fa4dcc6..9ebc853 100644
--- 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);