From: Gabriel Corona Date: Fri, 13 Mar 2015 11:13:55 +0000 (+0100) Subject: [mc] mc_comm_pattern.c containing all communication pattern functions X-Git-Tag: v3_12~732^2~106 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e0300cbd373040c590de77e64cc6c6e5fc3c28bb?ds=sidebyside [mc] mc_comm_pattern.c containing all communication pattern functions --- diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 6a07df0a3e..ff3495096c 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -613,6 +613,7 @@ set(MC_SRC src/mc/mc_page_store.cpp src/mc/mc_page_snapshot.cpp src/mc/mc_comm_pattern.h + src/mc/mc_comm_pattern.c src/mc/mc_comm_determinism.c src/mc/mc_compare.cpp src/mc/mc_diff.c diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index 1017b33579..8b59b3ada3 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -186,11 +186,12 @@ void list_comm_pattern_free_voidp(void *p) { 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); + + mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->data_size = -1; pattern->data = NULL; + // Fill initial_pattern->index_comm: 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); diff --git a/src/mc/mc_comm_pattern.c b/src/mc/mc_comm_pattern.c new file mode 100644 index 0000000000..1367432595 --- /dev/null +++ b/src/mc/mc_comm_pattern.c @@ -0,0 +1,95 @@ +/* Copyright (c) 2007-2014. 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 + +#include "mc_comm_pattern.h" + +mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm) +{ + mc_comm_pattern_t res = xbt_new0(s_mc_comm_pattern_t, 1); + res->index = comm->index; + res->type = comm->type; + res->comm = comm->comm; + res->rdv = strdup(comm->rdv); + res->data_size = -1; + res->data = NULL; + if (comm->type == SIMIX_COMM_SEND) { + res->src_proc = comm->src_proc; + res->src_host = comm->src_host; + if (comm->data != NULL) { + res->data_size = comm->data_size; + res->data = xbt_malloc0(comm->data_size); + memcpy(res->data, comm->data, comm->data_size); + } + } else { + res->dst_proc = comm->dst_proc; + res->dst_host = comm->dst_host; + } + return res; +} + +xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t patterns) +{ + xbt_dynar_t res = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); + + mc_comm_pattern_t comm; + unsigned int cursor; + xbt_dynar_foreach(patterns, cursor, comm) { + mc_comm_pattern_t copy_comm = MC_comm_pattern_dup(comm); + xbt_dynar_push(res, ©_comm); + } + + return res; +} + +void MC_restore_communications_pattern(mc_state_t state) +{ + mc_list_comm_pattern_t list_process_comm; + unsigned int cursor; + + xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){ + list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int); + } + + for (int i = 0; i < MC_smx_get_maxpid(); i++) { + xbt_dynar_t initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t); + xbt_dynar_reset(initial_incomplete_process_comms); + xbt_dynar_t incomplete_process_comms = xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t); + + mc_comm_pattern_t comm; + xbt_dynar_foreach(incomplete_process_comms, cursor, comm) { + mc_comm_pattern_t copy_comm = MC_comm_pattern_dup(comm); + xbt_dynar_push(initial_incomplete_process_comms, ©_comm); + } + + } +} + +void MC_state_copy_incomplete_communications_pattern(mc_state_t state) +{ + state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp); + + int i; + for (i=0; i < MC_smx_get_maxpid(); i++) { + xbt_dynar_t comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t); + xbt_dynar_t copy = MC_comm_patterns_dup(comms); + xbt_dynar_insert_at(state->incomplete_comm_pattern, i, ©); + } +} + +void MC_state_copy_index_communications_pattern(mc_state_t state) +{ + state->index_comm = xbt_dynar_new(sizeof(unsigned int), NULL); + mc_list_comm_pattern_t list_process_comm; + unsigned int cursor; + xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){ + xbt_dynar_push_as(state->index_comm, unsigned int, list_process_comm->index_comm); + } +} diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h index 2bb40d2540..3201a1a8a6 100644 --- a/src/mc/mc_comm_pattern.h +++ b/src/mc/mc_comm_pattern.h @@ -13,6 +13,8 @@ #include "../smpi/private.h" #include +#include "mc_state.h" + #ifndef MC_COMM_PATTERN_H #define MC_COMM_PATTERN_H @@ -84,6 +86,14 @@ void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int is void MC_pre_modelcheck_comm_determinism(void); void MC_modelcheck_comm_determinism(void); +void MC_restore_communications_pattern(mc_state_t state); + +mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm); +xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state); + +void MC_state_copy_incomplete_communications_pattern(mc_state_t state); +void MC_state_copy_index_communications_pattern(mc_state_t state); + SG_END_DECL() #endif diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 9d7bd56181..c867495992 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -389,44 +389,6 @@ void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int valu } -static void MC_restore_communications_pattern(mc_state_t state) { - mc_list_comm_pattern_t list_process_comm; - unsigned int cursor, cursor2; - xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){ - list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int); - } - mc_comm_pattern_t comm; - cursor = 0; - xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms; - for(int i=0; i < MC_smx_get_maxpid(); i++){ - initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t); - xbt_dynar_reset(initial_incomplete_process_comms); - incomplete_process_comms = xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t); - xbt_dynar_foreach(incomplete_process_comms, cursor2, comm) { - mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1); - copy_comm->index = comm->index; - copy_comm->type = comm->type; - copy_comm->comm = comm->comm; - copy_comm->rdv = strdup(comm->rdv); - copy_comm->data_size = -1; - copy_comm->data = NULL; - if(comm->type == SIMIX_COMM_SEND){ - copy_comm->src_proc = comm->src_proc; - copy_comm->src_host = comm->src_host; - if(comm->data != NULL){ - copy_comm->data_size = comm->data_size; - copy_comm->data = xbt_malloc0(comm->data_size); - memcpy(copy_comm->data, comm->data, comm->data_size); - } - }else{ - copy_comm->dst_proc = comm->dst_proc; - copy_comm->dst_host = comm->dst_host; - } - xbt_dynar_push(initial_incomplete_process_comms, ©_comm); - } - } -} - /** * \brief Re-executes from the state at position start all the transitions indicated by * a given model-checker stack. diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index 02dc8ad39e..2331919167 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -14,51 +14,6 @@ #include "mc_comm_pattern.h" #include "mc_smx.h" -static void copy_incomplete_communications_pattern(mc_state_t state) { - int i; - xbt_dynar_t incomplete_process_comms; - mc_comm_pattern_t comm; - unsigned int cursor; - state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp); - for (i=0; i < MC_smx_get_maxpid(); i++) { - incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t); - xbt_dynar_t incomplete_process_comms_copy = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); - xbt_dynar_foreach(incomplete_process_comms, cursor, comm) { - mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1); - copy_comm->index = comm->index; - copy_comm->type = comm->type; - copy_comm->comm = comm->comm; - copy_comm->rdv = strdup(comm->rdv); - copy_comm->data_size = -1; - copy_comm->data = NULL; - if(comm->type == SIMIX_COMM_SEND){ - copy_comm->src_proc = comm->src_proc; - copy_comm->src_host = comm->src_host; - if (comm->data != NULL) { - copy_comm->data_size = comm->data_size; - copy_comm->data = xbt_malloc0(comm->data_size); - memcpy(copy_comm->data, comm->data, comm->data_size); - } - }else{ - copy_comm->dst_proc = comm->dst_proc; - copy_comm->dst_host = comm->dst_host; - } - xbt_dynar_push(incomplete_process_comms_copy, ©_comm); - } - xbt_dynar_insert_at(state->incomplete_comm_pattern, i, &incomplete_process_comms_copy); - } -} - -static void copy_index_communications_pattern(mc_state_t state) { - - state->index_comm = xbt_dynar_new(sizeof(unsigned int), NULL); - mc_list_comm_pattern_t list_process_comm; - unsigned int cursor; - xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){ - xbt_dynar_push_as(state->index_comm, unsigned int, list_process_comm->index_comm); - } -} - /** * \brief Creates a state data structure used by the exploration algorithm */ @@ -75,8 +30,8 @@ mc_state_t MC_state_new() 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); - copy_index_communications_pattern(state); + MC_state_copy_incomplete_communications_pattern(state); + MC_state_copy_index_communications_pattern(state); } } return state; @@ -277,6 +232,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) case SIMCALL_COMM_WAIT: act = simcall_comm_wait__get__comm(&process->simcall); + if (act->comm.src_proc && act->comm.dst_proc) { *value = 0; } else { diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 863a21a09f..a60464b58d 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -47,7 +47,8 @@ typedef struct mc_state { mc_snapshot_t system_state; /* Snapshot of system state */ int num; int in_visited_states; - xbt_dynar_t incomplete_comm_pattern; // comm determinism verification + // comm determinism verification (xbt_dynar_t): + xbt_dynar_t incomplete_comm_pattern; xbt_dynar_t index_comm; // comm determinism verification } s_mc_state_t, *mc_state_t;