From 28d7faa60b9789a70d99c922e163c4aa7de363de Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 27 Apr 2015 14:44:13 +0200 Subject: [PATCH] [mc] Cleanup MC init code (split MCer and MCed init) --- src/mc/mc_base.cpp | 8 +-- src/mc/mc_global.cpp | 113 ++++++++++++---------------------- src/mc/mc_private.h | 2 +- src/mc/mc_process.cpp | 8 ++- src/mc/mc_smx.cpp | 14 +++-- src/mc/mc_smx.h | 2 +- src/mc/mcer_ignore.cpp | 5 -- src/mc/simgrid_mc.cpp | 2 +- src/simix/popping_generated.c | 5 -- src/simix/simcalls.py | 5 -- 10 files changed, 59 insertions(+), 105 deletions(-) diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 9144932640..d63ceef4d7 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -67,7 +67,7 @@ int MC_request_is_enabled(smx_simcall_t req) #ifdef HAVE_MC // Fetch from MCed memory: - if (!MC_process_is_self(&mc_model_checker->process())) { + if (mc_mode == MC_MODE_SERVER) { MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE, &temp_synchro, act, sizeof(temp_synchro), MC_PROCESS_INDEX_ANY); @@ -111,7 +111,7 @@ int MC_request_is_enabled(smx_simcall_t req) #ifdef HAVE_MC // Fetch from MCed memory: - if (!MC_process_is_self(&mc_model_checker->process())) { + if (mc_mode == MC_MODE_SERVER) { MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE, &temp_synchro, act, sizeof(temp_synchro), MC_PROCESS_INDEX_ANY); @@ -129,7 +129,7 @@ int MC_request_is_enabled(smx_simcall_t req) smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req); #ifdef HAVE_MC s_smx_mutex_t temp_mutex; - if (!MC_process_is_self(&mc_model_checker->process())) { + if (mc_mode == MC_MODE_SERVER) { MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE, &temp_mutex, mutex, sizeof(temp_mutex), MC_PROCESS_INDEX_ANY); @@ -210,7 +210,7 @@ void MC_simcall_handle(smx_simcall_t req, int value) #ifndef HAVE_MC SIMIX_simcall_handle(req, value); #else - if (MC_process_is_self(&mc_model_checker->process())) { + if (mc_mode == MC_MODE_CLIENT) { SIMIX_simcall_handle(req, value); return; } diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index ae886a48d8..3565626380 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -110,28 +110,24 @@ static void MC_init_dot_output() #ifdef HAVE_MC void MC_init() { - MC_init_pid(getpid(), -1); -} + mc_time = xbt_new0(double, simix_process_maxpid); -void MC_init_pid(pid_t pid, int socket) -{ - /* Initialize the data structures that must be persistent across every - iteration of the model-checker (in RAW memory) */ + if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination || mc_mode == MC_MODE_SERVER) { + /* Those requests are handled on the client side and propagated by message + * to the server: */ - xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - mc_model_checker = new simgrid::mc::ModelChecker(pid, socket); + MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); - // It's not useful anymore: - if (0 && mc_mode == MC_MODE_SERVER) { - unsigned long maxpid; - MC_process_read_variable(&mc_model_checker->process(), "simix_process_maxpid", - &maxpid, sizeof(maxpid)); - simix_process_maxpid = maxpid; + 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(std_heap); - mc_time = xbt_new0(double, MC_smx_get_maxpid()); - mmalloc_set_current_heap(mc_heap); +void MC_init_model_checker(pid_t pid, int socket) +{ + mc_model_checker = new simgrid::mc::ModelChecker(pid, socket); mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); @@ -145,62 +141,29 @@ void MC_init_pid(pid_t pid, int socket) /* Init parmap */ //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT); - mmalloc_set_current_heap(std_heap); - - if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination || mc_mode == MC_MODE_SERVER) { - /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ - MC_ignore_local_variable("e", "*"); - MC_ignore_local_variable("__ex_cleanup", "*"); - MC_ignore_local_variable("__ex_mctx_en", "*"); - MC_ignore_local_variable("__ex_mctx_me", "*"); - MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*"); - MC_ignore_local_variable("_log_ev", "*"); - MC_ignore_local_variable("_throw_ctx", "*"); - MC_ignore_local_variable("ctx", "*"); - - MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot"); - MC_ignore_local_variable("next_cont" - "ext", "smx_ctx_sysv_suspend_serial"); - MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial"); - - /* Ignore local variable about time used for tracing */ - MC_ignore_local_variable("start_time", "*"); - - /* Main MC state: */ - MCer_ignore_global_variable("mc_model_checker"); - MCer_ignore_global_variable("initial_communications_pattern"); - MCer_ignore_global_variable("incomplete_communications_pattern"); - MCer_ignore_global_variable("nb_comm_pattern"); - - /* MC __thread variables: */ - MCer_ignore_global_variable("mc_diff_info"); - MCer_ignore_global_variable("mc_comp_times"); - MCer_ignore_global_variable("mc_snapshot_comparison_time"); - - /* This MC state is used in MC replay as well: */ - MCer_ignore_global_variable("mc_time"); - - /* Static variable used for tracing */ - MCer_ignore_global_variable("counter"); - - /* SIMIX */ - MCer_ignore_global_variable("smx_total_comms"); - - if (mc_mode == MC_MODE_CLIENT) { - /* Those requests are handled on the client side and propagated by message - * to the server: */ - - 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); + /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ + MC_ignore_local_variable("e", "*"); + MC_ignore_local_variable("__ex_cleanup", "*"); + MC_ignore_local_variable("__ex_mctx_en", "*"); + MC_ignore_local_variable("__ex_mctx_me", "*"); + MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*"); + MC_ignore_local_variable("_log_ev", "*"); + MC_ignore_local_variable("_throw_ctx", "*"); + MC_ignore_local_variable("ctx", "*"); + + MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot"); + MC_ignore_local_variable("next_cont" + "ext", "smx_ctx_sysv_suspend_serial"); + MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial"); + + /* Ignore local variable about time used for tracing */ + MC_ignore_local_variable("start_time", "*"); + + /* Static variable used for tracing */ + MCer_ignore_global_variable("counter"); + + /* SIMIX */ + MCer_ignore_global_variable("smx_total_comms"); } #endif @@ -250,12 +213,12 @@ int MC_deadlock_check() smx_process_t process; if (xbt_swag_size(simix_global->process_list)) { deadlock = TRUE; - MC_EACH_SIMIX_PROCESS(process, + xbt_swag_foreach(process, simix_global->process_list) { if (MC_process_is_enabled(process)) { deadlock = FALSE; break; } - ); + } } return deadlock; } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 85e0f21878..c9ea7c2599 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -48,7 +48,7 @@ typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function * @param pid PID of the target process * @param socket FD for the communication socket **in server mode** (or -1 otherwise) */ -void MC_init_pid(pid_t pid, int socket); +void MC_init_model_checker(pid_t pid, int socket); extern FILE *dot_output; extern const char* colors[13]; diff --git a/src/mc/mc_process.cpp b/src/mc/mc_process.cpp index 5dbbddd211..40e9d03add 100644 --- a/src/mc/mc_process.cpp +++ b/src/mc/mc_process.cpp @@ -154,7 +154,8 @@ void MC_process_clear(mc_process_t process) void MC_process_refresh_heap(mc_process_t process) { - assert(!MC_process_is_self(process)); + xbt_assert(mc_mode == MC_MODE_SERVER); + xbt_assert(!MC_process_is_self(process)); // Read/dereference/refresh the std_heap pointer: if (!process->heap) { process->heap = (struct mdesc*) malloc(sizeof(struct mdesc)); @@ -163,11 +164,13 @@ void MC_process_refresh_heap(mc_process_t process) process->heap, process->heap_address, sizeof(struct mdesc), MC_PROCESS_INDEX_DISABLED ); + process->cache_flags |= MC_PROCESS_CACHE_FLAG_HEAP; } void MC_process_refresh_malloc_info(mc_process_t process) { - assert(!MC_process_is_self(process)); + xbt_assert(mc_mode == MC_MODE_SERVER); + xbt_assert(!MC_process_is_self(process)); if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP)) MC_process_refresh_heap(process); // Refresh process->heapinfo: @@ -178,6 +181,7 @@ void MC_process_refresh_malloc_info(mc_process_t process) process->heap_info, process->heap->heapinfo, malloc_info_bytesize, MC_PROCESS_INDEX_DISABLED); + process->cache_flags |= MC_PROCESS_CACHE_FLAG_MALLOC_INFO; } #define SO_RE "\\.so[\\.0-9]*$" diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp index b2039335c4..ab326898e6 100644 --- a/src/mc/mc_smx.cpp +++ b/src/mc/mc_smx.cpp @@ -86,6 +86,8 @@ static void MC_process_refresh_simix_process_list( void MC_process_smx_refresh(mc_process_t process) { + xbt_assert(mc_mode == MC_MODE_SERVER); + xbt_assert(!MC_process_is_self(process)); if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES) return; @@ -119,7 +121,7 @@ void MC_process_smx_refresh(mc_process_t process) */ smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req) { - if (MC_process_is_self(&mc_model_checker->process())) + if (mc_mode == MC_MODE_CLIENT) return req->issuer; MC_process_smx_refresh(&mc_model_checker->process()); @@ -145,7 +147,7 @@ smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address) { if (!process_remote_address) return NULL; - if (MC_process_is_self(&mc_model_checker->process())) + if (mc_mode == MC_MODE_CLIENT) return process_remote_address; mc_smx_process_info_t process_info = MC_smx_resolve_process_info(process_remote_address); @@ -157,7 +159,7 @@ smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address) mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address) { - if (MC_process_is_self(&mc_model_checker->process())) + if (mc_mode == MC_MODE_CLIENT) xbt_die("No process_info for local process is not enabled."); unsigned index; @@ -173,7 +175,7 @@ mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_a const char* MC_smx_process_get_host_name(smx_process_t p) { - if (MC_process_is_self(&mc_model_checker->process())) + if (mc_mode == MC_MODE_CLIENT) return SIMIX_host_get_name(p->smx_host); mc_process_t process = &mc_model_checker->process(); @@ -198,7 +200,7 @@ const char* MC_smx_process_get_host_name(smx_process_t p) const char* MC_smx_process_get_name(smx_process_t p) { mc_process_t process = &mc_model_checker->process(); - if (MC_process_is_self(process)) + if (mc_mode == MC_MODE_CLIENT) return p->name; if (!p->name) return NULL; @@ -212,7 +214,7 @@ const char* MC_smx_process_get_name(smx_process_t p) int MC_smpi_process_count(void) { - if (MC_process_is_self(&mc_model_checker->process())) + if (mc_mode == MC_MODE_CLIENT) return smpi_process_count(); else { int res; diff --git a/src/mc/mc_smx.h b/src/mc/mc_smx.h index 123052c50a..32b78cc569 100644 --- a/src/mc/mc_smx.h +++ b/src/mc/mc_smx.h @@ -68,7 +68,7 @@ const char* MC_smx_process_get_name(smx_process_t p); const char* MC_smx_process_get_host_name(smx_process_t p); #define MC_EACH_SIMIX_PROCESS(process, code) \ - if (MC_process_is_self(&mc_model_checker->process())) { \ + if (mc_mode == MC_MODE_CLIENT) { \ xbt_swag_foreach(process, simix_global->process_list) { \ code; \ } \ diff --git a/src/mc/mcer_ignore.cpp b/src/mc/mcer_ignore.cpp index 3e8b3bf870..54d2da2aec 100644 --- a/src/mc/mcer_ignore.cpp +++ b/src/mc/mcer_ignore.cpp @@ -112,7 +112,6 @@ void MC_heap_region_ignore_remove(void *address, size_t size) void MCer_ignore_global_variable(const char *name) { mc_process_t process = &mc_model_checker->process(); - xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); xbt_assert(process->object_infos, "MC subsystem not initialized"); size_t n = process->object_infos_size; @@ -138,7 +137,6 @@ void MCer_ignore_global_variable(const char *name) } } } - mmalloc_set_current_heap(heap); } // ***** Ignore local variables @@ -156,15 +154,12 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name) mc_process_t process = &mc_model_checker->process(); if (strcmp(frame_name, "*") == 0) frame_name = NULL; - xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); size_t n = process->object_infos_size; size_t i; for (i=0; i!=n; ++i) { MC_ignore_local_variable_in_object(var_name, frame_name, process->object_infos[i]); } - - mmalloc_set_current_heap(heap); } static void MC_ignore_local_variable_in_object(const char *var_name, diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index 29d5fe2093..f06240ef84 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -82,7 +82,7 @@ static int do_parent(int socket, pid_t child) mc_mode = MC_MODE_SERVER; mc_server = new s_mc_server(child, socket); mc_server->start(); - MC_init_pid(child, socket); + MC_init_model_checker(child, socket); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) MC_modelcheck_comm_determinism(); else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') diff --git a/src/simix/popping_generated.c b/src/simix/popping_generated.c index 9f8e55c92f..9b302ca10e 100644 --- a/src/simix/popping_generated.c +++ b/src/simix/popping_generated.c @@ -160,11 +160,6 @@ const char* simcall_names[] = { */ void SIMIX_simcall_handle(smx_simcall_t simcall, int value) { XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call)); - #ifdef HAVE_MC - if (mc_model_checker) { - MC_invalidate_cache(); - } - #endif SIMCALL_SET_MC_VALUE(simcall, value); if (simcall->issuer->context->iwannadie && simcall->call != SIMCALL_PROCESS_CLEANUP) return; diff --git a/src/simix/simcalls.py b/src/simix/simcalls.py index 997a60b67e..15d7c9991d 100755 --- a/src/simix/simcalls.py +++ b/src/simix/simcalls.py @@ -302,11 +302,6 @@ if __name__=='__main__': fd.write(' */\n'); fd.write('void SIMIX_simcall_handle(smx_simcall_t simcall, int value) {\n'); fd.write(' XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call));\n'); - fd.write(' #ifdef HAVE_MC\n'); - fd.write(' if (mc_model_checker) {\n'); - fd.write(' MC_invalidate_cache();\n'); - fd.write(' }\n'); - fd.write(' #endif\n'); fd.write(' SIMCALL_SET_MC_VALUE(simcall, value);\n'); fd.write(' if (simcall->issuer->context->iwannadie && simcall->call != SIMCALL_PROCESS_CLEANUP)\n'); fd.write(' return;\n'); -- 2.20.1