X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/8fc11b8e2c3f486babc8be5494ddd53ffcc659f4..48e9fb0982ced660ff66fd7d83281dc3fdc57432:/src/mc/mc_dpor.c diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index a3e2949111..b7af5b4f0b 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2013. The SimGrid Team. +/* Copyright (c) 2008-2014. The SimGrid Team. * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it @@ -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"); @@ -14,6 +16,7 @@ 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 incomplete_communications_pattern; xbt_dynar_t communications_pattern; int nb_comm_pattern; @@ -61,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("Damn ! Some communications are incomplete that means one or several simcalls are not handle ... "); + unsigned int cursor = 0, send_index = 0, recv_index = 0; mc_comm_pattern_t comm1, comm2; int comm_comparison = 0; @@ -82,6 +89,8 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte comm_comparison = compare_comm_pattern(comm1, comm2); if(comm_comparison == 1){ initial_state_safety->comm_deterministic = 0; + if(!_sg_mc_send_determinism) + return; } recv_index++; } @@ -92,72 +101,83 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte 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){ +void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){ 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; + 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){ + current_pattern->src_proc = comm->comm.src_proc->pid; + current_pattern->dst_proc = comm->comm.dst_proc->pid; + current_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host); + current_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host); + if(current_pattern->data_size == -1){ + current_pattern->data_size = *(comm->comm.dst_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; + 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++; + if(completed == 2) + return; + cursor--; } } - 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; + pattern->data_size = -1; + void * addr_pointed; 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->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; - 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; + pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); } + 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); + + xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1); + } 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); + if(current_comm->type == SIMIX_COMM_SEND) + XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_proc, current_comm->dst_host, "iSend"); + else + XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_proc, current_comm->src_host, "iRecv"); } } @@ -172,6 +192,10 @@ static void visited_state_free_voidp(void *s){ visited_state_free((mc_visited_state_t) * (void **) s); } +/** \brief Save the current state + * + * \return Snapshot of the current state. + */ static mc_visited_state_t visited_state_new(){ mc_visited_state_t new_state = NULL; @@ -186,11 +210,29 @@ static mc_visited_state_t visited_state_new(){ } +/** \brief Find a suitable subrange of candidate duplicates for a given state + * + * \param all_ pairs dynamic array of states with candidate duplicates of the current state; + * \param pair current state; + * \param min (output) index of the beginning of the the subrange + * \param max (output) index of the enf of the subrange + * + * Given a suitably ordered array of state, this function extracts a subrange + * (with index *min <= i <= *max) with candidate duplicates of the given state. + * This function uses only fast discriminating criterions and does not use the + * full state comparison algorithms. + * + * The states in all_pairs MUST be ordered using a (given) weak order + * (based on nb_processes and heap_bytes_used). + * The subrange is the subrange of "equivalence" of the given state. + */ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){ + XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu", + state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used); - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; int cursor = 0, previous_cursor, next_cursor; mc_visited_state_t state_test; @@ -228,26 +270,30 @@ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, next_cursor++; } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; } } } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return cursor; } +/** \brief Take a snapshot the current state and process it. + * + * \return number of the duplicate state or -1 (not visited) + */ static int is_visited_state(){ if(_sg_mc_visited == 0) return -1; - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_visited_state_t new_state = visited_state_new(); @@ -256,7 +302,7 @@ static int is_visited_state(){ xbt_dynar_push(visited_states, &new_state); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; @@ -270,6 +316,8 @@ static int is_visited_state(){ index = get_search_interval(visited_states, new_state, &min, &max); if(min != -1 && max != -1){ + + // Parallell implementation /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state); if(res != -1){ state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t); @@ -284,13 +332,16 @@ static int is_visited_state(){ xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL); xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return new_state->other_num; }*/ + cursor = min; while(cursor <= max){ state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); if(snapshot_compare(state_test, new_state) == 0){ + // The state has been visited: + if(state_test->other_num == -1) new_state->other_num = state_test->num; else @@ -299,16 +350,24 @@ static int is_visited_state(){ XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num); else XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num); + + // Replace the old state with the new one (why?): xbt_dynar_remove_at(visited_states, cursor, NULL); xbt_dynar_insert_at(visited_states, cursor, &new_state); + if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return new_state->other_num; } cursor++; } + + // The state has not been visited, add it to the list: xbt_dynar_insert_at(visited_states, min, &new_state); + }else{ + + // The state has not been visited: insert the state in the dynamic array. state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t); if(state_test->nb_processes < new_state->nb_processes){ xbt_dynar_insert_at(visited_states, index+1, &new_state); @@ -318,9 +377,13 @@ static int is_visited_state(){ else xbt_dynar_insert_at(visited_states, index, &new_state); } + } + // We have reached the maximum number of stored states; if(xbt_dynar_length(visited_states) > _sg_mc_visited){ + + // Find the (index of the) older state: int min2 = mc_stats->expanded_states; unsigned int cursor2 = 0; unsigned int index2 = 0; @@ -330,11 +393,13 @@ static int is_visited_state(){ min2 = state_test->num; } } + + // and drop it: xbt_dynar_remove_at(visited_states, index2, NULL); } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; @@ -347,26 +412,30 @@ static int is_visited_state(){ void MC_dpor_init() { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); mc_state_t initial_state = NULL; smx_process_t process; /* Create the initial state and push it into the exploration stack */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; 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); + if(mc_reduce_kind == e_mc_reduce_dpor) + 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; + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ + 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); + incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL); + nb_comm_pattern = 0; + } initial_state = MC_state_new(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); @@ -377,7 +446,7 @@ void MC_dpor_init() MC_ignore_heap(simix_global->process_to_run->data, 0); MC_ignore_heap(simix_global->process_that_ran->data, 0); - MC_SET_RAW_MEM; + 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){ @@ -390,32 +459,33 @@ void MC_dpor_init() xbt_fifo_unshift(mc_stack_safety, initial_state); - /* To ensure the soundness of DPOR, we have to keep a list of - processes which are still enabled at each step of the exploration. - If max depth is reached, we interleave them in the state in which they have - been enabled for the first time. */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - char *key = bprintf("%lu", process->pid); - char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety)); - xbt_dict_set(first_enabled_state, key, data, NULL); - xbt_free(key); + if(mc_reduce_kind == e_mc_reduce_dpor){ + /* To ensure the soundness of DPOR, we have to keep a list of + processes which are still enabled at each step of the exploration. + If max depth is reached, we interleave them in the state in which they have + been enabled for the first time. */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + char *key = bprintf("%lu", process->pid); + char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety)); + xbt_dict_set(first_enabled_state, key, data, NULL); + xbt_free(key); + } } } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } -/** - * \brief Perform the model-checking operation using a depth-first search exploration - * with Dynamic Partial Order Reductions +/** \brief Model-check the application using a DFS exploration + * with DPOR (Dynamic Partial Order Reductions) */ void MC_dpor(void) { @@ -432,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) { @@ -461,39 +532,62 @@ void MC_dpor(void) xbt_free(req_str); } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(dot_output != NULL) req_str = MC_request_get_dot_output(req, value); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; - MC_SET_RAW_MEM; - char *key = bprintf("%lu", req->issuer->pid); - xbt_dict_remove(first_enabled_state, key); - xbt_free(key); - MC_UNSET_RAW_MEM; - - if(_sg_mc_comms_determinism){ + if(mc_reduce_kind == e_mc_reduce_dpor){ + MC_SET_MC_HEAP; + char *key = bprintf("%lu", req->issuer->pid); + xbt_dict_remove(first_enabled_state, key); + xbt_free(key); + MC_SET_STD_HEAP; + } + + /* TODO : handle test and testany simcalls */ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND) comm_pattern = 1; else if(req->call == SIMCALL_COMM_IRECV) 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 */ SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ - if(_sg_mc_comms_determinism){ - MC_SET_RAW_MEM; - if(comm_pattern != 0){ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ + MC_SET_MC_HEAP; + if(comm_pattern == 1 || comm_pattern == 2){ 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); + }else if(comm_pattern == 3){ + 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; + MC_SET_STD_HEAP; comm_pattern = 0; } @@ -501,7 +595,7 @@ void MC_dpor(void) MC_wait_for_requests(); /* Create the new expanded state */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; next_state = MC_state_new(); @@ -532,22 +626,24 @@ void MC_dpor(void) xbt_fifo_unshift(mc_stack_safety, next_state); - /* Insert in dict all enabled processes, if not included yet */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - char *key = bprintf("%lu", process->pid); - if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){ - char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety)); - xbt_dict_set(first_enabled_state, key, data, NULL); + if(mc_reduce_kind == e_mc_reduce_dpor){ + /* Insert in dict all enabled processes, if not included yet */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + char *key = bprintf("%lu", process->pid); + if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){ + char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety)); + xbt_dict_set(first_enabled_state, key, data, NULL); + } + xbt_free(key); } - xbt_free(key); } } if(dot_output != NULL) xbt_free(req_str); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Let's loop again */ @@ -563,19 +659,21 @@ void MC_dpor(void) visited_state = -1; - /* Interleave enabled processes in the state in which they have been enabled for the first time */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - char *key = bprintf("%lu", process->pid); - enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10); - xbt_free(key); - int cursor = xbt_fifo_size(mc_stack_safety); - xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){ - if(cursor-- == enabled){ - if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){ - XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num); - MC_state_interleave_process(state_test, process); - break; + if(mc_reduce_kind == e_mc_reduce_dpor){ + /* Interleave enabled processes in the state in which they have been enabled for the first time */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + char *key = bprintf("%lu", process->pid); + enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10); + xbt_free(key); + int cursor = xbt_fifo_size(mc_stack_safety); + xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){ + if(cursor-- == enabled){ + if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){ + XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num); + MC_state_interleave_process(state_test, process); + break; + } } } } @@ -588,18 +686,38 @@ void MC_dpor(void) } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; - if(_sg_mc_comms_determinism){ - if(!initial_state_safety->initial_communications_pattern_done){ - //print_communications_pattern(initial_communications_pattern); - }else{ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ + if(initial_state_safety->initial_communications_pattern_done){ 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); + if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){ + XBT_INFO("****************************************************"); + XBT_INFO("***** Non-deterministic communications pattern *****"); + XBT_INFO("****************************************************"); + XBT_INFO("Initial communications pattern:"); + print_communications_pattern(initial_communications_pattern); + XBT_INFO("Communications pattern counter-example:"); + print_communications_pattern(communications_pattern); + MC_print_statistics(mc_stats); + return; + }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){ + XBT_INFO("****************************************************"); + XBT_INFO("***** Non-send-deterministic communications pattern *****"); + XBT_INFO("****************************************************"); + XBT_INFO("Initial communications pattern:"); + print_communications_pattern(initial_communications_pattern); + XBT_INFO("Communications pattern counter-example:"); + print_communications_pattern(communications_pattern); + MC_print_statistics(mc_stats); + return; + } } + }else{ + initial_state_safety->initial_communications_pattern_done = 1; } - initial_state_safety->initial_communications_pattern_done = 1; } /* Trash the current state, no longer needed */ @@ -607,7 +725,7 @@ void MC_dpor(void) MC_state_delete(state); XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Check for deadlocks */ if(MC_deadlock_check()){ @@ -615,7 +733,7 @@ void MC_dpor(void) return; } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that have it empty in the way. For each deleted state, check if the request that has generated it @@ -624,7 +742,7 @@ void MC_dpor(void) state that executed that previous request. */ while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) { - if(mc_reduce_kind != e_mc_reduce_none){ + if(mc_reduce_kind == e_mc_reduce_dpor){ req = MC_state_get_internal_request(state); xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) { if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){ @@ -667,7 +785,7 @@ void MC_dpor(void) if(state->system_state != NULL){ MC_restore_snapshot(state->system_state); xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; }else{ pos = xbt_fifo_size(mc_stack_safety); item = xbt_fifo_get_first_item(mc_stack_safety); @@ -682,33 +800,33 @@ void MC_dpor(void) } MC_restore_snapshot(restored_state->system_state); xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_replay(mc_stack_safety, pos); } }else{ xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_replay(mc_stack_safety, -1); } 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(_sg_mc_comms_determinism){ + /*req = MC_state_get_internal_request(state); + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){ 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); } } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } } MC_print_statistics(mc_stats); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; }