From: Gabriel Corona Date: Tue, 14 Apr 2015 12:02:51 +0000 (+0200) Subject: Merge branch 'master' into mc-process X-Git-Tag: v3_12~732^2~61 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/9932a0c0d2c44e34633c97a827b2b04d615cb4e9?hp=-c Merge branch 'master' into mc-process Conflicts: teshsuite/mc/replay/random_bug.c --- 9932a0c0d2c44e34633c97a827b2b04d615cb4e9 diff --combined buildtools/Cmake/CompleteInFiles.cmake index a8410adfb5,d15f1c6ad6..ff67e27e8b --- a/buildtools/Cmake/CompleteInFiles.cmake +++ b/buildtools/Cmake/CompleteInFiles.cmake @@@ -172,7 -172,6 +172,7 @@@ CHECK_FUNCTION_EXISTS(asprintf HAVE_ASP CHECK_FUNCTION_EXISTS(vasprintf HAVE_VASPRINTF) CHECK_FUNCTION_EXISTS(makecontext HAVE_MAKECONTEXT) CHECK_FUNCTION_EXISTS(mmap HAVE_MMAP) +CHECK_FUNCTION_EXISTS(process_vm_readv HAVE_PROCESS_VM_READV) #Check if __thread is defined execute_process( @@@ -208,13 -207,6 +208,6 @@@ endif( set(CONTEXT_UCONTEXT 0) SET(CONTEXT_THREADS 0) - SET(HAVE_TRACING 1) - - if(enable_tracing) - SET(HAVE_TRACING 1) - else() - SET(HAVE_TRACING 0) - endif() if(enable_jedule) SET(HAVE_JEDULE 1) diff --combined buildtools/Cmake/DefinePackages.cmake index ff3495096c,75b1d8aaad..15a6ec5c8f --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@@ -539,13 -539,8 +539,8 @@@ set(JTRACE_JAVA_SR src/bindings/java/org/simgrid/trace/Trace.java ) - if(HAVE_TRACING) - list(APPEND JMSG_C_SRC ${JTRACE_C_SRC}) - list(APPEND JMSG_JAVA_SRC ${JTRACE_JAVA_SRC}) - else() - list(APPEND EXTRA_DIST ${JTRACE_C_SRC}) - list(APPEND EXTRA_DIST ${JTRACE_JAVA_SRC}) - endif() + list(APPEND JMSG_C_SRC ${JTRACE_C_SRC}) + list(APPEND JMSG_JAVA_SRC ${JTRACE_JAVA_SRC}) set(LUA_SRC src/bindings/lua/lua_comm.c @@@ -573,10 -568,10 +568,10 @@@ set(TRACING_SR ) set(JEDULE_SRC - include/instr/jedule/jedule_events.h - include/instr/jedule/jedule_output.h - include/instr/jedule/jedule_platform.h - include/instr/jedule/jedule_sd_binding.h + include/simgrid/jedule/jedule_events.h + include/simgrid/jedule/jedule_output.h + include/simgrid/jedule/jedule_platform.h + include/simgrid/jedule/jedule_sd_binding.h src/instr/jedule/jedule_events.c src/instr/jedule/jedule_output.c src/instr/jedule/jedule_platform.c @@@ -593,19 -588,10 +588,19 @@@ set(MC_SRC_BAS ) set(MC_SRC + src/mc/mc_address_space.h + src/mc/mc_address_space.c src/mc/mc_forward.h + src/mc/mc_process.h + src/mc/mc_process.c + src/mc/mc_unw.h + src/mc/mc_unw.c + src/mc/mc_unw_vmread.c src/mc/mc_mmalloc.h src/mc/mc_model_checker.h + src/mc/mc_model_checker.c src/mc/mc_object_info.h + src/mc/mc_object_info.c src/mc/mc_checkpoint.c src/mc/mc_snapshot.h src/mc/mc_snapshot.c @@@ -613,7 -599,6 +608,7 @@@ 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 @@@ -642,26 -627,17 +637,29 @@@ src/mc/mc_visited.c src/mc/mc_memory_map.h src/mc/memory_map.c + src/mc/mc_client.c + src/mc/mc_client_api.c + src/mc/mc_client.h + src/mc/mc_protocol.h + src/mc/mc_protocol.c + src/mc/mc_server.cpp + src/mc/mc_server.h + src/mc/mc_smx.h + src/mc/mc_smx.c ) +set(MC_SIMGRID_MC_SRC + src/mc/simgrid_mc.cpp) + set(headers_to_install - include/instr/instr.h - include/msg/datatypes.h include/msg/msg.h - include/simdag/datatypes.h + include/msg/datatypes.h include/simdag/simdag.h + include/simdag/datatypes.h + + include/simgrid/instr.h + include/simgrid/msg.h + include/simgrid/simdag.h include/simgrid.h include/simgrid/datatypes.h include/simgrid/modelchecker.h @@@ -791,17 -767,10 +789,10 @@@ if(enable_smpi ) endif() - if(${HAVE_TRACING}) - set(simgrid_sources + set(simgrid_sources ${simgrid_sources} ${TRACING_SRC} ) - else() - set(EXTRA_DIST - ${EXTRA_DIST} - ${TRACING_SRC} - ) - endif() set(simgrid_sources ${simgrid_sources} diff --combined buildtools/Cmake/src/internal_config.h.in index 577178acd6,31589378e9..71ffdbd5c3 --- a/buildtools/Cmake/src/internal_config.h.in +++ b/buildtools/Cmake/src/internal_config.h.in @@@ -132,9 -132,6 +132,9 @@@ /* Define to 1 if mmap is available */ #cmakedefine HAVE_MMAP @HAVE_MMAP@ +/* Define to 1 if process_vm_readv is available */ +#cmakedefine HAVE_PROCESS_VM_READV @HAVE_PROCESS_VM_READV@ + /* Define to 1 if you have the `getdtablesize' function. */ #cmakedefine HAVE_GETDTABLESIZE @HAVE_GETDTABLESIZE@ @@@ -299,9 -296,6 +299,6 @@@ /* Define to 1 if you can safely include both and . */ #cmakedefine TIME_WITH_SYS_TIME @TIME_WITH_SYS_TIME@ - /* Tracing SimGrid */ - #cmakedefine HAVE_TRACING @HAVE_TRACING@ - /* Tracking of latency bound */ #cmakedefine HAVE_LATENCY_BOUND_TRACKING @HAVE_LATENCY_BOUND_TRACKING@ diff --combined examples/msg/mc/bugged1.c index 62539cd4c1,62539cd4c1..4a7aa9eb95 --- a/examples/msg/mc/bugged1.c +++ b/examples/msg/mc/bugged1.c @@@ -9,7 -9,7 +9,7 @@@ /* which is incorrect because the message ordering is non-deterministic */ /******************************************************************************/ --#include ++#include #include #define N 3 diff --combined examples/msg/mc/bugged1_liveness.c index 5a0d66b78a,50ad0ae3f4..b463bf9981 --- a/examples/msg/mc/bugged1_liveness.c +++ b/examples/msg/mc/bugged1_liveness.c @@@ -16,7 -16,7 +16,7 @@@ #include #endif - #include "msg/msg.h" + #include "simgrid/msg.h" #include "mc/mc.h" #include "xbt/automaton.h" #include "bugged1_liveness.h" @@@ -26,6 -26,14 +26,6 @@@ XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_li int r=0; int cs=0; -int predR(){ - return r; -} - -int predCS(){ - return cs; -} - #ifdef GARBAGE_STACK /** Do not use a clean stack */ static void garbage_stack(void) { @@@ -39,6 -47,7 +39,6 @@@ int coordinator(int argc, char *argv[]) { - int CS_used = 0; msg_task_t task = NULL, answer = NULL; xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); @@@ -150,21 -159,22 +150,21 @@@ static int raw_client(int argc, char *a int main(int argc, char *argv[]) { - MSG_init(&argc, argv); - char **options = &argv[1]; - MSG_config("model-check/property","promela_bugged1_liveness"); - MC_automaton_new_propositional_symbol("r", &predR); - MC_automaton_new_propositional_symbol("cs", &predCS); + MC_automaton_new_propositional_symbol_pointer("r", &r); + MC_automaton_new_propositional_symbol_pointer("cs", &cs); const char* platform_file = options[0]; const char* application_file = options[1]; - + MSG_create_environment(platform_file); + MSG_function_register("coordinator", coordinator); MSG_function_register("client", raw_client); MSG_launch_application(application_file); + MSG_main(); return 0; diff --combined examples/msg/mc/bugged2.c index 5d0e375af3,5d0e375af3..93bf21d89f --- a/examples/msg/mc/bugged2.c +++ b/examples/msg/mc/bugged2.c @@@ -9,7 -9,7 +9,7 @@@ /* which is incorrect because the message ordering is non-deterministic */ /******************************************************************************/ --#include ++#include #include #define N 3 diff --combined examples/msg/mc/bugged2_liveness.c index ee5519f272,3cdb50a211..51e572fc6f --- a/examples/msg/mc/bugged2_liveness.c +++ b/examples/msg/mc/bugged2_liveness.c @@@ -10,7 -10,7 +10,7 @@@ /* LTL property checked : !(GFcs) */ /******************************************************************************/ - #include "msg/msg.h" + #include "simgrid/msg.h" #include "mc/mc.h" #include "xbt/automaton.h" #include "bugged2_liveness.h" @@@ -19,6 -19,11 +19,6 @@@ XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, " int cs = 0; -int predCS(){ - return cs; -} - - int coordinator(int argc, char **argv); int client(int argc, char **argv); @@@ -97,7 -102,8 +97,7 @@@ int main(int argc, char *argv[] MSG_init(&argc, argv); - MSG_config("model-check/property","promela_bugged2_liveness"); - MC_automaton_new_propositional_symbol("cs", &predCS); + MC_automaton_new_propositional_symbol_pointer("cs", &cs); MSG_create_environment("../msg_platform.xml"); MSG_function_register("coordinator", coordinator); diff --combined examples/msg/mc/bugged3.c index 5f949c0d45,5f949c0d45..f7c1d26f98 --- a/examples/msg/mc/bugged3.c +++ b/examples/msg/mc/bugged3.c @@@ -13,7 -13,7 +13,7 @@@ /* same buffer for reception (task1). */ /******************************************************************************/ --#include ++#include #include XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "this example"); diff --combined examples/msg/mc/electric_fence.c index 0e031419ca,0e031419ca..a067724807 --- a/examples/msg/mc/electric_fence.c +++ b/examples/msg/mc/electric_fence.c @@@ -11,7 -11,7 +11,7 @@@ /* --cfg=model-check/max_depth:) is reached. */ /******************************************************************************/ --#include ++#include #include #define N 2 diff --combined src/mc/mc_base.c index b380bb3b16,2a587228ab..65052ef791 --- a/src/mc/mc_base.c +++ b/src/mc/mc_base.c @@@ -4,31 -4,19 +4,33 @@@ /* 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 + #include #include "mc_base.h" #include "../simix/smx_private.h" #include "mc_record.h" +#ifdef HAVE_MC +#include "mc_process.h" +#include "mc_model_checker.h" +#include "mc_protocol.h" +#include "mc_smx.h" +#include "mc_server.h" +#endif + XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); -/** - * \brief Schedules all the process that are ready to run - */ void MC_wait_for_requests(void) { ++#ifdef HAVE_MC + if (mc_mode == MC_MODE_SERVER) { + MC_server_wait_client(&mc_model_checker->process); + return; + } ++#endif + smx_process_t process; smx_simcall_t req; unsigned int iter; @@@ -47,9 -35,7 +49,9 @@@ int MC_request_is_enabled(smx_simcall_ { unsigned int index = 0; smx_synchro_t act = 0; - smx_mutex_t mutex = NULL; +#ifdef HAVE_MC + s_smx_synchro_t temp_synchro; +#endif switch (req->call) { case SIMCALL_NONE: @@@ -58,17 -44,6 +60,17 @@@ case SIMCALL_COMM_WAIT: /* FIXME: check also that src and dst processes are not suspended */ act = simcall_comm_wait__get__comm(req); + +#ifdef HAVE_MC + // Fetch from MCed memory: + if (!MC_process_is_self(&mc_model_checker->process)) { + MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG, + &temp_synchro, act, sizeof(temp_synchro), + MC_PROCESS_INDEX_ANY); + act = &temp_synchro; + } +#endif + if (simcall_comm_wait__get__timeout(req) >= 0) { /* If it has a timeout it will be always be enabled, because even if the * communication is not ready, it can timeout and won't block. */ @@@ -82,65 -57,19 +84,65 @@@ } return (act->comm.src_proc && act->comm.dst_proc); - case SIMCALL_COMM_WAITANY: - /* Check if it has at least one communication ready */ - xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) + case SIMCALL_COMM_WAITANY: { +#ifdef HAVE_MC + // Read dynar: + s_xbt_dynar_t comms; + MC_process_read_simple(&mc_model_checker->process, + &comms, simcall_comm_waitany__get__comms(req), sizeof(comms)); + // Read dynar buffer: + assert(comms.elmsize == sizeof(act)); + size_t buffer_size = comms.elmsize * comms.used; + char buffer[buffer_size]; + MC_process_read_simple(&mc_model_checker->process, + buffer, comms.data, sizeof(buffer)); +#endif + +#ifdef HAVE_MC + for (index = 0; index < comms.used; ++index) { + memcpy(&act, buffer + comms.elmsize * index, sizeof(act)); +#else + xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) { +#endif + +#ifdef HAVE_MC + // Fetch from MCed memory: + if (!MC_process_is_self(&mc_model_checker->process)) { + MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG, + &temp_synchro, act, sizeof(temp_synchro), + MC_PROCESS_INDEX_ANY); + act = &temp_synchro; + } +#endif + if (act->comm.src_proc && act->comm.dst_proc) return TRUE; + } return FALSE; + } - case SIMCALL_MUTEX_LOCK: - mutex = simcall_mutex_lock__get__mutex(req); + case SIMCALL_MUTEX_LOCK: { + 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)) { + MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG, + &temp_mutex, mutex, sizeof(temp_mutex), + MC_PROCESS_INDEX_ANY); + mutex = &temp_mutex; + } +#endif if(mutex->owner == NULL) return TRUE; else - return (mutex->owner->pid == req->issuer->pid); +#ifdef HAVE_MC + // TODO, *(mutex->owner) :/ + return MC_smx_resolve_process(mutex->owner)->pid == + MC_smx_resolve_process(req->issuer)->pid; +#else + return mutex->owner->pid == req->issuer->pid; +#endif + } default: /* The rest of the requests are always enabled */ diff --combined src/mc/mc_global.c index 8d498deacb,790d1e9b22..faf1eaf685 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@@ -4,16 -4,15 +4,16 @@@ /* 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 +#include +#include + #include "mc_base.h" #ifndef _XBT_WIN32 #include -#include #include #include -#include -#include #endif #include "simgrid/sg_config.h" @@@ -22,12 -21,11 +22,12 @@@ #include "xbt/fifo.h" #include "xbt/automaton.h" #include "xbt/dict.h" - #include "mc_server.h" ++#include "mc_record.h" #ifdef HAVE_MC -#define UNW_LOCAL_ONLY ++#include "mc_server.h" #include - +#include - #include "../xbt/mmalloc/mmprivate.h" #include "mc_object_info.h" #include "mc_comm_pattern.h" @@@ -37,18 -35,12 +37,18 @@@ #include "mc_snapshot.h" #include "mc_liveness.h" #include "mc_private.h" +#include "mc_unw.h" +#include "mc_smx.h" #endif #include "mc_record.h" +#include "mc_protocol.h" +#include "mc_client.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); +e_mc_mode_t mc_mode; + double *mc_time = NULL; #ifdef HAVE_MC @@@ -67,6 -59,14 +67,6 @@@ xbt_fifo_t mc_stack = NULL /* Liveness */ xbt_automaton_t _mc_property_automaton = NULL; -/* Variables */ -mc_object_info_t mc_libsimgrid_info = NULL; -mc_object_info_t mc_binary_info = NULL; - -mc_object_info_t mc_object_infos[2] = { NULL, NULL }; - -size_t mc_object_infos_size = 2; - /* Dot output */ FILE *dot_output = NULL; const char *colors[13]; @@@ -104,41 -104,57 +104,41 @@@ static void MC_init_dot_output( } -static void MC_init_debug_info(void) +void MC_init() { - XBT_INFO("Get debug information ..."); - - memory_map_t maps = MC_get_memory_map(); - - /* Get local variables for state equality detection */ - mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1); - mc_object_infos[0] = mc_binary_info; - - mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0); - mc_object_infos[1] = mc_libsimgrid_info; - - // Use information of the other objects: - MC_post_process_object_info(mc_binary_info); - MC_post_process_object_info(mc_libsimgrid_info); - - MC_free_memory_map(maps); - XBT_INFO("Get debug information done !"); + MC_init_pid(getpid(), -1); } - -mc_model_checker_t mc_model_checker = NULL; - -mc_model_checker_t MC_model_checker_new() +static void MC_init_mode(void) { - mc_model_checker_t mc = xbt_new0(s_mc_model_checker_t, 1); - mc->pages = mc_pages_store_new(); - mc->fd_clear_refs = -1; - mc->fd_pagemap = -1; - return mc; -} - -void MC_model_checker_delete(mc_model_checker_t mc) { - mc_pages_store_delete(mc->pages); - if(mc->record) - xbt_dynar_free(&mc->record); + if (mc_mode == MC_MODE_NONE) { + if (getenv(MC_ENV_SOCKET_FD)) { + mc_mode = MC_MODE_CLIENT; + } else { + mc_mode = MC_MODE_STANDALONE; + } + } } -void MC_init() +void MC_init_pid(pid_t pid, int socket) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - 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) */ - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + mc_model_checker = MC_model_checker_new(pid, socket); - mc_model_checker = MC_model_checker_new(); + // 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; + } + + 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); @@@ -146,6 -162,9 +146,6 @@@ mc_stats = xbt_new0(s_mc_stats_t, 1); mc_stats->state_size = 1; - MC_init_memory_map_info(); - MC_init_debug_info(); /* FIXME : get debug information only if liveness verification or visited state reduction */ - if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) MC_init_dot_output(); @@@ -154,7 -173,7 +154,7 @@@ MC_SET_STD_HEAP; - if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination) { + 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", "*"); @@@ -193,75 -212,143 +193,75 @@@ /* SIMIX */ MC_ignore_global_variable("smx_total_comms"); - MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); + if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) { + /* Those requests are handled on the client side and propagated by message + * to the server: */ - smx_process_t process; - xbt_swag_foreach(process, simix_global->process_list) { - MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); + 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)); + } } - } - if (raw_mem_set) - MC_SET_MC_HEAP; + } + mmalloc_set_current_heap(heap); } /******************************* Core of MC *******************************/ /**************************************************************************/ -static void MC_modelcheck_comm_determinism_init(void) -{ - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_init(); - - if (!mc_mem_set) - MC_SET_MC_HEAP; - - /* Create exploration stack */ - mc_stack = xbt_fifo_new(); - - MC_SET_STD_HEAP; - - MC_pre_modelcheck_comm_determinism(); - - MC_SET_MC_HEAP; - initial_global_state = xbt_new0(s_mc_global_t, 1); - initial_global_state->snapshot = MC_take_snapshot(0); - initial_global_state->initial_communications_pattern_done = 0; - initial_global_state->recv_deterministic = 1; - initial_global_state->send_deterministic = 1; - initial_global_state->recv_diff = NULL; - initial_global_state->send_diff = NULL; - - MC_SET_STD_HEAP; - - MC_modelcheck_comm_determinism(); - - if(mc_mem_set) - MC_SET_MC_HEAP; - -} - -static void MC_modelcheck_safety_init(void) -{ - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - _sg_mc_safety = 1; - - MC_init(); - - if (!mc_mem_set) - MC_SET_MC_HEAP; - - /* Create exploration stack */ - mc_stack = xbt_fifo_new(); - - MC_SET_STD_HEAP; - - MC_pre_modelcheck_safety(); - - MC_SET_MC_HEAP; - /* Save the initial state */ - initial_global_state = xbt_new0(s_mc_global_t, 1); - initial_global_state->snapshot = MC_take_snapshot(0); - MC_SET_STD_HEAP; - - MC_modelcheck_safety(); - - if (mc_mem_set) - MC_SET_MC_HEAP; - - xbt_abort(); - //MC_exit(); -} - -static void MC_modelcheck_liveness_init() -{ - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - _sg_mc_liveness = 1; - - MC_init(); - - if (!mc_mem_set) - MC_SET_MC_HEAP; - - /* Create exploration stack */ - mc_stack = xbt_fifo_new(); - - /* Create the initial state */ - initial_global_state = xbt_new0(s_mc_global_t, 1); - - MC_SET_STD_HEAP; - - MC_pre_modelcheck_liveness(); - - /* We're done */ - MC_print_statistics(mc_stats); - xbt_free(mc_time); - - if (mc_mem_set) - MC_SET_MC_HEAP; - -} - void MC_do_the_modelcheck_for_real() { + MC_init_mode(); + + switch(mc_mode) { + default: + xbt_die("Unexpected mc mode"); + break; + case MC_MODE_CLIENT: + MC_init(); + MC_client_main_loop(); + return; + case MC_MODE_SERVER: + break; + case MC_MODE_STANDALONE: + MC_init(); + break; + } if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { XBT_INFO("Check communication determinism"); mc_reduce_kind = e_mc_reduce_none; - MC_modelcheck_comm_determinism_init(); - } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') { - if(_sg_mc_termination){ - XBT_INFO("Check non progressive cycles"); + MC_wait_for_requests(); + MC_modelcheck_comm_determinism(); + } + + else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') { + if(_sg_mc_termination) mc_reduce_kind = e_mc_reduce_none; - }else{ + else if (mc_reduce_kind == e_mc_reduce_unset) + mc_reduce_kind = e_mc_reduce_dpor; + _sg_mc_safety = 1; + if (_sg_mc_termination) + XBT_INFO("Check non progressive cycles"); + else XBT_INFO("Check a safety property"); - } - MC_modelcheck_safety_init(); - } else { + MC_wait_for_requests(); + MC_modelcheck_safety(); + } + + else { if (mc_reduce_kind == e_mc_reduce_unset) mc_reduce_kind = e_mc_reduce_none; XBT_INFO("Check the liveness property %s", _sg_mc_property_file); MC_automaton_load(_sg_mc_property_file); - MC_modelcheck_liveness_init(); + MC_wait_for_requests(); + MC_modelcheck_liveness(); } + } @@@ -275,41 -362,84 +275,41 @@@ void MC_exit(void int MC_deadlock_check() { + if (mc_mode == MC_MODE_SERVER) { + int res; + if ((res = MC_protocol_send_simple_message(mc_model_checker->process.socket, + MC_MESSAGE_DEADLOCK_CHECK))) + xbt_die("Could not check deadlock state"); + s_mc_int_message_t message; + ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message), 0); + if (s == -1) + xbt_die("Could not receive message"); + else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) { + xbt_die("%s received unexpected message %s (%i, size=%i) " + "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)", + MC_mode_name(mc_mode), + MC_message_type_name(message.type), (int) message.type, (int) s, + (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message) + ); + } + else + return message.value; + } + int deadlock = FALSE; smx_process_t process; if (xbt_swag_size(simix_global->process_list)) { deadlock = TRUE; - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_request_is_enabled(&process->simcall)) { + MC_EACH_SIMIX_PROCESS(process, + if (MC_process_is_enabled(process)) { deadlock = FALSE; break; } - } + ); } return deadlock; } -void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) { - - switch(call_type) { - case MC_CALL_TYPE_NONE: - break; - case MC_CALL_TYPE_SEND: - case MC_CALL_TYPE_RECV: - get_comm_pattern(pattern, req, call_type, backtracking); - break; - case MC_CALL_TYPE_WAIT: - case MC_CALL_TYPE_WAITANY: - { - smx_synchro_t current_comm = NULL; - if (call_type == MC_CALL_TYPE_WAIT) - current_comm = simcall_comm_wait__get__comm(req); - else - current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t); - complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking); - } - break; - default: - xbt_die("Unexpected call type %i", (int)call_type); - } - -} - -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; iincomplete_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, ©_comm); - } - } -} - /** * \brief Re-executes from the state at position start all the transitions indicated by * a given model-checker stack. @@@ -318,7 -448,7 +318,7 @@@ */ void MC_replay(xbt_fifo_t stack) { - int raw_mem = (mmalloc_get_current_heap() == mc_heap); + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int value, count = 1, j; char *req_str; @@@ -353,13 -483,9 +353,13 @@@ MC_SET_MC_HEAP; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - for (j=0; jindex_comm = 0; + xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t)->index_comm = 0; } } @@@ -376,13 -502,11 +376,13 @@@ if (saved_req) { /* because we got a copy of the executed request, we have to fetch the real one, pointed by the request field of the issuer process */ - req = &saved_req->issuer->simcall; + + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + req = &issuer->simcall; /* Debug information */ if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { - req_str = MC_request_to_string(req, value); + req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX); XBT_DEBUG("Replay: %s (%p)", req_str, state); xbt_free(req_str); } @@@ -390,15 -514,15 +390,15 @@@ /* TODO : handle test and testany simcalls */ e_mc_call_type_t call = MC_CALL_TYPE_NONE; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - call = mc_get_call_type(req); + call = MC_get_call_type(req); - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); MC_SET_MC_HEAP; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - handle_comm_pattern(call, req, value, NULL, 1); + MC_handle_comm_pattern(call, req, value, NULL, 1); MC_SET_STD_HEAP; - + MC_wait_for_requests(); count++; @@@ -411,7 -535,13 +411,7 @@@ } XBT_DEBUG("**** End Replay ****"); - - if (raw_mem) - MC_SET_MC_HEAP; - else - MC_SET_STD_HEAP; - - + mmalloc_set_current_heap(heap); } void MC_replay_liveness(xbt_fifo_t stack) @@@ -463,19 -593,18 +463,19 @@@ if (saved_req != NULL) { /* because we got a copy of the executed request, we have to fetch the real one, pointed by the request field of the issuer process */ - req = &saved_req->issuer->simcall; + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + req = &issuer->simcall; /* Debug information */ if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { - req_str = MC_request_to_string(req, value); + req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX); XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); xbt_free(req_str); } } - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); MC_wait_for_requests(); } @@@ -503,7 -632,8 +503,7 @@@ */ void MC_dump_stack_safety(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); MC_show_stack_safety(stack); @@@ -512,13 -642,22 +512,13 @@@ MC_SET_MC_HEAP; while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) MC_state_delete(state, !state->in_visited_states ? 1 : 0); - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - else - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); } void MC_show_stack_safety(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int value; mc_state_t state; @@@ -531,13 -670,14 +531,13 @@@ : (NULL)); item = xbt_fifo_get_prev_item(item)) { req = MC_state_get_executed_request(state, &value); if (req) { - req_str = MC_request_to_string(req, value); + req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED); XBT_INFO("%s", req_str); xbt_free(req_str); } } - if (!raw_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } void MC_show_deadlock(smx_simcall_t req) @@@ -578,7 -718,7 +578,7 @@@ void MC_show_stack_liveness(xbt_fifo_t item = xbt_fifo_get_prev_item(item)) { req = MC_state_get_executed_request(pair->graph_state, &value); if (req && req->call != SIMCALL_NONE) { - req_str = MC_request_to_string(req, value); + req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED); XBT_INFO("%s", req_str); xbt_free(req_str); } @@@ -588,15 -728,25 +588,15 @@@ void MC_dump_stack_liveness(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); mc_pair_t pair; - - MC_SET_MC_HEAP; while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL) MC_pair_delete(pair); - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - + mmalloc_set_current_heap(heap); } void MC_print_statistics(mc_stats_t stats) { - xbt_mheap_t previous_heap = mmalloc_get_current_heap(); - if(_sg_mc_comms_determinism) { if (!initial_global_state->recv_deterministic && initial_global_state->send_deterministic){ XBT_INFO("******************************************************"); @@@ -610,7 -760,6 +610,7 @@@ XBT_INFO("%s", initial_global_state->send_diff); } } + if (stats->expanded_pairs == 0) { XBT_INFO("Expanded states = %lu", stats->expanded_states); XBT_INFO("Visited states = %lu", stats->visited_states); @@@ -619,7 -768,7 +619,7 @@@ XBT_INFO("Visited pairs = %lu", stats->visited_pairs); } XBT_INFO("Executed transitions = %lu", stats->executed_transitions); - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) { fprintf(dot_output, "}\n"); fclose(dot_output); @@@ -629,74 -778,70 +629,74 @@@ if (_sg_mc_comms_determinism) XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes"); } - mmalloc_set_current_heap(previous_heap); -} - -void MC_assert(int prop) -{ - if (MC_is_active() && !prop) { - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - MC_record_dump_path(mc_stack); - MC_dump_stack_safety(mc_stack); - MC_print_statistics(mc_stats); - xbt_abort(); - } -} - -void MC_cut(void) -{ - user_max_depth_reached = 1; + mmalloc_set_current_heap(heap); } void MC_automaton_load(const char *file) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); xbt_automaton_load(_mc_property_automaton, file); - - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - + mmalloc_set_current_heap(heap); } -void MC_automaton_new_propositional_symbol(const char *id, void *fct) +static void register_symbol(xbt_automaton_propositional_symbol_t symbol) { + if (mc_mode != MC_MODE_CLIENT) + return; + s_mc_register_symbol_message_t message; + message.type = MC_MESSAGE_REGISTER_SYMBOL; + const char* name = xbt_automaton_propositional_symbol_get_name(symbol); + if (strlen(name) + 1 > sizeof(message.name)) + xbt_die("Symbol is too long"); + strncpy(message.name, name, sizeof(message.name)); + message.callback = xbt_automaton_propositional_symbol_get_callback(symbol); + message.data = xbt_automaton_propositional_symbol_get_data(symbol); + MC_client_send_message(&message, sizeof(message)); +} - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; +void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); - xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct); - - MC_SET_STD_HEAP; + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct); + register_symbol(symbol); + mmalloc_set_current_heap(heap); +} - if (raw_mem_set) - MC_SET_MC_HEAP; +void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + if (_mc_property_automaton == NULL) + _mc_property_automaton = xbt_automaton_new(); + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value); + register_symbol(symbol); + mmalloc_set_current_heap(heap); +} +void MC_automaton_new_propositional_symbol_callback(const char* id, + xbt_automaton_propositional_symbol_callback_type callback, + void* data, xbt_automaton_propositional_symbol_free_function_type free_function) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + if (_mc_property_automaton == NULL) + _mc_property_automaton = xbt_automaton_new(); + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_callback( + _mc_property_automaton, id, callback, data, free_function); + register_symbol(symbol); + mmalloc_set_current_heap(heap); } +// TODO, fix cross-process access (this function is not used) void MC_dump_stacks(FILE* file) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int nstack = 0; stack_region_t current_stack; @@@ -712,22 -857,15 +712,22 @@@ unw_word_t off; do { const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?"; +#if defined(__x86_64__) + unw_word_t rip = 0; + unw_word_t rsp = 0; + unw_get_reg(&c, UNW_X86_64_RIP, &rip); + unw_get_reg(&c, UNW_X86_64_RSP, &rsp); + fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n", + nframe, name, rip, rsp); +#else fprintf(file, " %i: %s\n", nframe, name); +#endif ++nframe; } while(unw_step(&c)); ++nstack; } - - if (raw_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); } #endif @@@ -747,14 -885,3 +747,16 @@@ void MC_process_clock_add(smx_process_ { mc_time[process->pid] += amount; } + ++#ifdef HAVE_MC +void MC_report_assertion_error(void) +{ + XBT_INFO("**************************"); + XBT_INFO("*** PROPERTY NOT VALID ***"); + XBT_INFO("**************************"); + XBT_INFO("Counter-example execution trace:"); + MC_record_dump_path(mc_stack); + MC_dump_stack_safety(mc_stack); + MC_print_statistics(mc_stats); +} ++#endif diff --combined src/mc/mc_private.h index fed2f4d562,997aca035a..c19aa1fac7 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@@ -7,8 -7,6 +7,8 @@@ #ifndef MC_PRIVATE_H #define MC_PRIVATE_H +#include + #include "simgrid_config.h" #include #include @@@ -23,34 -21,29 +23,33 @@@ #include "mc/datatypes.h" #include "xbt/fifo.h" #include "xbt/config.h" + #include "xbt/function_types.h" #include "xbt/mmalloc.h" #include "../simix/smx_private.h" #include "../xbt/mmalloc/mmprivate.h" #include "xbt/automaton.h" #include "xbt/hash.h" - #include "msg/msg.h" -#include "simgrid/msg.h" --#include "msg/datatypes.h" ++#include #include "xbt/strbuff.h" #include "xbt/parmap.h" #include "mc_forward.h" +#include "mc_protocol.h" SG_BEGIN_DECL() typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function_index_item_t; -/****************************** Snapshots ***********************************/ - -extern xbt_dynar_t mc_checkpoint_ignore; - /********************************* MC Global **********************************/ +/** Initialisation of the model-checker + * + * @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); + extern FILE *dot_output; extern const char* colors[13]; extern xbt_parmap_t parmap; @@@ -90,13 -83,16 +89,13 @@@ extern mc_stats_t mc_stats void MC_print_statistics(mc_stats_t stats); -extern char *libsimgrid_path; - /********************************** Snapshot comparison **********************************/ typedef struct s_mc_comparison_times{ double nb_processes_comparison_time; double bytes_used_comparison_time; double stacks_sizes_comparison_time; - double binary_global_variables_comparison_time; - double libsimgrid_global_variables_comparison_time; + double global_variables_comparison_time; double heap_comparison_time; double stacks_comparison_time; }s_mc_comparison_times_t, *mc_comparison_times_t; @@@ -112,6 -108,9 +111,6 @@@ void print_comparison_times(void) /********************************** Variables with DWARF **********************************/ -dw_frame_t MC_find_function_by_ip(void* ip); -mc_object_info_t MC_ip_find_object_info(void* ip); - void MC_find_object_address(memory_map_t maps, mc_object_info_t result); /********************************** Miscellaneous **********************************/ @@@ -152,8 -151,6 +151,8 @@@ uint64_t mc_hash_processes_state(int nu */ void MC_dump_stacks(FILE* file); +void MC_report_assertion_error(void); + SG_END_DECL() #endif diff --combined src/mc/mc_process.h index 8159b3e700,0000000000..5e2175c716 mode 100644,000000..100644 --- a/src/mc/mc_process.h +++ b/src/mc/mc_process.h @@@ -1,215 -1,0 +1,218 @@@ +/* Copyright (c) 2008-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. */ + +#ifndef MC_PROCESS_H +#define MC_PROCESS_H + +#include +#include + +#include "simgrid_config.h" + +#include + +#include ++ ++#ifdef HAVE_MC +#include "xbt/mmalloc/mmprivate.h" ++#endif + +#include "simix/popping_private.h" +#include "simix/smx_private.h" + +#include "mc_forward.h" +#include "mc_mmalloc.h" // std_heap +#include "mc_memory_map.h" +#include "mc_address_space.h" +#include "mc_protocol.h" + +SG_BEGIN_DECL() + +int MC_process_vm_open(pid_t pid, int flags); + +typedef enum { + MC_PROCESS_NO_FLAG = 0, + MC_PROCESS_SELF_FLAG = 1, +} e_mc_process_flags_t; + +// Those flags are used to track down which cached information +// is still up to date and which information needs to be updated. +typedef enum { + MC_PROCESS_CACHE_FLAG_HEAP = 1, + MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2, + MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4, +} e_mc_process_cache_flags_t ; + +typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t; + +/** Representation of a process + */ +struct s_mc_process { + s_mc_address_space_t address_space; + e_mc_process_flags_t process_flags; + pid_t pid; + int socket; + int status; + bool running; + memory_map_t memory_map; + void *maestro_stack_start, *maestro_stack_end; + mc_object_info_t libsimgrid_info; + mc_object_info_t binary_info; + mc_object_info_t* object_infos; + size_t object_infos_size; + int memory_file; + + /** Copy of `simix_global->process_list` + * + * See mc_smx.c. + */ + xbt_dynar_t smx_process_infos; + + /** Copy of `simix_global->process_to_destroy` + * + * See mc_smx.c. + */ + xbt_dynar_t smx_old_process_infos; + + /** State of the cache (which variables are up to date) */ + e_mc_process_cache_flags_t cache_flags; + + /** Address of the heap structure in the MCed process. */ + void* heap_address; + + /** Copy of the heap structure of the process + * + * This is refreshed with the `MC_process_refresh` call. + * This is not used if the process is the current one: + * use `MC_process_get_heap_info` in order to use it. + */ + xbt_mheap_t heap; + + /** Copy of the allocation info structure + * + * This is refreshed with the `MC_process_refresh` call. + * This is not used if the process is the current one: + * use `MC_process_get_malloc_info` in order to use it. + */ + malloc_info* heap_info; + + // ***** Libunwind-data + + /** Full-featured MC-aware libunwind address space for the process + * + * This address space is using a mc_unw_context_t + * (with mc_process_t/mc_address_space_t and unw_context_t). + */ + unw_addr_space_t unw_addr_space; + + /** Underlying libunwind addres-space + * + * The `find_proc_info`, `put_unwind_info`, `get_dyn_info_list_addr` + * operations of the native MC address space is currently delegated + * to this address space (either the local or a ptrace unwinder). + */ + unw_addr_space_t unw_underlying_addr_space; + + /** The corresponding context + */ + void* unw_underlying_context; + + xbt_dynar_t checkpoint_ignore; +}; + +bool MC_is_process(mc_address_space_t p); + +void MC_process_init(mc_process_t process, pid_t pid, int sockfd); +void MC_process_clear(mc_process_t process); + +/** Refresh the information about the process + * + * Do not use direclty, this is used by the getters when appropriate + * in order to have fresh data. + */ +void MC_process_refresh_heap(mc_process_t process); + +/** Refresh the information about the process + * + * Do not use direclty, this is used by the getters when appropriate + * in order to have fresh data. + * */ +void MC_process_refresh_malloc_info(mc_process_t process); + +static inline +bool MC_process_is_self(mc_process_t process) +{ + return process->process_flags & MC_PROCESS_SELF_FLAG; +} + +/* Process memory access: */ + +/** Read data from a process memory + * + * @param process the process + * @param local local memory address (destination) + * @param remote target process memory address (source) + * @param len data size + */ +const void* MC_process_read(mc_process_t process, + e_adress_space_read_flags_t flags, + void* local, const void* remote, size_t len, + int process_index); + +// Simplified versions/wrappers (whould be moved in mc_address_space): +const void* MC_process_read_simple(mc_process_t process, + void* local, const void* remote, size_t len); +const void* MC_process_read_dynar_element(mc_process_t process, + void* local, const void* remote_dynar, size_t i, size_t len); +unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar); + +/** Write data to a process memory + * + * @param process the process + * @param local local memory address (source) + * @param remote target process memory address (target) + * @param len data size + */ +void MC_process_write(mc_process_t process, const void* local, void* remote, size_t len); + +void MC_process_clear_memory(mc_process_t process, void* remote, size_t len); + +/* Functions, variables of the process: */ + +mc_object_info_t MC_process_find_object_info(mc_process_t process, const void* addr); +mc_object_info_t MC_process_find_object_info_exec(mc_process_t process, const void* addr); +mc_object_info_t MC_process_find_object_info_rw(mc_process_t process, const void* addr); + +dw_frame_t MC_process_find_function(mc_process_t process, const void* ip); + +void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size); +char* MC_process_read_string(mc_process_t, void* address); + +static inline xbt_mheap_t MC_process_get_heap(mc_process_t process) +{ + if (MC_process_is_self(process)) + return std_heap; + if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP)) + MC_process_refresh_heap(process); + return process->heap; +} + +static inline malloc_info* MC_process_get_malloc_info(mc_process_t process) +{ + if (MC_process_is_self(process)) + return std_heap->heapinfo; + if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_MALLOC_INFO)) + MC_process_refresh_malloc_info(process); + return process->heap_info; +} + +/** Find (one occurence of) the named variable definition + */ +dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name); + +SG_END_DECL() + +#endif diff --combined src/mc/mc_record.c index 9d615b33c0,d9d79e1de8..d57816899c --- a/src/mc/mc_record.c +++ b/src/mc/mc_record.c @@@ -17,7 -17,6 +17,7 @@@ #include "mc_private.h" #include "mc_model_checker.h" #include "mc_state.h" +#include "mc_smx.h" #endif XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, @@@ -109,8 -108,7 +109,8 @@@ char* MC_record_stack_to_string(xbt_fif mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item); int value = 0; smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); - int pid = saved_req->issuer->pid; + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + const int pid = issuer->pid; // Serialization the (pid, value) pair: const char* sep = (item!=start) ? ";" : ""; @@@ -144,5 -142,5 +144,5 @@@ void MC_record_replay_from_string(cons void MC_record_replay_init() { - mc_time = xbt_new0(double, MC_smx_get_maxpid()); + mc_time = xbt_new0(double, simix_process_maxpid); } diff --combined src/msg/msg_mailbox.c index d7ae79962d,cffff60504..4a3f158d79 --- a/src/msg/msg_mailbox.c +++ b/src/msg/msg_mailbox.c @@@ -116,10 -116,8 +116,8 @@@ MSG_mailbox_get_task_ext_bounded(msg_ma if (host) THROW_UNIMPLEMENTED; - #ifdef HAVE_TRACING TRACE_msg_task_get_start(); double start_time = MSG_get_clock(); - #endif /* Sanity check */ xbt_assert(task, "Null pointer for the task storage"); @@@ -153,13 -151,11 +151,11 @@@ xbt_ex_free(e); } - #ifdef HAVE_TRACING if (ret != MSG_HOST_FAILURE && ret != MSG_TRANSFER_FAILURE && ret != MSG_TIMEOUT) { TRACE_msg_task_get_end(start_time, *task); } - #endif MSG_RETURN(ret); } @@@ -167,14 -163,13 +163,12 @@@ msg_error_ MSG_mailbox_put_with_timeout(msg_mailbox_t mailbox, msg_task_t task, double timeout) { - xbt_ex_t e; msg_error_t ret = MSG_OK; simdata_task_t t_simdata = NULL; msg_process_t process = MSG_process_self(); simdata_process_t p_simdata = SIMIX_process_self_get_data(process); - #ifdef HAVE_TRACING int call_end = TRACE_msg_task_put_start(task); //must be after CHECK_HOST() - #endif /* Prepare the task to send */ t_simdata = task->simdata; @@@ -203,18 -198,14 +197,15 @@@ p_simdata->waiting_task = task; + xbt_ex_t e; /* Try to send it by calling SIMIX network layer */ TRY { smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simix call */ - comm = simcall_comm_isend(SIMIX_process_self(), mailbox,t_simdata->message_size, + comm = simcall_comm_isend(SIMIX_process_self(), mailbox,t_simdata->bytes_amount, t_simdata->rate, task, sizeof(void *), NULL, NULL, NULL, task, 0); - #ifdef HAVE_TRACING - if (TRACE_is_enabled()) { + if (TRACE_is_enabled()) simcall_set_category(comm, task->category); - } - #endif t_simdata->comm = comm; simcall_comm_wait(comm, timeout); } @@@ -243,10 -234,8 +234,8 @@@ p_simdata->waiting_task = NULL; - #ifdef HAVE_TRACING if (call_end) TRACE_msg_task_put_end(); - #endif MSG_RETURN(ret); } diff --combined src/simgrid/sg_config.c index e753e76ec4,ac0f9bb8a2..ad2bbb84ee --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@@ -21,7 -21,7 +21,7 @@@ #include "smpi/smpi_interface.h" #include "mc/mc.h" #include "mc/mc_record.h" - #include "instr/instr.h" + #include "simgrid/instr.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_config, surf, "About the configuration of simgrid"); @@@ -70,10 -70,8 +70,8 @@@ static void sg_config_cmd_line(int *arg "to the command line.\n" "\n" "You can also use --help-models to see the details of all models known by this simulator.\n" - #ifdef HAVE_TRACING "\n" "You can also use --help-tracing to see the details of all tracing options known by this simulator.\n" - #endif "\n" "You can also use --help-logs and --help-log-categories to see the details of logging output.\n" "\n" @@@ -96,11 -94,9 +94,9 @@@ surf_optimization_mode_description[k].description); printf("Both network and CPU models have 'Lazy' as default optimization level\n\n"); shall_exit = 1; - #ifdef HAVE_TRACING } else if (!strcmp(argv[i], "--help-tracing")) { TRACE_help (1); shall_exit = 1; - #endif } else { argv[j++] = argv[i]; } @@@ -695,12 -691,6 +691,12 @@@ void sg_config_init(int *argc, char **a xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_hash, NULL); xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no"); + /* Set max depth exploration */ + xbt_cfg_register(&_sg_cfg_set, "model-check/snapshot_fds", + "Whether file descriptors must be snapshoted", + xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_snapshot_fds, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/snapshot_fds", "no"); + /* Set max depth exploration */ xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth", "Specify the max depth of exploration (default : 1000)", diff --combined src/simix/popping_generated.c index 69806ac5df,fb72a40b29..c8a3c3ca97 --- a/src/simix/popping_generated.c +++ b/src/simix/popping_generated.c @@@ -15,8 -15,6 +15,8 @@@ #include "smx_private.h" #ifdef HAVE_MC +#include "mc/mc_process.h" +#include "mc/mc_model_checker.h" #endif XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping); @@@ -142,14 -140,11 +142,11 @@@ const char* simcall_names[] = [SIMCALL_STORAGE_GET_CONTENT] = "SIMCALL_STORAGE_GET_CONTENT", [SIMCALL_ASR_GET_PROPERTIES] = "SIMCALL_ASR_GET_PROPERTIES", [SIMCALL_MC_RANDOM] = "SIMCALL_MC_RANDOM", + [SIMCALL_SET_CATEGORY] = "SIMCALL_SET_CATEGORY", #ifdef HAVE_LATENCY_BOUND_TRACKING [SIMCALL_COMM_IS_LATENCY_BOUNDED] = "SIMCALL_COMM_IS_LATENCY_BOUNDED", #endif - #ifdef HAVE_TRACING - [SIMCALL_SET_CATEGORY] = "SIMCALL_SET_CATEGORY", - #endif - #ifdef HAVE_MC [SIMCALL_MC_SNAPSHOT] = "SIMCALL_MC_SNAPSHOT", [SIMCALL_MC_COMPARE_SNAPSHOTS] = "SIMCALL_MC_COMPARE_SNAPSHOTS", @@@ -164,11 -159,6 +161,11 @@@ */ 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_model_checker->process.cache_flags = 0; + } + #endif SIMCALL_SET_MC_VALUE(simcall, value); if (simcall->issuer->context->iwannadie && simcall->call != SIMCALL_PROCESS_CLEANUP) return; @@@ -749,17 -739,14 +746,14 @@@ case SIMCALL_MC_RANDOM SIMIX_simcall_answer(simcall); break; - #ifdef HAVE_LATENCY_BOUND_TRACKING - case SIMCALL_COMM_IS_LATENCY_BOUNDED: - simcall->result.i = SIMIX_comm_is_latency_bounded((smx_synchro_t) simcall->args[0].dp); + case SIMCALL_SET_CATEGORY: + SIMIX_set_category((smx_synchro_t) simcall->args[0].dp, simcall->args[1].cc); SIMIX_simcall_answer(simcall); break; - #endif - - #ifdef HAVE_TRACING - case SIMCALL_SET_CATEGORY: - SIMIX_set_category((smx_synchro_t) simcall->args[0].dp, simcall->args[1].cc); + #ifdef HAVE_LATENCY_BOUND_TRACKING + case SIMCALL_COMM_IS_LATENCY_BOUNDED: + simcall->result.i = SIMIX_comm_is_latency_bounded((smx_synchro_t) simcall->args[0].dp); SIMIX_simcall_answer(simcall); break; diff --combined src/simix/smx_global.c index fd7b9d93af,43e7f830ea..0011f977f2 --- a/src/simix/smx_global.c +++ b/src/simix/smx_global.c @@@ -4,8 -4,6 +4,8 @@@ /* 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 + #include "smx_private.h" #include "xbt/heap.h" #include "xbt/sysdep.h" @@@ -17,9 -15,6 +17,9 @@@ #ifdef HAVE_MC #include "mc/mc_private.h" +#include "mc/mc_model_checker.h" +#include "mc/mc_protocol.h" +#include "mc/mc_client.h" #endif #include "mc/mc_record.h" @@@ -211,21 -206,6 +211,21 @@@ void SIMIX_global_init(int *argc, char if (sg_cfg_get_boolean("clean_atexit")) atexit(SIMIX_clean); +#ifdef HAVE_MC + // The communication initialisation is done ASAP. + // We need to commuicate initialisation of the different layers to the model-checker. + if (mc_mode == MC_MODE_NONE) { + if (getenv(MC_ENV_SOCKET_FD)) { + mc_mode = MC_MODE_CLIENT; + MC_client_init(); + MC_client_hello(); + MC_client_handle_messages(); + } else { + mc_mode = MC_MODE_STANDALONE; + } + } +#endif + if (_sg_cfg_exit_asap) exit(0); } @@@ -424,12 -404,30 +424,30 @@@ void SIMIX_run(void SIMIX_simcall_handle(&process->simcall, 0); } } + /* Wake up all processes waiting for a Surf action to finish */ + xbt_dynar_foreach(model_list, iter, model) { + XBT_DEBUG("Handling process whose action failed"); + while ((action = surf_model_extract_failed_action_set(model))) { + XBT_DEBUG(" Handling Action %p",action); + SIMIX_simcall_exit((smx_synchro_t) surf_action_get_data(action)); + } + XBT_DEBUG("Handling process whose action terminated normally"); + while ((action = surf_model_extract_done_action_set(model))) { + XBT_DEBUG(" Handling Action %p",action); + if (surf_action_get_data(action) == NULL) + XBT_DEBUG("probably vcpu's action %p, skip", action); + else + SIMIX_simcall_exit((smx_synchro_t) surf_action_get_data(action)); + } + } } time = SIMIX_timer_next(); - if (time != -1.0 || xbt_swag_size(simix_global->process_list) != 0) + if (time != -1.0 || xbt_swag_size(simix_global->process_list) != 0) { + XBT_DEBUG("Calling surf_solve"); time = surf_solve(time); - + XBT_DEBUG("Moving time ahead : %g", time); + } /* Notify all the hosts that have failed */ /* FIXME: iterate through the list of failed host and mark each of them */ /* as failed. On each host, signal all the running processes with host_fail */ @@@ -446,14 -444,19 +464,19 @@@ /* Wake up all processes waiting for a Surf action to finish */ xbt_dynar_foreach(model_list, iter, model) { - while ((action = surf_model_extract_failed_action_set(model))) + XBT_DEBUG("Handling process whose action failed"); + while ((action = surf_model_extract_failed_action_set(model))) { + XBT_DEBUG(" Handling Action %p",action); SIMIX_simcall_exit((smx_synchro_t) surf_action_get_data(action)); - - while ((action = surf_model_extract_done_action_set(model))) + } + XBT_DEBUG("Handling process whose action terminated normally"); + while ((action = surf_model_extract_done_action_set(model))) { + XBT_DEBUG(" Handling Action %p",action); if (surf_action_get_data(action) == NULL) XBT_DEBUG("probably vcpu's action %p, skip", action); else SIMIX_simcall_exit((smx_synchro_t) surf_action_get_data(action)); + } } /* Autorestart all process */ @@@ -476,9 -479,7 +499,7 @@@ if (xbt_swag_size(simix_global->process_list) != 0) { - #ifdef HAVE_TRACING - TRACE_end(); - #endif + TRACE_end(); XBT_CRITICAL("Oops ! Deadlock or code not perfectly clean."); SIMIX_display_process_status(); diff --combined src/simix/smx_process.c index 9d6e02b71a,b7389741f9..8fa3c6b8da --- a/src/simix/smx_process.c +++ b/src/simix/smx_process.c @@@ -9,7 -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)"); @@@ -87,6 -86,7 +87,7 @@@ void SIMIX_process_cleanup(smx_process_ } } + XBT_DEBUG("%p should not be run anymore",process); xbt_swag_remove(process, simix_global->process_list); xbt_swag_remove(process, SIMIX_host_priv(process->smx_host)->process_list); xbt_swag_insert(process, simix_global->process_to_destroy); @@@ -104,6 -104,8 +105,8 @@@ void SIMIX_process_empty_trash(void smx_process_t process = NULL; while ((process = xbt_swag_extract(simix_global->process_to_destroy))) { + XBT_DEBUG("Getting rid of %p",process); + SIMIX_context_free(process->context); /* Free the exception allocated at creation time */ @@@ -368,6 -370,7 +371,7 @@@ void SIMIX_process_kill(smx_process_t p } } if(!xbt_dynar_member(simix_global->process_to_run, &(process)) && process != issuer) { + XBT_DEBUG("Inserting %s in the to_run list", process->name); xbt_dynar_push_as(simix_global->process_to_run, smx_process_t, process); } @@@ -401,11 -404,12 +405,12 @@@ void SIMIX_process_throw(smx_process_t break; case SIMIX_SYNC_SLEEP: - SIMIX_process_sleep_destroy(process->waiting_synchro); - break; - case SIMIX_SYNC_JOIN: SIMIX_process_sleep_destroy(process->waiting_synchro); + if (!xbt_dynar_member(simix_global->process_to_run, &(process)) && process != SIMIX_process_self()) { + XBT_DEBUG("Inserting %s in the to_run list", process->name); + xbt_dynar_push_as(simix_global->process_to_run, smx_process_t, process); + } break; case SIMIX_SYNC_SYNCHRO: @@@ -420,8 -424,6 +425,6 @@@ } process->waiting_synchro = NULL; - if (!xbt_dynar_member(simix_global->process_to_run, &(process)) && process != SIMIX_process_self()) - xbt_dynar_push_as(simix_global->process_to_run, smx_process_t, process); } void simcall_HANDLER_process_killall(smx_simcall_t simcall, int reset_pid) { @@@ -740,9 -742,7 +743,7 @@@ smx_synchro_t SIMIX_process_sleep(smx_p synchro = xbt_mallocator_get(simix_global->synchro_mallocator); synchro->type = SIMIX_SYNC_SLEEP; synchro->name = NULL; - #ifdef HAVE_TRACING synchro->category = NULL; - #endif synchro->sleep.host = host; synchro->sleep.surf_sleep = diff --combined src/smpi/private.h index cd4fdcb92f,a9817576c8..050f2198e5 --- a/src/smpi/private.h +++ b/src/smpi/private.h @@@ -108,10 -108,8 +108,8 @@@ typedef struct s_smpi_mpi_request MPI_Request detached_sender; int refcount; MPI_Op op; - #ifdef HAVE_TRACING int send; int recv; - #endif } s_smpi_mpi_request_t; typedef struct s_smpi_mpi_comm_key_elem { @@@ -449,8 -447,8 +447,8 @@@ int smpi_type_keyval_free(int* keyval) extern double smpi_cpu_threshold; extern double smpi_running_power; extern int smpi_privatize_global_variables; -extern char* start_data_exe; //start of the data+bss segment of the executable -extern int size_data_exe; //size of the data+bss segment of the executable +extern char* smpi_start_data_exe; //start of the data+bss segment of the executable +extern int smpi_size_data_exe; //size of the data+bss segment of the executable void smpi_switch_data_segment(int dest); @@@ -738,7 -736,6 +736,6 @@@ void mpi_comm_spawn_multiple_ ( int* co void mpi_comm_get_parent_ ( int*parent, int* ierr); - #ifdef HAVE_TRACING /********** Tracing **********/ /* from smpi_instr.c */ void TRACE_internal_smpi_set_category (const char *category); @@@ -761,7 -758,6 +758,6 @@@ void TRACE_smpi_send(int rank, int src void TRACE_smpi_recv(int rank, int src, int dst); void TRACE_smpi_init(int rank); void TRACE_smpi_finalize(int rank); - #endif const char* encode_datatype(MPI_Datatype datatype, int* known); @@@ -770,9 -766,10 +766,9 @@@ typedef struct s_smpi_privatisation_region { void* address; int file_descriptor; -} *smpi_privatisation_region_t; +} s_smpi_privatisation_region_t, *smpi_privatisation_region_t; extern smpi_privatisation_region_t smpi_privatisation_regions; - extern int smpi_loaded_page; int SIMIX_process_get_PID(smx_process_t self); diff --combined src/smpi/smpi_base.c index 6acebc9d2f,bc7ac717e2..c75e51dabf --- a/src/smpi/smpi_base.c +++ b/src/smpi/smpi_base.c @@@ -250,10 -250,8 +250,8 @@@ static MPI_Request build_request(void * else request->refcount = 0; request->op = MPI_REPLACE; - #ifdef HAVE_TRACING request->send = 0; request->recv = 0; - #endif if (flags & SEND) smpi_datatype_unuse(datatype); return request; @@@ -402,12 -400,10 +400,10 @@@ void smpi_mpi_start(MPI_Request request int receiver = request->dst; - #ifdef HAVE_TRACING - int rank = request->src; - if (TRACE_smpi_view_internals()) { - TRACE_smpi_send(rank, rank, receiver,request->size); - } - #endif + int rank = request->src; + if (TRACE_smpi_view_internals()) { + TRACE_smpi_send(rank, rank, receiver,request->size); + } print_request("New send", request); //if we are giving back the control to the user without waiting for completion, we have to inject timings @@@ -460,11 -456,11 +456,11 @@@ oldbuf = request->buf; if (!smpi_process_get_replaying() && oldbuf && request->size!=0){ if((smpi_privatize_global_variables) - && ((char*)request->buf >= start_data_exe) - && ((char*)request->buf < start_data_exe + size_data_exe )){ + && ((char*) request->buf >= smpi_start_data_exe) + && ((char*)request->buf < smpi_start_data_exe + smpi_size_data_exe )){ XBT_DEBUG("Privatization : We are sending from a zone inside global memory. Switch data segment "); - smpi_switch_data_segment(request->src); - } + smpi_switch_data_segment(request->src); + } buf = xbt_malloc(request->size); memcpy(buf,oldbuf,request->size); XBT_DEBUG("buf %p copied into %p",oldbuf,buf); @@@ -490,12 -486,10 +486,10 @@@ - #ifdef HAVE_TRACING /* FIXME: detached sends are not traceable (request->action == NULL) */ if (request->action) - simcall_set_category(request->action, TRACE_internal_smpi_get_category()); + simcall_set_category(request->action, TRACE_internal_smpi_get_category()); - #endif xbt_mutex_release(mut); } @@@ -700,8 -694,8 +694,8 @@@ static void finish_wait(MPI_Request * r if((req->flags & ACCUMULATE) || (datatype->has_subtype == 1)){ if (!smpi_process_get_replaying()){ if( smpi_privatize_global_variables - && ((char*)req->old_buf >= start_data_exe) - && ((char*)req->old_buf < start_data_exe + size_data_exe ) + && ((char*)req->old_buf >= smpi_start_data_exe) + && ((char*)req->old_buf < smpi_start_data_exe + smpi_size_data_exe ) ){ XBT_VERB("Privatization : We are unserializing to a zone in global memory - Switch data segment "); smpi_switch_data_segment(smpi_process_index()); @@@ -725,7 -719,6 +719,6 @@@ } - #ifdef HAVE_TRACING if (TRACE_smpi_view_internals()) { if(req->flags & RECV){ int rank = smpi_process_index(); @@@ -733,7 -726,6 +726,6 @@@ TRACE_smpi_recv(rank, src_traced, rank); } } - #endif if(req->detached_sender!=NULL){ smpi_mpi_request_free(&(req->detached_sender)); diff --combined src/smpi/smpi_bench.c index 9f58470608,79179a7a42..35971e220e --- a/src/smpi/smpi_bench.c +++ b/src/smpi/smpi_bench.c @@@ -75,10 -75,12 +75,10 @@@ double smpi_cpu_threshold double smpi_running_power; int smpi_loaded_page = -1; -char* start_data_exe = NULL; -int size_data_exe = 0; +char* smpi_start_data_exe = NULL; +int smpi_size_data_exe = 0; int smpi_privatize_global_variables; double smpi_total_benched_time = 0; - - smpi_privatisation_region_t smpi_privatisation_regions; typedef struct { @@@ -156,9 -158,7 +156,7 @@@ void smpi_execute_flops(double flops) host = SIMIX_host_self(); XBT_DEBUG("Handle real computation time: %f flops", flops); action = simcall_host_execute("computation", host, flops, 1, 0, 0); - #ifdef HAVE_TRACING simcall_set_category (action, TRACE_internal_smpi_get_category()); - #endif simcall_host_execution_wait(action); smpi_switch_data_segment(smpi_process_index()); } @@@ -168,18 -168,14 +166,14 @@@ void smpi_execute(double duration if (duration >= smpi_cpu_threshold) { XBT_DEBUG("Sleep for %g to handle real computation time", duration); double flops = duration * smpi_running_power; - #ifdef HAVE_TRACING int rank = smpi_process_index(); instr_extra_data extra = xbt_new0(s_instr_extra_data_t,1); extra->type=TRACING_COMPUTING; extra->comp_size=flops; TRACE_smpi_computing_in(rank, extra); - #endif smpi_execute_flops(flops); - #ifdef HAVE_TRACING TRACE_smpi_computing_out(rank); - #endif } else { XBT_DEBUG("Real computation took %g while option smpi/cpu_threshold is set to %g => ignore it", @@@ -228,17 -224,15 +222,15 @@@ static unsigned int private_sleep(doubl smpi_bench_end(); XBT_DEBUG("Sleep for: %lf secs", secs); - #ifdef HAVE_TRACING int rank = smpi_comm_rank(MPI_COMM_WORLD); instr_extra_data extra = xbt_new0(s_instr_extra_data_t,1); extra->type=TRACING_SLEEPING; extra->sleep_duration=secs; TRACE_smpi_sleeping_in(rank, extra); - #endif + simcall_process_sleep(secs); - #ifdef HAVE_TRACING + TRACE_smpi_sleeping_out(rank); - #endif smpi_bench_begin(); return 0; @@@ -625,26 -619,23 +617,26 @@@ void smpi_switch_data_segment(int dest) */ void smpi_really_switch_data_segment(int dest) { - if(size_data_exe == 0)//no need to switch + if(smpi_size_data_exe == 0)//no need to switch return; #ifdef HAVE_MMAP int i; if(smpi_loaded_page==-1){//initial switch, do the copy from the real page here for (i=0; i< SIMIX_process_count(); i++){ - memcpy(smpi_privatisation_regions[i].address,TOPAGE(start_data_exe),size_data_exe); + memcpy(smpi_privatisation_regions[i].address, + TOPAGE(smpi_start_data_exe), smpi_size_data_exe); } } + // FIXME, cross-process support (mmap across process when necessary) int current = smpi_privatisation_regions[dest].file_descriptor; XBT_DEBUG("Switching data frame to the one of process %d", dest); - void* tmp = mmap (TOPAGE(start_data_exe), size_data_exe, PROT_READ | PROT_WRITE, MAP_FIXED | MAP_SHARED, current, 0); - if (tmp != TOPAGE(start_data_exe)) + void* tmp = mmap (TOPAGE(smpi_start_data_exe), smpi_size_data_exe, + PROT_READ | PROT_WRITE, MAP_FIXED | MAP_SHARED, current, 0); + if (tmp != TOPAGE(smpi_start_data_exe)) xbt_die("Couldn't map the new region"); - smpi_loaded_page=dest; + smpi_loaded_page = dest; #endif } @@@ -706,12 -697,12 +698,12 @@@ void smpi_get_executable_global_size() if(i>=6){ if(strcmp(lfields[1], ".data") == 0){ size_data_binary = strtoul(lfields[2], NULL, 16); - start_data_exe = (char*) strtoul(lfields[4], NULL, 16); + smpi_start_data_exe = (char*) strtoul(lfields[4], NULL, 16); found++; }else if(strcmp(lfields[1], ".bss") == 0){ //the beginning of bss is not exactly the end of data if not aligned, grow bss reported size accordingly //TODO : check if this is OK, as some segments may be inserted between them.. - size_bss_binary = ((char*) strtoul(lfields[4], NULL, 16) - (start_data_exe + size_data_binary)) + size_bss_binary = ((char*) strtoul(lfields[4], NULL, 16) - (smpi_start_data_exe + size_data_binary)) + strtoul(lfields[2], NULL, 16); found++; } @@@ -720,9 -711,7 +712,9 @@@ } - size_data_exe =(unsigned long)start_data_exe - (unsigned long)TOPAGE(start_data_exe)+ size_data_binary+size_bss_binary; + smpi_size_data_exe = (unsigned long) smpi_start_data_exe + - (unsigned long) TOPAGE(smpi_start_data_exe) + + size_data_binary+size_bss_binary; xbt_free(command); xbt_free(line); pclose(fp); @@@ -739,10 -728,9 +731,10 @@@ void smpi_initialize_global_memory_segm unsigned int i = 0; smpi_get_executable_global_size(); - XBT_DEBUG ("bss+data segment found : size %d starting at %p",size_data_exe, start_data_exe ); + XBT_DEBUG ("bss+data segment found : size %d starting at %p", + smpi_size_data_exe, smpi_start_data_exe ); - if(size_data_exe == 0){//no need to switch + if (smpi_size_data_exe == 0){//no need to switch smpi_privatize_global_variables=0; return; } @@@ -781,17 -769,17 +773,17 @@@ Ask the Internet about tutorials on ho if (status) xbt_die("Impossible to unlink temporary file for memory mapping"); - status = ftruncate(file_descriptor, size_data_exe); + status = ftruncate(file_descriptor, smpi_size_data_exe); if(status) xbt_die("Impossible to set the size of the temporary file for memory mapping"); /* Ask for a free region */ - address = mmap (NULL, size_data_exe, PROT_READ | PROT_WRITE, MAP_SHARED, file_descriptor, 0); + address = mmap (NULL, smpi_size_data_exe, PROT_READ | PROT_WRITE, MAP_SHARED, file_descriptor, 0); if (address == MAP_FAILED) xbt_die("Couldn't find a free region for memory mapping"); //initialize the values - memcpy(address,TOPAGE(start_data_exe),size_data_exe); + memcpy(address, TOPAGE(smpi_start_data_exe), smpi_size_data_exe); //store the address of the mapping for further switches smpi_privatisation_regions[i].file_descriptor = file_descriptor; @@@ -803,12 -791,12 +795,12 @@@ } void smpi_destroy_global_memory_segments(){ - if(size_data_exe == 0)//no need to switch + if (smpi_size_data_exe == 0)//no need to switch return; #ifdef HAVE_MMAP int i; for (i=0; i< smpi_process_count(); i++){ - if(munmap(smpi_privatisation_regions[i].address,size_data_exe) < 0) { + if(munmap(smpi_privatisation_regions[i].address, smpi_size_data_exe) < 0) { XBT_WARN("Unmapping of fd %d failed: %s", smpi_privatisation_regions[i].file_descriptor, strerror(errno)); } diff --combined src/smpi/smpi_global.c index 7a4711704a,4e8202c77b..ac3cd86c9e --- a/src/smpi/smpi_global.c +++ b/src/smpi/smpi_global.c @@@ -350,8 -350,8 +350,8 @@@ void smpi_comm_copy_buffer_callback(smx void* tmpbuff=buff; if((smpi_privatize_global_variables) - && ((char*)buff >= start_data_exe) - && ((char*)buff < start_data_exe + size_data_exe ) + && ((char*)buff >= smpi_start_data_exe) + && ((char*)buff < smpi_start_data_exe + smpi_size_data_exe ) ){ XBT_DEBUG("Privatization : We are copying from a zone inside global memory... Saving data to temp buffer !"); smpi_switch_data_segment(((smpi_process_data_t)SIMIX_process_get_data(comm->comm.src_proc))->index); @@@ -361,8 -361,8 +361,8 @@@ if((smpi_privatize_global_variables) - && ((char*)comm->comm.dst_buff >= start_data_exe) - && ((char*)comm->comm.dst_buff < start_data_exe + size_data_exe ) + && ((char*)comm->comm.dst_buff >= smpi_start_data_exe) + && ((char*)comm->comm.dst_buff < smpi_start_data_exe + smpi_size_data_exe ) ){ XBT_DEBUG("Privatization : We are copying to a zone inside global memory - Switch data segment"); smpi_switch_data_segment(((smpi_process_data_t)SIMIX_process_get_data(comm->comm.dst_proc))->index); @@@ -528,9 -528,7 +528,7 @@@ static void smpi_init_logs() function: xbt_log_appender_file.c depends on it DO NOT connect this in XBT or so, or it will be useless to xbt_log_appender_file.c */ - #ifdef HAVE_TRACING XBT_LOG_CONNECT(instr_smpi); - #endif XBT_LOG_CONNECT(smpi_base); XBT_LOG_CONNECT(smpi_bench); XBT_LOG_CONNECT(smpi_coll); @@@ -641,12 -639,10 +639,10 @@@ int smpi_main(int (*realmain) (int argc smpi_init_logs(); - #ifdef HAVE_TRACING TRACE_global_init(&argc, argv); TRACE_add_start_function(TRACE_smpi_alloc); TRACE_add_end_function(TRACE_smpi_release); - #endif SIMIX_global_init(&argc, argv); @@@ -691,9 -687,7 +687,7 @@@ smpi_global_destroy(); - #ifdef HAVE_TRACING TRACE_end(); - #endif return 0; } @@@ -705,11 -699,8 +699,8 @@@ void SMPI_init() smpi_init_options(); smpi_global_init(); smpi_check_options(); - #ifdef HAVE_TRACING - if (TRACE_is_enabled() && TRACE_is_configured()) { + if (TRACE_is_enabled() && TRACE_is_configured()) TRACE_smpi_alloc(); - } - #endif if(smpi_privatize_global_variables) smpi_initialize_global_memory_segments(); } diff --combined src/surf/surf_interface.cpp index c3adc90047,db8618de28..71e9355bf3 --- a/src/surf/surf_interface.cpp +++ b/src/surf/surf_interface.cpp @@@ -422,10 -422,8 +422,8 @@@ void surf_init(int *argc, char **argv if (!history) history = tmgr_history_new(); - #ifdef HAVE_TRACING TRACE_add_start_function(TRACE_surf_alloc); TRACE_add_end_function(TRACE_surf_release); - #endif sg_config_init(argc, argv); @@@ -438,10 -436,8 +436,8 @@@ void surf_exit(void unsigned int iter; ModelPtr model = NULL; - #ifdef HAVE_TRACING TRACE_end(); /* Just in case it was not called by the upper * layer (or there is no upper layer) */ - #endif sg_config_finalize(); @@@ -791,9 -787,7 +787,7 @@@ void Action::initialize(ModelPtr model Action::Action(ModelPtr model, double cost, bool failed) { initialize(model, cost, failed); - #ifdef HAVE_TRACING - p_category = NULL; - #endif + p_category = NULL; p_stateHookup.prev = 0; p_stateHookup.next = 0; if (failed) @@@ -807,9 -801,7 +801,7 @@@ Action::Action(ModelPtr model, double cost, bool failed, lmm_variable_t var) { initialize(model, cost, failed, var); - #ifdef HAVE_TRACING - p_category = NULL; - #endif + p_category = NULL; p_stateHookup.prev = 0; p_stateHookup.next = 0; if (failed) @@@ -821,9 -813,7 +813,7 @@@ } Action::~Action() { - #ifdef HAVE_TRACING xbt_free(p_category); - #endif } void Action::finish() { @@@ -896,14 -886,12 +886,12 @@@ void Action::setData(void* data p_data = data; } - #ifdef HAVE_TRACING void Action::setCategory(const char *category) { XBT_IN("(%p,%s)", this, category); p_category = xbt_strdup(category); XBT_OUT(); } - #endif void Action::ref(){ m_refcount++; @@@ -1068,12 -1056,10 +1056,10 @@@ void Action::updateRemainingLazy(doubl XBT_DEBUG("Updating action(%p): remains was %f, last_update was: %f", this, m_remains, m_lastUpdate); double_update(&m_remains, m_lastValue * delta, sg_surf_precision*sg_maxmin_precision); - #ifdef HAVE_TRACING if (getModel() == surf_cpu_model_pm && TRACE_is_enabled()) { ResourcePtr cpu = static_cast(lmm_constraint_id(lmm_get_cnst_from_var(getModel()->getMaxminSystem(), getVariable(), 0))); TRACE_surf_host_set_utilization(cpu->getName(), getCategory(), m_lastValue, m_lastUpdate, now - m_lastUpdate); } - #endif XBT_DEBUG("Updating action(%p): remains is now %f", this, m_remains); } @@@ -1099,3 -1085,4 +1085,3 @@@ m_lastUpdate = now; m_lastValue = lmm_variable_getvalue(getVariable()); } - diff --combined teshsuite/mc/replay/random_bug.c index 4b8613c747,fea8c27ac3..fba41c7ef2 --- a/teshsuite/mc/replay/random_bug.c +++ b/teshsuite/mc/replay/random_bug.c @@@ -6,13 -6,9 +6,12 @@@ #include +#include - - #include + #include #include +XBT_LOG_NEW_DEFAULT_CATEGORY(random_bug, "Application"); + /** An (fake) application with a bug occuring for some random values */ static int app(int argc, char *argv[]) @@@ -37,5 -33,5 +36,5 @@@ int main(int argc, char *argv[] MSG_function_register("app", &app); MSG_create_environment(argv[1]); MSG_launch_application(argv[2]); - return (int) MSG_main(); + return MSG_main(); }