Add dead-lock detection to MC

[simgrid.git] / src / mc / mc_dpor.c

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index eb4dd9b..9c84b30 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -44,8 +44,6 @@ void MC_dpor_init()
     xbt_setset_set_insert(initial_state->interleave, trans);
   MC_UNSET_RAW_MEM;
 
-  trans->refcount++;
-
   /* Update Statistics */
   mc_stats->state_size += xbt_setset_set_size(initial_state->enabled_transitions);
 }
@@ -96,7 +94,6 @@ void MC_dpor(void)
         xbt_setset_set_remove(mc_current_state->interleave, trans);
         /* Add the transition in the done set of the current state */
         xbt_setset_set_insert(mc_current_state->done, trans);
-        trans->refcount++;
       }
       
       next_state = MC_state_new();
@@ -152,7 +149,20 @@ void MC_dpor(void)
     /* The interleave set is empty or the maximum depth is reached, let's back-track */
     }else{
       DEBUG0("There are no more transitions to interleave.");
-      
+
+  
+      /* Check for deadlocks */
+      xbt_setset_substract(mc_current_state->transitions, mc_current_state->done);
+      if(xbt_setset_set_size(mc_current_state->transitions) > 0){
+        INFO0("**************************");
+        INFO0("*** DEAD-LOCK DETECTED ***");
+        INFO0("**************************");
+        INFO0("Counter-example execution trace:");
+        MC_dump_stack(mc_stack);
+        MC_print_statistics(mc_stats);
+        xbt_abort();
+      }
+              
       mc_transition_t q = NULL;
       xbt_fifo_item_t item = NULL;
       mc_state_t state = NULL;