From 7f77334a27782aab84799c21a0dc42143241ab0f Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 16 Jan 2014 15:24:03 +0100 Subject: [PATCH] model-checker : first steps for the study of MPI communications patterns --- src/mc/mc_dpor.c | 190 +++++++++++++++++++++++++++++++++++++++++++- src/mc/mc_global.c | 23 ++++++ src/mc/mc_private.h | 22 +++++ 3 files changed, 234 insertions(+), 1 deletion(-) diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index ebda309ad6..9d11c2803a 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -13,9 +13,154 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, xbt_dynar_t visited_states; xbt_dict_t first_enabled_state; +xbt_dynar_t initial_communications_pattern; +xbt_dynar_t communications_pattern; +int nb_comm_pattern; /********** Static functions ***********/ +static void comm_pattern_free(mc_comm_pattern_t p){ + xbt_free(p->rdv); + xbt_free(p->data); + xbt_free(p); + p = NULL; +} + +static void comm_pattern_free_voidp( void *p){ + comm_pattern_free((mc_comm_pattern_t) * (void **)p); +} + +static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern, unsigned int *idx, e_smx_comm_type_t type, unsigned long proc){ + mc_comm_pattern_t current_comm; + while(*idx < xbt_dynar_length(pattern)){ + current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t); + if(current_comm->type == type && type == SIMIX_COMM_SEND){ + if(current_comm->src_proc == proc) + return current_comm; + }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){ + if(current_comm->dst_proc == proc) + return current_comm; + } + (*idx)++; + } + return NULL; +} + +static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){ + if(strcmp(comm1->rdv, comm2->rdv) != 0) + return 1; + if(comm1->src_proc != comm2->src_proc) + return 1; + if(comm1->dst_proc != comm2->dst_proc) + return 1; + if(comm1->data_size != comm2->data_size) + return 1; + if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0) + return 1; + return 0; +} + +static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){ + unsigned int cursor = 0, send_index = 0, recv_index = 0; + mc_comm_pattern_t comm1, comm2; + int comm_comparison = 0; + int current_process = 0; + while(current_process < simix_process_maxpid){ + while(cursor < xbt_dynar_length(initial_pattern)){ + comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(initial_pattern, cursor, mc_comm_pattern_t); + if(comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process){ + comm2 = get_comm_pattern_from_idx(pattern, &send_index, comm1->type, current_process); + comm_comparison = compare_comm_pattern(comm1, comm2); + if(comm_comparison == 1){ + initial_state_safety->send_deterministic = 0; + initial_state_safety->comm_deterministic = 0; + return; + } + send_index++; + }else if(comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process){ + comm2 = get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, current_process); + comm_comparison = compare_comm_pattern(comm1, comm2); + if(comm_comparison == 1){ + initial_state_safety->comm_deterministic = 0; + } + recv_index++; + } + cursor++; + } + cursor = 0; + send_index = 0; + recv_index = 0; + current_process++; + } + XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic); +} + +static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){ + mc_comm_pattern_t current_pattern; + unsigned int cursor = 0; + xbt_dynar_foreach(list, cursor, current_pattern){ + if(current_pattern->comm == pattern->comm){ + if(!current_pattern->completed){ + current_pattern->src_proc = pattern->comm->comm.src_proc->pid; + current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid; + current_pattern->data_size = pattern->comm->comm.src_buff_size; + current_pattern->data = xbt_malloc0(current_pattern->data_size); + current_pattern->matched_comm = pattern->num; + memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size); + current_pattern->completed = 1; + return current_pattern->num; + } + } + } + return -1; +} + +void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){ + mc_comm_pattern_t pattern = NULL; + pattern = xbt_new0(s_mc_comm_pattern_t, 1); + pattern->num = ++nb_comm_pattern; + pattern->completed = 0; + if(call == 1){ // ISEND + pattern->comm = simcall_comm_isend__get__result(request); + pattern->type = SIMIX_COMM_SEND; + if(pattern->comm->comm.dst_proc != NULL){ + + pattern->matched_comm = complete_comm_pattern(list, pattern); + pattern->dst_proc = pattern->comm->comm.dst_proc->pid; + pattern->completed = 1; + } + pattern->src_proc = pattern->comm->comm.src_proc->pid; + pattern->data_size = pattern->comm->comm.src_buff_size; + pattern->data=xbt_malloc0(pattern->data_size); + memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); + }else{ // IRECV + pattern->comm = simcall_comm_irecv__get__result(request); + pattern->type = SIMIX_COMM_RECEIVE; + if(pattern->comm->comm.src_proc != NULL){ + pattern->matched_comm = complete_comm_pattern(list, pattern); + pattern->src_proc = pattern->comm->comm.src_proc->pid; + pattern->completed = 1; + pattern->data_size = pattern->comm->comm.src_buff_size; + pattern->data=xbt_malloc0(pattern->data_size); + memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); + } + pattern->dst_proc = pattern->comm->comm.dst_proc->pid; + } + if(pattern->comm->comm.rdv != NULL) + pattern->rdv = strdup(pattern->comm->comm.rdv->name); + else + pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name); + xbt_dynar_push(list, &pattern); +} + +static void print_communications_pattern(xbt_dynar_t comms_pattern){ + unsigned int cursor = 0; + mc_comm_pattern_t current_comm; + xbt_dynar_foreach(comms_pattern, cursor, current_comm){ + fprintf(stderr, "%s (%d - comm %p, src : %lu, dst %lu, rdv name %s, data %p, matched with %d)\n", current_comm->type == SIMIX_COMM_SEND ? "iSend" : "iRecv", current_comm->num, current_comm->comm, current_comm->src_proc, current_comm->dst_proc, current_comm->rdv, current_comm->data, current_comm->matched_comm); + } +} + static void visited_state_free(mc_visited_state_t state){ if(state){ MC_free_snapshot(state->system_state); @@ -210,12 +355,17 @@ void MC_dpor_init() /* Create the initial state and push it into the exploration stack */ MC_SET_RAW_MEM; - initial_state = MC_state_new(); if(_sg_mc_visited > 0) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f); + initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); + communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); + nb_comm_pattern = 0; + + initial_state = MC_state_new(); + MC_UNSET_RAW_MEM; XBT_DEBUG("**************************************************"); @@ -280,6 +430,8 @@ void MC_dpor(void) int pos; int visited_state = -1; int enabled = 0; + int comm_pattern = 0; + int interleave_size = 0; while (xbt_fifo_size(mc_stack_safety) > 0) { @@ -292,6 +444,8 @@ void MC_dpor(void) xbt_fifo_size(mc_stack_safety), state, state->num, MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state)); + interleave_size = MC_state_interleave_size(state); + /* Update statistics */ mc_stats->visited_states++; @@ -321,9 +475,25 @@ void MC_dpor(void) xbt_free(key); MC_UNSET_RAW_MEM; + if(req->call == SIMCALL_COMM_ISEND) + comm_pattern = 1; + else if(req->call == SIMCALL_COMM_IRECV) + comm_pattern = 2; + /* Answer the request */ SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ + MC_SET_RAW_MEM; + if(comm_pattern != 0){ + if(!initial_state_safety->initial_communications_pattern_done) + get_comm_pattern(initial_communications_pattern, req, comm_pattern); + else + get_comm_pattern(communications_pattern, req, comm_pattern); + } + MC_UNSET_RAW_MEM; + + comm_pattern = 0; + /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@ -415,6 +585,18 @@ void MC_dpor(void) } + MC_SET_RAW_MEM; + if(!initial_state_safety->initial_communications_pattern_done){ + print_communications_pattern(initial_communications_pattern); + }else{ + if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */ + print_communications_pattern(communications_pattern); + deterministic_pattern(initial_communications_pattern, communications_pattern); + } + } + initial_state_safety->initial_communications_pattern_done = 1; + MC_UNSET_RAW_MEM; + /* Trash the current state, no longer needed */ MC_SET_RAW_MEM; xbt_fifo_shift(mc_stack_safety); @@ -506,6 +688,12 @@ void MC_dpor(void) XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety)); break; } else { + req = MC_state_get_internal_request(state); + if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){ + fprintf(stderr, "Remove state with isend or irecv\n"); + if(!xbt_dynar_is_empty(communications_pattern)) + xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL); + } XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); MC_state_delete(state); } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 4ae023d8dd..a4d9bc358f 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -1876,6 +1876,9 @@ void MC_modelcheck_safety(void) /* Save the initial state */ initial_state_safety = xbt_new0(s_mc_global_t, 1); initial_state_safety->snapshot = MC_take_snapshot(0); + initial_state_safety->initial_communications_pattern_done = 0; + initial_state_safety->comm_deterministic = 1; + initial_state_safety->send_deterministic = 1; MC_UNSET_RAW_MEM; MC_dpor(); @@ -1998,6 +2001,7 @@ void MC_replay(xbt_fifo_t stack, int start) xbt_fifo_item_t item, start_item; mc_state_t state; smx_process_t process = NULL; + int comm_pattern = 0; XBT_DEBUG("**** Begin Replay ****"); @@ -2027,6 +2031,7 @@ void MC_replay(xbt_fifo_t stack, int start) xbt_free(key); } } + xbt_dynar_reset(communications_pattern); MC_UNSET_RAW_MEM; @@ -2056,8 +2061,22 @@ void MC_replay(xbt_fifo_t stack, int start) xbt_free(req_str); } } + + if(req->call == SIMCALL_COMM_ISEND) + comm_pattern = 1; + else if(req->call == SIMCALL_COMM_IRECV) + comm_pattern = 2; SIMIX_simcall_pre(req, value); + + MC_SET_RAW_MEM; + if(comm_pattern != 0){ + get_comm_pattern(communications_pattern, req, comm_pattern); + } + MC_UNSET_RAW_MEM; + + comm_pattern = 0; + MC_wait_for_requests(); count++; @@ -2338,6 +2357,10 @@ void MC_print_statistics(mc_stats_t stats) fprintf(dot_output, "}\n"); fclose(dot_output); } + if(initial_state_safety != NULL){ + XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes"); + XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); + } MC_UNSET_RAW_MEM; } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 9e1db34965..e43b409652 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -58,6 +58,9 @@ typedef struct s_mc_global_t{ int raw_mem_set; int prev_pair; char *prev_req; + int initial_communications_pattern_done; + int comm_deterministic; + int send_deterministic; }s_mc_global_t, *mc_global_t; typedef struct s_mc_checkpoint_ignore_region{ @@ -433,5 +436,24 @@ typedef struct s_local_variable{ int region; }s_local_variable_t, *local_variable_t; +/********************************* Communications pattern ***************************/ + +typedef struct s_mc_comm_pattern{ + int num; + smx_action_t comm; + e_smx_comm_type_t type; + int completed; + unsigned long src_proc; + unsigned long dst_proc; + char *rdv; + size_t data_size; + void *data; + int matched_comm; +}s_mc_comm_pattern_t, *mc_comm_pattern_t; + +extern xbt_dynar_t communications_pattern; + +void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call); + #endif -- 2.20.1