From 85bde9428d7b222a626c2dcc547b2a827d384ee4 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 13 May 2014 18:18:36 +0200 Subject: [PATCH] model-checker : handle waitany simcall --- src/mc/mc_dpor.c | 45 ++++++++++++++++++++++++++++++++++++++------- src/mc/mc_global.c | 16 ++++++++++++++-- 2 files changed, 52 insertions(+), 9 deletions(-) diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 73d6907d45..e98e8dd150 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -6,6 +6,8 @@ #include "mc_private.h" +#include "xbt/mmalloc/mmprivate.h" + XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, "Logging specific to MC DPOR exploration"); @@ -62,6 +64,10 @@ static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2 } static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){ + + if(!xbt_dynar_is_empty(incomplete_communications_pattern)) + xbt_die("Oh oh ..."); + unsigned int cursor = 0, send_index = 0, recv_index = 0; mc_comm_pattern_t comm1, comm2; int comm_comparison = 0; @@ -102,6 +108,7 @@ void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){ unsigned int cursor = 0; int index; int completed = 0; + void *addr_pointed; xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){ current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t); if(current_pattern->comm == comm){ @@ -112,7 +119,11 @@ void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){ if(current_pattern->data_size == -1){ current_pattern->data_size = *(comm->comm.dst_buff_size); current_pattern->data = xbt_malloc0(current_pattern->data_size); - memcpy(current_pattern->data, current_pattern->comm->comm.dst_buff, current_pattern->data_size); + addr_pointed = *(void **)comm->comm.src_buff; + if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval) + memcpy(current_pattern->data, addr_pointed, current_pattern->data_size); + else + memcpy(current_pattern->data, comm->comm.src_buff, current_pattern->data_size); } xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL); completed++; @@ -128,14 +139,19 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){ pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->num = ++nb_comm_pattern; pattern->data_size = -1; + void * addr_pointed; if(call == 1){ // ISEND pattern->comm = simcall_comm_isend__get__result(request); pattern->type = SIMIX_COMM_SEND; pattern->src_proc = pattern->comm->comm.src_proc->pid; pattern->src_host = simcall_host_get_name(request->issuer->smx_host); 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->data = xbt_malloc0(pattern->data_size); + addr_pointed = *(void **)pattern->comm->comm.src_buff; + if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval) + memcpy(pattern->data, addr_pointed, pattern->data_size); + else + 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; @@ -486,6 +502,7 @@ void MC_dpor(void) int enabled = 0; int interleave_size = 0; int comm_pattern = 0; + smx_action_t current_comm; while (xbt_fifo_size(mc_stack_safety) > 0) { @@ -531,6 +548,7 @@ void MC_dpor(void) MC_UNSET_RAW_MEM; } + /* TODO : handle test and testany simcalls */ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND) comm_pattern = 1; @@ -538,6 +556,8 @@ void MC_dpor(void) comm_pattern = 2; else if(req->call == SIMCALL_COMM_WAIT) comm_pattern = 3; + else if(req->call == SIMCALL_COMM_WAITANY) + comm_pattern = 4; } /* Answer the request */ @@ -551,10 +571,21 @@ void MC_dpor(void) else get_comm_pattern(communications_pattern, req, comm_pattern); }else if(comm_pattern == 3){ - if(!initial_state_safety->initial_communications_pattern_done) - complete_comm_pattern(initial_communications_pattern, simcall_comm_wait__get__comm(req)); - else - complete_comm_pattern(communications_pattern, simcall_comm_wait__get__comm(req)); + current_comm = simcall_comm_wait__get__comm(req); + if(current_comm->comm.refcount == 1){ /* First wait only must be considered */ + if(!initial_state_safety->initial_communications_pattern_done) + complete_comm_pattern(initial_communications_pattern, current_comm); + else + complete_comm_pattern(communications_pattern, current_comm); + } + }else if(comm_pattern == 4){ + current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t); + if(current_comm->comm.refcount == 1){ /* First wait only must be considered */ + if(!initial_state_safety->initial_communications_pattern_done) + complete_comm_pattern(initial_communications_pattern, current_comm); + else + complete_comm_pattern(communications_pattern, current_comm); + } } MC_UNSET_RAW_MEM; comm_pattern = 0; diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 77a5a5d818..1365469a50 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -1095,6 +1095,7 @@ void MC_replay(xbt_fifo_t stack, int start) mc_state_t state; smx_process_t process = NULL; int comm_pattern = 0; + smx_action_t current_comm; XBT_DEBUG("**** Begin Replay ****"); @@ -1164,6 +1165,7 @@ void MC_replay(xbt_fifo_t stack, int start) xbt_free(req_str); } + /* TODO : handle test and testany simcalls */ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND) comm_pattern = 1; @@ -1171,6 +1173,8 @@ void MC_replay(xbt_fifo_t stack, int start) comm_pattern = 2; else if(req->call == SIMCALL_COMM_WAIT) comm_pattern = 3; + else if(req->call == SIMCALL_COMM_WAITANY) + comm_pattern = 4; } SIMIX_simcall_pre(req, value); @@ -1179,8 +1183,16 @@ void MC_replay(xbt_fifo_t stack, int start) MC_SET_RAW_MEM; if(comm_pattern == 1 || comm_pattern == 2){ get_comm_pattern(communications_pattern, req, comm_pattern); - }else if (comm_pattern == 3){ - complete_comm_pattern(communications_pattern, simcall_comm_wait__get__comm(req)); + }else if (comm_pattern == 3/* || comm_pattern == 4*/){ + current_comm = simcall_comm_wait__get__comm(req); + if(current_comm->comm.refcount == 1){ /* First wait only must be considered */ + complete_comm_pattern(communications_pattern, current_comm); + } + }else if (comm_pattern == 4/* || comm_pattern == 4*/){ + current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t); + if(current_comm->comm.refcount == 1){ /* First wait only must be considered */ + complete_comm_pattern(communications_pattern, current_comm); + } } MC_UNSET_RAW_MEM; comm_pattern = 0; -- 2.20.1