X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/5dfafb1072cfc6a351514e002f730be75888d531..71f886401650b3aa9f05d2eebec723af25fff9f0:/src/mc/mc_dpor.c diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 40178859de..6c22b82738 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 @@ -14,6 +14,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; @@ -82,6 +83,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,24 +95,28 @@ 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){ mc_comm_pattern_t current_pattern; unsigned int cursor = 0; - xbt_dynar_foreach(list, cursor, current_pattern){ + int index; + 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 == 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->src_proc = pattern->comm->comm.src_proc->pid; + current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid; + current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host); + current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); + if(current_pattern->data_size == -1){ 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; } + current_pattern->matched_comm = pattern->num; + current_pattern->completed = 1; + xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL); + return current_pattern->num; } } return -1; @@ -120,16 +127,18 @@ 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->completed = 0; + pattern->data_size = -1; if(call == 1){ // ISEND pattern->comm = simcall_comm_isend__get__result(request); pattern->type = SIMIX_COMM_SEND; - if(pattern->comm->comm.dst_proc != NULL){ - + 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->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); 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); @@ -139,25 +148,36 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){ 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->src_host = simcall_host_get_name(request->issuer->smx_host); 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); + + if(!pattern->completed) + 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 -> %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_host, "iSend"); + else + XBT_INFO("[(%lu) %s <- %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_host, "iRecv"); } } @@ -207,6 +227,8 @@ static mc_visited_state_t visited_state_new(){ * 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); @@ -401,11 +423,15 @@ void MC_dpor_init() 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(); @@ -433,16 +459,18 @@ 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); + } } } @@ -465,15 +493,15 @@ void MC_dpor(void) char *req_str = NULL; int value; smx_simcall_t req = NULL, prev_req = NULL; - mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL; + mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL; smx_process_t process = NULL; xbt_fifo_item_t item = NULL; mc_state_t state_test = NULL; int pos; int visited_state = -1; int enabled = 0; - int comm_pattern = 0; int interleave_size = 0; + int comm_pattern = 0; while (xbt_fifo_size(mc_stack_safety) > 0) { @@ -511,30 +539,35 @@ void MC_dpor(void) 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(mc_reduce_kind == e_mc_reduce_dpor){ + 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(req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; - else if(req->call == SIMCALL_COMM_IRECV) - comm_pattern = 2; + 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; + } /* 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); + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ + 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; } - MC_UNSET_RAW_MEM; - - comm_pattern = 0; /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@ -571,15 +604,17 @@ 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); } } @@ -602,19 +637,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; + } } } } @@ -628,24 +665,44 @@ void MC_dpor(void) } MC_SET_RAW_MEM; - if(0) { - 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); + + 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; - } - MC_UNSET_RAW_MEM; /* Trash the current state, no longer needed */ - MC_SET_RAW_MEM; xbt_fifo_shift(mc_stack_safety); 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; /* Check for deadlocks */ @@ -711,15 +768,15 @@ void MC_dpor(void) pos = xbt_fifo_size(mc_stack_safety); item = xbt_fifo_get_first_item(mc_stack_safety); while(pos>0){ - restore_state = (mc_state_t) xbt_fifo_get_item_content(item); - if(restore_state->system_state != NULL){ + restored_state = (mc_state_t) xbt_fifo_get_item_content(item); + if(restored_state->system_state != NULL){ break; }else{ item = xbt_fifo_get_next_item(item); pos--; } } - MC_restore_snapshot(restore_state->system_state); + MC_restore_snapshot(restored_state->system_state); xbt_fifo_unshift(mc_stack_safety, state); MC_UNSET_RAW_MEM; MC_replay(mc_stack_safety, pos); @@ -732,12 +789,13 @@ 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); - } + /*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); }