X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/21756925d57a6fb6de1dfea9c3e1842d0f101d2c..554145f555b981fd5760349c5910f169055babec:/src/mc/mc_dpor.c

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 53bd9cfb5e..c67d36de1f 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -15,7 +15,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
 void MC_dpor_init()
 {
   mc_state_t initial_state = NULL;
-  mc_transition_t trans = NULL;
+  mc_transition_t trans, trans_tmp = NULL;
   xbt_setset_cursor_t cursor = NULL;
   
   /* Create the initial state and push it into the exploration stack */
@@ -30,18 +30,18 @@ void MC_dpor_init()
   MC_schedule_enabled_processes();
 
   MC_SET_RAW_MEM;
-  xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions);
-  xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){
-    if(trans->type == mc_wait
-       && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
-      xbt_setset_set_remove(initial_state->enabled_transitions, trans);
-    }
-  }
+  MC_trans_compute_enabled(initial_state->enabled_transitions,
+                           initial_state->transitions);
 
   /* Fill the interleave set of the initial state with an enabled process */
   trans = xbt_setset_set_choose(initial_state->enabled_transitions);  
-  if(trans)
-    xbt_setset_set_insert(initial_state->interleave, trans);
+  if(trans){
+    DEBUG1("Choosing process %s for next interleave", trans->process->name);
+    xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans_tmp){
+      if(trans_tmp->process == trans->process)
+        xbt_setset_set_insert(initial_state->interleave, trans_tmp);    
+    }
+  }
   MC_UNSET_RAW_MEM;
 
   /* Update Statistics */
@@ -55,7 +55,7 @@ void MC_dpor_init()
  */
 void MC_dpor(void)
 {
-  mc_transition_t trans = NULL;  
+  mc_transition_t trans, trans_tmp = NULL;  
   mc_state_t next_state = NULL;
   xbt_setset_cursor_t cursor = NULL;
   
@@ -76,10 +76,6 @@ void MC_dpor(void)
       DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack),
         mc_current_state, xbt_setset_set_size(mc_current_state->interleave),
         xbt_setset_set_size(mc_current_state->enabled_transitions));
-
-      xbt_setset_foreach(mc_current_state->enabled_transitions, cursor, trans){
-        DEBUG1("\t %s", trans->name);
-      }
       
       /* Update statistics */
       mc_stats->visited_states++;
@@ -89,12 +85,10 @@ void MC_dpor(void)
          state, and create the data structures for the new expanded state in the
          exploration stack. */
       MC_SET_RAW_MEM;
-      trans = xbt_setset_set_choose(mc_current_state->interleave);
-      if(!trans->type == mc_random){
-        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 = xbt_setset_set_extract(mc_current_state->interleave);
+
+      /* Add the transition in the done set of the current state */
+      xbt_setset_set_insert(mc_current_state->done, trans);
       
       next_state = MC_state_new();
       xbt_fifo_unshift(mc_stack, next_state);
@@ -110,35 +104,27 @@ void MC_dpor(void)
       SIMIX_process_schedule(trans->process);
       MC_execute_surf_actions();        /* Do surf's related black magic */
       MC_schedule_enabled_processes();
-
-      if(trans->type == mc_random && trans->current_value < trans->max ){
-        trans->current_value++;
-      }else{
-        trans->current_value = trans->min;
-        xbt_setset_set_remove(mc_current_state->interleave, trans);
-        xbt_setset_set_insert(mc_current_state->done, trans);
-      }
       
-      /* Calculate the enabled transitions set of the next state:
-          -add the transition sets of the current state and the next state 
-          -remove the executed transition from that set
-          -remove all the transitions that are disabled (mc_wait only)
-          -use the resulting set as the enabled transitions of the next state */
+      /* Calculate the enabled transitions set of the next state */
       MC_SET_RAW_MEM;
-      xbt_setset_add(next_state->transitions, mc_current_state->transitions);
-      xbt_setset_set_remove(next_state->transitions, trans);
-      xbt_setset_add(next_state->enabled_transitions, next_state->transitions);
-      xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){
-        if(trans->type == mc_wait
-           && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
-          xbt_setset_set_remove(next_state->enabled_transitions, trans);
+
+      xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp){
+        if(trans_tmp->process != trans->process){
+          xbt_setset_set_insert(next_state->transitions, trans_tmp);
         }
       }
-
+      
+      MC_trans_compute_enabled(next_state->enabled_transitions, next_state->transitions);
+      
       /* Choose one transition to interleave from the enabled transition set */      
       trans = xbt_setset_set_choose(next_state->enabled_transitions);
-      if(trans)
-        xbt_setset_set_insert(next_state->interleave, trans);
+      if(trans){
+        DEBUG1("Choosing process %s for next interleave", trans->process->name);
+        xbt_setset_foreach(next_state->enabled_transitions, cursor, trans_tmp){
+          if(trans_tmp->process == trans->process)
+            xbt_setset_set_insert(next_state->interleave, trans_tmp);    
+        }
+      }
       MC_UNSET_RAW_MEM;
 
       /* Update Statistics */
@@ -149,7 +135,26 @@ 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("Locked transitions:");
+        xbt_setset_foreach(mc_current_state->transitions, cursor, trans){
+          INFO1("%s", trans->name);
+        }
+
+        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;
@@ -171,11 +176,17 @@ void MC_dpor(void)
         q = mc_current_state->executed_transition;
         xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
           if(MC_transition_depend(q, state->executed_transition)){
-            DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q);
+            DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q); 
             xbt_setset_foreach(state->enabled_transitions, cursor, trans){
               if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){
                 DEBUG2("Unexplored interleaving found at state %p (%p)", state, trans);
-                xbt_setset_set_insert(state->interleave, trans);
+
+                xbt_setset_foreach(state->enabled_transitions, cursor, trans){
+                  if(trans->process == q->process)
+                    xbt_setset_set_insert(state->interleave, trans);    
+                }
+                /* FIXME: hack to make it work*/
+                trans = q;
                 break;
               }
             }