X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a0fcde6efb589d65005c77e7d64b8634cbe277fc..50b36cfb6864e719576327d1289cf9ba31d652da:/src/mc/mc_compare.cpp diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp index 1891f31d8a..3420b02989 100644 --- a/src/mc/mc_compare.cpp +++ b/src/mc/mc_compare.cpp @@ -9,7 +9,11 @@ #include #include "internal_config.h" +#include "mc_object_info.h" +#include "mc_safety.h" +#include "mc_liveness.h" #include "mc_private.h" +#include "mc_smx.h" #ifdef HAVE_SMPI #include "smpi/private.h" @@ -18,6 +22,8 @@ #include "xbt/mmalloc.h" #include "xbt/mmalloc/mmprivate.h" +#include + XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc, "Logging specific to mc_compare"); @@ -55,7 +61,6 @@ extern "C" { static void stack_region_free(stack_region_t s) { if (s) { - xbt_free(s->process_name); xbt_free(s); } } @@ -97,6 +102,8 @@ static int compare_areas_with_type(struct mc_compare_state& state, void* real_area2, mc_snapshot_t snapshot2, mc_mem_region_t region2, dw_type_t type, int pointer_level) { + mc_process_t process = &mc_model_checker->process; + unsigned int cursor = 0; dw_type_t member, subtype, subsubtype; int elm_size, i, res; @@ -110,7 +117,7 @@ static int compare_areas_with_type(struct mc_compare_state& state, case DW_TAG_enumeration_type: case DW_TAG_union_type: { - return mc_snapshot_region_memcmp( + return MC_snapshot_region_memcmp( real_area1, region1, real_area2, region2, type->byte_size) != 0; } @@ -164,8 +171,8 @@ static int compare_areas_with_type(struct mc_compare_state& state, case DW_TAG_reference_type: case DW_TAG_rvalue_reference_type: { - void* addr_pointed1 = mc_snapshot_read_pointer_region(real_area1, region1); - void* addr_pointed2 = mc_snapshot_read_pointer_region(real_area2, region2); + void* addr_pointed1 = MC_region_read_pointer(region1, real_area1); + void* addr_pointed2 = MC_region_read_pointer(region2, real_area2); if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) { return (addr_pointed1 != addr_pointed2); @@ -185,10 +192,10 @@ static int compare_areas_with_type(struct mc_compare_state& state, // * a pointer leads to the read-only segment of the current object; // * a pointer lead to a different ELF object. - if (addr_pointed1 > std_heap + if (addr_pointed1 > process->heap_address && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)) { if (! - (addr_pointed2 > std_heap + (addr_pointed2 > process->heap_address && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))) return 1; // The pointers are both in the heap: @@ -223,9 +230,9 @@ static int compare_areas_with_type(struct mc_compare_state& state, case DW_TAG_class_type: xbt_dynar_foreach(type->members, cursor, member) { void *member1 = - mc_member_resolve(real_area1, type, member, snapshot1, process_index); + mc_member_resolve(real_area1, type, member, (mc_address_space_t) snapshot1, process_index); void *member2 = - mc_member_resolve(real_area2, type, member, snapshot2, process_index); + mc_member_resolve(real_area2, type, member, (mc_address_space_t) snapshot2, process_index); mc_mem_region_t subregion1 = mc_get_region_hinted(member1, snapshot1, process_index, region1); mc_mem_region_t subregion2 = mc_get_region_hinted(member2, snapshot2, process_index, region2); res = @@ -255,6 +262,32 @@ static int compare_global_variables(mc_object_info_t object_info, mc_snapshot_t snapshot2) { xbt_assert(r1 && r2, "Missing region."); + +#ifdef HAVE_SMPI + if (r1->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED) { + xbt_assert(process_index >= 0); + if (r2->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED) { + return 1; + } + + size_t process_count = MC_smpi_process_count(); + xbt_assert(process_count == r1->privatized.regions_count + && process_count == r2->privatized.regions_count); + + // Compare the global variables separately for each simulates process: + for (size_t process_index = 0; process_index < process_count; process_index++) { + int is_diff = compare_global_variables(object_info, process_index, + r1->privatized.regions[process_index], r2->privatized.regions[process_index], + snapshot1, snapshot2); + if (is_diff) return 1; + } + return 0; + } +#else + xbt_assert(r1->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED); +#endif + xbt_assert(r2->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED); + struct mc_compare_state state; xbt_dynar_t variables; @@ -280,6 +313,7 @@ static int compare_global_variables(mc_object_info_t object_info, (char *) current_var->address, snapshot2, r2, bvariable_type, 0); if (res == 1) { + XBT_TRACE3(mc, global_diff, -1, -1, current_var->name); XBT_VERB("Global variable %s (%p) is different between snapshots", current_var->name, (char *) current_var->address); return 1; @@ -336,6 +370,7 @@ static int compare_local_variables(int process_index, if (res == 1) { // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram + XBT_TRACE3(mc, local_diff, -1, -1, current_var1->name); XBT_VERB ("Local variable %s (%p - %p) in frame %s is different between snapshots", current_var1->name, current_var1->address, current_var2->address, @@ -350,6 +385,7 @@ static int compare_local_variables(int process_index, int snapshot_compare(void *state1, void *state2) { + mc_process_t process = &mc_model_checker->process; mc_snapshot_t s1, s2; int num1, num2; @@ -359,6 +395,11 @@ int snapshot_compare(void *state1, void *state2) s2 = ((mc_visited_pair_t) state2)->graph_state->system_state; num1 = ((mc_visited_pair_t) state1)->num; num2 = ((mc_visited_pair_t) state2)->num; + }else if (_sg_mc_termination) { /* Non-progressive cycle MC */ + s1 = ((mc_state_t) state1)->system_state; + s2 = ((mc_state_t) state2)->system_state; + num1 = ((mc_state_t) state1)->num; + num2 = ((mc_state_t) state2)->num; } else { /* Safety or comm determinism MC */ s1 = ((mc_visited_state_t) state1)->system_state; s2 = ((mc_visited_state_t) state2)->system_state; @@ -382,6 +423,7 @@ int snapshot_compare(void *state1, void *state2) if (_sg_mc_hash) { hash_result = (s1->hash != s2->hash); if (hash_result) { + XBT_TRACE2(mc, hash_diff, num1, num2); XBT_VERB("(%d - %d) Different hash : 0x%" PRIx64 "--0x%" PRIx64, num1, num2, s1->hash, s2->hash); #ifndef MC_DEBUG @@ -396,8 +438,11 @@ int snapshot_compare(void *state1, void *state2) unsigned int cursor; int pid; xbt_dynar_foreach(s1->enabled_processes, cursor, pid){ - if(!xbt_dynar_member(s2->enabled_processes, &pid)) + if(!xbt_dynar_member(s2->enabled_processes, &pid)) { + //XBT_TRACE3(mc, state_diff, num1, num2, "Different enabled processes"); XBT_VERB("(%d - %d) Different enabled processes", num1, num2); + // return 1; ?? + } } unsigned long i = 0; @@ -424,6 +469,7 @@ int snapshot_compare(void *state1, void *state2) XBT_VERB("(%d - %d) Different size used in stacks : %zu - %zu", num1, num2, size_used1, size_used2); #endif + XBT_TRACE3(mc, state_diff, num1, num2, "Different stack size"); xbt_os_walltimer_stop(timer); xbt_os_timer_free(timer); @@ -444,10 +490,14 @@ int snapshot_compare(void *state1, void *state2) #endif /* Init heap information used in heap comparison algorithm */ - xbt_mheap_t heap1 = (xbt_mheap_t) mc_snapshot_read(std_heap, s1, MC_NO_PROCESS_INDEX, - alloca(sizeof(struct mdesc)), sizeof(struct mdesc)); - xbt_mheap_t heap2 = (xbt_mheap_t) mc_snapshot_read(std_heap, s2, MC_NO_PROCESS_INDEX, - alloca(sizeof(struct mdesc)), sizeof(struct mdesc)); + xbt_mheap_t heap1 = (xbt_mheap_t) MC_snapshot_read( + s1, MC_ADDRESS_SPACE_READ_FLAGS_LAZY, + alloca(sizeof(struct mdesc)), process->heap_address, sizeof(struct mdesc), + MC_PROCESS_INDEX_MISSING); + xbt_mheap_t heap2 = (xbt_mheap_t) MC_snapshot_read( + s2, MC_ADDRESS_SPACE_READ_FLAGS_LAZY, + alloca(sizeof(struct mdesc)), process->heap_address, sizeof(struct mdesc), + MC_PROCESS_INDEX_MISSING); res_init = init_heap_information(heap1, heap2, s1->to_ignore, s2->to_ignore); if (res_init == -1) { #ifdef MC_DEBUG @@ -455,6 +505,7 @@ int snapshot_compare(void *state1, void *state2) errors++; #else #ifdef MC_VERBOSE + XBT_TRACE3(mc, state_diff, num1, num2, "Different heap information"); XBT_VERB("(%d - %d) Different heap information", num1, num2); #endif @@ -492,6 +543,7 @@ int snapshot_compare(void *state1, void *state2) else diff_local = compare_local_variables(stack1->process_index, s1, s2, stack1, stack2); if (diff_local > 0) { + XBT_TRACE3(mc, state_diff, num1, num2, "Different local variables"); #ifdef MC_DEBUG if (is_diff == 0) { xbt_os_walltimer_stop(timer); @@ -521,21 +573,27 @@ int snapshot_compare(void *state1, void *state2) cursor++; } + size_t regions_count = s1->snapshot_regions_count; + // TODO, raise a difference instead? + xbt_assert(regions_count == s2->snapshot_regions_count); + mc_comp_times->global_variables_comparison_time = 0; - const char *names[3] = { "?", "libsimgrid", "binary" }; -#ifdef MC_DEBUG - double *times[3] = { - NULL, - &mc_comp_times->libsimgrid_global_variables_comparison_time, - &mc_comp_times->binary_global_variables_comparison_time - }; -#endif + for (size_t k = 0; k != regions_count; ++k) { + mc_mem_region_t region1 = s1->snapshot_regions[k]; + mc_mem_region_t region2 = s2->snapshot_regions[k]; - mc_object_info_t object_infos[] = { NULL, mc_libsimgrid_info, mc_binary_info }; + // Preconditions: + if (region1->region_type != MC_REGION_TYPE_DATA) + continue; + + xbt_assert(region1->region_type == region2->region_type); + xbt_assert(region1->object_info == region2->object_info); + + xbt_assert(region1->object_info); + + const char* name = region1->object_info->file_name; - int k = 0; - for (k = 2; k != 0; --k) { #ifdef MC_DEBUG if (is_diff == 0) xbt_os_walltimer_stop(timer); @@ -543,32 +601,24 @@ int snapshot_compare(void *state1, void *state2) #endif /* Compare global variables */ -#ifdef HAVE_SMPI - if (object_infos[k] == mc_binary_info && smpi_privatize_global_variables) { - // Compare the global variables separately for each simulates process: - for (int process_index = 0; process_index < smpi_process_count(); process_index++) { - is_diff = - compare_global_variables(object_infos[k], process_index, - s1->privatization_regions[process_index], s2->privatization_regions[process_index], s1, s2); - if (is_diff) break; - } - } - else -#endif - is_diff = - compare_global_variables(object_infos[k], MC_NO_PROCESS_INDEX, s1->regions[k], s2->regions[k], s1, s2); + is_diff = + compare_global_variables(region1->object_info, MC_ADDRESS_SPACE_READ_FLAGS_NONE, + region1, region2, + s1, s2); if (is_diff != 0) { + XBT_TRACE3(mc, state_diff, num1, num2, "Different global variables"); #ifdef MC_DEBUG xbt_os_walltimer_stop(timer); - *times[k] = xbt_os_timer_elapsed(timer); + mc_comp_times->global_variables_comparison_time + += xbt_os_timer_elapsed(timer); XBT_DEBUG("(%d - %d) Different global variables in %s", num1, num2, - names[k]); + name); errors++; #else #ifdef MC_VERBOSE XBT_VERB("(%d - %d) Different global variables in %s", num1, num2, - names[k]); + name); #endif reset_heap_information(); @@ -589,6 +639,7 @@ int snapshot_compare(void *state1, void *state2) /* Compare heap */ if (mmalloc_compare_heap(s1, s2) > 0) { + XBT_TRACE3(mc, state_diff, num1, num2, "Different heap"); #ifdef MC_DEBUG xbt_os_walltimer_stop(timer); @@ -663,28 +714,9 @@ void print_comparison_times() XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time); XBT_DEBUG("- Nb bytes used : %f", mc_comp_times->bytes_used_comparison_time); XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time); - XBT_DEBUG("- Binary global variables : %f", - mc_comp_times->binary_global_variables_comparison_time); - XBT_DEBUG("- Libsimgrid global variables : %f", - mc_comp_times->libsimgrid_global_variables_comparison_time); + XBT_DEBUG("- GLobal variables : %f", mc_comp_times->global_variables_comparison_time); XBT_DEBUG("- Heap : %f", mc_comp_times->heap_comparison_time); XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time); } -/**************************** MC snapshot compare simcall **************************/ -/***********************************************************************************/ - -int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, - mc_snapshot_t s1, mc_snapshot_t s2) -{ - return snapshot_compare(s1, s2); -} - -int MC_compare_snapshots(void *s1, void *s2) -{ - - return simcall_mc_compare_snapshots(s1, s2); - -} - }