From eb3b6cccf71b9eeee035e2c98566dfa279e402ae Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Tue, 2 Oct 2012 02:09:13 -0700
Subject: [PATCH] start support for drawing execution diagrams

fix some signed/unsigned warnings
---
 cyclegraph.cc | 14 +++++++++-----
 cyclegraph.h  |  1 +
 model.cc      | 29 +++++++++++++++++++++++++++++
 model.h       |  4 ++++
 nodestack.cc  |  8 ++++----
 5 files changed, 47 insertions(+), 9 deletions(-)

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 7f430cca..321ebe9e 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -122,11 +122,7 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 }
 
 #if SUPPORT_MOD_ORDER_DUMP
-void CycleGraph::dumpGraphToFile(const char *filename) {
-	char buffer[200];
-  sprintf(buffer, "%s.dot",filename);
-  FILE *file=fopen(buffer, "w");
-  fprintf(file, "digraph %s {\n",filename);
+void CycleGraph::dumpNodes(FILE *file) {
   for(unsigned int i=0;i<nodeList.size();i++) {
 		CycleNode *cn=nodeList[i];
 		std::vector<CycleNode *> * edges=cn->getEdges();
@@ -141,6 +137,14 @@ void CycleGraph::dumpGraphToFile(const char *filename) {
       fprintf(file, "N%u -> N%u;\n", action->get_seq_number(), dstaction->get_seq_number());
 	  }
 	}
+}
+
+void CycleGraph::dumpGraphToFile(const char *filename) {
+	char buffer[200];
+  sprintf(buffer, "%s.dot",filename);
+  FILE *file=fopen(buffer, "w");
+  fprintf(file, "digraph %s {\n",filename);
+	dumpNodes(file);
   fprintf(file,"}\n");
   fclose(file);	
 }
diff --git a/cyclegraph.h b/cyclegraph.h
index c8e8956b..42866a3b 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -29,6 +29,7 @@ class CycleGraph {
 	void commitChanges();
 	void rollbackChanges();
 #if SUPPORT_MOD_ORDER_DUMP
+	void dumpNodes(FILE *file);
 	void dumpGraphToFile(const char * filename);
 #endif
 
diff --git a/model.cc b/model.cc
index 0665ff49..1598fb9a 100644
--- a/model.cc
+++ b/model.cc
@@ -1598,6 +1598,33 @@ static void print_list(action_list_t *list)
 	printf("---------------------------------------------------------------------\n");
 }
 
+#if SUPPORT_MOD_ORDER_DUMP
+void ModelChecker::dumpGraph(char *filename) {
+	char buffer[200];
+  sprintf(buffer, "%s.dot",filename);
+  FILE *file=fopen(buffer, "w");
+  fprintf(file, "digraph %s {\n",filename);
+	mo_graph->dumpNodes(file);
+	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=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
+			fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+		}
+		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());
+		}
+		
+		thread_array[action->get_tid()]=action;
+	}
+  fprintf(file,"}\n");
+	model_free(thread_array);
+  fclose(file);	
+}
+#endif
+
 void ModelChecker::print_summary()
 {
 	printf("\n");
@@ -1610,6 +1637,8 @@ void ModelChecker::print_summary()
 	char buffername[100];
 	sprintf(buffername, "exec%04u", num_executions);
 	mo_graph->dumpGraphToFile(buffername);
+	sprintf(buffername, "graph%04u", num_executions);
+  dumpGraph(buffername);
 #endif
 
 	if (!isfinalfeasible())
diff --git a/model.h b/model.h
index 073b96b9..6f082c66 100644
--- a/model.h
+++ b/model.h
@@ -18,6 +18,7 @@
 #include "clockvector.h"
 #include "hashtable.h"
 #include "workqueue.h"
+#include "config.h"
 
 /* Forward declaration */
 class NodeStack;
@@ -66,6 +67,9 @@ public:
 
 	/** Prints an execution summary with trace information. */
 	void print_summary();
+#if SUPPORT_MOD_ORDER_DUMP
+	void dumpGraph(char *filename);
+#endif
 
 	void add_thread(Thread *t);
 	void remove_thread(Thread *t);
diff --git a/nodestack.cc b/nodestack.cc
index 533f75a7..28bba4d0 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -178,7 +178,7 @@ bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
  * @return true if the future_values set is empty.
  */
 bool Node::future_value_empty() {
-	return ((future_index + 1) >= future_values.size());
+	return ((future_index + 1) >= ((int)future_values.size()));
 }
 
 /**
@@ -288,12 +288,12 @@ void Node::add_read_from(const ModelAction *act)
  * @return The first element in future_values
  */
 uint64_t Node::get_future_value() {
-	ASSERT(future_index<future_values.size());
+	ASSERT(future_index<((int)future_values.size()));
 	return future_values[future_index].value;
 }
 
 modelclock_t Node::get_future_value_expiration() {
-	ASSERT(future_index<future_values.size());
+	ASSERT(future_index<((int)future_values.size()));
 	return future_values[future_index].expiration;
 }
 
@@ -339,7 +339,7 @@ bool Node::increment_read_from() {
 bool Node::increment_future_value() {
 	DBG();
 	promises.clear();
-	if ((future_index+1) < future_values.size()) {
+	if ((future_index+1) < ((int)future_values.size())) {
 		future_index++;
 		return true;
 	}
-- 
2.34.1