model-checker : complete comm pattern only after a comm wait

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 6c22b82..73d6907 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -97,46 +97,40 @@ 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;
   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);
+        memcpy(current_pattern->data, current_pattern->comm->comm.dst_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;
   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;
@@ -145,15 +139,6 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
   }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 +150,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 +159,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");
   }
 }
 
@@ -552,6 +536,8 @@ void MC_dpor(void)
           comm_pattern = 1;
         else if(req->call == SIMCALL_COMM_IRECV)
           comm_pattern = 2;
+        else if(req->call == SIMCALL_COMM_WAIT)
+          comm_pattern = 3;
       }
 
       /* Answer the request */
@@ -559,11 +545,16 @@ void MC_dpor(void)
 
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
         MC_SET_RAW_MEM;
-        if(comm_pattern != 0){
+        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){
+           if(!initial_state_safety->initial_communications_pattern_done)
+             complete_comm_pattern(initial_communications_pattern, simcall_comm_wait__get__comm(req));
+          else
+            complete_comm_pattern(communications_pattern, simcall_comm_wait__get__comm(req));
         }
         MC_UNSET_RAW_MEM; 
         comm_pattern = 0;
@@ -720,7 +711,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))){

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 89b9855..77a5a5d 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -1163,44 +1163,49 @@ void MC_replay(xbt_fifo_t stack, int start)
         XBT_DEBUG("Replay: %s (%p)", req_str, state);
         xbt_free(req_str);
       }
-    }
 
-    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;
-    }
+      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;
+      }
 
-    SIMIX_simcall_pre(req, value);
+      SIMIX_simcall_pre(req, value);
 
-    if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
-      MC_SET_RAW_MEM;
-      if(comm_pattern != 0){
-        get_comm_pattern(communications_pattern, req, comm_pattern);
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+        MC_SET_RAW_MEM;
+        if(comm_pattern == 1 || comm_pattern == 2){
+          get_comm_pattern(communications_pattern, req, comm_pattern);
+        }else if (comm_pattern == 3){
+          complete_comm_pattern(communications_pattern, simcall_comm_wait__get__comm(req));
+        }
+        MC_UNSET_RAW_MEM;
+        comm_pattern = 0;
       }
-      MC_UNSET_RAW_MEM;
-      comm_pattern = 0;
-    }
     
-    MC_wait_for_requests();
-
-    count++;
-
-    if(mc_reduce_kind ==  e_mc_reduce_dpor){
-      MC_SET_RAW_MEM;
-      /* Insert in dict all enabled processes */
-      xbt_swag_foreach(process, simix_global->process_list){
-        if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
-          char *key = bprintf("%lu", process->pid);
-          if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
-            char *data = bprintf("%d", count);
-            xbt_dict_set(first_enabled_state, key, data, NULL);
+    
+      MC_wait_for_requests();
+
+      count++;
+
+      if(mc_reduce_kind ==  e_mc_reduce_dpor){
+        MC_SET_RAW_MEM;
+        /* Insert in dict all enabled processes */
+        xbt_swag_foreach(process, simix_global->process_list){
+          if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+            char *key = bprintf("%lu", process->pid);
+            if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+              char *data = bprintf("%d", count);
+              xbt_dict_set(first_enabled_state, key, data, NULL);
+            }
+            xbt_free(key);
           }
-          xbt_free(key);
         }
+        MC_UNSET_RAW_MEM;
       }
-      MC_UNSET_RAW_MEM;
     }
          
     /* Update statistics */

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 0d45e74..0641d0c 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -556,7 +556,6 @@ typedef struct s_mc_comm_pattern{
   int num;
   smx_action_t comm;
   e_smx_comm_type_t type;
-  int completed;
   unsigned long src_proc;
   unsigned long dst_proc;
   const char *src_host;
@@ -564,13 +563,13 @@ typedef struct s_mc_comm_pattern{
   char *rdv;
   ssize_t data_size;
   void *data;
-  int matched_comm;
 }s_mc_comm_pattern_t, *mc_comm_pattern_t;
 
 extern xbt_dynar_t communications_pattern;
 extern xbt_dynar_t incomplete_communications_pattern;
 
 void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);
+void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm);
 
 /* *********** Sets *********** */