From: Marion Guthmuller Date: Tue, 18 Feb 2014 14:41:16 +0000 (+0100) Subject: model-checker : conflit X-Git-Tag: v3_11~199^2~2^2~26 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/8fc11b8e2c3f486babc8be5494ddd53ffcc659f4?hp=-c model-checker : conflit --- 8fc11b8e2c3f486babc8be5494ddd53ffcc659f4 diff --combined src/mc/mc_dpor.c index a45cc5f31e,507b6df393..a3e2949111 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@@ -92,7 -92,7 +92,7 @@@ static void deterministic_pattern(xbt_d recv_index = 0; current_process++; } - XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic); + // 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){ @@@ -157,7 -157,7 +157,7 @@@ static void print_communications_patter 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); + // 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); } } @@@ -423,15 -423,15 +423,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) { @@@ -474,28 -474,25 +474,28 @@@ 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){ + 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){ + 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(); @@@ -589,24 -586,24 +589,24 @@@ } 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){ + 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); + } } + 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 */ @@@ -672,15 -669,15 +672,15 @@@ 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); @@@ -694,11 -691,10 +694,11 @@@ 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); + if(_sg_mc_comms_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); diff --combined src/mc/mc_global.c index a72abfea07,e0a8bddb6a..668bea076b --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@@ -19,8 -19,6 +19,6 @@@ #include "xbt/automaton.h" #include "xbt/dict.h" - static void MC_post_process_types(mc_object_info_t info); - XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); @@@ -35,7 -33,6 +33,7 @@@ int _sg_mc_timeout=0 int _sg_mc_max_depth=1000; int _sg_mc_visited=0; char *_sg_mc_dot_output_file = NULL; +int _sg_mc_comms_determinism=0; int user_max_depth_reached = 0; @@@ -94,13 -91,6 +92,13 @@@ void _mc_cfg_cb_dot_output(const char * _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name); } +void _mc_cfg_cb_comms_determinism(const char *name, int pos) { + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name); +} + /* MC global data structures */ mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; @@@ -174,7 -164,7 +172,7 @@@ void dw_variable_free(dw_variable_t v) xbt_free(v->name); xbt_free(v->type_origin); if(!v->global) - dw_location_free(v->address.location); + dw_location_free(v->location); xbt_free(v); } } @@@ -186,11 -176,7 +184,7 @@@ void dw_variable_free_voidp(void *t) // object_info mc_object_info_t MC_new_object_info(void) { - mc_object_info_t res = xbt_new(s_mc_object_info_t, 1); - res->file_name = NULL; - res->start_text = NULL; - res->start_data = NULL; - res->start_bss = NULL; + mc_object_info_t res = xbt_new0(s_mc_object_info_t, 1); res->local_variables = xbt_dict_new_homogeneous(NULL); res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp); res->types = xbt_dict_new_homogeneous(NULL); @@@ -399,9 -385,9 +393,9 @@@ static int MC_dwarf_get_variable_index( end = cursor - 1; }else{ if(address){ /* global variable */ - if(var_test->address.address == address) + if(var_test->address == address) return -1; - if(var_test->address.address > address) + if(var_test->address > address) end = cursor - 1; else start = cursor + 1; @@@ -412,7 -398,7 +406,7 @@@ } if(strcmp(var_test->name, var) == 0){ - if(address && var_test->address.address < address) + if(address && var_test->address < address) return cursor+1; else return cursor; @@@ -424,7 -410,7 +418,7 @@@ } void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable) { - int index = MC_dwarf_get_variable_index(info->global_variables, variable->name, variable->address.address); + int index = MC_dwarf_get_variable_index(info->global_variables, variable->name, variable->address); if (index != -1) xbt_dynar_insert_at(info->global_variables, index, &variable); // TODO, else ? @@@ -447,26 -433,6 +441,6 @@@ void MC_dwarf_register_variable(mc_obje MC_dwarf_register_non_global_variable(info, frame, variable); } - static void MC_post_process_array_size(mc_object_info_t info, dw_type_t type) { - xbt_assert(type->dw_type_id, "No base type for array <%p>%s", type->id, type->name); - dw_type_t subtype = xbt_dict_get_or_null(info->types, type->dw_type_id); - xbt_assert(subtype, "Unkown base type <%s> for array <%p>%s", type->dw_type_id, type->id, type->name); - if(subtype->type==DW_TAG_array_type && type->byte_size==0) { - MC_post_process_array_size(info, subtype); - } - type->byte_size = type->element_count*subtype->byte_size; - } - - static void MC_post_process_types(mc_object_info_t info) { - xbt_dict_cursor_t cursor; - char *origin; - dw_type_t type; - xbt_dict_foreach(info->types, cursor, origin, type){ - if(type->type==DW_TAG_array_type && type->byte_size==0) - MC_post_process_array_size(info, type); - } - } - /******************************* Ignore mechanism *******************************/ /*********************************************************************************/ @@@ -1270,8 -1236,7 +1244,8 @@@ void MC_replay(xbt_fifo_t stack, int st xbt_free(key); } } - xbt_dynar_reset(communications_pattern); + if(_sg_mc_comms_determinism) + xbt_dynar_reset(communications_pattern); MC_UNSET_RAW_MEM; @@@ -1302,23 -1267,20 +1276,23 @@@ } } - if(req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; - else if(req->call == SIMCALL_COMM_IRECV) + if(_sg_mc_comms_determinism){ + if(req->call == SIMCALL_COMM_ISEND) + comm_pattern = 1; + else if(req->call == SIMCALL_COMM_IRECV) comm_pattern = 2; - + } + SIMIX_simcall_pre(req, value); - MC_SET_RAW_MEM; - if(comm_pattern != 0){ - get_comm_pattern(communications_pattern, req, comm_pattern); + if(_sg_mc_comms_determinism){ + MC_SET_RAW_MEM; + if(comm_pattern != 0){ + get_comm_pattern(communications_pattern, req, comm_pattern); + } + MC_UNSET_RAW_MEM; + comm_pattern = 0; } - MC_UNSET_RAW_MEM; - - comm_pattern = 0; MC_wait_for_requests(); @@@ -1600,9 -1562,9 +1574,9 @@@ void MC_print_statistics(mc_stats_t sta fprintf(dot_output, "}\n"); fclose(dot_output); } - if(initial_state_safety != NULL){ - // XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes"); - // XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); + if(initial_state_safety != NULL && _sg_mc_comms_determinism){ + XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes"); + XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); } MC_UNSET_RAW_MEM; }