[mc] Fetch simix_process_maxpid from MCed

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 635bc9d..1017b33 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -293,14 +293,14 @@ void MC_pre_modelcheck_comm_determinism(void)
     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);
     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++){
+  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->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);
     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->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);
   }
     xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), NULL);
     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
   }

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index eaba624..9d7bd56 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -116,14 +116,22 @@ void MC_init_pid(pid_t pid, int socket)
     }
   }
 
     }
   }
 

-  mc_time = xbt_new0(double, simix_process_maxpid);
-

   /* Initialize the data structures that must be persistent across every
      iteration of the model-checker (in RAW memory) */
 
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   mc_model_checker = MC_model_checker_new(pid, socket);
   /* Initialize the data structures that must be persistent across every
      iteration of the model-checker (in RAW memory) */
 
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   mc_model_checker = MC_model_checker_new(pid, socket);

+  if (mc_mode == MC_MODE_SERVER) {
+    int maxpid;
+    MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
+      &maxpid, sizeof(maxpid));
+    simix_process_maxpid = maxpid;
+  }
+
+  mmalloc_set_current_heap(std_heap);
+  mc_time = xbt_new0(double, MC_smx_get_maxpid());
+  mmalloc_set_current_heap(mc_heap);

 
   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
 
 
   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
 


@@ -182,13 +190,14 @@ void MC_init_pid(pid_t pid, int socket)
       /* Those requests are handled on the client side and propagated by message
        * to the server: */
 
       /* Those requests are handled on the client side and propagated by message
        * to the server: */
 

-      MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+      MC_ignore_heap(mc_time, MC_smx_get_maxpid() * sizeof(double));

 
       smx_process_t process;
       xbt_swag_foreach(process, simix_global->process_list) {
         MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
       }
     }
 
       smx_process_t process;
       xbt_swag_foreach(process, simix_global->process_list) {
         MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
       }
     }

+

   }
 
   mmalloc_set_current_heap(heap);
   }
 
   mmalloc_set_current_heap(heap);


@@ -389,7 +398,7 @@ static void MC_restore_communications_pattern(mc_state_t state) {
   mc_comm_pattern_t comm;
   cursor = 0;
   xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms;
   mc_comm_pattern_t comm;
   cursor = 0;
   xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms;

-  for(int i=0; i<simix_process_maxpid; i++){
+  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);
     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);


@@ -461,7 +470,7 @@ void MC_replay(xbt_fifo_t stack)
   MC_SET_MC_HEAP;
 
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
   MC_SET_MC_HEAP;
 
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {

-    for (j=0; j<simix_process_maxpid; j++) {
+    for (j=0; j < simix_process_maxpid; j++) {

       xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
       ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t))->index_comm = 0;
     }
       xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
       ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t))->index_comm = 0;
     }

diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h
index 45790f3..0b07e8e 100644 (file)
--- a/src/mc/mc_model_checker.h
+++ b/src/mc/mc_model_checker.h
@@ -41,6 +41,13 @@ struct s_mc_model_checker {
 mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
 void MC_model_checker_delete(mc_model_checker_t mc);
 
 mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
 void MC_model_checker_delete(mc_model_checker_t mc);
 

+static inline
+int MC_smx_get_maxpid(void)
+{
+  // Currently we use the same variable in STANDALONE and in SERVER mode:
+  return simix_process_maxpid;
+}
+

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index b5f061a..250c77f 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -36,6 +36,7 @@
 #include "xbt/parmap.h"
 
 #include "mc_forward.h"
 #include "xbt/parmap.h"
 
 #include "mc_forward.h"

+#include "mc_protocol.h"

 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 

diff --git a/src/mc/mc_record.c b/src/mc/mc_record.c
index d578168..9d615b3 100644 (file)
--- a/src/mc/mc_record.c
+++ b/src/mc/mc_record.c
@@ -144,5 +144,5 @@ void MC_record_replay_from_string(const char* path_string)
 
 void MC_record_replay_init()
 {
 
 void MC_record_replay_init()
 {

-  mc_time = xbt_new0(double, simix_process_maxpid);
+  mc_time = xbt_new0(double, MC_smx_get_maxpid());

 }
 }

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index bb53fa5..0c079d5 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -20,7 +20,7 @@ static void copy_incomplete_communications_pattern(mc_state_t state) {
   mc_comm_pattern_t comm;
   unsigned int cursor;
   state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
   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<simix_process_maxpid; i++) {
+  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) {
     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) {


@@ -64,10 +64,8 @@ static void copy_index_communications_pattern(mc_state_t state) {
  */
 mc_state_t MC_state_new()
 {
  */
 mc_state_t MC_state_new()
 {

-  mc_state_t state = NULL;
-
-  state = xbt_new0(s_mc_state_t, 1);
-  state->max_pid = simix_process_maxpid;
+  mc_state_t state = xbt_new0(s_mc_state_t, 1);
+  state->max_pid = MC_smx_get_maxpid();

   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
   state->system_state = NULL;
   state->num = ++mc_stats->expanded_states;
   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
   state->system_state = NULL;
   state->num = ++mc_stats->expanded_states;

diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c
index 77548d8..941a780 100644 (file)
--- a/src/mc/mc_visited.c
+++ b/src/mc/mc_visited.c
@@ -230,7 +230,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
      are incomplete and they cannot be analyzed and compared with the initial pattern. */
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     int current_process = 1;
      are incomplete and they cannot be analyzed and compared with the initial pattern. */
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     int current_process = 1;

-    while (current_process < simix_process_maxpid) {
+    while (current_process < MC_smx_get_maxpid()) {

       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
         partial_comm = 1;
       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
         partial_comm = 1;

diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c
index d2e80ba..9d6e02b 100644 (file)
--- a/src/simix/smx_process.c
+++ b/src/simix/smx_process.c
@@ -9,6 +9,7 @@
 #include "xbt/log.h"
 #include "xbt/dict.h"
 #include "mc/mc.h"
 #include "xbt/log.h"
 #include "xbt/dict.h"
 #include "mc/mc.h"

+#include "mc/mc_client.h"

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix,
                                 "Logging specific to SIMIX (process)");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix,
                                 "Logging specific to SIMIX (process)");