From: Gabriel Corona Date: Fri, 27 Feb 2015 10:58:55 +0000 (+0100) Subject: [mc] Read host name from remote process X-Git-Tag: v3_12~732^2~114 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e47b3e4c9b5ea0bd18d8c088320844200e4ff07e [mc] Read host name from remote process --- diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 76cc745f56..bf6b18cdda 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -649,6 +649,8 @@ set(MC_SRC 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 diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 0a5d94eb57..d36881019b 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -35,6 +35,7 @@ #include "mc_mmu.h" #include "mc_unw.h" #include "mc_protocol.h" +#include "mc_smx.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc, "Logging specific to mc_checkpoint"); diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index d892dde8ee..ed68099c96 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -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"); @@ -172,9 +173,9 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co void *addr_pointed; comm_pattern->src_proc = comm->comm.src_proc->pid; comm_pattern->dst_proc = comm->comm.dst_proc->pid; - // FIXME, get remote host name - 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); + // TODO, resolve host name + comm_pattern->src_host = MC_smx_process_get_host_name(MC_smx_resolve_process(comm->comm.src_proc)); + comm_pattern->dst_host = MC_smx_process_get_host_name(MC_smx_resolve_process(comm->comm.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); @@ -226,7 +227,7 @@ void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const pattern->data_size = -1; pattern->data = NULL; - const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, request); + 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 = @@ -243,7 +244,7 @@ void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const 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; // FIXME, get remote host name - pattern->src_host = simcall_host_get_name(issuer->smx_host); + pattern->src_host = MC_smx_process_get_host_name(issuer); if(pattern->comm->comm.src_buff != NULL){ pattern->data_size = pattern->comm->comm.src_buff_size; pattern->data = xbt_malloc0(pattern->data_size); @@ -260,7 +261,7 @@ void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const 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; // FIXME, remote process access - pattern->dst_host = simcall_host_get_name(issuer->smx_host); + pattern->dst_host = MC_smx_process_get_host_name(issuer); } else { xbt_die("Unexpected call_type %i", (int) call_type); } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 0ea7c5f8a6..56ad792d39 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -35,6 +35,7 @@ #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" @@ -475,7 +476,7 @@ void MC_replay(xbt_fifo_t stack) /* 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 */ - const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req); + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); req = &issuer->simcall; /* Debug information */ @@ -561,7 +562,7 @@ void MC_replay_liveness(xbt_fifo_t stack) 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 */ - const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req); + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); req = &issuer->simcall; /* Debug information */ diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 07fbd74847..4d7c048ec0 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -14,6 +14,7 @@ #include "mc_liveness.h" #include "mc_private.h" #include "mc_record.h" +#include "mc_smx.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); diff --git a/src/mc/mc_model_checker.c b/src/mc/mc_model_checker.c index e3cc96165c..9482e45f04 100644 --- a/src/mc/mc_model_checker.c +++ b/src/mc/mc_model_checker.c @@ -16,6 +16,7 @@ mc_model_checker_t MC_model_checker_new(pid_t pid, int socket) mc->fd_clear_refs = -1; mc->fd_pagemap = -1; MC_process_init(&mc->process, pid, socket); + mc->hosts = xbt_dict_new(); return mc; } @@ -25,4 +26,5 @@ void MC_model_checker_delete(mc_model_checker_t mc) if(mc->record) xbt_dynar_free(&mc->record); MC_process_clear(&mc->process); + xbt_dict_free(&mc->hosts); } diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h index 9c6b87670f..45790f35e5 100644 --- a/src/mc/mc_model_checker.h +++ b/src/mc/mc_model_checker.h @@ -34,26 +34,13 @@ struct s_mc_model_checker { int fd_pagemap; xbt_dynar_t record; s_mc_process_t process; + /** String pool for host names */ + xbt_dict_t /* */ hosts; }; mc_model_checker_t MC_model_checker_new(pid_t pid, int socket); void MC_model_checker_delete(mc_model_checker_t mc); -#define MC_EACH_SIMIX_PROCESS(process, code) \ - if (MC_process_is_self(&mc_model_checker->process)) { \ - xbt_swag_foreach(process, simix_global->process_list) { \ - code; \ - } \ - } else { \ - MC_process_refresh_simix_processes(&mc_model_checker->process); \ - unsigned int _smx_process_index; \ - mc_smx_process_info_t _smx_process_info; \ - xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, _smx_process_index, _smx_process_info) { \ - smx_process_t process = &_smx_process_info->copy; \ - code; \ - } \ - } - SG_END_DECL() #endif diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c index 0beaf82fac..e3f4eb8378 100644 --- a/src/mc/mc_process.c +++ b/src/mc/mc_process.c @@ -25,8 +25,7 @@ #include "mc_unw.h" #include "mc_snapshot.h" #include "mc_ignore.h" - -#include "simix/smx_private.h" +#include "mc_smx.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc, "MC process information"); @@ -82,8 +81,8 @@ void MC_process_init(mc_process_t process, pid_t pid, int sockfd) &process->heap_address, std_heap_var->address, sizeof(struct mdesc*), MC_PROCESS_INDEX_DISABLED); - process->smx_process_infos = mc_smx_process_info_list_new(); - process->smx_old_process_infos = mc_smx_process_info_list_new(); + process->smx_process_infos = MC_smx_process_info_list_new(); + process->smx_old_process_infos = MC_smx_process_info_list_new(); process->checkpoint_ignore = MC_checkpoint_ignore_new(); @@ -178,66 +177,6 @@ void MC_process_refresh_malloc_info(mc_process_t process) MC_PROCESS_INDEX_DISABLED); } -/** Load the remote swag of processes into a dynar - * - * @param process MCed process - * @param target Local dynar (to be filled with copies of `s_smx_process_t`) - * @param remote_swag Address of the process SWAG in the remote list - */ -static void MC_process_refresh_simix_process_list( - mc_process_t process, - xbt_dynar_t target, xbt_swag_t remote_swag) -{ - // swag = REMOTE(*simix_global->process_list) - s_xbt_swag_t swag; - MC_process_read(process, MC_PROCESS_NO_FLAG, &swag, remote_swag, sizeof(swag), - MC_PROCESS_INDEX_ANY); - - smx_process_t p; - xbt_dynar_reset(target); - - int i = 0; - for (p = swag.head; p; ++i) { - - s_mc_smx_process_info_t info; - info.address = p; - MC_process_read(process, MC_PROCESS_NO_FLAG, - &info.copy, p, sizeof(info.copy), MC_PROCESS_INDEX_ANY); - xbt_dynar_push(target, &info); - - // Lookup next process address: - p = xbt_swag_getNext(&info.copy, swag.offset); - } - assert(i == swag.count); -} - -void MC_process_refresh_simix_processes(mc_process_t process) -{ - if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES) - return; - - xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - - // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global` - - // simix_global_p = REMOTE(simix_global); - smx_global_t simix_global_p; - MC_process_read_variable(process, "simix_global", &simix_global_p, sizeof(simix_global_p)); - - // simix_global = REMOTE(*simix_global) - s_smx_global_t simix_global; - MC_process_read(process, MC_PROCESS_NO_FLAG, &simix_global, simix_global_p, sizeof(simix_global), - MC_PROCESS_INDEX_ANY); - - MC_process_refresh_simix_process_list( - process, process->smx_process_infos, simix_global.process_list); - MC_process_refresh_simix_process_list( - process, process->smx_old_process_infos, simix_global.process_to_destroy); - - process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES; - mmalloc_set_current_heap(heap); -} - #define SO_RE "\\.so[\\.0-9]*$" #define VERSION_RE "-[\\.0-9]*$" @@ -563,6 +502,14 @@ const void* MC_process_read(mc_process_t process, e_adress_space_read_flags_t fl } } +const void* MC_process_read_simple(mc_process_t process, + void* local, const void* remote, size_t len) +{ + e_adress_space_read_flags_t flags = MC_PROCESS_NO_FLAG; + int index = MC_PROCESS_INDEX_ANY; + return MC_process_read(process, flags, local, remote, len, index); +} + void MC_process_write(mc_process_t process, const void* local, void* remote, size_t len) { if (MC_process_is_self(process)) { @@ -603,38 +550,6 @@ void MC_process_clear_memory(mc_process_t process, void* remote, size_t len) } } -/** Get the issuer of a simcall (`req->issuer`) - * - * In split-process mode, it does the black magic necessary to get an address - * of a (shallow) copy of the data structure the issuer SIMIX process in the local - * address space. - * - * @param process the MCed process - * @param req the simcall (copied in the local process) - */ -smx_process_t MC_process_get_issuer(mc_process_t process, smx_simcall_t req) -{ - if (MC_process_is_self(&mc_model_checker->process)) - return req->issuer; - - MC_process_refresh_simix_processes(process); - - // This is the address of the smx_process in the MCed process: - void* address = req->issuer; - - unsigned i; - mc_smx_process_info_t p; - - xbt_dynar_foreach_ptr(process->smx_process_infos, i, p) - if (p->address == address) - return &p->copy; - xbt_dynar_foreach_ptr(process->smx_old_process_infos, i, p) - if (p->address == address) - return &p->copy; - - xbt_die("Issuer not found"); -} - void MC_simcall_handle(smx_simcall_t req, int value) { if (MC_process_is_self(&mc_model_checker->process)) { @@ -642,7 +557,7 @@ void MC_simcall_handle(smx_simcall_t req, int value) return; } - MC_process_refresh_simix_processes(&mc_model_checker->process); + MC_process_smx_refresh(&mc_model_checker->process); unsigned i; mc_smx_process_info_t pi = NULL; @@ -666,8 +581,3 @@ void MC_simcall_handle(smx_simcall_t req, int value) xbt_die("Could not find the request"); } - -void mc_smx_process_info_clear(mc_smx_process_info_t p) -{ - // Nothing yet -} diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h index 762cb695e3..c16802d7b2 100644 --- a/src/mc/mc_process.h +++ b/src/mc/mc_process.h @@ -43,11 +43,6 @@ typedef enum { MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4, } e_mc_process_cache_flags_t ; -struct s_mc_smx_process_info { - void* address; - struct s_smx_process copy; -}; - typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t; /** Representation of a process @@ -67,7 +62,16 @@ struct s_mc_process { size_t object_infos_size; int memory_file; + /** Copy of `simix_global->process_list` + * + * See mc_smx.c. + */ xbt_dynar_t smx_process_infos; + + /** Copy of `simix_global->process_to_destroy` + * + * See mc_smx.c. + */ xbt_dynar_t smx_old_process_infos; /** State of the cache (which variables are up to date) */ @@ -135,8 +139,6 @@ void MC_process_refresh_heap(mc_process_t process); * */ void MC_process_refresh_malloc_info(mc_process_t process); -void MC_process_refresh_simix_processes(mc_process_t process); - static inline bool MC_process_is_self(mc_process_t process) { @@ -157,6 +159,9 @@ const void* MC_process_read(mc_process_t process, void* local, const void* remote, size_t len, int process_index); +const void* MC_process_read_simple(mc_process_t process, + void* local, const void* remote, size_t len); + /** Write data to a process memory * * @param process the process @@ -200,21 +205,6 @@ static inline malloc_info* MC_process_get_malloc_info(mc_process_t process) */ dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name); -// ***** Things to move somewhere else: - -smx_process_t MC_process_get_issuer(mc_process_t process, smx_simcall_t req); - -void MC_simcall_handle(smx_simcall_t req, int value); - -void mc_smx_process_info_clear(mc_smx_process_info_t p); - -static inline -xbt_dynar_t mc_smx_process_info_list_new() -{ - return xbt_dynar_new( - sizeof(s_mc_smx_process_info_t), (void_f_pvoid_t) &mc_smx_process_info_clear); -} - SG_END_DECL() #endif diff --git a/src/mc/mc_record.c b/src/mc/mc_record.c index de2242d0ee..d57816899c 100644 --- a/src/mc/mc_record.c +++ b/src/mc/mc_record.c @@ -17,6 +17,7 @@ #include "mc_private.h" #include "mc_model_checker.h" #include "mc_state.h" +#include "mc_smx.h" #endif XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, @@ -108,7 +109,7 @@ char* MC_record_stack_to_string(xbt_fifo_t stack) mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item); int value = 0; smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); - const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req); + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); const int pid = issuer->pid; // Serialization the (pid, value) pair: diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 2d6bdeebdd..942fe9c412 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -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)"); @@ -238,7 +239,7 @@ char *MC_request_to_string(smx_simcall_t req, int value) // FIXME, host_get_name // FIXME, buffer access (issuer->name, issuer->smx_host) - smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req); + smx_process_t issuer = MC_smx_simcall_get_issuer(req); switch (req->call) { case SIMCALL_COMM_ISEND: @@ -248,7 +249,7 @@ char *MC_request_to_string(smx_simcall_t req, int value) if (issuer->smx_host) args = bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid, - MSG_host_get_name(issuer->smx_host), issuer->name, + MC_smx_process_get_host_name(issuer), issuer->name, p, bs); else args = @@ -265,7 +266,7 @@ char *MC_request_to_string(smx_simcall_t req, int value) if (issuer->smx_host) args = bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid, - MSG_host_get_name(issuer->smx_host), issuer->name, + MC_smx_process_get_host_name(issuer), issuer->name, p, bs); else args = @@ -283,12 +284,12 @@ char *MC_request_to_string(smx_simcall_t req, int value) p = pointer_to_string(act); 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) : "", + // TODO, get process + act->comm.src_proc ? MC_smx_process_get_host_name(MC_smx_resolve_process(act->comm.src_proc)) : "", 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) : "", + // TOTO get process + act->comm.dst_proc ? MC_smx_process_get_host_name(MC_smx_resolve_process(act->comm.dst_proc)) : "", act->comm.dst_proc ? act->comm.dst_proc->name : ""); } break; @@ -301,11 +302,12 @@ char *MC_request_to_string(smx_simcall_t req, int value) } else { type = xbt_strdup("Test TRUE"); p = pointer_to_string(act); + // TODO, get process, get process name 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), + MC_smx_process_get_host_name(MC_smx_resolve_process(act->comm.src_proc)), act->comm.dst_proc->pid, act->comm.dst_proc->name, - MSG_host_get_name(act->comm.dst_proc->smx_host)); + MC_smx_process_get_host_name(MC_smx_resolve_process(act->comm.dst_proc))); } break; @@ -355,14 +357,16 @@ char *MC_request_to_string(smx_simcall_t req, int value) } if (args != NULL) { + // FIXME, get process name str = bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid, - MSG_host_get_name(issuer->smx_host), issuer->name, + MC_smx_process_get_host_name(issuer), issuer->name, type, args); } else { + // FIXME, get process name str = bprintf("[(%lu)%s (%s)] %s ", issuer->pid, - MSG_host_get_name(issuer->smx_host), issuer->name, + MC_smx_process_get_host_name(issuer), issuer->name, type); } @@ -424,19 +428,17 @@ int MC_process_is_enabled(smx_process_t process) char *MC_request_get_dot_output(smx_simcall_t req, int value) { - // TODO, remote access to MSG_host_get_name(issuer->smx_host) - char *str = NULL, *label = NULL; smx_synchro_t act = NULL; - const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req); + const smx_process_t issuer = MC_smx_simcall_get_issuer(req); switch (req->call) { case SIMCALL_COMM_ISEND: if (issuer->smx_host) label = bprintf("[(%lu)%s] iSend", issuer->pid, - MSG_host_get_name(issuer->smx_host)); + MC_smx_process_get_host_name(issuer)); else label = bprintf("[(%lu)] iSend", issuer->pid); break; @@ -445,7 +447,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) if (issuer->smx_host) label = bprintf("[(%lu)%s] iRecv", issuer->pid, - MSG_host_get_name(issuer->smx_host)); + MC_smx_process_get_host_name(issuer)); else label = bprintf("[(%lu)] iRecv", issuer->pid); break; @@ -456,14 +458,14 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) if (issuer->smx_host) label = bprintf("[(%lu)%s] WaitTimeout", issuer->pid, - MSG_host_get_name(issuer->smx_host)); + MC_smx_process_get_host_name(issuer)); else label = bprintf("[(%lu)] WaitTimeout", issuer->pid); } else { if (issuer->smx_host) label = bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid, - MSG_host_get_name(issuer->smx_host), + MC_smx_process_get_host_name(issuer), act->comm.src_proc ? act->comm.src_proc->pid : 0, act->comm.dst_proc ? act->comm.dst_proc->pid : 0); else @@ -480,14 +482,14 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) if (issuer->smx_host) label = bprintf("[(%lu)%s] Test FALSE", issuer->pid, - MSG_host_get_name(issuer->smx_host)); + MC_smx_process_get_host_name(issuer)); else label = bprintf("[(%lu)] Test FALSE", issuer->pid); } else { if (issuer->smx_host) label = bprintf("[(%lu)%s] Test TRUE", issuer->pid, - MSG_host_get_name(issuer->smx_host)); + MC_smx_process_get_host_name(issuer)); else label = bprintf("[(%lu)] Test TRUE", issuer->pid); } @@ -497,7 +499,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) if (issuer->smx_host) label = bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid, - MSG_host_get_name(issuer->smx_host), value + 1, + MC_smx_process_get_host_name(issuer), value + 1, xbt_dynar_length(simcall_comm_waitany__get__comms(req))); else label = @@ -510,14 +512,14 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) if (issuer->smx_host) label = bprintf("[(%lu)%s] TestAny FALSE", issuer->pid, - MSG_host_get_name(issuer->smx_host)); + MC_smx_process_get_host_name(issuer)); else label = bprintf("[(%lu)] TestAny FALSE", issuer->pid); } else { if (issuer->smx_host) label = bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid, - MSG_host_get_name(issuer->smx_host), value + 1, + MC_smx_process_get_host_name(issuer), value + 1, xbt_dynar_length(simcall_comm_testany__get__comms(req))); else label = @@ -531,7 +533,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) if (issuer->smx_host) label = bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid, - MSG_host_get_name(issuer->smx_host), value); + MC_smx_process_get_host_name(issuer), value); else label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value); break; @@ -540,7 +542,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) if (issuer->smx_host) label = bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid, - MSG_host_get_name(issuer->smx_host)); + MC_smx_process_get_host_name(issuer)); else label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid); break; @@ -549,7 +551,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) if (issuer->smx_host) label = bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid, - MSG_host_get_name(issuer->smx_host)); + MC_smx_process_get_host_name(issuer)); else label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid); break; diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c index 2aafad6574..544cf510a1 100644 --- a/src/mc/mc_safety.c +++ b/src/mc/mc_safety.c @@ -11,6 +11,7 @@ #include "mc_safety.h" #include "mc_private.h" #include "mc_record.h" +#include "mc_smx.h" #include "xbt/mmalloc/mmprivate.h" @@ -188,7 +189,7 @@ void MC_modelcheck_safety(void) 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_process_get_issuer(&mc_model_checker->process, req); + 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)) { @@ -217,7 +218,7 @@ void MC_modelcheck_safety(void) } else { - const smx_process_t previous_issuer = MC_process_get_issuer(&mc_model_checker->process, MC_state_get_internal_request(prev_state)); + 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, issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, diff --git a/src/mc/mc_smx.c b/src/mc/mc_smx.c new file mode 100644 index 0000000000..1180faa8a3 --- /dev/null +++ b/src/mc/mc_smx.c @@ -0,0 +1,196 @@ +/* Copyright (c) 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 + +#include + +#include "simix/smx_private.h" + +#include "mc_smx.h" +#include "mc_model_checker.h" + +xbt_dynar_t MC_smx_process_info_list_new(void) +{ + return xbt_dynar_new( + sizeof(s_mc_smx_process_info_t), NULL); +} + +static inline +bool is_in_dynar(smx_process_t p, xbt_dynar_t dynar) +{ + return (uintptr_t) p >= (uintptr_t) dynar->data + && (uintptr_t) p < ((uintptr_t) dynar->data + dynar->used * dynar->elmsize); +} + +static inline +mc_smx_process_info_t MC_smx_process_get_info(smx_process_t p) +{ + assert(is_in_dynar(p, mc_model_checker->process.smx_process_infos) + || is_in_dynar(p, mc_model_checker->process.smx_old_process_infos)); + mc_smx_process_info_t process_info = + (mc_smx_process_info_t) + ((char*) p - offsetof(s_mc_smx_process_info_t, copy)); + return process_info; +} + +/** Load the remote swag of processes into a dynar + * + * @param process MCed process + * @param target Local dynar (to be filled with copies of `s_smx_process_t`) + * @param remote_swag Address of the process SWAG in the remote list + */ +static void MC_process_refresh_simix_process_list( + mc_process_t process, + xbt_dynar_t target, xbt_swag_t remote_swag) +{ + // swag = REMOTE(*simix_global->process_list) + s_xbt_swag_t swag; + MC_process_read(process, MC_PROCESS_NO_FLAG, &swag, remote_swag, sizeof(swag), + MC_PROCESS_INDEX_ANY); + + smx_process_t p; + xbt_dynar_reset(target); + + // Load each element of the dynar from the MCed process: + int i = 0; + for (p = swag.head; p; ++i) { + + s_mc_smx_process_info_t info; + info.address = p; + info.hostname = NULL; + MC_process_read(process, MC_PROCESS_NO_FLAG, + &info.copy, p, sizeof(info.copy), MC_PROCESS_INDEX_ANY); + xbt_dynar_push(target, &info); + + // Lookup next process address: + p = xbt_swag_getNext(&info.copy, swag.offset); + } + assert(i == swag.count); +} + +void MC_process_smx_refresh(mc_process_t process) +{ + if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES) + return; + + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + + // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global` + + // simix_global_p = REMOTE(simix_global); + smx_global_t simix_global_p; + MC_process_read_variable(process, "simix_global", &simix_global_p, sizeof(simix_global_p)); + + // simix_global = REMOTE(*simix_global) + s_smx_global_t simix_global; + MC_process_read(process, MC_PROCESS_NO_FLAG, &simix_global, simix_global_p, sizeof(simix_global), + MC_PROCESS_INDEX_ANY); + + MC_process_refresh_simix_process_list( + process, process->smx_process_infos, simix_global.process_list); + MC_process_refresh_simix_process_list( + process, process->smx_old_process_infos, simix_global.process_to_destroy); + + process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES; + mmalloc_set_current_heap(heap); +} + +/** Get the issuer of a simcall (`req->issuer`) + * + * In split-process mode, it does the black magic necessary to get an address + * of a (shallow) copy of the data structure the issuer SIMIX process in the local + * address space. + * + * @param process the MCed process + * @param req the simcall (copied in the local process) + */ +smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req) +{ + if (MC_process_is_self(&mc_model_checker->process)) + return req->issuer; + + MC_process_smx_refresh(&mc_model_checker->process); + + // This is the address of the smx_process in the MCed process: + void* address = req->issuer; + + unsigned i; + mc_smx_process_info_t p; + + // Lookup by address: + xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, p) + if (p->address == address) + return &p->copy; + xbt_dynar_foreach_ptr(mc_model_checker->process.smx_old_process_infos, i, p) + if (p->address == address) + return &p->copy; + + xbt_die("Issuer not found"); +} + +smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address) +{ + if (MC_process_is_self(&mc_model_checker->process)) + return process_remote_address; + + mc_smx_process_info_t process_info = MC_smx_resolve_process_info(process_remote_address); + if (process_info) + return &process_info->copy; + else + return NULL; +} + +mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address) +{ + if (MC_process_is_self(&mc_model_checker->process)) + xbt_die("No process_info for local process is not enabled."); + + unsigned index; + mc_smx_process_info_t process_info; + xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, index, process_info) + if (process_info->address == process_remote_address) + return process_info; + xbt_dynar_foreach_ptr(mc_model_checker->process.smx_old_process_infos, index, process_info) + if (process_info->address == process_remote_address) + return process_info; + xbt_die("Process info not found"); +} + +const char* MC_smx_process_get_host_name(smx_process_t p) +{ + if (MC_process_is_self(&mc_model_checker->process)) + return SIMIX_host_get_name(p->smx_host); + + mc_process_t process = &mc_model_checker->process; + + // Currently, smx_host_t = xbt_dictelm_t. + // TODO, add an static_assert on this if switching to C++ + // The host name is host->key and the host->key_len==strlen(host->key). + s_xbt_dictelm_t host_copy; + mc_smx_process_info_t info = MC_smx_process_get_info(p); + if (!info->hostname) { + + // Read the hostname from the MCed process: + MC_process_read_simple(process, &host_copy, p->smx_host, sizeof(host_copy)); + int len = host_copy.key_len + 1; + char hostname[len]; + MC_process_read_simple(process, hostname, host_copy.key, len); + + // Lookup the host name in the dictionary (or create it): + xbt_dictelm_t elt = xbt_dict_get_elm_or_null(mc_model_checker->hosts, hostname); + if (!elt) { + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + xbt_dict_set(mc_model_checker->hosts, hostname, NULL, NULL); + elt = xbt_dict_get_elm_or_null(mc_model_checker->hosts, hostname); + assert(elt); + mmalloc_set_current_heap(heap); + } + + info->hostname = elt->key; + } + return info->hostname; +} diff --git a/src/mc/mc_smx.h b/src/mc/mc_smx.h new file mode 100644 index 0000000000..363bd89092 --- /dev/null +++ b/src/mc/mc_smx.h @@ -0,0 +1,98 @@ +/* Copyright (c) 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. */ + +#ifndef MC_SMX_H +#define MC_SMX_H + +#include + +#include +#include + +#include "mc_process.h" +#include "mc_protocol.h" + +/** @file + * @brief (Cross-process, MCer/MCed) Access to SMX structures + * + * We copy some C data structure from the MCed process in the MCer process. + * This is implemented by: + * + * - `model_checker->process.smx_process_infos` + * (copy of `simix_global->process_list`); + * + * - `model_checker->process.smx_old_process_infos` + * (copy of `simix_global->process_to_destroy`); + * + * - `model_checker->hostnames`. + * + * The process lists are currently refreshed each time MCed code is executed. + * We don't try to give a persistent MCer address for a given MCed process. + * For this reason, a MCer mc_process_t is currently not reusable after + * MCed code. + */ + +SG_BEGIN_DECL() + +struct s_mc_smx_process_info { + /** MCed address of the process */ + void* address; + /** (Flat) Copy of the process data structure */ + struct s_smx_process copy; + /** Hostname (owned by `mc_modelchecker->hostnames`) */ + char* hostname; +}; + +xbt_dynar_t MC_smx_process_info_list_new(void); + +void MC_process_smx_refresh(mc_process_t process); + +/** Get the issuer of a simcall (`req->issuer`) + * + * In split-process mode, it does the black magic necessary to get an address + * of a (shallow) copy of the data structure the issuer SIMIX process in the local + * address space. + * + * @param process the MCed process + * @param req the simcall (copied in the local process) + */ +smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req); + +const char* MC_smx_process_get_host_name(smx_process_t p); + +#define MC_EACH_SIMIX_PROCESS(process, code) \ + if (MC_process_is_self(&mc_model_checker->process)) { \ + xbt_swag_foreach(process, simix_global->process_list) { \ + code; \ + } \ + } else { \ + MC_process_smx_refresh(&mc_model_checker->process); \ + unsigned int _smx_process_index; \ + mc_smx_process_info_t _smx_process_info; \ + xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, _smx_process_index, _smx_process_info) { \ + smx_process_t process = &_smx_process_info->copy; \ + code; \ + } \ + } + +/** Execute a given simcall */ +void MC_simcall_handle(smx_simcall_t req, int value); + + + +/* ***** Resolve (local/MCer structure from remote/MCed addresses) ***** */ + +/** Get a local copy of the process from the process remote address */ +smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address); + +/** Get the process info structure from the process remote address */ +mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address); + + + +SG_END_DECL() + +#endif diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index 49dbb7e448..09643b4aef 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -12,6 +12,7 @@ #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; @@ -189,7 +190,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, if (value != random_max) { MC_EACH_SIMIX_PROCESS(process, procstate = &state->proc_status[process->pid]; - const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req); + const smx_process_t issuer = MC_smx_simcall_get_issuer(req); if (process->pid == issuer->pid) { procstate->state = MC_MORE_INTERLEAVE; break;