[mc] mc_comm_pattern.c containing all communication pattern functions

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 6a07df0..ff34950 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -613,6 +613,7 @@ set(MC_SRC
   src/mc/mc_page_store.cpp
   src/mc/mc_page_snapshot.cpp
   src/mc/mc_comm_pattern.h
   src/mc/mc_page_store.cpp
   src/mc/mc_page_snapshot.cpp
   src/mc/mc_comm_pattern.h

+  src/mc/mc_comm_pattern.c

   src/mc/mc_comm_determinism.c
   src/mc/mc_compare.cpp
   src/mc/mc_diff.c
   src/mc/mc_comm_determinism.c
   src/mc/mc_compare.cpp
   src/mc/mc_diff.c

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 1017b33..8b59b3a 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -186,11 +186,12 @@ void list_comm_pattern_free_voidp(void *p) {
 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
 {
   mc_process_t process = &mc_model_checker->process;
 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
 {
   mc_process_t process = &mc_model_checker->process;

-  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;
 
   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);
   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);

diff --git a/src/mc/mc_comm_pattern.c b/src/mc/mc_comm_pattern.c
new file mode 100644 (file)
index 0000000..1367432
--- /dev/null
+++ b/src/mc/mc_comm_pattern.c
@@ -0,0 +1,95 @@
+/* Copyright (c) 2007-2014. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <string.h>
+
+#include <xbt/sysdep.h>
+#include <xbt/dynar.h>
+
+#include "mc_comm_pattern.h"
+
+mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm)
+{
+  mc_comm_pattern_t res = xbt_new0(s_mc_comm_pattern_t, 1);
+  res->index = comm->index;
+  res->type = comm->type;
+  res->comm = comm->comm;
+  res->rdv = strdup(comm->rdv);
+  res->data_size = -1;
+  res->data = NULL;
+  if (comm->type == SIMIX_COMM_SEND) {
+    res->src_proc = comm->src_proc;
+    res->src_host = comm->src_host;
+    if (comm->data != NULL) {
+      res->data_size = comm->data_size;
+      res->data = xbt_malloc0(comm->data_size);
+      memcpy(res->data, comm->data, comm->data_size);
+    }
+  } else {
+    res->dst_proc = comm->dst_proc;
+    res->dst_host = comm->dst_host;
+  }
+  return res;
+}
+
+xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t patterns)
+{
+  xbt_dynar_t res = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+
+  mc_comm_pattern_t comm;
+  unsigned int cursor;
+  xbt_dynar_foreach(patterns, cursor, comm) {
+    mc_comm_pattern_t copy_comm = MC_comm_pattern_dup(comm);
+    xbt_dynar_push(res, &copy_comm);
+  }
+
+  return res;
+}
+
+void MC_restore_communications_pattern(mc_state_t state)
+{
+  mc_list_comm_pattern_t list_process_comm;
+  unsigned int cursor;
+
+  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
+    list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int);
+  }
+
+  for (int i = 0; i < MC_smx_get_maxpid(); i++) {
+    xbt_dynar_t initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
+    xbt_dynar_reset(initial_incomplete_process_comms);
+    xbt_dynar_t incomplete_process_comms = xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t);
+
+    mc_comm_pattern_t comm;
+    xbt_dynar_foreach(incomplete_process_comms, cursor, comm) {
+      mc_comm_pattern_t copy_comm = MC_comm_pattern_dup(comm);
+      xbt_dynar_push(initial_incomplete_process_comms, &copy_comm);
+    }
+
+  }
+}
+
+void MC_state_copy_incomplete_communications_pattern(mc_state_t state)
+{
+  state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+
+  int i;
+  for (i=0; i < MC_smx_get_maxpid(); i++) {
+    xbt_dynar_t comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
+    xbt_dynar_t copy = MC_comm_patterns_dup(comms);
+    xbt_dynar_insert_at(state->incomplete_comm_pattern, i, &copy);
+  }
+}
+
+void MC_state_copy_index_communications_pattern(mc_state_t state)
+{
+  state->index_comm = xbt_dynar_new(sizeof(unsigned int), NULL);
+  mc_list_comm_pattern_t list_process_comm;
+  unsigned int cursor;
+  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
+    xbt_dynar_push_as(state->index_comm, unsigned int, list_process_comm->index_comm);
+  }
+}

diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h
index 2bb40d2..3201a1a 100644 (file)
--- a/src/mc/mc_comm_pattern.h
+++ b/src/mc/mc_comm_pattern.h
@@ -13,6 +13,8 @@
 #include "../smpi/private.h"
 #include <smpi/smpi.h>
 
 #include "../smpi/private.h"
 #include <smpi/smpi.h>
 

+#include "mc_state.h"
+

 #ifndef MC_COMM_PATTERN_H
 #define MC_COMM_PATTERN_H
 
 #ifndef MC_COMM_PATTERN_H
 #define MC_COMM_PATTERN_H
 


@@ -84,6 +86,14 @@ void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int is
 void MC_pre_modelcheck_comm_determinism(void);
 void MC_modelcheck_comm_determinism(void);
 
 void MC_pre_modelcheck_comm_determinism(void);
 void MC_modelcheck_comm_determinism(void);
 

+void MC_restore_communications_pattern(mc_state_t state);
+
+mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm);
+xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state);
+
+void MC_state_copy_incomplete_communications_pattern(mc_state_t state);
+void MC_state_copy_index_communications_pattern(mc_state_t state);
+

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 9d7bd56..c867495 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -389,44 +389,6 @@ void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int valu
   
 }
 
   
 }
 

-static void MC_restore_communications_pattern(mc_state_t state) {
-  mc_list_comm_pattern_t list_process_comm;
-  unsigned int cursor, cursor2;
-  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
-    list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int);
-  }
-  mc_comm_pattern_t comm;
-  cursor = 0;
-  xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms;
-  for(int i=0; i < MC_smx_get_maxpid(); i++){
-    initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
-    xbt_dynar_reset(initial_incomplete_process_comms);
-    incomplete_process_comms = xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t);
-    xbt_dynar_foreach(incomplete_process_comms, cursor2, comm) {
-      mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1);
-      copy_comm->index = comm->index;
-      copy_comm->type = comm->type;
-      copy_comm->comm = comm->comm;
-      copy_comm->rdv = strdup(comm->rdv);
-      copy_comm->data_size = -1;
-      copy_comm->data = NULL;
-      if(comm->type == SIMIX_COMM_SEND){
-        copy_comm->src_proc = comm->src_proc;
-        copy_comm->src_host = comm->src_host;
-        if(comm->data != NULL){
-          copy_comm->data_size = comm->data_size;
-          copy_comm->data = xbt_malloc0(comm->data_size);
-          memcpy(copy_comm->data, comm->data, comm->data_size);
-        }
-      }else{
-        copy_comm->dst_proc = comm->dst_proc;
-        copy_comm->dst_host = comm->dst_host;
-      }
-      xbt_dynar_push(initial_incomplete_process_comms, &copy_comm);
-    }
-  }
-}
-

 /**
  * \brief Re-executes from the state at position start all the transitions indicated by
  *        a given model-checker stack.
 /**
  * \brief Re-executes from the state at position start all the transitions indicated by
  *        a given model-checker stack.

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 02dc8ad..2331919 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -14,51 +14,6 @@
 #include "mc_comm_pattern.h"
 #include "mc_smx.h"
 
 #include "mc_comm_pattern.h"
 #include "mc_smx.h"
 

-static void copy_incomplete_communications_pattern(mc_state_t state) {
-  int i;
-  xbt_dynar_t incomplete_process_comms;
-  mc_comm_pattern_t comm;
-  unsigned int cursor;
-  state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
-  for (i=0; i < MC_smx_get_maxpid(); i++) {
-    incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
-    xbt_dynar_t incomplete_process_comms_copy = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
-    xbt_dynar_foreach(incomplete_process_comms, cursor, comm) {
-      mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1);
-      copy_comm->index = comm->index;
-      copy_comm->type = comm->type;
-      copy_comm->comm = comm->comm;
-      copy_comm->rdv = strdup(comm->rdv);
-      copy_comm->data_size = -1;
-      copy_comm->data = NULL;
-      if(comm->type == SIMIX_COMM_SEND){
-        copy_comm->src_proc = comm->src_proc;
-        copy_comm->src_host = comm->src_host;
-        if (comm->data != NULL) {
-          copy_comm->data_size = comm->data_size;
-          copy_comm->data = xbt_malloc0(comm->data_size);
-          memcpy(copy_comm->data, comm->data, comm->data_size);
-        }
-      }else{
-        copy_comm->dst_proc = comm->dst_proc;
-        copy_comm->dst_host = comm->dst_host;
-      }
-      xbt_dynar_push(incomplete_process_comms_copy, &copy_comm);
-    }
-    xbt_dynar_insert_at(state->incomplete_comm_pattern, i, &incomplete_process_comms_copy);
-  }
-}
-
-static void copy_index_communications_pattern(mc_state_t state) {
-
-  state->index_comm = xbt_dynar_new(sizeof(unsigned int), NULL);
-  mc_list_comm_pattern_t list_process_comm;
-  unsigned int cursor;
-  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
-    xbt_dynar_push_as(state->index_comm, unsigned int, list_process_comm->index_comm);
-  }
-}
-

 /**
  * \brief Creates a state data structure used by the exploration algorithm
  */
 /**
  * \brief Creates a state data structure used by the exploration algorithm
  */


@@ -75,8 +30,8 @@ mc_state_t MC_state_new()
   if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) ||  _sg_mc_termination){
     state->system_state = MC_take_snapshot(state->num);
     if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
   if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) ||  _sg_mc_termination){
     state->system_state = MC_take_snapshot(state->num);
     if(_sg_mc_comms_determinism || _sg_mc_send_determinism){

-      copy_incomplete_communications_pattern(state);
-      copy_index_communications_pattern(state);
+      MC_state_copy_incomplete_communications_pattern(state);
+      MC_state_copy_index_communications_pattern(state);

     }
   }
   return state;
     }
   }
   return state;


@@ -277,6 +232,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
 
         case SIMCALL_COMM_WAIT:
           act = simcall_comm_wait__get__comm(&process->simcall);
 
         case SIMCALL_COMM_WAIT:
           act = simcall_comm_wait__get__comm(&process->simcall);

+

           if (act->comm.src_proc && act->comm.dst_proc) {
             *value = 0;
           } else {
           if (act->comm.src_proc && act->comm.dst_proc) {
             *value = 0;
           } else {

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index 863a21a..a60464b 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -47,7 +47,8 @@ typedef struct mc_state {
   mc_snapshot_t system_state;      /* Snapshot of system state */
   int num;
   int in_visited_states;
   mc_snapshot_t system_state;      /* Snapshot of system state */
   int num;
   int in_visited_states;

-  xbt_dynar_t incomplete_comm_pattern; // comm determinism verification
+  // comm determinism verification (xbt_dynar_t<xbt_dynar_t<mc_comm_pattern_t>):
+  xbt_dynar_t incomplete_comm_pattern;

   xbt_dynar_t index_comm; // comm determinism verification
 } s_mc_state_t, *mc_state_t;
 
   xbt_dynar_t index_comm; // comm determinism verification
 } s_mc_state_t, *mc_state_t;