From: Gabriel Corona Date: Mon, 23 Feb 2015 15:08:17 +0000 (+0100) Subject: [mc] Cross-process access to smx_process and simcall X-Git-Tag: v3_12~732^2~115 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/95bcda88a7fcfa168381cba0eedadb1e4937d0b3 [mc] Cross-process access to smx_process and simcall Process and host names are not handled yet. --- diff --git a/include/xbt/dynar.h b/include/xbt/dynar.h index 823dd418a2..31b5adbaf7 100644 --- a/include/xbt/dynar.h +++ b/include/xbt/dynar.h @@ -284,6 +284,11 @@ xbt_dynar_foreach (dyn,cpt,str) { _xbt_dynar_cursor_get(_dynar,_cursor,&_data) ; \ (_cursor)++ ) +#define xbt_dynar_foreach_ptr(_dynar,_cursor,_ptr) \ + for (_xbt_dynar_cursor_first(_dynar,&(_cursor)) ; \ + (_ptr = _cursor < _dynar->used ? xbt_dynar_get_ptr(_dynar,_cursor) : NULL) ; \ + (_cursor)++ ) + /** @} */ SG_END_DECL() diff --git a/src/mc/mc_base.c b/src/mc/mc_base.c index 96c14b2606..20d8f436ad 100644 --- a/src/mc/mc_base.c +++ b/src/mc/mc_base.c @@ -13,6 +13,7 @@ #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"); @@ -37,6 +38,9 @@ int MC_request_is_enabled(smx_simcall_t req) { unsigned int index = 0; smx_synchro_t act = 0; +#ifdef HAVE_MC + s_smx_synchro_t temp_synchro; +#endif switch (req->call) { case SIMCALL_NONE: @@ -45,6 +49,17 @@ int MC_request_is_enabled(smx_simcall_t req) 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. */ @@ -60,9 +75,21 @@ int MC_request_is_enabled(smx_simcall_t req) 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; default: diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 1fdf717986..0a5d94eb57 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -737,11 +737,10 @@ mc_snapshot_t MC_take_snapshot(int num_state) snapshot->address_space.address_space_class = &mc_snapshot_class; snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL); + smx_process_t process; - // FIXME, cross-process support (simix_global->process_list) - xbt_swag_foreach(process, simix_global->process_list) { - xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid); - } + MC_EACH_SIMIX_PROCESS(process, + xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid)); MC_snapshot_handle_ignore(snapshot); diff --git a/src/mc/mc_client.h b/src/mc/mc_client.h index 638a8eafda..f5d01a57bf 100644 --- a/src/mc/mc_client.h +++ b/src/mc/mc_client.h @@ -23,8 +23,9 @@ void MC_client_hello(void); void MC_client_handle_messages(void); void MC_client_send_message(void* message, size_t size); +#ifdef HAVE_MC void MC_ignore(void* addr, size_t size); - +#endif SG_END_DECL() diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index 6576d606c2..d892dde8ee 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -165,12 +165,14 @@ static void print_incomplete_communications_pattern(){ } } +// 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; + // 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); if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) { @@ -216,7 +218,7 @@ void list_comm_pattern_free_voidp(void *p) { list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p); } -void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type) +void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const e_mc_call_type_t call_type) { mc_process_t process = &mc_model_checker->process; mc_comm_pattern_t pattern = NULL; @@ -224,7 +226,13 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t pattern->data_size = -1; pattern->data = NULL; - pattern->index = ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, request->issuer->pid, mc_list_comm_pattern_t))->index_comm + xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t)); + const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, 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; @@ -234,7 +242,8 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t pattern->comm = simcall_comm_isend__get__result(request); 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); + // FIXME, get remote host name + pattern->src_host = simcall_host_get_name(issuer->smx_host); if(pattern->comm->comm.src_buff != NULL){ pattern->data_size = pattern->comm->comm.src_buff_size; pattern->data = xbt_malloc0(pattern->data_size); @@ -250,14 +259,15 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t pattern->comm = simcall_comm_irecv__get__result(request); 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); + // FIXME, remote process access + pattern->dst_host = simcall_host_get_name(issuer->smx_host); } 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) { @@ -358,11 +368,11 @@ void MC_pre_modelcheck_comm_determinism(void) 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); @@ -417,7 +427,7 @@ void MC_modelcheck_comm_determinism(void) } /* 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) @@ -437,11 +447,11 @@ void MC_modelcheck_comm_determinism(void) 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 --git a/src/mc/mc_global.c b/src/mc/mc_global.c index d520ffb0d2..0ea7c5f8a6 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -336,12 +336,12 @@ int MC_deadlock_check() smx_process_t process; if (xbt_swag_size(simix_global->process_list)) { deadlock = TRUE; - xbt_swag_foreach(process, simix_global->process_list) { + MC_EACH_SIMIX_PROCESS(process, if (MC_process_is_enabled(process)) { deadlock = FALSE; break; } - } + ); } return deadlock; } @@ -474,7 +474,9 @@ void MC_replay(xbt_fifo_t stack) 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_process_get_issuer(&mc_model_checker->process, saved_req); + req = &issuer->simcall; /* Debug information */ if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { @@ -488,7 +490,7 @@ void MC_replay(xbt_fifo_t stack) 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) @@ -559,7 +561,8 @@ 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 */ - req = &saved_req->issuer->simcall; + const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req); + req = &issuer->simcall; /* Debug information */ if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { @@ -570,7 +573,7 @@ void MC_replay_liveness(xbt_fifo_t stack) } - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); MC_wait_for_requests(); } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index ec50dad337..07fbd74847 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -201,11 +201,11 @@ void MC_pre_modelcheck_liveness(void) { initial_pair->depth = 1; /* Get enabled processes and insert them in the interleave set of the graph_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_pair->graph_state, process); } - } + ); initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state); initial_pair->search_cycle = 0; @@ -311,7 +311,7 @@ void MC_modelcheck_liveness() mc_stats->visited_pairs++; /* Answer the request */ - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@ -336,11 +336,11 @@ void MC_modelcheck_liveness() next_pair->atomic_propositions = get_atomic_propositions_values(); next_pair->depth = current_pair->depth + 1; /* Get enabled processes and insert them in the interleave set of the next graph_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_pair->graph_state, process); } - } + ); next_pair->requests = MC_state_interleave_size(next_pair->graph_state); diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h index 308cf127ff..9c6b87670f 100644 --- a/src/mc/mc_model_checker.h +++ b/src/mc/mc_model_checker.h @@ -10,10 +10,12 @@ #include #include +#include #include "mc_forward.h" #include "mc_process.h" #include "mc_page_store.h" +#include "mc_protocol.h" SG_BEGIN_DECL() @@ -37,6 +39,21 @@ struct s_mc_model_checker { mc_model_checker_t MC_model_checker_new(pid_t pid, int socket); void MC_model_checker_delete(mc_model_checker_t mc); +#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 65c77a85db..0beaf82fac 100644 --- a/src/mc/mc_process.c +++ b/src/mc/mc_process.c @@ -26,6 +26,8 @@ #include "mc_snapshot.h" #include "mc_ignore.h" +#include "simix/smx_private.h" + XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc, "MC process information"); @@ -80,6 +82,9 @@ 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->checkpoint_ignore = MC_checkpoint_ignore_new(); process->unw_addr_space = unw_create_addr_space(&mc_unw_accessors , __BYTE_ORDER); @@ -106,6 +111,9 @@ void MC_process_clear(mc_process_t process) xbt_dynar_free(&process->checkpoint_ignore); + xbt_dynar_free(&process->smx_process_infos); + xbt_dynar_free(&process->smx_old_process_infos); + size_t i; for (i=0; i!=process->object_infos_size; ++i) { MC_free_object_info(&process->object_infos[i]); @@ -170,6 +178,66 @@ 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]*$" @@ -371,15 +439,37 @@ dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* { const size_t n = process->object_infos_size; size_t i; + + // First lookup the variable in the executable shared object. + // A global variable used directly by the executable code from a library + // is reinstanciated in the executable memory .data/.bss. + // We need to look up the variable in the execvutable first. + if (process->binary_info) { + mc_object_info_t info = process->binary_info; + dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name); + if (var) + return var; + } + for (i=0; i!=n; ++i) { mc_object_info_t info =process->object_infos[i]; dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name); if (var) return var; } + return NULL; } +void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size) +{ + dw_variable_t var = MC_process_find_variable_by_name(process, name); + if (!var->address) + xbt_die("No simple location for this variable"); + MC_process_read(process, MC_PROCESS_NO_FLAG, target, var->address, size, + MC_PROCESS_INDEX_ANY); +} + // ***** Memory access int MC_process_vm_open(pid_t pid, int flags) @@ -512,3 +602,72 @@ 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)) { + SIMIX_simcall_handle(req, value); + return; + } + + MC_process_refresh_simix_processes(&mc_model_checker->process); + + unsigned i; + mc_smx_process_info_t pi = NULL; + + xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) { + smx_process_t p = (smx_process_t) pi->address; + if (req == &pi->copy.simcall) { + smx_simcall_t real_req = &p->simcall; + // TODO, use a remote call + SIMIX_simcall_handle(real_req, value); + return; + } + } + + // Check (remove afterwards): + xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) { + smx_process_t p = (smx_process_t) pi->address; + if (req == &p->simcall) + xbt_die("The real simcall was passed. We expected the local copy."); + } + + 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 1e4384d153..762cb695e3 100644 --- a/src/mc/mc_process.h +++ b/src/mc/mc_process.h @@ -18,11 +18,13 @@ #include "xbt/mmalloc/mmprivate.h" #include "simix/popping_private.h" +#include "simix/smx_private.h" #include "mc_forward.h" #include "mc_mmalloc.h" // std_heap #include "mc_memory_map.h" #include "mc_address_space.h" +#include "mc_protocol.h" SG_BEGIN_DECL() @@ -38,8 +40,16 @@ typedef enum { typedef enum { MC_PROCESS_CACHE_FLAG_HEAP = 1, MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2, + MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4, } e_mc_process_cache_flags_t ; +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 */ struct s_mc_process { @@ -57,13 +67,13 @@ struct s_mc_process { size_t object_infos_size; int memory_file; - // Cache: don't use those fields directly but with the getters - // which ensure that proper synchronisation has been done. + xbt_dynar_t smx_process_infos; + xbt_dynar_t smx_old_process_infos; + /** State of the cache (which variables are up to date) */ e_mc_process_cache_flags_t cache_flags; - /** Address of the heap structure in the target process. - */ + /** Address of the heap structure in the MCed process. */ void* heap_address; /** Copy of the heap structure of the process @@ -125,6 +135,8 @@ 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) { @@ -164,6 +176,8 @@ mc_object_info_t MC_process_find_object_info_rw(mc_process_t process, const void dw_frame_t MC_process_find_function(mc_process_t process, const void* ip); +void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size); + static inline xbt_mheap_t MC_process_get_heap(mc_process_t process) { if (MC_process_is_self(process)) @@ -186,6 +200,21 @@ 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 d9d79e1de8..de2242d0ee 100644 --- a/src/mc/mc_record.c +++ b/src/mc/mc_record.c @@ -108,7 +108,8 @@ 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); - int pid = saved_req->issuer->pid; + const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req); + const int pid = issuer->pid; // Serialization the (pid, value) pair: const char* sep = (item!=start) ? ";" : ""; diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index af7f1ef766..2d6bdeebdd 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -42,6 +42,8 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) 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; @@ -233,20 +235,25 @@ char *MC_request_to_string(smx_simcall_t req, int value) smx_synchro_t act = NULL; size_t size = 0; + // 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); + 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, + MSG_host_get_name(issuer->smx_host), issuer->name, 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, + issuer->name, p, bs); break; case SIMCALL_COMM_IRECV: size = @@ -255,15 +262,15 @@ char *MC_request_to_string(smx_simcall_t req, int value) 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, + MSG_host_get_name(issuer->smx_host), issuer->name, 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, + issuer->name, p, bs); break; case SIMCALL_COMM_WAIT: act = simcall_comm_wait__get__comm(req); @@ -349,13 +356,13 @@ char *MC_request_to_string(smx_simcall_t req, int value) if (args != NULL) { 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, + MSG_host_get_name(issuer->smx_host), issuer->name, type, args); } else { 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, + MSG_host_get_name(issuer->smx_host), issuer->name, type); } @@ -417,48 +424,51 @@ 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); + 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, + MSG_host_get_name(issuer->smx_host)); 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, + MSG_host_get_name(issuer->smx_host)); 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, + MSG_host_get_name(issuer->smx_host)); else - label = bprintf("[(%lu)] WaitTimeout", req->issuer->pid); + label = bprintf("[(%lu)] WaitTimeout", issuer->pid); } else { - if (req->issuer->smx_host) + if (issuer->smx_host) label = - bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", req->issuer->pid, - MSG_host_get_name(req->issuer->smx_host), + bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid, + MSG_host_get_name(issuer->smx_host), act->comm.src_proc ? act->comm.src_proc->pid : 0, act->comm.dst_proc ? act->comm.dst_proc->pid : 0); else label = - bprintf("[(%lu)] Wait [(%lu)->(%lu)]", req->issuer->pid, + bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid, act->comm.src_proc ? act->comm.src_proc->pid : 0, act->comm.dst_proc ? act->comm.dst_proc->pid : 0); } @@ -467,81 +477,81 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) 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, + MSG_host_get_name(issuer->smx_host)); 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, + MSG_host_get_name(issuer->smx_host)); 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, + MSG_host_get_name(issuer->smx_host), 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, + MSG_host_get_name(issuer->smx_host)); 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, + MSG_host_get_name(issuer->smx_host), 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_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, + MSG_host_get_name(issuer->smx_host), 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, + MSG_host_get_name(issuer->smx_host)); 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, + MSG_host_get_name(issuer->smx_host)); else - label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", req->issuer->pid); + label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid); break; default: @@ -550,7 +560,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) 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 --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c index 3d0fc9e41b..2aafad6574 100644 --- a/src/mc/mc_safety.c +++ b/src/mc/mc_safety.c @@ -4,6 +4,8 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ +#include + #include "mc_state.h" #include "mc_request.h" #include "mc_safety.h" @@ -29,7 +31,6 @@ void MC_pre_modelcheck_safety() 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("**************************************************"); @@ -41,13 +42,13 @@ void MC_pre_modelcheck_safety() 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); mmalloc_set_current_heap(heap); @@ -101,7 +102,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(); @@ -114,13 +115,13 @@ void MC_modelcheck_safety(void) 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); @@ -187,6 +188,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); 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)) { @@ -201,8 +203,8 @@ void MC_modelcheck_safety(void) 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); @@ -215,10 +217,11 @@ 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)); 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 --git a/src/mc/mc_state.c b/src/mc/mc_state.c index 84db3e8ec3..49dbb7e448 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -4,6 +4,8 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ +#include + #include "../simix/smx_private.h" #include "xbt/fifo.h" #include "mc_state.h" @@ -99,6 +101,7 @@ void MC_state_delete(mc_state_t state, int free_snapshot){ 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; } @@ -142,6 +145,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, 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); @@ -154,6 +158,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, 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); @@ -164,6 +169,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, 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); @@ -171,6 +177,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, 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); @@ -178,14 +185,16 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, 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_process_get_issuer(&mc_model_checker->process, req); + if (process->pid == issuer->pid) { procstate->state = MC_MORE_INTERLEAVE; break; } - } + ); } break; @@ -213,7 +222,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) 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 @@ -300,7 +309,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) } } } - } + ); return NULL; } diff --git a/src/xbt/dynar.c b/src/xbt/dynar.c index 26c9196a7f..e5919676a2 100644 --- a/src/xbt/dynar.c +++ b/src/xbt/dynar.c @@ -827,6 +827,20 @@ XBT_TEST_UNIT("int", test_dynar_int, "Dynars of integers") xbt_test_log("Pop %d, length=%lu", cpt, xbt_dynar_length(d)); } + int* pi; + xbt_dynar_foreach_ptr(d, cursor, pi) { + *pi = 0; + } + xbt_dynar_foreach(d, cursor, i) { + xbt_test_assert(i == 0, "The value is not the same as the expected one."); + } + xbt_dynar_foreach_ptr(d, cursor, pi) { + *pi = 1; + } + xbt_dynar_foreach(d, cursor, i) { + xbt_test_assert(i == 1, "The value is not the same as the expected one."); + } + /* 5. Free the resources */ xbt_dynar_free(&d); /* This code is used both as example and as regression test, so we try to */ xbt_dynar_free(&d); /* free the struct twice here to check that it's ok, but freeing it only once */