X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/73ca6a5bc359768f69ee1e7181ab19578c6e181e..941b7b09d7e8c0926a2fa56141c47537badc11ca:/src/mc/mc_comm_determinism.c

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 0636fa4952..d5aff260a9 100644
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -10,6 +10,7 @@
 #include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_record.h"
+#include "mc_smx.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
                                 "Logging specific to MC communication determinism detection");
@@ -21,21 +22,6 @@ xbt_dynar_t incomplete_communications_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 list_comm_pattern_free(mc_list_comm_pattern_t l)
-{
-  xbt_dynar_free(&(l->list));
-  xbt_free(l);
-  l = NULL;
-}
-
 static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
   if(comm1->type != comm2->type)
     return TYPE_DIFF;
@@ -101,19 +87,17 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p
 
 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm)
 {
-  void *addr_pointed;
-  comm_pattern->src_proc = comm->comm.src_proc->pid;
-  comm_pattern->dst_proc = comm->comm.dst_proc->pid;
-  comm_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
-  comm_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
+  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);
     comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
-    addr_pointed = *(void **) comm->comm.src_buff;
-    if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval)
-      memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size);
-    else
-      memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size);
+    MC_process_read_simple(&mc_model_checker->process,
+      comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size);
   }
 }
 
@@ -162,46 +146,47 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int
     }
   }
     
-  comm_pattern_free(comm);
+  MC_comm_pattern_free(comm);
 
 }
 
 /********** Non Static functions ***********/
 
-void comm_pattern_free_voidp(void *p) {
-  comm_pattern_free((mc_comm_pattern_t) * (void **) p);
-}
-
-void list_comm_pattern_free_voidp(void *p) {
-  list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
-}
-
-void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
+void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
 {
-
-  mc_comm_pattern_t pattern = NULL;
-  pattern = xbt_new0(s_mc_comm_pattern_t, 1);
+  mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1);
   pattern->data_size = -1;
   pattern->data = NULL;
-  
-  void *addr_pointed;
+
+  // 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);
-    pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
-    pattern->src_proc = pattern->comm->comm.src_proc->pid;
-    pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
+
+    s_smx_synchro_t synchro;
+    MC_process_read_simple(&mc_model_checker->process,
+      &synchro, pattern->comm, sizeof(synchro));
+
+    // TODO, remote access to rdv->name and rdv_copy->name
+    pattern->rdv = (synchro.comm.rdv != NULL) ? strdup(synchro.comm.rdv->name) : strdup(synchro.comm.rdv_cpy->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;
+    if(synchro.comm.src_buff != NULL){
+      pattern->data_size = synchro.comm.src_buff_size;
       pattern->data = xbt_malloc0(pattern->data_size);
-      addr_pointed = *(void **) pattern->comm->comm.src_buff;
-      if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval)
-        memcpy(pattern->data, addr_pointed, pattern->data_size);
-      else
-        memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
+      MC_process_read_simple(&mc_model_checker->process,
+        pattern->data, synchro.comm.src_buff, pattern->data_size);
     }
     if(((MPI_Request)simcall_comm_isend__get__data(request))->detached){
       if (!initial_global_state->initial_communications_pattern_done) {
@@ -217,21 +202,27 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t
   } 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 = pattern->comm->comm.dst_proc->pid;
-    pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
+
+    s_smx_synchro_t synchro;
+    MC_process_read_simple(&mc_model_checker->process,
+      &synchro, pattern->comm, sizeof(synchro));
+
+    pattern->rdv = (synchro.comm.rdv != NULL) ? strdup(synchro.comm.rdv->name) : strdup(synchro.comm.rdv_cpy->name);
+    pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
+    // FIXME, remote process access
+    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, request->issuer->pid, xbt_dynar_t), &pattern);
+  xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), &pattern);
 
-  XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, request->issuer->pid);
+  XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
 }
 
-void 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, unsigned int issuer, int backtracking) {
   mc_comm_pattern_t current_comm_pattern;
   unsigned int cursor = 0;
   mc_comm_pattern_t comm_pattern;
@@ -265,28 +256,24 @@ void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int is
 
 void MC_pre_modelcheck_comm_determinism(void)
 {
-
-  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
+  MC_SET_MC_HEAP;
 
   mc_state_t initial_state = NULL;
   smx_process_t process;
   int i;
 
-  if (!mc_mem_set)
-    MC_SET_MC_HEAP;
-
   if (_sg_mc_visited > 0)
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
  
-  initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), list_comm_pattern_free_voidp);
-  for (i=0; i<simix_process_maxpid; i++){
+  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++){
     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), comm_pattern_free_voidp);
+    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);
   }
   incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
-  for (i=0; i<simix_process_maxpid; i++){
+  for (i=0; i < MC_smx_get_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);
   }
@@ -302,11 +289,11 @@ void MC_pre_modelcheck_comm_determinism(void)
   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) {
+  MC_EACH_SIMIX_PROCESS(process,
     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
     }
-  }
+  );
 
   xbt_fifo_unshift(mc_stack, initial_state);
 
@@ -357,17 +344,17 @@ void MC_modelcheck_comm_determinism(void)
       /* TODO : handle test and testany simcalls */
       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-        call = mc_get_call_type(req);
+        call = MC_get_call_type(req);
       }
 
       /* Answer the request */
-      SIMIX_simcall_handle(req, value);    /* After this call req is no longer useful */
+      MC_simcall_handle(req, value);    /* After this call req is no longer useful */
 
       MC_SET_MC_HEAP;
       if(!initial_global_state->initial_communications_pattern_done)
-        handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
+        MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
       else
-        handle_comm_pattern(call, req, value, NULL, 0);
+        MC_handle_comm_pattern(call, req, value, NULL, 0);
       MC_SET_STD_HEAP;
 
       /* Wait for requests (schedules processes) */
@@ -381,11 +368,11 @@ void MC_modelcheck_comm_determinism(void)
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get enabled processes and insert them in the interleave set of the next state */
-        xbt_swag_foreach(process, simix_global->process_list) {
+        MC_EACH_SIMIX_PROCESS(process,
           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
           }
-        }
+        );
 
         if (dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);