X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/464f89a9c5bd6322317dd01fc1edfec57cf48db7..45cf10e0c743664310be804ca1d8d25edd3a18a7:/src/mc/mc_dpor.c

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index f039affaf9..58d9728dde 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -1,4 +1,5 @@
-/* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved.           */
+/* Copyright (c) 2008-2013. The SimGrid Team.
+ * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -8,69 +9,189 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
                                 "Logging specific to MC DPOR exploration");
 
+/********** Global variables **********/
+
 xbt_dynar_t visited_states;
+xbt_dict_t first_enabled_state;
 
-static int is_visited_state(void);
+/********** Static functions ***********/
 
-static int is_visited_state(){
+static void visited_state_free(mc_visited_state_t state){
+  if(state){
+    MC_free_snapshot(state->system_state);
+    xbt_free(state);
+  }
+}
+
+static void visited_state_free_voidp(void *s){
+  visited_state_free((mc_visited_state_t) * (void **) s);
+}
+
+static mc_visited_state_t visited_state_new(){
 
-  if(_surf_mc_visited == 0)
-    return 0;
+  mc_visited_state_t new_state = NULL;
+  new_state = xbt_new0(s_mc_visited_state_t, 1);
+  new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+  new_state->nb_processes = xbt_swag_size(simix_global->process_list);
+  new_state->system_state = MC_take_snapshot();
+  new_state->num = mc_stats->expanded_states;
+  new_state->other_num = -1;
+
+  return new_state;
+  
+}
+
+static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
 
-  mc_snapshot_t new_state = NULL;
-  new_state = MC_take_snapshot();  
+  int cursor = 0, previous_cursor, next_cursor;
+  mc_visited_state_t state_test;
+  int start = 0;
+  int end = xbt_dynar_length(all_states) - 1;
+  
+  while(start <= end){
+    cursor = (start + end) / 2;
+    state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
+    if(state_test->nb_processes < state->nb_processes){
+      start = cursor + 1;
+    }else if(state_test->nb_processes > state->nb_processes){
+      end = cursor - 1;
+    }else{
+      if(state_test->heap_bytes_used < state->heap_bytes_used){
+        start = cursor +1;
+      }else if(state_test->heap_bytes_used > state->heap_bytes_used){
+        end = cursor - 1;
+      }else{
+        *min = *max = cursor;
+        previous_cursor = cursor - 1;
+        while(previous_cursor >= 0){
+          state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
+          if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
+            break;
+          *min = previous_cursor;
+          previous_cursor--;
+        }
+        next_cursor = cursor + 1;
+        while(next_cursor < xbt_dynar_length(all_states)){
+          state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
+          if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
+            break;
+          *max = next_cursor;
+          next_cursor++;
+        }
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
+        return -1;
+      }
+     }
+  }
 
-  MC_UNSET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
+
+  return cursor;
+}
+
+static int is_visited_state(){
+
+  if(_sg_mc_visited == 0)
+    return -1;
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+
+  mc_visited_state_t new_state = visited_state_new();
   
   if(xbt_dynar_is_empty(visited_states)){
 
-    MC_SET_RAW_MEM;
     xbt_dynar_push(visited_states, &new_state); 
-    MC_UNSET_RAW_MEM;
 
-    if(raw_mem_set)
-      MC_SET_RAW_MEM;
- 
-    return 0;
+    if(!raw_mem_set)
+      MC_UNSET_RAW_MEM;
+
+    return -1;
 
   }else{
 
-    MC_SET_RAW_MEM;
-    
-    unsigned int cursor = 0;
-    mc_snapshot_t state_test = NULL;
-     
-    xbt_dynar_foreach(visited_states, cursor, state_test){
-      if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug))
-        XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
-      if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
-        if(raw_mem_set)
-          MC_SET_RAW_MEM;
+    int min = -1, max = -1, index;
+    //int res;
+    mc_visited_state_t state_test;
+    int cursor;
+
+    index = get_search_interval(visited_states, new_state, &min, &max);
+
+    if(min != -1 && max != -1){
+      /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
+      if(res != -1){
+        state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
+        if(state_test->other_num == -1)
+          new_state->other_num = state_test->num;
+        else
+          new_state->other_num = state_test->other_num;
+        if(dot_output == NULL)
+          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
         else
+          XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
+        xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
+        xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
+        if(!raw_mem_set)
           MC_UNSET_RAW_MEM;
-        
-        return 1;
-      }   
+        return new_state->other_num;
+        }*/
+      cursor = min;
+      while(cursor <= max){
+        state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
+        if(snapshot_compare(state_test, new_state) == 0){
+          if(state_test->other_num == -1)
+            new_state->other_num = state_test->num;
+          else
+            new_state->other_num = state_test->other_num;
+          if(dot_output == NULL)
+            XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
+          else
+            XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
+          xbt_dynar_remove_at(visited_states, cursor, NULL);
+          xbt_dynar_insert_at(visited_states, cursor, &new_state);
+          if(!raw_mem_set)
+            MC_UNSET_RAW_MEM;
+          return new_state->other_num;
+        }
+        cursor++;
+      }
+      xbt_dynar_insert_at(visited_states, min, &new_state);
+    }else{
+      state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
+      if(state_test->nb_processes < new_state->nb_processes){
+        xbt_dynar_insert_at(visited_states, index+1, &new_state);
+      }else{
+        if(state_test->heap_bytes_used < new_state->heap_bytes_used)
+          xbt_dynar_insert_at(visited_states, index + 1, &new_state);
+        else
+          xbt_dynar_insert_at(visited_states, index, &new_state);
+      }
     }
 
-    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);
+    if(xbt_dynar_length(visited_states) > _sg_mc_visited){
+      int min2 = mc_stats->expanded_states;
+      unsigned int cursor2 = 0;
+      unsigned int index2 = 0;
+      xbt_dynar_foreach(visited_states, cursor2, state_test){
+        if(state_test->num < min2){
+          index2 = cursor2;
+          min2 = state_test->num;
+        }
+      }
+      xbt_dynar_remove_at(visited_states, index2, NULL);
     }
 
-    xbt_dynar_push(visited_states, &new_state); 
-    
-    MC_UNSET_RAW_MEM;
-
-    if(raw_mem_set)
-      MC_SET_RAW_MEM;
+    if(!raw_mem_set)
+      MC_UNSET_RAW_MEM;
     
-    return 0;
+    return -1;
     
   }
 }
@@ -90,7 +211,10 @@ void MC_dpor_init()
   MC_SET_RAW_MEM;
 
   initial_state = MC_state_new();
-  visited_states = xbt_dynar_new(sizeof(mc_snapshot_t), NULL);
+  if(_sg_mc_visited > 0)
+    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;
 
@@ -106,11 +230,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);
+      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)
@@ -128,14 +267,15 @@ void MC_dpor_init()
 void MC_dpor(void)
 {
 
-  char *req_str;
+  char *req_str = NULL;
   int value;
   smx_simcall_t req = NULL, prev_req = NULL;
   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;
-  int proc_eval[simix_process_maxpid];
+  int pos;
+  int visited_state = -1;
+  int enabled = 0;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -144,17 +284,17 @@ void MC_dpor(void)
       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
-              xbt_fifo_size(mc_stack_safety), state,
-              MC_state_interleave_size(state));
-
+    XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
+              xbt_fifo_size(mc_stack_safety), state, state->num,
+              MC_state_interleave_size(state), user_max_depth_reached);
+      
     /* Update statistics */
     mc_stats->visited_states++;
 
     /* 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) < _surf_mc_max_depth &&
-        (req = MC_state_get_request(state, &value))) {
+    if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
+        (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 
       /* Debug information */
       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
@@ -162,10 +302,21 @@ void MC_dpor(void)
         XBT_DEBUG("Execute: %s", req_str);
         xbt_free(req_str);
       }
+      
+      MC_SET_RAW_MEM;
+      if(dot_output != NULL)
+        req_str = MC_request_get_dot_output(req, value);
+      MC_UNSET_RAW_MEM;
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
+      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;
+
       /* Answer the request */
       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 
@@ -177,48 +328,98 @@ void MC_dpor(void)
 
       next_state = MC_state_new();
 
-      if(!is_visited_state()){
+      if((visited_state = is_visited_state()) == -1){
      
         /* Get an enabled process and insert it in the interleave set of the next state */
         xbt_swag_foreach(process, simix_global->process_list){
           if(MC_process_is_enabled(process)){
             MC_state_interleave_process(next_state, process);
+            if(mc_reduce_kind != e_mc_reduce_none)
+              break;
           }
         }
 
-        if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
+        if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
           next_state->system_state = MC_take_snapshot();
         }
 
+        if(dot_output != NULL)
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
+
       }else{
 
-        XBT_DEBUG("State already visited !");
-        
+        if(dot_output != NULL)
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
+
       }
 
       xbt_fifo_unshift(mc_stack_safety, next_state);
-      MC_UNSET_RAW_MEM;
 
-      /* FIXME: Update Statistics
-         mc_stats->state_size +=
-         xbt_setset_set_size(next_state->enabled_transitions);*/
+      /* 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);
+        }
+      }
+      
+      if(dot_output != NULL)
+        xbt_free(req_str);
+
+      MC_UNSET_RAW_MEM;
 
       /* Let's loop again */
 
       /* 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)  
-        XBT_WARN("/!\\ Max depth reached ! /!\\ ");
-      else
-        XBT_DEBUG("There are no more processes to interleave.");
+      if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){  
+
+        if(user_max_depth_reached && visited_state == -1)
+          XBT_DEBUG("User max depth reached !");
+        else if(visited_state == -1)
+          XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+
+        visited_state = -1;
+
+        /* Interleave enabled processes 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);
+            enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
+            xbt_free(key);
+            mc_state_t state_test = NULL;
+            xbt_fifo_item_t item = NULL;
+            int cursor = xbt_fifo_size(mc_stack_safety);
+            xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
+              if(cursor-- == enabled){ 
+                if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){ 
+                  XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
+                  MC_state_interleave_process(state_test, process);
+                  break;
+                }
+              }
+            } 
+          }
+        }
+
+      }else{
+
+        XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
+
+      }
 
       /* Trash the current state, no longer needed */
       MC_SET_RAW_MEM;
       xbt_fifo_shift(mc_stack_safety);
       MC_state_delete(state);
-      MC_UNSET_RAW_MEM;
-
+      XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
+      MC_UNSET_RAW_MEM;        
+      
       /* Check for deadlocks */
       if(MC_deadlock_check()){
         MC_show_deadlock(NULL);
@@ -234,11 +435,7 @@ 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){
+        if(mc_reduce_kind != e_mc_reduce_none){
           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))){
@@ -246,38 +443,41 @@ void MC_dpor(void)
                 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_DEBUG("%s (state=%d)", req_str, prev_state->num);
                 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_DEBUG("%s (state=%d)", req_str, state->num);
                 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){
+            }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 
+              XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
               break;
 
-            }else if(proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] == 0){
+            }else{
 
-              MC_state_remove_interleave_process(prev_state, MC_state_get_executed_request(prev_state, &value)->issuer);
+              XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", req->call, req->issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid, prev_state->num);
 
             }
-
-            proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] = 1;
-
           }
         }
-
-        if (MC_state_interleave_size(state)) {
+             
+        if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
-          if(_surf_mc_checkpoint){
+          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
+          if(_sg_mc_checkpoint){
             if(state->system_state != NULL){
               MC_restore_snapshot(state->system_state);
               xbt_fifo_unshift(mc_stack_safety, state);
-              XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
               MC_UNSET_RAW_MEM;
             }else{
               pos = xbt_fifo_size(mc_stack_safety);
@@ -293,18 +493,18 @@ void MC_dpor(void)
               }
               MC_restore_snapshot(restore_state->system_state);
               xbt_fifo_unshift(mc_stack_safety, state);
-              XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
               MC_UNSET_RAW_MEM;
               MC_replay(mc_stack_safety, pos);
             }
           }else{
             xbt_fifo_unshift(mc_stack_safety, state);
-            XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
             MC_UNSET_RAW_MEM;
             MC_replay(mc_stack_safety, -1);
           }
+          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety));
           break;
         } else {
+          XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); 
           MC_state_delete(state);
         }
       }