Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/simgrid/simgrid

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index de9b988..a97440a 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -9,10 +9,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
                                 "Logging specific to MC DPOR exploration");
 
 xbt_dynar_t visited_states;
-
-static int is_visited_state(void);
-static void visited_state_free(mc_visited_state_t state);
-static void visited_state_free_voidp(void *s);
+xbt_dict_t first_enabled_state;
 
 static void visited_state_free(mc_visited_state_t state){
   if(state){
@@ -196,6 +193,8 @@ void MC_dpor_init()
   initial_state = MC_state_new();
   visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 
+  first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
+
   MC_UNSET_RAW_MEM;
 
   XBT_DEBUG("**************************************************");
@@ -210,12 +209,26 @@ void MC_dpor_init()
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
       MC_state_interleave_process(initial_state, process);
-      XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
+      if(mc_reduce_kind != e_mc_reduce_none)
+        break;
     }
   }
 
   xbt_fifo_unshift(mc_stack_safety, initial_state);
 
+  /* To ensure the soundness of DPOR, we have to keep a list of 
+     processes which are still enabled at each step of the exploration. 
+     If max depth is reached, we interleave them in the state in which they have 
+     been enabled for the first time. */
+  xbt_swag_foreach(process, simix_global->process_list){
+    if(MC_process_is_enabled(process)){
+      char *key = bprintf("%lu", process->pid);
+      char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
+      xbt_dict_set(first_enabled_state, key, data, NULL);
+      xbt_free(key);
+    }
+  }
+
   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)
@@ -240,8 +253,7 @@ 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, i, interleave_size;
-  int interleave_proc[simix_process_maxpid];
+  int pos;
   int visited_state;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
@@ -260,7 +272,7 @@ void MC_dpor(void)
 
     /* If there are processes to interleave and the maximum depth has not been reached
        then perform one step of the exploration algorithm */
-    if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
+    if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth &&
         (req = MC_state_get_request(state, &value))) {
 
       /* Debug information */
@@ -275,35 +287,11 @@ void MC_dpor(void)
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
-      if(MC_state_interleave_size(state)){
-        MC_SET_RAW_MEM;
-        req2 = MC_state_get_internal_request(state);
-        req3 = *req2;
-        for(i=0; i<simix_process_maxpid; i++)
-          interleave_proc[i] = 0;
-        i=0;
-        interleave_size = MC_state_interleave_size(state);
-        while(i < interleave_size){
-          i++;
-          prev_req = MC_state_get_request(state, &value2);
-          if(prev_req != NULL){
-            MC_state_set_executed_request(state, prev_req, value2);
-            prev_req = MC_state_get_internal_request(state);
-            if(MC_request_depend(&req3, prev_req)){
-              XBT_DEBUG("Simcall %d in process %lu dependant with simcall %d in process %lu", req3.call, req3.issuer->pid, prev_req->call, prev_req->issuer->pid);  
-              interleave_proc[prev_req->issuer->pid] = 1;
-            }else{
-              XBT_DEBUG("Simcall %d in process %lu independant with simcall %d in process %lu", req3.call, req3.issuer->pid, prev_req->call, prev_req->issuer->pid); 
-              MC_state_remove_interleave_process(state, prev_req->issuer);
-            }
-          }
-        }
-        xbt_swag_foreach(process, simix_global->process_list){
-          if(interleave_proc[process->pid] == 1)
-            MC_state_interleave_process(state, process);
-        }
-        MC_UNSET_RAW_MEM;
-      }
+      MC_SET_RAW_MEM;
+      char *key = bprintf("%lu", req->issuer->pid);
+      xbt_dict_remove(first_enabled_state, key); 
+      xbt_free(key);
+      MC_UNSET_RAW_MEM;
 
       MC_state_set_executed_request(state, req, value);
 
@@ -324,7 +312,8 @@ 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);
+            if(mc_reduce_kind != e_mc_reduce_none)
+              break;
           }
         }
 
@@ -343,6 +332,19 @@ void MC_dpor(void)
       }
 
       xbt_fifo_unshift(mc_stack_safety, next_state);
+
+      /* Insert in dict all enabled processes, if not included yet */
+      xbt_swag_foreach(process, simix_global->process_list){
+        if(MC_process_is_enabled(process)){
+          char *key = bprintf("%lu", process->pid);
+          if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+            char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
+            xbt_dict_set(first_enabled_state, key, data, NULL); 
+          }
+          xbt_free(key);
+        }
+      }
+
       MC_UNSET_RAW_MEM;
 
       xbt_free(req_str);
@@ -378,36 +380,64 @@ void MC_dpor(void)
          state that executed that previous request. */
       
       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
-        req = MC_state_get_internal_request(state);
-        xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
-          if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
-            if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
-              XBT_DEBUG("Dependent Transitions:");
-              prev_req = MC_state_get_executed_request(prev_state, &value);
-              req_str = MC_request_to_string(prev_req, value);
-              XBT_DEBUG("%s (state=%p)", req_str, prev_state);
-              xbt_free(req_str);
-              prev_req = MC_state_get_executed_request(state, &value);
-              req_str = MC_request_to_string(prev_req, value);
-              XBT_DEBUG("%s (state=%p)", req_str, state);
-              xbt_free(req_str);              
+        if(mc_reduce_kind != e_mc_reduce_none){
+          req = MC_state_get_internal_request(state);
+          /* If max_depth reached, check only for the last state if the request that has generated
+             it, depends on any other processes still enabled when max_depth reached */
+          if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth - 1){
+            req3 = *req;
+            xbt_swag_foreach(process, simix_global->process_list){
+              if(MC_process_is_enabled(process) && !MC_state_process_is_done(state, process)){
+                MC_state_interleave_process(state, process);
+                req2 = MC_state_get_request(state, &value2);
+                MC_state_set_executed_request(state, req2, value2);
+                req2 = MC_state_get_internal_request(state);
+                if(MC_request_depend(&req3, req2)){
+                  if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
+                    XBT_DEBUG("Dependent Transitions:");
+                    req_str = MC_request_to_string(&req3, value);
+                    XBT_DEBUG("%s (state=%p)", req_str, state);
+                    xbt_free(req_str);
+                    req_str = MC_request_to_string(req2, value);
+                    XBT_DEBUG("%s (state=%p)", req_str, state);
+                    xbt_free(req_str);              
+                  } 
+                  MC_state_interleave_process(state, process);
+                  break;
+                }
+              }
             }
+          }
+          xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
+            if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
+              if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
+                XBT_DEBUG("Dependent Transitions:");
+                prev_req = MC_state_get_executed_request(prev_state, &value);
+                req_str = MC_request_to_string(prev_req, value);
+                XBT_DEBUG("%s (state=%p)", req_str, prev_state);
+                xbt_free(req_str);
+                prev_req = MC_state_get_executed_request(state, &value);
+                req_str = MC_request_to_string(prev_req, value);
+                XBT_DEBUG("%s (state=%p)", req_str, state);
+                xbt_free(req_str);              
+              }
 
-            break;
-
-          }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
+              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);
 
-            XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
-            break;
+              break;
 
-          }else{
+            }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 
-            MC_state_remove_interleave_process(prev_state, req->issuer);
-            XBT_DEBUG("Simcall %d in process %lu independant with simcall %d process %lu", req->call, req->issuer->pid, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid);  
+              XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
+              break;
 
+            }
           }
         }
-       
+             
         if (MC_state_interleave_size(state)) {
           /* We found a back-tracking point, let's loop */
           if(_sg_mc_checkpoint){

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 2fabb77..562eb37 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -406,11 +406,12 @@ void MC_replay(xbt_fifo_t stack, int start)
 {
   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
 
-  int value, i = 1;
+  int value, i = 1, count = 1;
   char *req_str;
   smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item, start_item;
   mc_state_t state;
+  smx_process_t process = NULL;
 
   XBT_DEBUG("**** Begin Replay ****");
 
@@ -430,6 +431,19 @@ void MC_replay(xbt_fifo_t stack, int start)
     }
   }
 
+  MC_SET_RAW_MEM;
+  xbt_dict_reset(first_enabled_state);
+  xbt_swag_foreach(process, simix_global->process_list){
+    if(MC_process_is_enabled(process)){
+      char *key = bprintf("%lu", process->pid);
+      char *data = bprintf("%d", count);
+      xbt_dict_set(first_enabled_state, key, data, NULL);
+      xbt_free(key);
+    }
+  }
+  MC_UNSET_RAW_MEM;
+  
+
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (item = start_item;
        item != xbt_fifo_get_first_item(stack);
@@ -438,6 +452,12 @@ void MC_replay(xbt_fifo_t stack, int start)
     state = (mc_state_t) xbt_fifo_get_item_content(item);
     saved_req = MC_state_get_executed_request(state, &value);
    
+    MC_SET_RAW_MEM;
+    char *key = bprintf("%lu", saved_req->issuer->pid);
+    xbt_dict_remove(first_enabled_state, key); 
+    xbt_free(key);
+    MC_UNSET_RAW_MEM;
+   
     if(saved_req){
       /* because we got a copy of the executed request, we have to fetch the  
          real one, pointed by the request field of the issuer process */
@@ -450,14 +470,32 @@ void MC_replay(xbt_fifo_t stack, int start)
         xbt_free(req_str);
       }
     }
-         
+    
     SIMIX_simcall_pre(req, value);
     MC_wait_for_requests();
+
+    count++;
+
+    MC_SET_RAW_MEM;
+    /* Insert in dict all enabled processes */
+    xbt_swag_foreach(process, simix_global->process_list){
+      if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+        char *key = bprintf("%lu", process->pid);
+        if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+          char *data = bprintf("%d", count);
+          xbt_dict_set(first_enabled_state, key, data, NULL);
+        }
+        xbt_free(key);
+      }
+    }
+    MC_UNSET_RAW_MEM;
          
     /* Update statistics */
     mc_stats->visited_states++;
     mc_stats->executed_transitions++;
+
   }
+
   XBT_DEBUG("**** End Replay ****");
 
   if(raw_mem)

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 4839b41..55ac046 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -261,6 +261,7 @@ typedef enum {
 extern e_mc_reduce_t mc_reduce_kind;
 extern mc_global_t initial_state_safety;
 extern xbt_fifo_t mc_stack_safety;
+extern xbt_dict_t first_enabled_state;
 
 void MC_dpor_init(void);
 void MC_dpor(void);