Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : improve error message
[simgrid.git] / src / mc / mc_dpor.c
index 6c22b82..b7af5b4 100644 (file)
@@ -6,6 +6,8 @@
 
 #include "mc_private.h"
 
+#include "xbt/mmalloc/mmprivate.h"
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
                                 "Logging specific to MC DPOR exploration");
 
@@ -62,6 +64,10 @@ static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2
 }
 
 static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
+
+  if(!xbt_dynar_is_empty(incomplete_communications_pattern))
+    xbt_die("Damn ! Some communications are incomplete that means one or several simcalls are not handle ... ");
+
   unsigned int cursor = 0, send_index = 0, recv_index = 0;
   mc_comm_pattern_t comm1, comm2;
   int comm_comparison = 0;
@@ -97,63 +103,58 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte
   }
 }
 
-static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
+void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){
   mc_comm_pattern_t current_pattern;
   unsigned int cursor = 0;
   int index;
+  int completed = 0;
+  void *addr_pointed;
   xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){
     current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t);
-    if(current_pattern->comm == pattern->comm){
-      current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
-      current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
-      current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
-      current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
+    if(current_pattern->comm == comm){
+      current_pattern->src_proc = comm->comm.src_proc->pid;
+      current_pattern->dst_proc = comm->comm.dst_proc->pid;
+      current_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
+      current_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
       if(current_pattern->data_size == -1){
-        current_pattern->data_size = pattern->comm->comm.src_buff_size;
+        current_pattern->data_size = *(comm->comm.dst_buff_size);
         current_pattern->data = xbt_malloc0(current_pattern->data_size);
-        memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size);
+        addr_pointed = *(void **)comm->comm.src_buff;
+        if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
+          memcpy(current_pattern->data, addr_pointed, current_pattern->data_size);
+        else
+          memcpy(current_pattern->data, comm->comm.src_buff, current_pattern->data_size);
       }
-      current_pattern->matched_comm = pattern->num;
-      current_pattern->completed = 1;
       xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL);
-      return current_pattern->num;
+      completed++;
+      if(completed == 2)
+        return;
+      cursor--;
     }
   }
-  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;
   pattern->data_size = -1;
+  void * addr_pointed;
   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->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
-      pattern->completed = 1;
-    }
     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);
+    pattern->data = xbt_malloc0(pattern->data_size);
+    addr_pointed = *(void **)pattern->comm->comm.src_buff;
+    if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
+      memcpy(pattern->data, addr_pointed, pattern->data_size);
+    else
+      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->src_host = simcall_host_get_name(request->issuer->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(pattern->comm->comm.dst_proc->smx_host);
   }
@@ -165,8 +166,7 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
   
   xbt_dynar_push(list, &pattern);
 
-  if(!pattern->completed)
-    xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1);
+  xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1);
 
 }
 
@@ -175,9 +175,9 @@ static void print_communications_pattern(xbt_dynar_t comms_pattern){
   mc_comm_pattern_t current_comm;
   xbt_dynar_foreach(comms_pattern, cursor, current_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");
+      XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_proc, 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");
+      XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_proc, current_comm->src_host, "iRecv");
   }
 }
 
@@ -230,9 +230,9 @@ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state,
   XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu",
     state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used);
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
 
   int cursor = 0, previous_cursor, next_cursor;
   mc_visited_state_t state_test;
@@ -270,14 +270,14 @@ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state,
           next_cursor++;
         }
         if(!raw_mem_set)
-          MC_UNSET_RAW_MEM;
+          MC_SET_STD_HEAP;
         return -1;
       }
      }
   }
 
   if(!raw_mem_set)
-    MC_UNSET_RAW_MEM;
+    MC_SET_STD_HEAP;
 
   return cursor;
 }
@@ -291,9 +291,9 @@ static int is_visited_state(){
   if(_sg_mc_visited == 0)
     return -1;
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
 
   mc_visited_state_t new_state = visited_state_new();
   
@@ -302,7 +302,7 @@ static int is_visited_state(){
     xbt_dynar_push(visited_states, &new_state); 
 
     if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
+      MC_SET_STD_HEAP;
 
     return -1;
 
@@ -332,7 +332,7 @@ static int is_visited_state(){
         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;
+          MC_SET_STD_HEAP;
         return new_state->other_num;
         }*/
 
@@ -356,7 +356,7 @@ static int is_visited_state(){
           xbt_dynar_insert_at(visited_states, cursor, &new_state);
 
           if(!raw_mem_set)
-            MC_UNSET_RAW_MEM;
+            MC_SET_STD_HEAP;
           return new_state->other_num;
         }
         cursor++;
@@ -399,7 +399,7 @@ static int is_visited_state(){
     }
 
     if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
+      MC_SET_STD_HEAP;
     
     return -1;
     
@@ -412,13 +412,13 @@ static int is_visited_state(){
 void MC_dpor_init()
 {
   
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
   mc_state_t initial_state = NULL;
   smx_process_t process;
   
   /* Create the initial state and push it into the exploration stack */
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
 
   if(_sg_mc_visited > 0)
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
@@ -435,7 +435,7 @@ void MC_dpor_init()
 
   initial_state = MC_state_new();
 
-  MC_UNSET_RAW_MEM;
+  MC_SET_STD_HEAP;
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");
@@ -446,7 +446,7 @@ void MC_dpor_init()
   MC_ignore_heap(simix_global->process_to_run->data, 0);
   MC_ignore_heap(simix_global->process_that_ran->data, 0);
 
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
  
   /* Get an enabled process and insert it in the interleave set of the initial state */
   xbt_swag_foreach(process, simix_global->process_list){
@@ -474,12 +474,12 @@ void MC_dpor_init()
     }
   }
 
-  MC_UNSET_RAW_MEM;
+  MC_SET_STD_HEAP;
 
   if(raw_mem_set)
-    MC_SET_RAW_MEM;
+    MC_SET_MC_HEAP;
   else
-    MC_UNSET_RAW_MEM;
+    MC_SET_STD_HEAP;
   
 }
 
@@ -502,6 +502,7 @@ void MC_dpor(void)
   int enabled = 0;
   int interleave_size = 0;
   int comm_pattern = 0;
+  smx_action_t current_comm;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -531,41 +532,62 @@ void MC_dpor(void)
         xbt_free(req_str);
       }
       
-      MC_SET_RAW_MEM;
+      MC_SET_MC_HEAP;
       if(dot_output != NULL)
         req_str = MC_request_get_dot_output(req, value);
-      MC_UNSET_RAW_MEM;
+      MC_SET_STD_HEAP;
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
       if(mc_reduce_kind ==  e_mc_reduce_dpor){
-        MC_SET_RAW_MEM;
+        MC_SET_MC_HEAP;
         char *key = bprintf("%lu", req->issuer->pid);
         xbt_dict_remove(first_enabled_state, key); 
         xbt_free(key);
-        MC_UNSET_RAW_MEM;
+        MC_SET_STD_HEAP;
       }
 
+      /* TODO : handle test and testany simcalls */
       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)
           comm_pattern = 2;
+        else if(req->call == SIMCALL_COMM_WAIT)
+          comm_pattern = 3;
+        else if(req->call == SIMCALL_COMM_WAITANY)
+          comm_pattern = 4;
       }
 
       /* Answer the request */
       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
-        MC_SET_RAW_MEM;
-        if(comm_pattern != 0){
+        MC_SET_MC_HEAP;
+        if(comm_pattern == 1 || comm_pattern == 2){
           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);
+        }else if(comm_pattern == 3){
+          current_comm = simcall_comm_wait__get__comm(req);
+          if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+            if(!initial_state_safety->initial_communications_pattern_done)
+              complete_comm_pattern(initial_communications_pattern, current_comm);
+            else
+              complete_comm_pattern(communications_pattern, current_comm);
+          }
+        }else if(comm_pattern == 4){
+          current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+          if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+            if(!initial_state_safety->initial_communications_pattern_done)
+              complete_comm_pattern(initial_communications_pattern, current_comm);
+            else
+              complete_comm_pattern(communications_pattern, current_comm);
+          }
         }
-        MC_UNSET_RAW_MEM; 
+        MC_SET_STD_HEAP;
         comm_pattern = 0;
       }
 
@@ -573,7 +595,7 @@ void MC_dpor(void)
       MC_wait_for_requests();
 
       /* Create the new expanded state */
-      MC_SET_RAW_MEM;
+      MC_SET_MC_HEAP;
 
       next_state = MC_state_new();
 
@@ -621,7 +643,7 @@ void MC_dpor(void)
       if(dot_output != NULL)
         xbt_free(req_str);
 
-      MC_UNSET_RAW_MEM;
+      MC_SET_STD_HEAP;
 
       /* Let's loop again */
 
@@ -664,7 +686,7 @@ void MC_dpor(void)
 
       }
 
-      MC_SET_RAW_MEM;
+      MC_SET_MC_HEAP;
 
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
         if(initial_state_safety->initial_communications_pattern_done){
@@ -703,7 +725,7 @@ void MC_dpor(void)
       MC_state_delete(state);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 
-      MC_UNSET_RAW_MEM;        
+      MC_SET_STD_HEAP;
       
       /* Check for deadlocks */
       if(MC_deadlock_check()){
@@ -711,7 +733,7 @@ void MC_dpor(void)
         return;
       }
 
-      MC_SET_RAW_MEM;
+      MC_SET_MC_HEAP;
       /* Traverse the stack backwards until a state with a non empty interleave
          set is found, deleting all the states that have it empty in the way.
          For each deleted state, check if the request that has generated it 
@@ -720,7 +742,7 @@ void MC_dpor(void)
          state that executed that previous request. */
       
       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
-        if(mc_reduce_kind != e_mc_reduce_none){
+        if(mc_reduce_kind == e_mc_reduce_dpor){
           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))){
@@ -763,7 +785,7 @@ void MC_dpor(void)
             if(state->system_state != NULL){
               MC_restore_snapshot(state->system_state);
               xbt_fifo_unshift(mc_stack_safety, state);
-              MC_UNSET_RAW_MEM;
+              MC_SET_STD_HEAP;
             }else{
               pos = xbt_fifo_size(mc_stack_safety);
               item = xbt_fifo_get_first_item(mc_stack_safety);
@@ -778,12 +800,12 @@ void MC_dpor(void)
               }
               MC_restore_snapshot(restored_state->system_state);
               xbt_fifo_unshift(mc_stack_safety, state);
-              MC_UNSET_RAW_MEM;
+              MC_SET_STD_HEAP;
               MC_replay(mc_stack_safety, pos);
             }
           }else{
             xbt_fifo_unshift(mc_stack_safety, state);
-            MC_UNSET_RAW_MEM;
+            MC_SET_STD_HEAP;
             MC_replay(mc_stack_safety, -1);
           }
           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
@@ -800,11 +822,11 @@ void MC_dpor(void)
           MC_state_delete(state);
         }
       }
-      MC_UNSET_RAW_MEM;
+      MC_SET_STD_HEAP;
     }
   }
   MC_print_statistics(mc_stats);
-  MC_UNSET_RAW_MEM;  
+  MC_SET_STD_HEAP;
 
   return;
 }