X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/8fc11b8e2c3f486babc8be5494ddd53ffcc659f4..7ef55d47978f2f2ef20bd27c85881faa99147034:/src/mc/mc_dpor.c

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index a3e2949111..7aaa065a07 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -92,7 +92,6 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte
     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){
@@ -102,7 +101,9 @@ static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
     if(current_pattern->comm == pattern->comm){
       if(!current_pattern->completed){
         current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
+        current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
         current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
+        current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
         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;
@@ -123,13 +124,14 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
   if(call == 1){ // ISEND
     pattern->comm = simcall_comm_isend__get__result(request);
     pattern->type = SIMIX_COMM_SEND;
-    if(pattern->comm->comm.dst_proc != NULL){
- 
+    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->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
     }
     pattern->src_proc = pattern->comm->comm.src_proc->pid;
+    pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
     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);
@@ -139,12 +141,14 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
     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->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
       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;
+    pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
   }
   if(pattern->comm->comm.rdv != NULL)
     pattern->rdv = strdup(pattern->comm->comm.rdv->name);
@@ -157,7 +161,10 @@ 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);
+    if(current_comm->type == SIMIX_COMM_SEND)
+      XBT_INFO("[(%lu) %s -> %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_host, "iSend");
+    else
+      XBT_INFO("[(%lu) %s <- %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_host, "iRecv");
   }
 }
 
@@ -172,6 +179,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;
@@ -186,6 +197,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);
@@ -240,6 +267,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)
@@ -270,6 +301,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);
@@ -287,10 +320,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
@@ -299,16 +335,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);
@@ -318,9 +362,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;
@@ -330,6 +378,8 @@ static int is_visited_state(){
           min2 = state_test->num;
         }
       }
+
+      // and drop it:
       xbt_dynar_remove_at(visited_states, index2, NULL);
     }
 
@@ -413,9 +463,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)
 {
@@ -475,7 +524,7 @@ void MC_dpor(void)
       xbt_free(key);
       MC_UNSET_RAW_MEM;
       
-      if(_sg_mc_comms_determinism){
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
         if(req->call == SIMCALL_COMM_ISEND)
           comm_pattern = 1;
         else if(req->call == SIMCALL_COMM_IRECV)
@@ -485,7 +534,7 @@ void MC_dpor(void)
       /* Answer the request */
       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 
-      if(_sg_mc_comms_determinism){
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
         MC_SET_RAW_MEM;
         if(comm_pattern != 0){
           if(!initial_state_safety->initial_communications_pattern_done)
@@ -590,16 +639,36 @@ void MC_dpor(void)
 
       MC_SET_RAW_MEM;
 
-      if(_sg_mc_comms_determinism){
-        if(!initial_state_safety->initial_communications_pattern_done){
-          //print_communications_pattern(initial_communications_pattern);
-        }else{
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+        if(initial_state_safety->initial_communications_pattern_done){
           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);
+            if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
+              XBT_INFO("****************************************************");
+              XBT_INFO("***** Non-deterministic communications pattern *****");
+              XBT_INFO("****************************************************");
+              XBT_INFO("Initial communications pattern:");
+              print_communications_pattern(initial_communications_pattern);
+              XBT_INFO("Communications pattern counter-example:");
+              print_communications_pattern(communications_pattern);
+              MC_print_statistics(mc_stats);
+              return;
+            }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
+              XBT_INFO("****************************************************");
+              XBT_INFO("***** Non-send-deterministic communications pattern *****");
+              XBT_INFO("****************************************************");
+              XBT_INFO("Initial communications pattern:");
+              print_communications_pattern(initial_communications_pattern);
+              XBT_INFO("Communications pattern counter-example:");
+              print_communications_pattern(communications_pattern);
+              MC_print_statistics(mc_stats);
+              return;
+            }
           }
+        }else{
+          initial_state_safety->initial_communications_pattern_done = 1;
         }
-        initial_state_safety->initial_communications_pattern_done = 1;
       }
 
       /* Trash the current state, no longer needed */