start support for drawing execution diagrams

fix some signed/unsigned warnings

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 7f430cca6e5db962d22e2d8dd31c7873e122a9b8..321ebe9e2f242babe1adad4e233dd7fe51427e71 100644 (file)
--- 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 c8e8956be10529d194304061f8f90a6c48181181..42866a3b370ceb52ab85967c1cfe0c80f4aedf6f 100644 (file)
--- 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 0665ff49b9762c0e9317d5688d21437f614535ca..1598fb9a276343ba3daf59f3beedad6d452115e7 100644 (file)
--- 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 073b96b976cd4807c45c8c5e6ffef415941a0a81..6f082c66a71653f7240fcf8102223f60845e870f 100644 (file)
--- 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 533f75a7fab1bbc2c014d7fc883133b957bb94ed..28bba4d003176c405f0ed65720639052aa6c3929 100644 (file)
--- 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;
        }