start support for drawing execution diagrams

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 9dc1d37c71bb6ac93844d057efd7928818d7e053..1598fb9a276343ba3daf59f3beedad6d452115e7 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -25,6 +25,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        num_executions(0),
        num_feasible_executions(0),
        diverge(NULL),
+       earliest_diverge(NULL),
        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
@@ -180,8 +181,13 @@ bool ModelChecker::next_execution()
        DBG();
 
        num_executions++;
-       if (isfinalfeasible())
+       if (isfinalfeasible()) {
+               printf("Earliest divergence point since last feasible execution:\n");
+               earliest_diverge->print();
+
+               earliest_diverge = NULL;
                num_feasible_executions++;
+       }
 
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
@@ -189,6 +195,9 @@ bool ModelChecker::next_execution()
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
+       if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+               earliest_diverge=diverge;
+
        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
                diverge->print();
@@ -658,7 +667,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        bool updated = false;
 
                        if (act->is_read()) {
-                               if (r_modification_order(act, act->get_reads_from()))
+                               const ModelAction *rf = act->get_reads_from();
+                               if (rf != NULL && r_modification_order(act, rf))
                                        updated = true;
                        }
                        if (act->is_write()) {
@@ -1588,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");
@@ -1600,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())