X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4942695a0bed6ef2acc8f1c4f75b4d2f47567d6a..da7ddf47cca7f83884a15a05778d3909fd0e4cfd:/src/mc/mc_comm_determinism.c

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index bc1c9cebac..2ae9d1c9d1 100644
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -11,6 +11,7 @@
 #include "mc_private.h"
 #include "mc_record.h"
 #include "mc_smx.h"
+#include "mc_client.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
                                 "Logging specific to MC communication determinism detection");
@@ -85,41 +86,51 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p
   return res;
 }
 
-static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm)
+static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
 {
-  smx_process_t src_proc = MC_smx_resolve_process(comm->comm.src_proc);
-  smx_process_t dst_proc = MC_smx_resolve_process(comm->comm.dst_proc);
+  s_smx_synchro_t comm;
+  MC_process_read_simple(&mc_model_checker->process,
+    &comm, comm_addr, sizeof(comm));
+
+  smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
+  smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc);
   comm_pattern->src_proc = src_proc->pid;
   comm_pattern->dst_proc = dst_proc->pid;
   comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
-  if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) {
-    comm_pattern->data_size = *(comm->comm.dst_buff_size);
+  if (comm_pattern->data_size == -1 && comm.comm.src_buff != NULL) {
+    size_t buff_size;
+    MC_process_read_simple(&mc_model_checker->process,
+      &buff_size, comm.comm.dst_buff_size, sizeof(buff_size));
+    comm_pattern->data_size = buff_size;
     comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
     MC_process_read_simple(&mc_model_checker->process,
-      comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size);
+      comm_pattern->data, comm.comm.src_buff, comm_pattern->data_size);
   }
 }
 
 static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
 
-  mc_list_comm_pattern_t list_comm_pattern = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
+  mc_list_comm_pattern_t list =
+    xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
 
   if(!backtracking){
-    mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, list_comm_pattern->index_comm, mc_comm_pattern_t);
-    e_mc_comm_pattern_difference_t diff;
-    
-    if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){
+    mc_comm_pattern_t initial_comm =
+      xbt_dynar_get_as(list->list, list->index_comm, mc_comm_pattern_t);
+    e_mc_comm_pattern_difference_t diff =
+      compare_comm_pattern(initial_comm, comm);
+
+    if (diff != NONE_DIFF) {
       if (comm->type == SIMIX_COMM_SEND){
         initial_global_state->send_deterministic = 0;
         if(initial_global_state->send_diff != NULL)
           xbt_free(initial_global_state->send_diff);
-        initial_global_state->send_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+        initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
       }else{
         initial_global_state->recv_deterministic = 0;
         if(initial_global_state->recv_diff != NULL)
           xbt_free(initial_global_state->recv_diff);
-        initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+        initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
       }
       if(_sg_mc_send_determinism && !initial_global_state->send_deterministic){
         XBT_INFO("*********************************************************");
@@ -154,77 +165,112 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int
 
 void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
 {
+  const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
+  mc_list_comm_pattern_t initial_pattern = xbt_dynar_get_as(
+    initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
+  xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
+    incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+
   mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1);
   pattern->data_size = -1;
   pattern->data = NULL;
-
-  // Fill initial_pattern->index_comm:
-  const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
-  mc_list_comm_pattern_t initial_pattern =
-    (mc_list_comm_pattern_t) xbt_dynar_get_as(initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
-  xbt_dynar_t incomplete_pattern =
-    (xbt_dynar_t) xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
   pattern->index =
     initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
 
-  
   if (call_type == MC_CALL_TYPE_SEND) {
     /* Create comm pattern */
     pattern->type = SIMIX_COMM_SEND;
-    pattern->comm = simcall_comm_isend__get__result(request);
-    // TODO, resolve comm
-    // FIXME, remote access to rdv->name
-    pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
-    pattern->src_proc = MC_smx_resolve_process(pattern->comm->comm.src_proc)->pid;
+    pattern->comm_addr = simcall_comm_isend__get__result(request);
+
+    s_smx_synchro_t synchro;
+    MC_process_read_simple(&mc_model_checker->process,
+      &synchro, pattern->comm_addr, sizeof(synchro));
+
+    char* remote_name;
+    MC_process_read_simple(&mc_model_checker->process, &remote_name,
+      synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name,
+      sizeof(remote_name));
+    pattern->rdv =
+      MC_process_read_string(&mc_model_checker->process, remote_name);
+    pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
     pattern->src_host = MC_smx_process_get_host_name(issuer);
-    pattern->tag = ((MPI_Request)simcall_comm_isend__get__data(request))->tag;
-    if(pattern->comm->comm.src_buff != NULL){
-      pattern->data_size = pattern->comm->comm.src_buff_size;
+
+    struct s_smpi_mpi_request mpi_request;
+    MC_process_read_simple(&mc_model_checker->process,
+      &mpi_request, (MPI_Request) simcall_comm_isend__get__data(request),
+      sizeof(mpi_request));
+    pattern->tag = mpi_request.tag;
+
+    if(synchro.comm.src_buff != NULL){
+      pattern->data_size = synchro.comm.src_buff_size;
       pattern->data = xbt_malloc0(pattern->data_size);
       MC_process_read_simple(&mc_model_checker->process,
-        pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
+        pattern->data, synchro.comm.src_buff, pattern->data_size);
     }
-    if(((MPI_Request)simcall_comm_isend__get__data(request))->detached){
+    if(mpi_request.detached){
       if (!initial_global_state->initial_communications_pattern_done) {
         /* Store comm pattern */
-        xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->list, &pattern);
+        xbt_dynar_push(
+          xbt_dynar_get_as(
+            initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
+          )->list,
+          &pattern);
       } else {
         /* Evaluate comm determinism */
         deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
-        ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->index_comm++;
+        xbt_dynar_get_as(
+          initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
+        )->index_comm++;
       }
       return;
     }
   } else if (call_type == MC_CALL_TYPE_RECV) {                      
     pattern->type = SIMIX_COMM_RECEIVE;
-    pattern->comm = simcall_comm_irecv__get__result(request);
-    // TODO, remote access
-    pattern->tag = ((MPI_Request)simcall_comm_irecv__get__data(request))->tag;
-    pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
-    pattern->dst_proc = MC_smx_resolve_process(pattern->comm->comm.dst_proc)->pid;
-    // FIXME, remote process access
+    pattern->comm_addr = simcall_comm_irecv__get__result(request);
+
+    struct s_smpi_mpi_request mpi_request;
+    MC_process_read_simple(&mc_model_checker->process,
+      &mpi_request, (MPI_Request) simcall_comm_irecv__get__data(request),
+      sizeof(mpi_request));
+    pattern->tag = mpi_request.tag;
+
+    s_smx_synchro_t synchro;
+    MC_process_read_simple(&mc_model_checker->process,
+      &synchro, pattern->comm_addr, sizeof(synchro));
+
+    char* remote_name;
+    MC_process_read_simple(&mc_model_checker->process, &remote_name,
+      synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name,
+      sizeof(remote_name));
+    pattern->rdv =
+      MC_process_read_string(&mc_model_checker->process, remote_name);
+    pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
     pattern->dst_host = MC_smx_process_get_host_name(issuer);
   } else {
     xbt_die("Unexpected call_type %i", (int) call_type);
   }
 
-  xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), &pattern);
+  xbt_dynar_push(
+    xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
+    &pattern);
 
   XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
 }
 
-void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int issuer, int backtracking) {
+void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
   mc_comm_pattern_t current_comm_pattern;
   unsigned int cursor = 0;
   mc_comm_pattern_t comm_pattern;
   int completed = 0;
 
   /* Complete comm pattern */
-  xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) {
-    if (current_comm_pattern-> comm == comm) {
-      update_comm_pattern(current_comm_pattern, comm);
+  xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) {
+    if (current_comm_pattern->comm_addr == comm_addr) {
+      update_comm_pattern(current_comm_pattern, comm_addr);
       completed = 1;
-      xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &comm_pattern);
+      xbt_dynar_remove_at(
+        xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
+        cursor, &comm_pattern);
       XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
       break;
     }
@@ -232,39 +278,48 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int
   if(!completed)
     xbt_die("Corresponding communication not found!");
 
+  mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
+    initial_communications_pattern, issuer, mc_list_comm_pattern_t);
+
   if (!initial_global_state->initial_communications_pattern_done) {
     /* Store comm pattern */
-    xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->list, &comm_pattern);
+    xbt_dynar_push(pattern->list, &comm_pattern);
   } else {
     /* Evaluate comm determinism */
     deterministic_comm_pattern(issuer, comm_pattern, backtracking);
-    ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->index_comm++;
+    pattern->index_comm++;
   }
 }
 
 
 /************************ Main algorithm ************************/
 
-void MC_pre_modelcheck_comm_determinism(void)
+static void MC_modelcheck_comm_determinism_main(void);
+
+static void MC_pre_modelcheck_comm_determinism(void)
 {
   MC_SET_MC_HEAP;
 
   mc_state_t initial_state = NULL;
   smx_process_t process;
   int i;
+  const int maxpid = MC_smx_get_maxpid();
 
   if (_sg_mc_visited > 0)
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
  
+  // Create initial_communications_pattern elements:
   initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
-  for (i=0; i < MC_smx_get_maxpid(); i++){
+  for (i=0; i < maxpid; i++){
     mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
     process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp);
     process_list_pattern->index_comm = 0;
     xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
   }
+
+  // Create incomplete_communications_pattern elements:
   incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
-  for (i=0; i < MC_smx_get_maxpid(); i++){
+  for (i=0; i < maxpid; i++){
     xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), NULL);
     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
   }
@@ -292,7 +347,7 @@ void MC_pre_modelcheck_comm_determinism(void)
 
 }
 
-void MC_modelcheck_comm_determinism(void)
+static void MC_modelcheck_comm_determinism_main(void)
 {
 
   char *req_str = NULL;
@@ -319,8 +374,8 @@ void MC_modelcheck_comm_determinism(void)
         && (req = MC_state_get_request(state, &value))
         && (visited_state == NULL)) {
 
-      req_str = MC_request_to_string(req, value);  
-      XBT_DEBUG("Execute: %s", req_str);                 
+      req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+      XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
       
       if (dot_output != NULL) {
@@ -439,5 +494,37 @@ void MC_modelcheck_comm_determinism(void)
   MC_print_statistics(mc_stats);
   MC_SET_STD_HEAP;
 
-  return;
+  exit(0);
+}
+
+void MC_modelcheck_comm_determinism(void)
+{
+  if (mc_mode == MC_MODE_CLIENT) {
+    // This will move somehwere else:
+    MC_client_handle_messages();
+  }
+
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+
+  /* Create exploration stack */
+  mc_stack = xbt_fifo_new();
+
+  MC_SET_STD_HEAP;
+
+  MC_pre_modelcheck_comm_determinism();
+
+  MC_SET_MC_HEAP;
+  initial_global_state = xbt_new0(s_mc_global_t, 1);
+  initial_global_state->snapshot = MC_take_snapshot(0);
+  initial_global_state->initial_communications_pattern_done = 0;
+  initial_global_state->recv_deterministic = 1;
+  initial_global_state->send_deterministic = 1;
+  initial_global_state->recv_diff = NULL;
+  initial_global_state->send_diff = NULL;
+
+  MC_SET_STD_HEAP;
+
+  MC_modelcheck_comm_determinism_main();
+
+  mmalloc_set_current_heap(heap);
 }