From 923896223efc203372ce0a7435cbdb7b539149f6 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 12 Mar 2015 13:37:55 +0100 Subject: [PATCH 1/1] [mc] Fetch simix_process_maxpid from MCed --- src/mc/mc_comm_determinism.c | 4 ++-- src/mc/mc_global.c | 19 ++++++++++++++----- src/mc/mc_model_checker.h | 7 +++++++ src/mc/mc_private.h | 1 + src/mc/mc_record.c | 2 +- src/mc/mc_state.c | 8 +++----- src/mc/mc_visited.c | 2 +- src/simix/smx_process.c | 1 + 8 files changed, 30 insertions(+), 14 deletions(-) diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index 635bc9d196..1017b33579 100644 --- 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); - for (i=0; ilist = 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; iprocess, "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); @@ -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: */ - 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)); } } + } 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; - for(int i=0; iincomplete_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) { - for (j=0; jindex_comm = 0; } diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h index 45790f35e5..0b07e8e71c 100644 --- 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); +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 diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index b5f061acd7..250c77f117 100644 --- 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 "mc_protocol.h" SG_BEGIN_DECL() diff --git a/src/mc/mc_record.c b/src/mc/mc_record.c index d57816899c..9d615b33c0 100644 --- 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() { - 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 bb53fa512d..0c079d5377 100644 --- 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); - for (i=0; imax_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; diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c index 77548d8330..941a780abd 100644 --- 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; - 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; diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c index d2e80ba4fe..9d6e02b71a 100644 --- 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 "mc/mc_client.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix, "Logging specific to SIMIX (process)"); -- 2.20.1