model-checker : interleave all enabled processes for each state and apply DPOR only...

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

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 1fe4044..f039aff 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -14,7 +14,7 @@ static int is_visited_state(void);
 
 static int is_visited_state(){
 
-  if(_surf_mc_stateful == 0)
+  if(_surf_mc_visited == 0)
     return 0;
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -57,7 +57,7 @@ static int is_visited_state(){
       }   
     }
 
-    if(xbt_dynar_length(visited_states) == _surf_mc_stateful){
+    if(xbt_dynar_length(visited_states) == _surf_mc_visited){
       mc_snapshot_t state_to_remove = NULL;
       xbt_dynar_shift(visited_states, &state_to_remove);
       MC_free_snapshot(state_to_remove);
@@ -101,18 +101,11 @@ void MC_dpor_init()
   MC_wait_for_requests();
 
   MC_SET_RAW_MEM;
-
-  xbt_swag_foreach(process, simix_global->process_list){
-    if(MC_process_is_enabled(process)){
-      XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
-    }
-  }
-  
+ 
   /* Get an enabled process and insert it in the interleave set of the initial state */
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
       MC_state_interleave_process(initial_state, process);
-      break;
     }
   }
 
@@ -125,10 +118,6 @@ void MC_dpor_init()
   else
     MC_UNSET_RAW_MEM;
   
-    
-  /* FIXME: Update Statistics 
-     mc_stats->state_size +=
-     xbt_setset_set_size(initial_state->enabled_transitions); */
 }
 
 
@@ -145,7 +134,8 @@ void MC_dpor(void)
   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
-  int pos;
+  int pos, i;
+  int proc_eval[simix_process_maxpid];
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -193,8 +183,6 @@ void MC_dpor(void)
         xbt_swag_foreach(process, simix_global->process_list){
           if(MC_process_is_enabled(process)){
             MC_state_interleave_process(next_state, process);
-            XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
-            //break;
           }
         }
 
@@ -220,20 +208,11 @@ void MC_dpor(void)
       /* The interleave set is empty or the maximum depth is reached, let's back-track */
     } else {
 
-      if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth){
-        
+      if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth)  
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
-        if(req != NULL){
-          XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
-          XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
-        }
-
-      }else{
-
+      else
         XBT_DEBUG("There are no more processes to interleave.");
 
-      }
-
       /* Trash the current state, no longer needed */
       MC_SET_RAW_MEM;
       xbt_fifo_shift(mc_stack_safety);
@@ -255,6 +234,10 @@ void MC_dpor(void)
          state that executed that previous request. */
       
       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
+
+        for(i=0; i<simix_process_maxpid; i++)
+          proc_eval[i] = 0;
+
         if(MC_state_interleave_size(state) == 0){
           req = MC_state_get_internal_request(state);
           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
@@ -271,22 +254,23 @@ void MC_dpor(void)
                 xbt_free(req_str);              
               }
 
-              /*if(!MC_state_process_is_done(prev_state, req->issuer))
-                MC_state_interleave_process(prev_state, req->issuer);
-              else
-              XBT_DEBUG("Process %p is in done set", req->issuer);*/
-              
+              break;
+
+            }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
 
               break;
 
-            }else{
-              
-              //XBT_DEBUG("Independant transitions : (%lu) %d - (%lu) %d", req->issuer->pid, req->call, MC_state_get_internal_request(prev_state)->issuer->pid, MC_state_get_internal_request(prev_state)->call);
-              MC_state_remove_interleave_process(prev_state, req->issuer);
+            }else if(proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] == 0){
+
+              MC_state_remove_interleave_process(prev_state, MC_state_get_executed_request(prev_state, &value)->issuer);
 
             }
+
+            proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] = 1;
+
           }
         }
+
         if (MC_state_interleave_size(state)) {
           /* We found a back-tracking point, let's loop */
           if(_surf_mc_checkpoint){