X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ea6f6b66934613235f03c2a768cb84cba48db423..5dfafb1072cfc6a351514e002f730be75888d531:/src/mc/mc_dpor.c

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index ebda309ad6..40178859de 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -13,9 +13,154 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
 
 xbt_dynar_t visited_states;
 xbt_dict_t first_enabled_state;
+xbt_dynar_t initial_communications_pattern;
+xbt_dynar_t communications_pattern;
+int nb_comm_pattern;
 
 /********** Static functions ***********/
 
+static void comm_pattern_free(mc_comm_pattern_t p){
+  xbt_free(p->rdv);
+  xbt_free(p->data);
+  xbt_free(p);
+  p = NULL;
+}
+
+static void comm_pattern_free_voidp( void *p){
+  comm_pattern_free((mc_comm_pattern_t) * (void **)p);
+}
+
+static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern, unsigned int *idx, e_smx_comm_type_t type, unsigned long proc){
+  mc_comm_pattern_t current_comm;
+  while(*idx < xbt_dynar_length(pattern)){
+    current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
+    if(current_comm->type == type && type == SIMIX_COMM_SEND){
+      if(current_comm->src_proc == proc)
+        return current_comm;
+    }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
+      if(current_comm->dst_proc == proc)
+        return current_comm;
+    }
+    (*idx)++;
+  }
+  return NULL;
+}
+
+static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
+  if(strcmp(comm1->rdv, comm2->rdv) != 0)
+    return 1;
+  if(comm1->src_proc != comm2->src_proc)
+    return 1;
+  if(comm1->dst_proc != comm2->dst_proc)
+    return 1;
+  if(comm1->data_size != comm2->data_size)
+    return 1;
+  if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
+    return 1;
+  return 0;
+}
+
+static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
+  unsigned int cursor = 0, send_index = 0, recv_index = 0;
+  mc_comm_pattern_t comm1, comm2;
+  int comm_comparison = 0;
+  int current_process = 0;
+  while(current_process < simix_process_maxpid){
+    while(cursor < xbt_dynar_length(initial_pattern)){
+      comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(initial_pattern, cursor, mc_comm_pattern_t);
+      if(comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process){
+        comm2 = get_comm_pattern_from_idx(pattern, &send_index, comm1->type, current_process);
+        comm_comparison = compare_comm_pattern(comm1, comm2);
+        if(comm_comparison == 1){
+          initial_state_safety->send_deterministic = 0;
+          initial_state_safety->comm_deterministic = 0;
+          return;
+        }
+        send_index++;
+      }else if(comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process){
+        comm2 = get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, current_process);
+        comm_comparison = compare_comm_pattern(comm1, comm2);
+        if(comm_comparison == 1){
+          initial_state_safety->comm_deterministic = 0;
+        }
+        recv_index++;
+      }
+      cursor++;
+    }
+    cursor = 0;
+    send_index = 0;
+    recv_index = 0;
+    current_process++;
+  }
+  // XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic);
+}
+
+static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
+  mc_comm_pattern_t current_pattern;
+  unsigned int cursor = 0;
+  xbt_dynar_foreach(list, cursor, current_pattern){
+    if(current_pattern->comm == pattern->comm){
+      if(!current_pattern->completed){
+        current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
+        current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
+        current_pattern->data_size = pattern->comm->comm.src_buff_size;
+        current_pattern->data = xbt_malloc0(current_pattern->data_size);
+        current_pattern->matched_comm = pattern->num;
+        memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size);
+        current_pattern->completed = 1;
+        return current_pattern->num;
+      }
+    }
+  }
+  return -1;
+}
+
+void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
+  mc_comm_pattern_t pattern = NULL;
+  pattern = xbt_new0(s_mc_comm_pattern_t, 1);
+  pattern->num = ++nb_comm_pattern;
+  pattern->completed = 0;
+  if(call == 1){ // ISEND
+    pattern->comm = simcall_comm_isend__get__result(request);
+    pattern->type = SIMIX_COMM_SEND;
+    if(pattern->comm->comm.dst_proc != NULL){
+ 
+      pattern->matched_comm = complete_comm_pattern(list, pattern);
+      pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
+      pattern->completed = 1;
+    }
+    pattern->src_proc = pattern->comm->comm.src_proc->pid;
+    pattern->data_size = pattern->comm->comm.src_buff_size;
+    pattern->data=xbt_malloc0(pattern->data_size);
+    memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
+  }else{ // IRECV
+    pattern->comm = simcall_comm_irecv__get__result(request);
+    pattern->type = SIMIX_COMM_RECEIVE;
+    if(pattern->comm->comm.src_proc != NULL){
+      pattern->matched_comm = complete_comm_pattern(list, pattern);
+      pattern->src_proc = pattern->comm->comm.src_proc->pid;
+      pattern->completed = 1;
+      pattern->data_size = pattern->comm->comm.src_buff_size;
+      pattern->data=xbt_malloc0(pattern->data_size);
+      memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
+    }
+    pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
+  }
+  if(pattern->comm->comm.rdv != NULL)
+    pattern->rdv = strdup(pattern->comm->comm.rdv->name);
+  else
+    pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
+  xbt_dynar_push(list, &pattern);
+}
+
+static void print_communications_pattern(xbt_dynar_t comms_pattern){
+  unsigned int cursor = 0;
+  mc_comm_pattern_t current_comm;
+  xbt_dynar_foreach(comms_pattern, cursor, current_comm){
+    // fprintf(stderr, "%s (%d - comm %p, src : %lu, dst %lu, rdv name %s, data %p, matched with %d)\n", current_comm->type == SIMIX_COMM_SEND ? "iSend" : "iRecv", current_comm->num, current_comm->comm, current_comm->src_proc, current_comm->dst_proc, current_comm->rdv, current_comm->data, current_comm->matched_comm);
+  }
+}
+
 static void visited_state_free(mc_visited_state_t state){
   if(state){
     MC_free_snapshot(state->system_state);
@@ -27,6 +172,10 @@ static void visited_state_free_voidp(void *s){
   visited_state_free((mc_visited_state_t) * (void **) s);
 }
 
+/** \brief Save the current state
+ *
+ *  \return Snapshot of the current state.
+ */
 static mc_visited_state_t visited_state_new(){
 
   mc_visited_state_t new_state = NULL;
@@ -41,6 +190,22 @@ static mc_visited_state_t visited_state_new(){
   
 }
 
+/** \brief Find a suitable subrange of candidate duplicates for a given state
+ *
+ *  \param all_ pairs dynamic array of states with candidate duplicates of the current state;
+ *  \param pair current state;
+ *  \param min (output) index of the beginning of the the subrange
+ *  \param max (output) index of the enf of the subrange
+ *
+ *  Given a suitably ordered array of state, this function extracts a subrange
+ *  (with index *min <= i <= *max) with candidate duplicates of the given state.
+ *  This function uses only fast discriminating criterions and does not use the
+ *  full state comparison algorithms.
+ *
+ *  The states in all_pairs MUST be ordered using a (given) weak order
+ *  (based on nb_processes and heap_bytes_used).
+ *  The subrange is the subrange of "equivalence" of the given 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);
@@ -95,6 +260,10 @@ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state,
   return cursor;
 }
 
+/** \brief Take a snapshot the current state and process it.
+ *
+ *  \return number of the duplicate state or -1 (not visited)
+ */
 static int is_visited_state(){
 
   if(_sg_mc_visited == 0)
@@ -125,6 +294,8 @@ static int is_visited_state(){
     index = get_search_interval(visited_states, new_state, &min, &max);
 
     if(min != -1 && max != -1){
+
+      // Parallell implementation
       /*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);
@@ -142,10 +313,13 @@ static int is_visited_state(){
           MC_UNSET_RAW_MEM;
         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){
+          // The state has been visited:
+
           if(state_test->other_num == -1)
             new_state->other_num = state_test->num;
           else
@@ -154,16 +328,24 @@ static int is_visited_state(){
             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);
+
+          // Replace the old state with the new one (why?):
           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++;
       }
+
+      // The state has not been visited, add it to the list:
       xbt_dynar_insert_at(visited_states, min, &new_state);
+
     }else{
+
+      // The state has not been visited: insert the state in the dynamic array.
       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);
@@ -173,9 +355,13 @@ static int is_visited_state(){
         else
           xbt_dynar_insert_at(visited_states, index, &new_state);
       }
+
     }
 
+    // We have reached the maximum number of stored states;
     if(xbt_dynar_length(visited_states) > _sg_mc_visited){
+
+      // Find the (index of the) older state:
       int min2 = mc_stats->expanded_states;
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
@@ -185,6 +371,8 @@ static int is_visited_state(){
           min2 = state_test->num;
         }
       }
+
+      // and drop it:
       xbt_dynar_remove_at(visited_states, index2, NULL);
     }
 
@@ -210,12 +398,17 @@ void MC_dpor_init()
   /* Create the initial state and push it into the exploration stack */
   MC_SET_RAW_MEM;
 
-  initial_state = MC_state_new();
   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);
 
+  initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+  communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+  nb_comm_pattern = 0;
+
+  initial_state = MC_state_new();
+
   MC_UNSET_RAW_MEM;
 
   XBT_DEBUG("**************************************************");
@@ -263,9 +456,8 @@ void MC_dpor_init()
 }
 
 
-/**
- *   \brief Perform the model-checking operation using a depth-first search exploration
- *         with Dynamic Partial Order Reductions
+/** \brief Model-check the application using a DFS exploration
+ *         with DPOR (Dynamic Partial Order Reductions)
  */
 void MC_dpor(void)
 {
@@ -280,6 +472,8 @@ void MC_dpor(void)
   int pos;
   int visited_state = -1;
   int enabled = 0;
+  int comm_pattern = 0;
+  int interleave_size = 0;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -292,6 +486,8 @@ void MC_dpor(void)
               xbt_fifo_size(mc_stack_safety), state, state->num,
               MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
       
+    interleave_size = MC_state_interleave_size(state);
+
     /* Update statistics */
     mc_stats->visited_states++;
 
@@ -321,9 +517,25 @@ void MC_dpor(void)
       xbt_free(key);
       MC_UNSET_RAW_MEM;
 
+      if(req->call == SIMCALL_COMM_ISEND)
+        comm_pattern = 1;
+      else if(req->call == SIMCALL_COMM_IRECV)
+        comm_pattern = 2;
+
       /* Answer the request */
       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 
+      MC_SET_RAW_MEM;
+      if(comm_pattern != 0){
+        if(!initial_state_safety->initial_communications_pattern_done)
+          get_comm_pattern(initial_communications_pattern, req, comm_pattern);
+        else
+          get_comm_pattern(communications_pattern, req, comm_pattern);
+      }
+      MC_UNSET_RAW_MEM;
+
+      comm_pattern = 0;
+
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
 
@@ -415,6 +627,20 @@ void MC_dpor(void)
 
       }
 
+      MC_SET_RAW_MEM;
+      if(0) {
+      if(!initial_state_safety->initial_communications_pattern_done){
+        print_communications_pattern(initial_communications_pattern);
+      }else{
+        if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
+          print_communications_pattern(communications_pattern);
+          deterministic_pattern(initial_communications_pattern, communications_pattern);
+        }
+      }
+      initial_state_safety->initial_communications_pattern_done = 1;
+      }
+      MC_UNSET_RAW_MEM;
+
       /* Trash the current state, no longer needed */
       MC_SET_RAW_MEM;
       xbt_fifo_shift(mc_stack_safety);
@@ -506,6 +732,12 @@ void MC_dpor(void)
           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
           break;
         } else {
+          req = MC_state_get_internal_request(state);
+          if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
+            // fprintf(stderr, "Remove state with isend or irecv\n");
+            if(!xbt_dynar_is_empty(communications_pattern))
+              xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
+          }
           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); 
           MC_state_delete(state);
         }