From 5c5074ba2e4ad898b83384cd41acfe541b5644d0 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 13 Feb 2015 15:00:33 +0100 Subject: [PATCH] model-checker : include tag in comm determinism verification --- src/mc/mc_comm_determinism.c | 58 ++++++++---------------------------- src/mc/mc_comm_pattern.h | 4 +++ 2 files changed, 16 insertions(+), 46 deletions(-) diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index b68e563946..1b11b1830b 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -45,11 +45,13 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t com return SRC_PROC_DIFF; if (comm1->dst_proc != comm2->dst_proc) return DST_PROC_DIFF; - if (comm1->data_size != comm2->data_size) + 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; @@ -72,6 +74,9 @@ static void print_determinism_result(e_mc_comm_pattern_difference_t diff, int pr case RDV_DIFF: XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); break; + case TAG_DIFF: + XBT_INFO("Different communication tag 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; @@ -101,6 +106,9 @@ static void print_determinism_result(e_mc_comm_pattern_difference_t diff, int pr case RDV_DIFF: XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); break; + case TAG_DIFF: + XBT_INFO("Different communication tag 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; @@ -121,50 +129,6 @@ static void print_determinism_result(e_mc_comm_pattern_difference_t diff, int pr } } -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; - } -} - static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm) { void *addr_pointed; @@ -233,6 +197,7 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t 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->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); @@ -245,6 +210,7 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t } else if (call_type == MC_CALL_TYPE_RECV) { pattern->type = SIMIX_COMM_RECEIVE; pattern->comm = simcall_comm_irecv__get__result(request); + 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); diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h index 667f24e529..e3cd1af92f 100644 --- a/src/mc/mc_comm_pattern.h +++ b/src/mc/mc_comm_pattern.h @@ -10,6 +10,8 @@ #include #include "../simix/smx_private.h" +#include "../smpi/private.h" +#include #ifndef MC_COMM_PATTERN_H #define MC_COMM_PATTERN_H @@ -27,6 +29,7 @@ typedef struct s_mc_comm_pattern{ char *rdv; ssize_t data_size; void *data; + int tag; int index; } s_mc_comm_pattern_t, *mc_comm_pattern_t; @@ -50,6 +53,7 @@ typedef enum { NONE_DIFF, TYPE_DIFF, RDV_DIFF, + TAG_DIFF, SRC_PROC_DIFF, DST_PROC_DIFF, DATA_SIZE_DIFF, -- 2.20.1