From: Gabriel Corona Date: Tue, 10 Mar 2015 11:13:14 +0000 (+0100) Subject: Merge branch 'master' into mc-process X-Git-Tag: v3_12~732^2~111 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/2bd9a37bbb72eac4ed613b3d6953aba6555e2e92?hp=-c Merge branch 'master' into mc-process Conflicts: examples/smpi/mc/non_deterministic.tesh examples/smpi/mc/only_send_deterministic.tesh src/include/mc/mc.h src/mc/mc_base.c src/mc/mc_comm_determinism.c src/mc/mc_config.c src/mc/mc_global.c src/mc/mc_page_snapshot.cpp src/mc/mc_request.c --- 2bd9a37bbb72eac4ed613b3d6953aba6555e2e92 diff --combined buildtools/Cmake/CompleteInFiles.cmake index b1ba41ffd8,786550e17e..a8410adfb5 --- 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( @@@ -550,6 -549,14 +550,14 @@@ if(EXISTS ${CMAKE_HOME_DIRECTORY}/.git/ string(REPLACE "\n" "" GIT_DATE "${GIT_DATE}") message(STATUS "Git date: ${GIT_DATE}") string(REGEX REPLACE " .*" "" GIT_VERSION "${GIT_VERSION}") + + execute_process(COMMAND git --git-dir=${CMAKE_HOME_DIRECTORY}/.git log --pretty=format:%H -1 + WORKING_DIRECTORY ${CMAKE_HOME_DIRECTORY}/.git/ + OUTPUT_VARIABLE SIMGRID_GITHASH + RESULT_VARIABLE ret + ) + string(REPLACE "\n" "" SIMGRID_GITHASH "${SIMGRID_GITHASH}") + endif() elseif(EXISTS ${CMAKE_HOME_DIRECTORY}/.gitversion) FILE(STRINGS ${CMAKE_HOME_DIRECTORY}/.gitversion GIT_VERSION) diff --combined buildtools/Cmake/DefinePackages.cmake index bf6b18cdda,e9ad635ddf..6a07df0a3e --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@@ -129,8 -129,7 +129,7 @@@ set(EXTRA_DIS tools/tesh/run_context.h tools/tesh/tesh.h tools/tesh/generate_tesh - examples/smpi/mc/non_deterministic.tesh - examples/smpi/mc/send_deterministic.tesh + examples/smpi/mc/only_send_deterministic.tesh ) set(SMPI_SRC @@@ -594,19 -593,10 +593,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 @@@ -642,20 -632,8 +641,20 @@@ 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 @@@ -1017,7 -995,7 +1016,7 @@@ set(EXAMPLES_CMAKEFILES_TX examples/msg/chainsend/CMakeLists.txt examples/msg/chord/CMakeLists.txt examples/msg/cloud/CMakeLists.txt - examples/msg/energy/e1/CMakeLists.txt + examples/msg/energy/pstate/CMakeLists.txt examples/msg/energy/e2/CMakeLists.txt examples/msg/energy/e3/CMakeLists.txt examples/msg/exception/CMakeLists.txt diff --combined examples/smpi/mc/only_send_deterministic.tesh index 0000000000,ac21435887..a9c854e33d mode 000000,100644..100644 --- a/examples/smpi/mc/only_send_deterministic.tesh +++ b/examples/smpi/mc/only_send_deterministic.tesh @@@ -1,0 -1,26 +1,15 @@@ + #! ./tesh + + ! timeout 60 -$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'surf/precision' to '1e-9' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/TCP_gamma' to '4194304' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check' to '1' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/communications_determinism' to '1' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/send_is_detached_thres' to '0' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/running_power' to '1e9' ++$ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic + > [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s) + > [0.000000] [mc_global/INFO] Check communication determinism -> [0.000000] [mc_global/INFO] Get debug information ... -> [0.000000] [mc_global/INFO] Get debug information done ! + > [0.000000] [mc_global/INFO] ****************************************************** + > [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern **** + > [0.000000] [mc_global/INFO] ****************************************************** + > [0.000000] [mc_global/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2 + > [0.000000] [mc_global/INFO] Expanded states = 1025 + > [0.000000] [mc_global/INFO] Visited states = 3640 + > [0.000000] [mc_global/INFO] Executed transitions = 3360 + > [0.000000] [mc_global/INFO] Send-deterministic : Yes + > [0.000000] [mc_global/INFO] Recv-deterministic : No - - diff --combined src/include/mc/mc.h index 23b17815c7,e3fcd97a6e..23be47f024 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@@ -51,10 -51,12 +51,11 @@@ extern int _sg_mc_comms_determinism extern int _sg_mc_send_determinism; extern int _sg_mc_safety; extern int _sg_mc_liveness; +extern int _sg_mc_snapshot_fds; + extern int _sg_mc_termination; extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; -extern void *maestro_stack_start; -extern void *maestro_stack_end; /********************************* Global *************************************/ void _mc_cfg_cb_reduce(const char *name, int pos); @@@ -64,12 -66,12 +65,13 @@@ void _mc_cfg_cb_soft_dirty(const char * void _mc_cfg_cb_property(const char *name, int pos); void _mc_cfg_cb_timeout(const char *name, int pos); void _mc_cfg_cb_hash(const char *name, int pos); +void _mc_cfg_cb_snapshot_fds(const char *name, int pos); void _mc_cfg_cb_max_depth(const char *name, int pos); void _mc_cfg_cb_visited(const char *name, int pos); void _mc_cfg_cb_dot_output(const char *name, int pos); void _mc_cfg_cb_comms_determinism(const char *name, int pos); void _mc_cfg_cb_send_determinism(const char *name, int pos); + void _mc_cfg_cb_termination(const char *name, int pos); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); XBT_PUBLIC(void) MC_init(void); @@@ -88,7 -90,6 +90,7 @@@ XBT_PUBLIC(void) MC_new_stack_area(voi /********************************* Memory *************************************/ XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */ XBT_PUBLIC(void) MC_memory_exit(void); +XBT_PUBLIC(void) MC_memory_init_server(void); SG_END_DECL() diff --combined src/mc/mc_base.c index 20d8f436ad,2a587228ab..63d7a58a7f --- a/src/mc/mc_base.c +++ b/src/mc/mc_base.c @@@ -10,14 -10,11 +10,14 @@@ #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" +#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) { smx_process_t process; @@@ -38,9 -35,7 +38,10 @@@ int MC_request_is_enabled(smx_simcall_ { unsigned int index = 0; smx_synchro_t act = 0; +#ifdef HAVE_MC + s_smx_synchro_t temp_synchro; +#endif + smx_mutex_t mutex = NULL; switch (req->call) { case SIMCALL_NONE: @@@ -49,17 -44,6 +50,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. */ @@@ -75,23 -59,18 +76,30 @@@ case SIMCALL_COMM_WAITANY: /* Check if it has at least one communication ready */ - xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) + xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) { + +#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); + if(mutex->owner == NULL) + return TRUE; + else + return (mutex->owner->pid == req->issuer->pid); + default: /* The rest of the requests are always enabled */ return TRUE; @@@ -107,6 -86,7 +115,7 @@@ int MC_request_is_visible(smx_simcall_ || req->call == SIMCALL_COMM_TEST || req->call == SIMCALL_COMM_TESTANY || req->call == SIMCALL_MC_RANDOM + || req->call == SIMCALL_MUTEX_LOCK #ifdef HAVE_MC || req->call == SIMCALL_MC_SNAPSHOT || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS diff --combined src/mc/mc_comm_determinism.c index 4043b1f41e,0636fa4952..635bc9d196 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@@ -10,7 -10,6 +10,7 @@@ #include "mc_safety.h" #include "mc_private.h" #include "mc_record.h" +#include "mc_smx.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection"); @@@ -46,144 -45,72 +46,78 @@@ static e_mc_comm_pattern_difference_t c return SRC_PROC_DIFF; if (comm1->dst_proc != comm2->dst_proc) return DST_PROC_DIFF; + if (comm1->tag != comm2->tag) + return TAG_DIFF; if (comm1->data_size != comm2->data_size) return DATA_SIZE_DIFF; if(comm1->data == NULL && comm2->data == NULL) return 0; - /*if(comm1->data != NULL && comm2->data !=NULL) { + if(comm1->data != NULL && comm2->data !=NULL) { if (!memcmp(comm1->data, comm2->data, comm1->data_size)) return 0; return DATA_DIFF; }else{ return DATA_DIFF; - }*/ + } return 0; } - static void print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) { - if (_sg_mc_comms_determinism && !initial_global_state->comm_deterministic) { - XBT_INFO("****************************************************"); - XBT_INFO("***** Non-deterministic communications pattern *****"); - XBT_INFO("****************************************************"); - XBT_INFO("The communications pattern of the process %d is different!", process); - switch(diff) { - case TYPE_DIFF: - XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case RDV_DIFF: - XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case SRC_PROC_DIFF: - XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DST_PROC_DIFF: - XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DATA_SIZE_DIFF: - XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DATA_DIFF: - XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - default: - break; - } - MC_print_statistics(mc_stats); - xbt_abort(); - } else if (_sg_mc_send_determinism && !initial_global_state->send_deterministic) { - XBT_INFO("*********************************************************"); - XBT_INFO("***** Non-send-deterministic communications pattern *****"); - XBT_INFO("*********************************************************"); - XBT_INFO("The communications pattern of the process %d is different!", process); - switch(diff) { - case TYPE_DIFF: - XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case RDV_DIFF: - XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case SRC_PROC_DIFF: - XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DST_PROC_DIFF: - XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DATA_SIZE_DIFF: - XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DATA_DIFF: - XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - default: - break; - } - MC_print_statistics(mc_stats); - xbt_abort(); + static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) { + char *type, *res; + + if(comm->type == SIMIX_COMM_SEND) + type = bprintf("The send communications pattern of the process %d is different!", process - 1); + else + type = bprintf("The recv communications pattern of the process %d is different!", process - 1); + + switch(diff) { + case TYPE_DIFF: + res = bprintf("%s Different type for communication #%d", type, cursor); + break; + case RDV_DIFF: + res = bprintf("%s Different rdv for communication #%d", type, cursor); + break; + case TAG_DIFF: + res = bprintf("%s Different tag for communication #%d", type, cursor); + break; + case SRC_PROC_DIFF: + res = bprintf("%s Different source for communication #%d", type, cursor); + break; + case DST_PROC_DIFF: + res = bprintf("%s Different destination for communication #%d", type, cursor); + break; + case DATA_SIZE_DIFF: + res = bprintf("%s\n Different data size for communication #%d", type, cursor); + break; + case DATA_DIFF: + res = bprintf("%s\n Different data for communication #%d", type, cursor); + break; + default: + res = NULL; + break; } - } - static void print_communications_pattern() - { - unsigned int cursor = 0, cursor2 = 0; - mc_comm_pattern_t current_comm; - mc_list_comm_pattern_t current_list; - unsigned int current_process = 1; - while (current_process < simix_process_maxpid) { - current_list = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, current_process, mc_list_comm_pattern_t); - XBT_INFO("Communications from the process %u:", current_process); - while(cursor2 < current_list->index_comm){ - current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(current_list->list, cursor2, mc_comm_pattern_t); - if (current_comm->type == SIMIX_COMM_SEND) { - XBT_INFO("(%u) [(%lu) %s -> (%lu) %s] %s ", cursor,current_comm->src_proc, - current_comm->src_host, current_comm->dst_proc, - current_comm->dst_host, "iSend"); - } else { - XBT_INFO("(%u) [(%lu) %s <- (%lu) %s] %s ", cursor, current_comm->dst_proc, - current_comm->dst_host, current_comm->src_proc, - current_comm->src_host, "iRecv"); - } - cursor2++; - } - current_process++; - cursor = 0; - cursor2 = 0; - } - } - - static void print_incomplete_communications_pattern(){ - unsigned int cursor = 0; - unsigned int current_process = 1; - xbt_dynar_t current_pattern; - mc_comm_pattern_t comm; - while (current_process < simix_process_maxpid) { - current_pattern = (xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t); - XBT_INFO("Incomplete communications from the process %u:", current_process); - xbt_dynar_foreach(current_pattern, cursor, comm) { - XBT_DEBUG("(%u) Communication %p", cursor, comm); - } - current_process++; - cursor = 0; - } + return res; } +// FIXME, remote comm static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm) { + mc_process_t process = &mc_model_checker->process; void *addr_pointed; - comm_pattern->src_proc = comm->comm.src_proc->pid; - comm_pattern->dst_proc = comm->comm.dst_proc->pid; - comm_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host); - comm_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host); + smx_process_t src_proc = MC_smx_resolve_process(comm->comm.src_proc); + smx_process_t dst_proc = MC_smx_resolve_process(comm->comm.dst_proc); + comm_pattern->src_proc = src_proc->pid; + comm_pattern->dst_proc = dst_proc->pid; + // TODO, resolve host name + comm_pattern->src_host = MC_smx_process_get_host_name(src_proc); + comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc); if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) { comm_pattern->data_size = *(comm->comm.dst_buff_size); comm_pattern->data = xbt_malloc0(comm_pattern->data_size); addr_pointed = *(void **) comm->comm.src_buff; - if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval) + if (addr_pointed > (void*) process->heap_address + && addr_pointed < MC_process_get_heap(process)->breakval) memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size); else memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size); @@@ -195,18 -122,46 +129,46 @@@ static void deterministic_comm_pattern( mc_list_comm_pattern_t list_comm_pattern = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t); if(!backtracking){ - mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, comm->index, mc_comm_pattern_t); + mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, list_comm_pattern->index_comm, mc_comm_pattern_t); e_mc_comm_pattern_difference_t diff; if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){ - if (comm->type == SIMIX_COMM_SEND) + if (comm->type == SIMIX_COMM_SEND){ initial_global_state->send_deterministic = 0; - initial_global_state->comm_deterministic = 0; - print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1); + if(initial_global_state->send_diff != NULL) + xbt_free(initial_global_state->send_diff); + initial_global_state->send_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1); + }else{ + initial_global_state->recv_deterministic = 0; + if(initial_global_state->recv_diff != NULL) + xbt_free(initial_global_state->recv_diff); + initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1); + } + if(_sg_mc_send_determinism && !initial_global_state->send_deterministic){ + XBT_INFO("*********************************************************"); + XBT_INFO("***** Non-send-deterministic communications pattern *****"); + XBT_INFO("*********************************************************"); + XBT_INFO("%s", initial_global_state->send_diff); + xbt_free(initial_global_state->send_diff); + initial_global_state->send_diff = NULL; + MC_print_statistics(mc_stats); + xbt_abort(); + }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) { + XBT_INFO("****************************************************"); + XBT_INFO("***** Non-deterministic communications pattern *****"); + XBT_INFO("****************************************************"); + XBT_INFO("%s", initial_global_state->send_diff); + XBT_INFO("%s", initial_global_state->recv_diff); + xbt_free(initial_global_state->send_diff); + initial_global_state->send_diff = NULL; + xbt_free(initial_global_state->recv_diff); + initial_global_state->recv_diff = NULL; + MC_print_statistics(mc_stats); + xbt_abort(); + } } } - list_comm_pattern->index_comm++; comm_pattern_free(comm); } @@@ -221,21 -176,13 +183,21 @@@ void list_comm_pattern_free_voidp(void list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p); } - void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const e_mc_call_type_t call_type) + void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking) { - + mc_process_t process = &mc_model_checker->process; mc_comm_pattern_t pattern = NULL; pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->data_size = -1; pattern->data = NULL; + + const smx_process_t issuer = MC_smx_simcall_get_issuer(request); + mc_list_comm_pattern_t initial_pattern = + (mc_list_comm_pattern_t) xbt_dynar_get_as(initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t); + xbt_dynar_t incomplete_pattern = + (xbt_dynar_t) xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t); + pattern->index = + initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern); void *addr_pointed; @@@ -243,111 -190,91 +205,90 @@@ /* Create comm pattern */ pattern->type = SIMIX_COMM_SEND; pattern->comm = simcall_comm_isend__get__result(request); + // FIXME, remote access to rdv->name pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name); - pattern->src_proc = pattern->comm->comm.src_proc->pid; - pattern->src_host = simcall_host_get_name(request->issuer->smx_host); + pattern->src_proc = MC_smx_resolve_process(pattern->comm->comm.src_proc)->pid; + pattern->src_host = MC_smx_process_get_host_name(issuer); + pattern->tag = ((MPI_Request)simcall_comm_isend__get__data(request))->tag; if(pattern->comm->comm.src_buff != NULL){ pattern->data_size = pattern->comm->comm.src_buff_size; pattern->data = xbt_malloc0(pattern->data_size); addr_pointed = *(void **) pattern->comm->comm.src_buff; - if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval) + if (addr_pointed > (void*) process->heap_address + && addr_pointed < MC_process_get_heap(process)->breakval) memcpy(pattern->data, addr_pointed, pattern->data_size); else memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); } + if(((MPI_Request)simcall_comm_isend__get__data(request))->detached){ + if (!initial_global_state->initial_communications_pattern_done) { + /* Store comm pattern */ + xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->list, &pattern); + } else { + /* Evaluate comm determinism */ + deterministic_comm_pattern(pattern->src_proc, pattern, backtracking); + ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->index_comm++; + } + return; + } } else if (call_type == MC_CALL_TYPE_RECV) { pattern->type = SIMIX_COMM_RECEIVE; pattern->comm = simcall_comm_irecv__get__result(request); + // TODO, remote access + pattern->tag = ((MPI_Request)simcall_comm_irecv__get__data(request))->tag; pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name); - pattern->dst_proc = pattern->comm->comm.dst_proc->pid; - pattern->dst_host = simcall_host_get_name(request->issuer->smx_host); + pattern->dst_proc = MC_smx_resolve_process(pattern->comm->comm.dst_proc)->pid; + // FIXME, remote process access + pattern->dst_host = MC_smx_process_get_host_name(issuer); } else { xbt_die("Unexpected call_type %i", (int) call_type); } - xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), &pattern); + xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), &pattern); - XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, request->issuer->pid); + XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid); } - void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) { + void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int issuer, int backtracking) { - mc_comm_pattern_t current_comm_pattern; unsigned int cursor = 0; - - smx_process_t src_proc = MC_smx_resolve_process(comm->comm.src_proc); - smx_process_t dst_proc = MC_smx_resolve_process(comm->comm.dst_proc); - unsigned int src = src_proc->pid; - unsigned int dst = dst_proc->pid; - - mc_comm_pattern_t src_comm_pattern; - mc_comm_pattern_t dst_comm_pattern; - int src_completed = 0, dst_completed = 0; + mc_comm_pattern_t comm_pattern; + int completed = 0; /* Complete comm pattern */ - xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, current_comm_pattern) { + xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) { if (current_comm_pattern-> comm == comm) { update_comm_pattern(current_comm_pattern, comm); - src_completed = 1; - xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, &src_comm_pattern); - XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", src, cursor); + completed = 1; + xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &comm_pattern); + XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor); break; } } - if(!src_completed) - xbt_die("Corresponding communication for the source process not found!"); + if(!completed) + xbt_die("Corresponding communication not found!"); - cursor = 0; - - xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, current_comm_pattern) { - if (current_comm_pattern-> comm == comm) { - update_comm_pattern(current_comm_pattern, comm); - dst_completed = 1; - xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, &dst_comm_pattern); - XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", dst, cursor); - break; - } - } - if(!dst_completed) - xbt_die("Corresponding communication for the destination process not found!"); - if (!initial_global_state->initial_communications_pattern_done) { /* Store comm pattern */ - if(src_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list)){ - xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern); - ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list->used++; - } else { - xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern); - } - - if(dst_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list)) { - xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern); - ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list->used++; - } else { - xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern); - } - ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->index_comm++; - ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->index_comm++; + xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->list, &comm_pattern); } else { /* Evaluate comm determinism */ - deterministic_comm_pattern(src, src_comm_pattern, backtracking); - deterministic_comm_pattern(dst, dst_comm_pattern, backtracking); + deterministic_comm_pattern(issuer, comm_pattern, backtracking); + ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->index_comm++; } } + /************************ Main algorithm ************************/ void MC_pre_modelcheck_comm_determinism(void) { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); + MC_SET_MC_HEAP; mc_state_t initial_state = NULL; smx_process_t process; int i; - if (!mc_mem_set) - MC_SET_MC_HEAP; - if (_sg_mc_visited > 0) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); @@@ -375,11 -302,11 +316,11 @@@ MC_SET_MC_HEAP; /* Get an enabled process and insert it in the interleave set of the initial state */ - xbt_swag_foreach(process, simix_global->process_list) { + MC_EACH_SIMIX_PROCESS(process, if (MC_process_is_enabled(process)) { MC_state_interleave_process(initial_state, process); } - } + ); xbt_fifo_unshift(mc_stack, initial_state); @@@ -434,7 -361,7 +375,7 @@@ void MC_modelcheck_comm_determinism(voi } /* Answer the request */ - SIMIX_simcall_handle(req, value); /* After this call req is no longer useful */ + MC_simcall_handle(req, value); /* After this call req is no longer useful */ MC_SET_MC_HEAP; if(!initial_global_state->initial_communications_pattern_done) @@@ -454,11 -381,11 +395,11 @@@ if ((visited_state = is_visited_state(next_state)) == NULL) { /* Get enabled processes and insert them in the interleave set of the next state */ - xbt_swag_foreach(process, simix_global->process_list) { + MC_EACH_SIMIX_PROCESS(process, if (MC_process_is_enabled(process)) { MC_state_interleave_process(next_state, process); } - } + ); if (dot_output != NULL) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); diff --combined src/mc/mc_compare.cpp index 5b6352ade7,2eb1d25999..696d6885e3 --- a/src/mc/mc_compare.cpp +++ b/src/mc/mc_compare.cpp @@@ -60,6 -60,7 +60,6 @@@ extern "C" static void stack_region_free(stack_region_t s) { if (s) { - xbt_free(s->process_name); xbt_free(s); } } @@@ -101,8 -102,6 +101,8 @@@ static int compare_areas_with_type(stru void* real_area2, mc_snapshot_t snapshot2, mc_mem_region_t region2, dw_type_t type, int pointer_level) { + mc_process_t process = &mc_model_checker->process; + unsigned int cursor = 0; dw_type_t member, subtype, subsubtype; int elm_size, i, res; @@@ -116,7 -115,7 +116,7 @@@ case DW_TAG_enumeration_type: case DW_TAG_union_type: { - return mc_snapshot_region_memcmp( + return MC_snapshot_region_memcmp( real_area1, region1, real_area2, region2, type->byte_size) != 0; } @@@ -170,8 -169,8 +170,8 @@@ case DW_TAG_reference_type: case DW_TAG_rvalue_reference_type: { - void* addr_pointed1 = mc_snapshot_read_pointer_region(real_area1, region1); - void* addr_pointed2 = mc_snapshot_read_pointer_region(real_area2, region2); + void* addr_pointed1 = MC_region_read_pointer(region1, real_area1); + void* addr_pointed2 = MC_region_read_pointer(region2, real_area2); if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) { return (addr_pointed1 != addr_pointed2); @@@ -191,10 -190,10 +191,10 @@@ // * a pointer leads to the read-only segment of the current object; // * a pointer lead to a different ELF object. - if (addr_pointed1 > std_heap + if (addr_pointed1 > process->heap_address && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)) { if (! - (addr_pointed2 > std_heap + (addr_pointed2 > process->heap_address && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))) return 1; // The pointers are both in the heap: @@@ -229,9 -228,9 +229,9 @@@ case DW_TAG_class_type: xbt_dynar_foreach(type->members, cursor, member) { void *member1 = - mc_member_resolve(real_area1, type, member, snapshot1, process_index); + mc_member_resolve(real_area1, type, member, (mc_address_space_t) snapshot1, process_index); void *member2 = - mc_member_resolve(real_area2, type, member, snapshot2, process_index); + mc_member_resolve(real_area2, type, member, (mc_address_space_t) snapshot2, process_index); mc_mem_region_t subregion1 = mc_get_region_hinted(member1, snapshot1, process_index, region1); mc_mem_region_t subregion2 = mc_get_region_hinted(member2, snapshot2, process_index, region2); res = @@@ -261,32 -260,6 +261,32 @@@ static int compare_global_variables(mc_ mc_snapshot_t snapshot2) { xbt_assert(r1 && r2, "Missing region."); + +#ifdef HAVE_SMPI + if (r1->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED) { + xbt_assert(process_index >= 0); + if (r2->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED) { + return 1; + } + + size_t process_count = smpi_process_count(); + xbt_assert(process_count == r1->privatized.regions_count + && process_count == r2->privatized.regions_count); + + // Compare the global variables separately for each simulates process: + for (size_t process_index = 0; process_index < process_count; process_index++) { + int is_diff = compare_global_variables(object_info, process_index, + r1->privatized.regions[process_index], r2->privatized.regions[process_index], + snapshot1, snapshot2); + if (is_diff) return 1; + } + return 0; + } +#else + xbt_assert(r1->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED); +#endif + xbt_assert(r2->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED); + struct mc_compare_state state; xbt_dynar_t variables; @@@ -384,7 -357,6 +384,7 @@@ static int compare_local_variables(int int snapshot_compare(void *state1, void *state2) { + mc_process_t process = &mc_model_checker->process; mc_snapshot_t s1, s2; int num1, num2; @@@ -394,6 -366,11 +394,11 @@@ s2 = ((mc_visited_pair_t) state2)->graph_state->system_state; num1 = ((mc_visited_pair_t) state1)->num; num2 = ((mc_visited_pair_t) state2)->num; + }else if (_sg_mc_termination) { /* Non-progressive cycle MC */ + s1 = ((mc_state_t) state1)->system_state; + s2 = ((mc_state_t) state2)->system_state; + num1 = ((mc_state_t) state1)->num; + num2 = ((mc_state_t) state2)->num; } else { /* Safety or comm determinism MC */ s1 = ((mc_visited_state_t) state1)->system_state; s2 = ((mc_visited_state_t) state2)->system_state; @@@ -484,14 -461,10 +489,14 @@@ #endif /* Init heap information used in heap comparison algorithm */ - xbt_mheap_t heap1 = (xbt_mheap_t) mc_snapshot_read(std_heap, s1, MC_NO_PROCESS_INDEX, - alloca(sizeof(struct mdesc)), sizeof(struct mdesc)); - xbt_mheap_t heap2 = (xbt_mheap_t) mc_snapshot_read(std_heap, s2, MC_NO_PROCESS_INDEX, - alloca(sizeof(struct mdesc)), sizeof(struct mdesc)); + xbt_mheap_t heap1 = (xbt_mheap_t) MC_snapshot_read( + s1, MC_ADDRESS_SPACE_READ_FLAGS_LAZY, + alloca(sizeof(struct mdesc)), process->heap_address, sizeof(struct mdesc), + MC_PROCESS_INDEX_MISSING); + xbt_mheap_t heap2 = (xbt_mheap_t) MC_snapshot_read( + s2, MC_ADDRESS_SPACE_READ_FLAGS_LAZY, + alloca(sizeof(struct mdesc)), process->heap_address, sizeof(struct mdesc), + MC_PROCESS_INDEX_MISSING); res_init = init_heap_information(heap1, heap2, s1->to_ignore, s2->to_ignore); if (res_init == -1) { #ifdef MC_DEBUG @@@ -567,27 -540,21 +572,27 @@@ cursor++; } + size_t regions_count = s1->snapshot_regions_count; + // TODO, raise a difference instead? + xbt_assert(regions_count == s2->snapshot_regions_count); + mc_comp_times->global_variables_comparison_time = 0; - const char *names[3] = { "?", "libsimgrid", "binary" }; -#ifdef MC_DEBUG - double *times[3] = { - NULL, - &mc_comp_times->libsimgrid_global_variables_comparison_time, - &mc_comp_times->binary_global_variables_comparison_time - }; -#endif + for (size_t k = 0; k != regions_count; ++k) { + mc_mem_region_t region1 = s1->snapshot_regions[k]; + mc_mem_region_t region2 = s2->snapshot_regions[k]; - mc_object_info_t object_infos[] = { NULL, mc_libsimgrid_info, mc_binary_info }; + // Preconditions: + if (region1->region_type != MC_REGION_TYPE_DATA) + continue; + + xbt_assert(region1->region_type == region2->region_type); + xbt_assert(region1->object_info == region2->object_info); + + xbt_assert(region1->object_info); + + const char* name = region1->object_info->file_name; - int k = 0; - for (k = 2; k != 0; --k) { #ifdef MC_DEBUG if (is_diff == 0) xbt_os_walltimer_stop(timer); @@@ -595,24 -562,33 +600,24 @@@ #endif /* Compare global variables */ -#ifdef HAVE_SMPI - if (object_infos[k] == mc_binary_info && smpi_privatize_global_variables) { - // Compare the global variables separately for each simulates process: - for (int process_index = 0; process_index < smpi_process_count(); process_index++) { - is_diff = - compare_global_variables(object_infos[k], process_index, - s1->privatization_regions[process_index], s2->privatization_regions[process_index], s1, s2); - if (is_diff) break; - } - } - else -#endif - is_diff = - compare_global_variables(object_infos[k], MC_NO_PROCESS_INDEX, s1->regions[k], s2->regions[k], s1, s2); + is_diff = + compare_global_variables(region1->object_info, MC_ADDRESS_SPACE_READ_FLAGS_NONE, + region1, region2, + s1, s2); if (is_diff != 0) { XBT_TRACE3(mc, state_diff, num1, num2, "Different global variables"); #ifdef MC_DEBUG xbt_os_walltimer_stop(timer); - *times[k] = xbt_os_timer_elapsed(timer); + mc_comp_times->global_variables_comparison_time + += xbt_os_timer_elapsed(timer); XBT_DEBUG("(%d - %d) Different global variables in %s", num1, num2, - names[k]); + name); errors++; #else #ifdef MC_VERBOSE XBT_VERB("(%d - %d) Different global variables in %s", num1, num2, - names[k]); + name); #endif reset_heap_information(); @@@ -708,9 -684,28 +713,9 @@@ void print_comparison_times( XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time); XBT_DEBUG("- Nb bytes used : %f", mc_comp_times->bytes_used_comparison_time); XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time); - XBT_DEBUG("- Binary global variables : %f", - mc_comp_times->binary_global_variables_comparison_time); - XBT_DEBUG("- Libsimgrid global variables : %f", - mc_comp_times->libsimgrid_global_variables_comparison_time); + XBT_DEBUG("- GLobal variables : %f", mc_comp_times->global_variables_comparison_time); XBT_DEBUG("- Heap : %f", mc_comp_times->heap_comparison_time); XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time); } -/**************************** MC snapshot compare simcall **************************/ -/***********************************************************************************/ - -int simcall_HANDLER_mc_compare_snapshots(smx_simcall_t simcall, - mc_snapshot_t s1, mc_snapshot_t s2) -{ - return snapshot_compare(s1, s2); -} - -int MC_compare_snapshots(void *s1, void *s2) -{ - - return simcall_mc_compare_snapshots(s1, s2); - -} - } diff --combined src/mc/mc_config.c index 62517120ba,d52c95a84d..79e2be36a0 --- a/src/mc/mc_config.c +++ b/src/mc/mc_config.c @@@ -58,8 -58,9 +58,9 @@@ int _sg_mc_comms_determinism = 0 int _sg_mc_send_determinism = 0; int _sg_mc_safety = 0; int _sg_mc_liveness = 0; +int _sg_mc_snapshot_fds = 0; + int _sg_mc_termination = 0; - void _mc_cfg_cb_reduce(const char *name, int pos) { if (_sg_cfg_init_status && !_sg_do_model_check) { @@@ -118,15 -119,6 +119,15 @@@ void _mc_cfg_cb_hash(const char *name, _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name); } +void _mc_cfg_cb_snapshot_fds(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a value to enable/disable the use of FD snapshoting, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_snapshot_fds = xbt_cfg_get_boolean(_sg_cfg_set, name); +} + void _mc_cfg_cb_max_depth(const char *name, int pos) { if (_sg_cfg_init_status && !_sg_do_model_check) { @@@ -161,7 -153,6 +162,6 @@@ void _mc_cfg_cb_comms_determinism(cons ("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); } _sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); - mc_reduce_kind = e_mc_reduce_none; } void _mc_cfg_cb_send_determinism(const char *name, int pos) @@@ -171,7 -162,15 +171,15 @@@ ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); } _sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); - mc_reduce_kind = e_mc_reduce_none; + } + + void _mc_cfg_cb_termination(const char *name, int pos) + { + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a value to enable/disable the detection of non progressive cycles after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_termination = xbt_cfg_get_boolean(_sg_cfg_set, name); } #endif diff --combined src/mc/mc_global.c index 56ad792d39,790d1e9b22..eaba624acf --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@@ -4,14 -4,15 +4,14 @@@ /* 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 "mc_base.h" #ifndef _XBT_WIN32 #include -#include #include #include -#include -#include #endif #include "simgrid/sg_config.h" @@@ -22,8 -23,8 +22,8 @@@ #include "xbt/dict.h" #ifdef HAVE_MC -#define UNW_LOCAL_ONLY #include +#include #include "../xbt/mmalloc/mmprivate.h" #include "mc_object_info.h" @@@ -34,18 -35,12 +34,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 @@@ -64,6 -59,14 +64,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]; @@@ -101,29 -104,57 +101,29 @@@ static void MC_init_dot_output( } -static void MC_init_debug_info(void) -{ - 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_model_checker_t mc_model_checker = NULL; - -mc_model_checker_t MC_model_checker_new() +void MC_init() { - 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); + MC_init_pid(getpid(), -1); } -void MC_init() +void MC_init_pid(pid_t pid, int socket) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + if (mc_mode == MC_MODE_NONE) { + if (getenv(MC_ENV_SOCKET_FD)) { + mc_mode = MC_MODE_CLIENT; + } else { + mc_mode = MC_MODE_STANDALONE; + } + } 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(); + mc_model_checker = MC_model_checker_new(pid, socket); mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); @@@ -131,6 -162,9 +131,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(); @@@ -139,7 -173,7 +139,7 @@@ MC_SET_STD_HEAP; - if (_sg_mc_visited > 0 || _sg_mc_liveness) { + if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination) { /* 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", "*"); @@@ -178,25 -212,16 +178,25 @@@ /* 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: */ + + MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); - smx_process_t process; - xbt_swag_foreach(process, simix_global->process_list) { - MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); + smx_process_t process; + xbt_swag_foreach(process, simix_global->process_list) { + MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); + } } } - if (raw_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); + + if (mc_mode == MC_MODE_CLIENT) { + // This will move somehwere else: + MC_client_handle_messages(); + } } @@@ -205,9 -230,13 +205,9 @@@ 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; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@@ -220,22 -249,30 +220,25 @@@ 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->comm_deterministic = 1; + 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; - + mmalloc_set_current_heap(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; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@@ -252,7 -289,8 +255,7 @@@ MC_modelcheck_safety(); - if (mc_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); xbt_abort(); //MC_exit(); @@@ -260,11 -298,15 +263,11 @@@ 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; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@@ -280,7 -322,8 +283,7 @@@ MC_print_statistics(mc_stats); xbt_free(mc_time); - if (mc_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); } @@@ -289,11 -332,15 +292,15 @@@ void MC_do_the_modelcheck_for_real( 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 (mc_reduce_kind == e_mc_reduce_unset) - mc_reduce_kind = e_mc_reduce_dpor; - XBT_INFO("Check a safety property"); + if(_sg_mc_termination){ + XBT_INFO("Check non progressive cycles"); + mc_reduce_kind = e_mc_reduce_none; + }else{ + XBT_INFO("Check a safety property"); + } MC_modelcheck_safety_init(); } else { if (mc_reduce_kind == e_mc_reduce_unset) @@@ -315,34 -362,16 +322,34 @@@ 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)); + if (s == -1) + xbt_die("Could not receive message"); + else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) { + xbt_die("Unexpected message, expected MC_MESSAGE_DEADLOCK_CHECK_REPLY %i %i vs %i %i", + (int) s, (int) message.type, (int) sizeof(message), (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY + ); + } + 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; } @@@ -354,7 -383,7 +361,7 @@@ void handle_comm_pattern(e_mc_call_type break; case MC_CALL_TYPE_SEND: case MC_CALL_TYPE_RECV: - get_comm_pattern(pattern, req, call_type); + get_comm_pattern(pattern, req, call_type, backtracking); break; case MC_CALL_TYPE_WAIT: case MC_CALL_TYPE_WAITANY: @@@ -364,11 -393,9 +371,9 @@@ 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); - // First wait only must be considered: - if (current_comm->comm.refcount == 1) - complete_comm_pattern(pattern, current_comm, backtracking); - break; + complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking); } + break; default: xbt_die("Unexpected call type %i", (int)call_type); } @@@ -421,7 -448,7 +426,7 @@@ static void MC_restore_communications_p */ 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; @@@ -432,7 -459,7 +437,7 @@@ XBT_DEBUG("**** Begin Replay ****"); /* Intermediate backtracking */ - if(_sg_mc_checkpoint > 0) { + if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) { start_item = xbt_fifo_get_first_item(stack); state = (mc_state_t)xbt_fifo_get_item_content(start_item); if(state->system_state){ @@@ -475,9 -502,7 +480,9 @@@ 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)) { @@@ -491,7 -516,7 +496,7 @@@ if (_sg_mc_comms_determinism || _sg_mc_send_determinism) 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) @@@ -510,7 -535,13 +515,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) @@@ -562,8 -593,7 +567,8 @@@ 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)) { @@@ -574,7 -604,7 +579,7 @@@ } - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); MC_wait_for_requests(); } @@@ -602,7 -632,8 +607,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); @@@ -611,13 -642,22 +616,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; @@@ -636,7 -676,8 +641,7 @@@ } } - if (!raw_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } void MC_show_deadlock(smx_simcall_t req) @@@ -654,6 -695,15 +659,15 @@@ MC_print_statistics(mc_stats); } + void MC_show_non_termination(void){ + XBT_INFO("******************************************"); + XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); + XBT_INFO("******************************************"); + XBT_INFO("Counter-example execution trace:"); + MC_dump_stack_safety(mc_stack); + MC_print_statistics(mc_stats); + } + void MC_show_stack_liveness(xbt_fifo_t stack) { @@@ -678,16 -728,38 +692,29 @@@ 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("******************************************************"); + XBT_INFO("**** Only-send-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", initial_global_state->recv_diff); + }else if(!initial_global_state->send_deterministic && initial_global_state->recv_deterministic) { + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-recv-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + 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); @@@ -696,84 -768,80 +723,83 @@@ 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); } - if (initial_global_state != NULL) { + if (initial_global_state != NULL && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) { + XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); if (_sg_mc_comms_determinism) - XBT_INFO("Communication-deterministic : %s", !initial_global_state->comm_deterministic ? "No" : "Yes"); - if (_sg_mc_send_determinism) - XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); + 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); } 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; @@@ -795,7 -863,9 +821,7 @@@ ++nstack; } - - if (raw_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); } #endif diff --combined src/mc/mc_page_snapshot.cpp index c8aa50fadd,5f0e601ea7..72997ba0b9 --- a/src/mc/mc_page_snapshot.cpp +++ b/src/mc/mc_page_snapshot.cpp @@@ -1,5 -1,10 +1,12 @@@ + /* MC interface: definitions that non-MC modules must see, but not the user */ + + /* Copyright (c) 2014-2015. The SimGrid Team. All rights reserved. */ + + /* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include // pread, pwrite + #include "mc_page_store.h" #include "mc_mmu.h" #include "mc_private.h" @@@ -22,17 -27,10 +29,17 @@@ extern "C" * @param reference_pages Snapshot page numbers of the previous soft_dirty_reset (or NULL) * @return Snapshot page numbers of this new snapshot */ -size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages) +size_t* mc_take_page_snapshot_region(mc_process_t process, + void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages) { size_t* pagenos = (size_t*) malloc(page_count * sizeof(size_t)); + const bool is_self = MC_process_is_self(process); + + void* temp = NULL; + if (!is_self) + temp = malloc(xbt_pagesize); + for (size_t i=0; i!=page_count; ++i) { bool softclean = pagemap && !(pagemap[i] & SOFT_DIRTY); if (softclean && reference_pages) { @@@ -43,27 -41,10 +50,27 @@@ // Otherwise, we need to store the page the hard way // (by reading its content): void* page = (char*) data + (i << xbt_pagebits); - pagenos[i] = mc_model_checker->pages->store_page(page); + xbt_assert(mc_page_offset(page)==0, "Not at the beginning of a page"); + void* page_data; + if (is_self) { + page_data = page; + } else { + /* Adding another copy (and a syscall) will probably slow things a lot. + TODO, optimize this somehow (at least by grouping the syscalls) + if needed. Either: + - reduce the number of syscalls; + - let the application snapshot itself; + - move the segments in shared memory (this will break `fork` however). + */ + page_data = temp; + MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE, + temp, page, xbt_pagesize, MC_PROCESS_INDEX_DISABLED); + } + pagenos[i] = mc_model_checker->pages->store_page(page_data); } } + free(temp); return pagenos; } @@@ -85,8 -66,7 +92,8 @@@ void mc_free_page_snapshot_region(size_ * @param pagemap Linux kernel pagemap values fot this region (or NULL) * @param reference_pages Snapshot page numbers of the previous soft_dirty_reset (or NULL) */ -void mc_restore_page_snapshot_region(void* start_addr, size_t page_count, size_t* pagenos, uint64_t* pagemap, size_t* reference_pagenos) +void mc_restore_page_snapshot_region(mc_process_t process, + void* start_addr, size_t page_count, size_t* pagenos, uint64_t* pagemap, size_t* reference_pagenos) { for (size_t i=0; i!=page_count; ++i) { @@@ -100,7 -80,7 +107,7 @@@ // Otherwise, copy the page: void* target_page = mc_page_from_number(start_addr, i); const void* source_page = mc_model_checker->pages->get_page(pagenos[i]); - memcpy(target_page, source_page, xbt_pagesize); + MC_process_write(process, source_page, target_page, xbt_pagesize); } } @@@ -186,18 -166,15 +193,18 @@@ static void mc_read_pagemap(uint64_t* p // ***** High level API -mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg) +mc_mem_region_t mc_region_new_sparse(mc_region_type_t region_type, + void *start_addr, void* permanent_addr, size_t size, + mc_mem_region_t ref_reg) { - mc_mem_region_t new_reg = xbt_new(s_mc_mem_region_t, 1); + mc_process_t process = &mc_model_checker->process; - new_reg->start_addr = start_addr; - new_reg->permanent_addr = permanent_addr; - new_reg->data = NULL; - new_reg->size = size; - new_reg->page_numbers = NULL; + mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1); + region->region_type = region_type; + region->storage_type = MC_REGION_STORAGE_TYPE_CHUNKED; + region->start_addr = start_addr; + region->permanent_addr = permanent_addr; + region->size = size; xbt_assert((((uintptr_t)start_addr) & (xbt_pagesize-1)) == 0, "Not at the beginning of a page"); @@@ -206,27 -183,22 +213,27 @@@ size_t page_count = mc_page_count(size); uint64_t* pagemap = NULL; - if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot) { - pagemap = (uint64_t*) mmalloc_no_memset(mc_heap, sizeof(uint64_t) * page_count); + if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot && + MC_process_is_self(process)) { + pagemap = (uint64_t*) malloc_no_memset(sizeof(uint64_t) * page_count); mc_read_pagemap(pagemap, mc_page_number(NULL, permanent_addr), page_count); } + size_t* reg_page_numbers = NULL; + if (ref_reg!=NULL && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_CHUNKED) + reg_page_numbers = ref_reg->chunked.page_numbers; + // Take incremental snapshot: - new_reg->page_numbers = mc_take_page_snapshot_region(permanent_addr, page_count, pagemap, - ref_reg==NULL ? NULL : ref_reg->page_numbers); + region->chunked.page_numbers = mc_take_page_snapshot_region(process, + permanent_addr, page_count, pagemap, reg_page_numbers); if(pagemap) { mfree(mc_heap, pagemap); } - return new_reg; + return region; } -void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg) +void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg, mc_mem_region_t ref_reg) { xbt_assert((((uintptr_t)reg->permanent_addr) & (xbt_pagesize-1)) == 0, "Not at the beginning of a page"); @@@ -235,20 -207,14 +242,20 @@@ uint64_t* pagemap = NULL; // Read soft-dirty bits if necessary in order to know which pages have changed: - if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot) { - pagemap = (uint64_t*) mmalloc_no_memset(mc_heap, sizeof(uint64_t) * page_count); + if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot + && MC_process_is_self(process)) { + pagemap = (uint64_t*) malloc_no_memset(sizeof(uint64_t) * page_count); mc_read_pagemap(pagemap, mc_page_number(NULL, reg->permanent_addr), page_count); } - // Incremental per-page snapshot restoration: - mc_restore_page_snapshot_region(reg->permanent_addr, page_count, reg->page_numbers, - pagemap, ref_reg ? ref_reg->page_numbers : NULL); + // Incremental per-page snapshot restoration:s + size_t* reg_page_numbers = NULL; + if (ref_reg && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_CHUNKED) + reg_page_numbers = ref_reg->chunked.page_numbers; + + mc_restore_page_snapshot_region(process, + reg->permanent_addr, page_count, reg->chunked.page_numbers, + pagemap, reg_page_numbers); if(pagemap) { free(pagemap); diff --combined src/mc/mc_private.h index bcc454fce1,86b7e64837..b5f061acd7 --- 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,7 -21,6 +23,7 @@@ #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" @@@ -41,15 -38,12 +41,15 @@@ 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; @@@ -62,6 -56,7 +62,7 @@@ void MC_replay_liveness(xbt_fifo_t stac void MC_show_deadlock(smx_simcall_t req); void MC_show_stack_safety(xbt_fifo_t stack); void MC_dump_stack_safety(xbt_fifo_t stack); + void MC_show_non_termination(void); /** Stack (of `mc_state_t`) representing the current position of the * the MC in the exploration graph @@@ -88,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; @@@ -110,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 **********************************/ diff --combined src/mc/mc_request.c index 1b12665d90,5c7d573392..ad4d1fab3c --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@@ -7,7 -7,6 +7,7 @@@ #include "mc_request.h" #include "mc_safety.h" #include "mc_private.h" +#include "mc_smx.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc, "Logging specific to MC (request)"); @@@ -43,8 -42,6 +43,8 @@@ int MC_request_depend(smx_simcall_t r1 SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) : simcall_comm_irecv__get__rdv(r1); + // FIXME, remote access to comm object + if (rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy && simcall_comm_wait__get__timeout(r2) <= 0) return FALSE; @@@ -234,25 -231,23 +234,26 @@@ char *MC_request_to_string(smx_simcall_ { char *type = NULL, *args = NULL, *str = NULL, *p = NULL, *bs = NULL; smx_synchro_t act = NULL; + smx_mutex_t mutex = NULL; size_t size = 0; + smx_process_t issuer = MC_smx_simcall_get_issuer(req); + switch (req->call) { case SIMCALL_COMM_ISEND: type = xbt_strdup("iSend"); p = pointer_to_string(simcall_comm_isend__get__src_buff(req)); bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req)); - if (req->issuer->smx_host) + if (issuer->smx_host) args = - bprintf("src=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), req->issuer->name, + bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid, + MC_smx_process_get_host_name(issuer), + MC_smx_process_get_name(issuer), p, bs); else args = - bprintf("src=(%lu)%s, buff=%s, size=%s", req->issuer->pid, - req->issuer->name, p, bs); + bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid, + MC_smx_process_get_name(issuer), p, bs); break; case SIMCALL_COMM_IRECV: size = @@@ -261,17 -256,15 +262,17 @@@ type = xbt_strdup("iRecv"); p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req)); bs = buff_size_to_string(size); - if (req->issuer->smx_host) + if (issuer->smx_host) args = - bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), req->issuer->name, + bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid, + MC_smx_process_get_host_name(issuer), + MC_smx_process_get_name(issuer), p, bs); else args = - bprintf("dst=(%lu)%s, buff=%s, size=%s", req->issuer->pid, - req->issuer->name, p, bs); + bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid, + MC_smx_process_get_name(issuer), + p, bs); break; case SIMCALL_COMM_WAIT: act = simcall_comm_wait__get__comm(req); @@@ -282,16 -275,15 +283,16 @@@ } else { type = xbt_strdup("Wait"); p = pointer_to_string(act); + // TODO, fix remote access to comm + smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc); + smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc); args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p, - act->comm.src_proc ? act->comm.src_proc->pid : 0, - act->comm.src_proc ? MSG_host_get_name(act->comm.src_proc-> - smx_host) : "", - act->comm.src_proc ? act->comm.src_proc->name : "", - act->comm.dst_proc ? act->comm.dst_proc->pid : 0, - act->comm.dst_proc ? MSG_host_get_name(act->comm.dst_proc-> - smx_host) : "", - act->comm.dst_proc ? act->comm.dst_proc->name : ""); + src_proc ? src_proc->pid : 0, + src_proc ? MC_smx_process_get_host_name(src_proc) : "", + src_proc ? MC_smx_process_get_name(src_proc) : "", + dst_proc ? dst_proc->pid : 0, + dst_proc ? MC_smx_process_get_host_name(dst_proc) : "", + dst_proc ? MC_smx_process_get_name(dst_proc) : ""); } break; case SIMCALL_COMM_TEST: @@@ -303,16 -295,11 +304,16 @@@ } else { type = xbt_strdup("Test TRUE"); p = pointer_to_string(act); + // TODO, get process, get process name + smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc); + smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc); args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p, - act->comm.src_proc->pid, act->comm.src_proc->name, - MSG_host_get_name(act->comm.src_proc->smx_host), - act->comm.dst_proc->pid, act->comm.dst_proc->name, - MSG_host_get_name(act->comm.dst_proc->smx_host)); + src_proc->pid, + MC_smx_process_get_name(src_proc), + MC_smx_process_get_host_name(src_proc), + dst_proc->pid, + MC_smx_process_get_name(dst_proc), + MC_smx_process_get_host_name(dst_proc)); } break; @@@ -342,6 -329,12 +343,12 @@@ } break; + case SIMCALL_MUTEX_LOCK: + mutex = simcall_mutex_lock__get__mutex(req); + type = xbt_strdup("Mutex LOCK"); + args = bprintf("locked = %d, owner = %d, sleeping = %d", mutex->locked, mutex->owner != NULL ? (int)mutex->owner->pid : -1, xbt_swag_size(mutex->sleeping)); + break; + case SIMCALL_MC_SNAPSHOT: type = xbt_strdup("MC_SNAPSHOT"); args = NULL; @@@ -362,18 -355,14 +369,18 @@@ } if (args != NULL) { + // FIXME, get process name str = - bprintf("[(%lu)%s (%s)] %s(%s)", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), req->issuer->name, + bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid, + MC_smx_process_get_host_name(issuer), + MC_smx_process_get_name(issuer), type, args); } else { + // FIXME, get process name str = - bprintf("[(%lu)%s (%s)] %s ", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), req->issuer->name, + bprintf("[(%lu)%s (%s)] %s ", issuer->pid, + MC_smx_process_get_host_name(issuer), + MC_smx_process_get_name(issuer), type); } @@@ -390,7 -379,6 +397,7 @@@ unsigned int MC_request_testany_fail(sm smx_synchro_t action; xbt_dynar_foreach(simcall_comm_testany__get__comms(req), cursor, action) { + // FIXME, remote access to comm object if (action->comm.src_proc && action->comm.dst_proc) return FALSE; } @@@ -402,8 -390,6 +409,8 @@@ int MC_request_is_enabled_by_idx(smx_si { smx_synchro_t act; + // FIXME, remote access to comm object + switch (req->call) { case SIMCALL_COMM_WAIT: @@@ -438,135 -424,135 +445,139 @@@ int MC_process_is_enabled(smx_process_ char *MC_request_get_dot_output(smx_simcall_t req, int value) { - char *str = NULL, *label = NULL; smx_synchro_t act = NULL; - + + const smx_process_t issuer = MC_smx_simcall_get_issuer(req); + switch (req->call) { case SIMCALL_COMM_ISEND: - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] iSend", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host)); + bprintf("[(%lu)%s] iSend", issuer->pid, + MC_smx_process_get_host_name(issuer)); else - label = bprintf("[(%lu)] iSend", req->issuer->pid); + label = bprintf("[(%lu)] iSend", issuer->pid); break; case SIMCALL_COMM_IRECV: - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] iRecv", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host)); + bprintf("[(%lu)%s] iRecv", issuer->pid, + MC_smx_process_get_host_name(issuer)); else - label = bprintf("[(%lu)] iRecv", req->issuer->pid); + label = bprintf("[(%lu)] iRecv", issuer->pid); break; case SIMCALL_COMM_WAIT: act = simcall_comm_wait__get__comm(req); if (value == -1) { - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] WaitTimeout", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host)); + bprintf("[(%lu)%s] WaitTimeout", issuer->pid, + MC_smx_process_get_host_name(issuer)); else - label = bprintf("[(%lu)] WaitTimeout", req->issuer->pid); + label = bprintf("[(%lu)] WaitTimeout", issuer->pid); } else { - if (req->issuer->smx_host) + // FIXME, remote access to act->comm + smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc); + smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc); + if (issuer->smx_host) label = - bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), - act->comm.src_proc ? act->comm.src_proc->pid : 0, - act->comm.dst_proc ? act->comm.dst_proc->pid : 0); + bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid, + MC_smx_process_get_host_name(issuer), + src_proc ? src_proc->pid : 0, + dst_proc ? dst_proc->pid : 0); else label = - bprintf("[(%lu)] Wait [(%lu)->(%lu)]", req->issuer->pid, - act->comm.src_proc ? act->comm.src_proc->pid : 0, - act->comm.dst_proc ? act->comm.dst_proc->pid : 0); + bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid, + src_proc ? src_proc->pid : 0, + dst_proc ? dst_proc->pid : 0); } break; case SIMCALL_COMM_TEST: act = simcall_comm_test__get__comm(req); if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) { - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] Test FALSE", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host)); + bprintf("[(%lu)%s] Test FALSE", issuer->pid, + MC_smx_process_get_host_name(issuer)); else - label = bprintf("[(%lu)] Test FALSE", req->issuer->pid); + label = bprintf("[(%lu)] Test FALSE", issuer->pid); } else { - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] Test TRUE", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host)); + bprintf("[(%lu)%s] Test TRUE", issuer->pid, + MC_smx_process_get_host_name(issuer)); else - label = bprintf("[(%lu)] Test TRUE", req->issuer->pid); + label = bprintf("[(%lu)] Test TRUE", issuer->pid); } break; case SIMCALL_COMM_WAITANY: - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] WaitAny [%d of %lu]", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), value + 1, + bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid, + MC_smx_process_get_host_name(issuer), value + 1, xbt_dynar_length(simcall_comm_waitany__get__comms(req))); else label = - bprintf("[(%lu)] WaitAny [%d of %lu]", req->issuer->pid, value + 1, + bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1, xbt_dynar_length(simcall_comm_waitany__get__comms(req))); break; case SIMCALL_COMM_TESTANY: if (value == -1) { - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] TestAny FALSE", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host)); + bprintf("[(%lu)%s] TestAny FALSE", issuer->pid, + MC_smx_process_get_host_name(issuer)); else - label = bprintf("[(%lu)] TestAny FALSE", req->issuer->pid); + label = bprintf("[(%lu)] TestAny FALSE", issuer->pid); } else { - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), value + 1, + bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid, + MC_smx_process_get_host_name(issuer), value + 1, xbt_dynar_length(simcall_comm_testany__get__comms(req))); else label = - bprintf("[(%lu)] TestAny TRUE [%d of %lu]", req->issuer->pid, + bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid, value + 1, xbt_dynar_length(simcall_comm_testany__get__comms(req))); } break; + case SIMCALL_MUTEX_LOCK: + label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid); + break; + case SIMCALL_MC_RANDOM: - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] MC_RANDOM (%d)", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), value); + bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid, + MC_smx_process_get_host_name(issuer), value); else - label = bprintf("[(%lu)] MC_RANDOM (%d)", req->issuer->pid, value); + label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value); break; case SIMCALL_MC_SNAPSHOT: - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] MC_SNAPSHOT", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host)); + bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid, + MC_smx_process_get_host_name(issuer)); else - label = bprintf("[(%lu)] MC_SNAPSHOT", req->issuer->pid); + label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid); break; case SIMCALL_MC_COMPARE_SNAPSHOTS: - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host)); + bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid, + MC_smx_process_get_host_name(issuer)); else - label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", req->issuer->pid); + label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid); break; default: @@@ -575,7 -561,7 +586,7 @@@ str = bprintf("label = \"%s\", color = %s, fontcolor = %s", label, - colors[req->issuer->pid - 1], colors[req->issuer->pid - 1]); + colors[issuer->pid - 1], colors[issuer->pid - 1]); xbt_free(label); return str; diff --combined src/mc/mc_safety.c index 544cf510a1,38e0999740..3dea427d7c --- a/src/mc/mc_safety.c +++ b/src/mc/mc_safety.c @@@ -4,34 -4,51 +4,48 @@@ /* 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 "mc_state.h" #include "mc_request.h" #include "mc_safety.h" #include "mc_private.h" #include "mc_record.h" +#include "mc_smx.h" #include "xbt/mmalloc/mmprivate.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety verification "); + static int is_exploration_stack_state(mc_state_t current_state){ + + xbt_fifo_item_t item; + mc_state_t stack_state; + for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) { + stack_state = (mc_state_t) xbt_fifo_get_item_content(item); + if(snapshot_compare(stack_state, current_state) == 0){ + XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num); + return 1; + } + } + return 0; + } + /** * \brief Initialize the DPOR exploration algorithm */ void MC_pre_modelcheck_safety() { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - mc_state_t initial_state = NULL; smx_process_t process; - /* Create the initial state and push it into the exploration stack */ - if (!mc_mem_set) - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if (_sg_mc_visited > 0) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); initial_state = MC_state_new(); - MC_SET_STD_HEAP; XBT_DEBUG("**************************************************"); @@@ -43,16 -60,18 +57,16 @@@ MC_SET_MC_HEAP; /* Get an enabled process and insert it in the interleave set of the initial state */ - xbt_swag_foreach(process, simix_global->process_list) { + MC_EACH_SIMIX_PROCESS(process, if (MC_process_is_enabled(process)) { MC_state_interleave_process(initial_state, process); if (mc_reduce_kind != e_mc_reduce_none) break; } - } + ); xbt_fifo_unshift(mc_stack, initial_state); - - if (!mc_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } @@@ -103,7 -122,7 +117,7 @@@ void MC_modelcheck_safety(void mc_stats->executed_transitions++; /* Answer the request */ - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@@ -113,16 -132,21 +127,21 @@@ next_state = MC_state_new(); + if(_sg_mc_termination && is_exploration_stack_state(next_state)){ + MC_show_non_termination(); + return; + } + if ((visited_state = is_visited_state(next_state)) == NULL) { /* Get an enabled process and insert it in the interleave set of the next state */ - xbt_swag_foreach(process, simix_global->process_list) { + MC_EACH_SIMIX_PROCESS(process, if (MC_process_is_enabled(process)) { MC_state_interleave_process(next_state, process); if (mc_reduce_kind != e_mc_reduce_none) break; } - } + ); if (dot_output != NULL) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); @@@ -189,7 -213,6 +208,7 @@@ while ((state = xbt_fifo_shift(mc_stack)) != NULL) { if (mc_reduce_kind == e_mc_reduce_dpor) { req = MC_state_get_internal_request(state); + const smx_process_t issuer = MC_smx_simcall_get_issuer(req); xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) { if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { @@@ -204,8 -227,8 +223,8 @@@ xbt_free(req_str); } - if (!MC_state_process_is_done(prev_state, req->issuer)) - MC_state_interleave_process(prev_state, req->issuer); + if (!MC_state_process_is_done(prev_state, issuer)) + MC_state_interleave_process(prev_state, issuer); else XBT_DEBUG("Process %p is in done set", req->issuer); @@@ -218,11 -241,10 +237,11 @@@ } else { + const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state)); XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", - req->call, req->issuer->pid, state->num, + req->call, issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, - MC_state_get_internal_request(prev_state)->issuer->pid, + previous_issuer->pid, prev_state->num); } diff --combined src/mc/mc_snapshot.h index 70b37f8b6e,d393116e2d..98a2c70a75 --- a/src/mc/mc_snapshot.h +++ b/src/mc/mc_snapshot.h @@@ -19,8 -19,6 +19,8 @@@ #include "mc_model_checker.h" #include "mc_page_store.h" #include "mc_mmalloc.h" +#include "mc_address_space.h" +#include "mc_unw.h" SG_BEGIN_DECL() @@@ -28,49 -26,21 +28,49 @@@ void mc_softdirty_reset(void) // ***** Snapshot region -#define NB_REGIONS 3 /* binary data (data + BSS) (type = 2), libsimgrid data (data + BSS) (type = 1), std_heap (type = 0)*/ +typedef enum e_mc_region_type_t { + MC_REGION_TYPE_UNKNOWN = 0, + MC_REGION_TYPE_HEAP = 1, + MC_REGION_TYPE_DATA = 2 +} mc_region_type_t; + +// TODO, use OO instead of this +typedef enum e_mc_region_storeage_type_t { + MC_REGION_STORAGE_TYPE_NONE = 0, + MC_REGION_STORAGE_TYPE_FLAT = 1, + MC_REGION_STORAGE_TYPE_CHUNKED = 2, + MC_REGION_STORAGE_TYPE_PRIVATIZED = 3 +} mc_region_storage_type_t; /** @brief Copy/snapshot of a given memory region * - * Two types of region snapshots exist: + * Different types of region snapshot storage types exist: *
    *
  • flat/dense snapshots are a simple copy of the region;
    • *
  • sparse/per-page snapshots are snaapshots which shared * identical pages.
    • + *
  • privatized (SMPI global variable privatisation). *
+ * + * This is handled with a variant based approch: + * + * * `storage_type` identified the type of storage; + * * an anonymous enum is used to distinguish the relevant types for + * each type. */ -typedef struct s_mc_mem_region{ +typedef struct s_mc_mem_region s_mc_mem_region_t, *mc_mem_region_t; + +struct s_mc_mem_region { + mc_region_type_t region_type; + mc_region_storage_type_t storage_type; + mc_object_info_t object_info; + /** @brief Virtual address of the region in the simulated process */ void *start_addr; + /** @brief Size of the data region in bytes */ + size_t size; + /** @brief Permanent virtual address of the region * * This is usually the same address as the simuilated process address. @@@ -82,29 -52,23 +82,29 @@@ * */ void *permanent_addr; - /** @brief Copy of the snapshot for flat snapshots regions (NULL otherwise) */ - void *data; + union { + struct { + /** @brief Copy of the snapshot for flat snapshots regions (NULL otherwise) */ + void *data; + } flat; + struct { + /** @brief Pages indices in the page store for per-page snapshots (NULL otherwise) */ + size_t* page_numbers; + } chunked; + struct { + size_t regions_count; + mc_mem_region_t* regions; + } privatized; + }; - /** @brief Size of the data region in bytes */ - size_t size; - - /** @brief Pages indices in the page store for per-page snapshots (NULL otherwise) */ - size_t* page_numbers; - -} s_mc_mem_region_t, *mc_mem_region_t; +}; -mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, void* data_addr, size_t size, mc_mem_region_t ref_reg); +mc_mem_region_t mc_region_new_sparse(mc_region_type_t type, void *start_addr, void* data_addr, size_t size, mc_mem_region_t ref_reg); void MC_region_destroy(mc_mem_region_t reg); -void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg); +void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg, mc_mem_region_t ref_reg); static inline __attribute__ ((always_inline)) -bool mc_region_contain(mc_mem_region_t region, void* p) +bool mc_region_contain(mc_mem_region_t region, const void* p) { return p >= region->start_addr && p < (void*)((char*) region->start_addr + region->size); @@@ -114,12 -78,12 +114,12 @@@ static inline __attribute__((always_inl void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region) { size_t pageno = mc_page_number(region->start_addr, (void*) addr); - size_t snapshot_pageno = region->page_numbers[pageno]; + size_t snapshot_pageno = region->chunked.page_numbers[pageno]; const void* snapshot_page = mc_page_store_get_page(mc_model_checker->pages, snapshot_pageno); return (char*) snapshot_page + mc_page_offset((void*) addr); } -mc_mem_region_t mc_get_snapshot_region(void* addr, mc_snapshot_t snapshot, int process_index); +mc_mem_region_t mc_get_snapshot_region(const void* addr, mc_snapshot_t snapshot, int process_index); /** \brief Translate a pointer from process address space to snapshot address space * @@@ -151,30 -115,19 +151,30 @@@ void* mc_translate_address(uintptr_t ad return (void *) addr; } - // Flat snapshot: - else if (region->data) { - uintptr_t offset = addr - (uintptr_t) region->start_addr; - return (void *) ((uintptr_t) region->data + offset); - } + switch (region->storage_type) { + case MC_REGION_STORAGE_TYPE_NONE: + default: + xbt_die("Storage type not supported"); + + case MC_REGION_STORAGE_TYPE_FLAT: + { + uintptr_t offset = addr - (uintptr_t) region->start_addr; + return (void *) ((uintptr_t) region->flat.data + offset); + } - // Per-page snapshot: - else if (region->page_numbers) { + case MC_REGION_STORAGE_TYPE_CHUNKED: return mc_translate_address_region(addr, region); - } - else { - xbt_die("No data for this memory region"); + case MC_REGION_STORAGE_TYPE_PRIVATIZED: + { + xbt_assert(process_index >=0, + "Missing process index for privatized region"); + xbt_assert((size_t) process_index < region->privatized.regions_count, + "Out of range process index"); + mc_mem_region_t subregion = region->privatized.regions[process_index]; + xbt_assert(subregion, "Missing memory region for process %i", process_index); + return mc_translate_address(addr, snapshot, process_index); + } } } @@@ -198,13 -151,11 +198,13 @@@ typedef struct s_fd_infos int flags; }s_fd_infos_t, *fd_infos_t; -struct s_mc_snapshot{ +struct s_mc_snapshot { + mc_process_t process; + s_mc_address_space_t address_space; size_t heap_bytes_used; - mc_mem_region_t regions[NB_REGIONS]; + mc_mem_region_t* snapshot_regions; + size_t snapshot_regions_count; xbt_dynar_t enabled_processes; - mc_mem_region_t* privatization_regions; int privatization_index; size_t *stack_sizes; xbt_dynar_t stacks; @@@ -215,6 -166,18 +215,6 @@@ fd_infos_t *current_fd; }; -/** @brief Process index used when no process is available - * - * The expected behaviour is that if a process index is needed it will fail. - * */ -#define MC_NO_PROCESS_INDEX -1 - -/** @brief Process index when any process is suitable - * - * We could use a special negative value in the future. - */ -#define MC_ANY_PROCESS_INDEX 0 - static inline __attribute__ ((always_inline)) mc_mem_region_t mc_get_region_hinted(void* addr, mc_snapshot_t snapshot, int process_index, mc_mem_region_t region) { @@@ -240,19 -203,20 +240,21 @@@ typedef struct s_mc_stack_frame typedef struct s_mc_snapshot_stack{ xbt_dynar_t local_variables; + mc_unw_context_t context; xbt_dynar_t stack_frames; // mc_stack_frame_t int process_index; }s_mc_snapshot_stack_t, *mc_snapshot_stack_t; -typedef struct s_mc_global_t{ +typedef struct s_mc_global_t { mc_snapshot_t snapshot; int raw_mem_set; int prev_pair; char *prev_req; int initial_communications_pattern_done; - int comm_deterministic; + int recv_deterministic; int send_deterministic; + char *send_diff; + char *recv_diff; }s_mc_global_t, *mc_global_t; typedef struct s_mc_checkpoint_ignore_region{ @@@ -260,7 -224,7 +262,7 @@@ size_t size; }s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t; -static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot); +static const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot); mc_snapshot_t MC_take_snapshot(int num_state); void MC_restore_snapshot(mc_snapshot_t); @@@ -268,42 -232,40 +270,42 @@@ void MC_free_snapshot(mc_snapshot_t) int mc_important_snapshot(mc_snapshot_t snapshot); -size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages); +size_t* mc_take_page_snapshot_region(mc_process_t process, + void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages); void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count); -void mc_restore_page_snapshot_region(void* start_addr, size_t page_count, size_t* pagenos, uint64_t* pagemap, size_t* reference_pagenos); - -static inline __attribute__((always_inline)) -bool mc_snapshot_region_linear(mc_mem_region_t region) { - return !region || !region->data; -} - -void* mc_snapshot_read_fragmented(void* addr, mc_mem_region_t region, void* target, size_t size); - -void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, int process_index, void* target, size_t size); -int mc_snapshot_region_memcmp( - void* addr1, mc_mem_region_t region1, - void* addr2, mc_mem_region_t region2, size_t size); -int mc_snapshot_memcmp( - void* addr1, mc_snapshot_t snapshot1, - void* addr2, mc_snapshot_t snapshot2, int process_index, size_t size); - -static void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot, int process_index); +void mc_restore_page_snapshot_region( + mc_process_t process, + void* start_addr, size_t page_count, size_t* pagenos, + uint64_t* pagemap, size_t* reference_pagenos); + +const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, const void* addr, size_t size); + +const void* MC_snapshot_read(mc_snapshot_t snapshot, e_adress_space_read_flags_t flags, + void* target, const void* addr, size_t size, int process_index); +int MC_snapshot_region_memcmp( + const void* addr1, mc_mem_region_t region1, + const void* addr2, mc_mem_region_t region2, size_t size); +int MC_snapshot_memcmp( + const void* addr1, mc_snapshot_t snapshot1, + const void* addr2, mc_snapshot_t snapshot2, int process_index, size_t size); static inline __attribute__ ((always_inline)) -void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot, int process_index) +const void* MC_snapshot_read_pointer(mc_snapshot_t snapshot, const void* addr, int process_index) { void* res; - return *(void**) mc_snapshot_read(addr, snapshot, process_index, &res, sizeof(void*)); + return *(const void**) MC_snapshot_read(snapshot, MC_ADDRESS_SPACE_READ_FLAGS_LAZY, + &res, addr, sizeof(void*), process_index); } static inline __attribute__ ((always_inline)) - void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) { +const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) +{ if(snapshot==NULL) xbt_die("snapshot is NULL"); - void** addr = &(std_heap->breakval); - return mc_snapshot_read_pointer(addr, snapshot, MC_ANY_PROCESS_INDEX); + // This is &std_heap->breakval in the target process: + void** addr = &MC_process_get_heap(&mc_model_checker->process)->breakval; + // Read (std_heap->breakval) in the target process (*addr i.e. std_heap->breakval): + return MC_snapshot_read_pointer(snapshot, addr, MC_PROCESS_INDEX_ANY); } /** @brief Read memory from a snapshot region @@@ -315,10 -277,9 +317,10 @@@ * @return Pointer where the data is located (target buffer of original location) */ static inline __attribute__((always_inline)) -void* mc_snapshot_read_region(void* addr, mc_mem_region_t region, void* target, size_t size) +const void* MC_region_read(mc_mem_region_t region, void* target, const void* addr, size_t size) { if (region==NULL) + // Should be deprecated: return addr; uintptr_t offset = (char*) addr - (char*) region->start_addr; @@@ -326,39 -287,34 +328,39 @@@ xbt_assert(mc_region_contain(region, addr), "Trying to read out of the region boundary."); - // Linear memory region: - if (region->data) { - return (char*) region->data + offset; - } - - // Fragmented memory region: - else if (region->page_numbers) { - // Last byte of the region: - void* end = (char*) addr + size - 1; - if( mc_same_page(addr, end) ) { - // The memory is contained in a single page: - return mc_translate_address_region((uintptr_t) addr, region); - } else { - // The memory spans several pages: - return mc_snapshot_read_fragmented(addr, region, target, size); + switch (region->storage_type) { + case MC_REGION_STORAGE_TYPE_NONE: + default: + xbt_die("Storage type not supported"); + + case MC_REGION_STORAGE_TYPE_FLAT: + return (char*) region->flat.data + offset; + + case MC_REGION_STORAGE_TYPE_CHUNKED: + { + // Last byte of the region: + void* end = (char*) addr + size - 1; + if (mc_same_page(addr, end) ) { + // The memory is contained in a single page: + return mc_translate_address_region((uintptr_t) addr, region); + } else { + // The memory spans several pages: + return MC_region_read_fragmented(region, target, addr, size); + } } - } - else { - xbt_die("No data available for this region"); + // We currently do not pass the process_index to this function so we assume + // that the privatized region has been resolved in the callers: + case MC_REGION_STORAGE_TYPE_PRIVATIZED: + xbt_die("Storage type not supported"); } } static inline __attribute__ ((always_inline)) -void* mc_snapshot_read_pointer_region(void* addr, mc_mem_region_t region) +void* MC_region_read_pointer(mc_mem_region_t region, const void* addr) { void* res; - return *(void**) mc_snapshot_read_region(addr, region, &res, sizeof(void*)); + return *(void**) MC_region_read(region, &res, addr, sizeof(void*)); } SG_END_DECL() diff --combined src/mc/mc_state.c index 09643b4aef,5830913ad5..09b523906f --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@@ -4,15 -4,12 +4,15 @@@ /* 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 "../simix/smx_private.h" #include "xbt/fifo.h" #include "mc_state.h" #include "mc_request.h" #include "mc_private.h" #include "mc_comm_pattern.h" +#include "mc_smx.h" static void copy_incomplete_communications_pattern(mc_state_t state) { int i; @@@ -74,7 -71,7 +74,7 @@@ mc_state_t MC_state_new( state->in_visited_states = 0; state->incomplete_comm_pattern = NULL; /* Stateful model checking */ - if(_sg_mc_checkpoint > 0 && mc_stats->expanded_states % _sg_mc_checkpoint == 0){ + if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){ state->system_state = MC_take_snapshot(state->num); if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ copy_incomplete_communications_pattern(state); @@@ -102,7 -99,6 +102,7 @@@ void MC_state_delete(mc_state_t state, void MC_state_interleave_process(mc_state_t state, smx_process_t process) { + assert(state); state->proc_status[process->pid].state = MC_INTERLEAVE; state->proc_status[process->pid].interleave_count = 0; } @@@ -146,7 -142,6 +146,7 @@@ void MC_state_set_executed_request(mc_s case SIMCALL_COMM_WAITANY: state->internal_req.call = SIMCALL_COMM_WAIT; state->internal_req.issuer = req->issuer; + // FIXME, read from remote process state->internal_comm = *xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t); @@@ -159,7 -154,6 +159,7 @@@ state->internal_req.issuer = req->issuer; if (value > 0) + // FIXME, read from remote process state->internal_comm = *xbt_dynar_get_as(simcall_comm_testany__get__comms(req), value, smx_synchro_t); @@@ -170,7 -164,6 +170,7 @@@ case SIMCALL_COMM_WAIT: state->internal_req = *req; + // FIXME, read from remote process state->internal_comm = *(simcall_comm_wait__get__comm(req)); simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm); simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm); @@@ -178,7 -171,6 +178,7 @@@ case SIMCALL_COMM_TEST: state->internal_req = *req; + // FIXME, read from remote process state->internal_comm = *simcall_comm_test__get__comm(req); simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm); simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); @@@ -186,16 -178,14 +186,16 @@@ case SIMCALL_MC_RANDOM: state->internal_req = *req; - if (value != simcall_mc_random__get__max(req)) { - xbt_swag_foreach(process, simix_global->process_list) { + int random_max = simcall_mc_random__get__max(req); + if (value != random_max) { + MC_EACH_SIMIX_PROCESS(process, procstate = &state->proc_status[process->pid]; - if (process->pid == req->issuer->pid) { + const smx_process_t issuer = MC_smx_simcall_get_issuer(req); + if (process->pid == issuer->pid) { procstate->state = MC_MORE_INTERLEAVE; break; } - } + ); } break; @@@ -223,7 -213,7 +223,7 @@@ smx_simcall_t MC_state_get_request(mc_s unsigned int start_count; smx_synchro_t act = NULL; - xbt_swag_foreach(process, simix_global->process_list) { + MC_EACH_SIMIX_PROCESS(process, procstate = &state->proc_status[process->pid]; if (procstate->state == MC_INTERLEAVE @@@ -310,7 -300,7 +310,7 @@@ } } } - } + ); return NULL; } diff --combined src/simgrid/sg_config.c index 18b73fbd10,b2bda9fcef..e753e76ec4 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@@ -303,7 -303,7 +303,7 @@@ static void _sg_cfg_cb__coll(const cha } /* New Module missing */ - find_coll_description(table, val); + find_coll_description(table, val, category); } static void _sg_cfg_cb__coll_gather(const char *name, int pos){ _sg_cfg_cb__coll("gather", mpi_coll_gather_description, name, pos); @@@ -695,12 -695,6 +695,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)", @@@ -718,6 -712,12 +718,12 @@@ "Specify the name of dot file corresponding to graph state", xbt_cfgelm_string, 1, 1, _mc_cfg_cb_dot_output, NULL); xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/dot_output", ""); + + /* Enable/disable non progressive cycles detection with model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/termination", + "Enable/Disable non progressive cycle detection", + xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_termination, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/termination", "no"); #endif /* do verbose-exit */ diff --combined src/surf/surf_interface.cpp index 16b6f4eacf,7d0ce714ff..c3adc90047 --- a/src/surf/surf_interface.cpp +++ b/src/surf/surf_interface.cpp @@@ -99,9 -99,7 +99,7 @@@ xbt_dict_t watched_hosts_lib surf_callback(void, void) surfExitCallbacks; s_surf_model_description_t surf_plugin_description[] = { - {"Energy", - "Cpu energy consumption.", - sg_energy_plugin_init}, + {"Energy", "Cpu energy consumption.", sg_energy_plugin_init}, {NULL, NULL, NULL} /* this array must be NULL terminated */ }; @@@ -1101,3 -1099,4 +1099,3 @@@ void Action::updateRemainingLazy(doubl m_lastUpdate = now; m_lastValue = lmm_variable_getvalue(getVariable()); } -