X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/9c40447cb76e20937a7c2a5acedcd84a22990514..e25984db80c73093c3e6ecf7cf4034f27e9b026c:/src/mc/mc_compare.cpp diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp index 55db66055c..174b889644 100644 --- a/src/mc/mc_compare.cpp +++ b/src/mc/mc_compare.cpp @@ -5,14 +5,17 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #define __STDC_FORMAT_MACROS -#include +#include #include +#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" @@ -23,8 +26,7 @@ #include -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc, - "Logging specific to mc_compare"); +using simgrid::mc::remote; typedef struct s_pointers_pair { void *p1; @@ -54,6 +56,9 @@ struct mc_compare_state { extern "C" { +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt, + "Logging specific to mc_compare in mc"); + /************************** Free functions ****************************/ /********************************************************************/ @@ -101,7 +106,7 @@ 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; + mc_process_t process = &mc_model_checker->process(); unsigned int cursor = 0; dw_type_t member, subtype, subsubtype; @@ -229,9 +234,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, (mc_address_space_t) snapshot1, process_index); + mc_member_resolve(real_area1, type, member, snapshot1, process_index); void *member2 = - mc_member_resolve(real_area2, type, member, (mc_address_space_t) snapshot2, process_index); + mc_member_resolve(real_area2, type, member, 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 = @@ -263,29 +268,30 @@ static int compare_global_variables(mc_object_info_t object_info, xbt_assert(r1 && r2, "Missing region."); #ifdef HAVE_SMPI - if (r1->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED) { + if (r1->storage_type() == simgrid::mc::StorageType::Privatized) { xbt_assert(process_index >= 0); - if (r2->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED) { + if (r2->storage_type() != simgrid::mc::StorageType::Privatized) { return 1; } - size_t process_count = smpi_process_count(); - xbt_assert(process_count == r1->privatized.regions_count - && process_count == r2->privatized.regions_count); + size_t process_count = MC_smpi_process_count(); + xbt_assert(process_count == r1->privatized_data().size() + && process_count == r2->privatized_data().size()); // 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], + &r1->privatized_data()[process_index], + &r2->privatized_data()[process_index], snapshot1, snapshot2); if (is_diff) return 1; } return 0; } #else - xbt_assert(r1->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED); + xbt_assert(r1->storage_type() != simgrid::mc::StorageType::Privatized); #endif - xbt_assert(r2->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED); + xbt_assert(r2->storage_type() != simgrid::mc::StorageType::Privatized); struct mc_compare_state state; @@ -384,7 +390,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_process_t process = &mc_model_checker->process(); mc_snapshot_t s1, s2; int num1, num2; @@ -394,6 +400,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; @@ -484,14 +495,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( - 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); + xbt_mheap_t heap1 = (xbt_mheap_t)s1->read_bytes( + alloca(sizeof(struct mdesc)), sizeof(struct mdesc), + remote(process->heap_address), + simgrid::mc::ProcessIndexMissing, simgrid::mc::AddressSpace::Lazy); + xbt_mheap_t heap2 = (xbt_mheap_t)s2->read_bytes( + alloca(sizeof(struct mdesc)), sizeof(struct mdesc), + remote(process->heap_address), + simgrid::mc::ProcessIndexMissing, simgrid::mc::AddressSpace::Lazy); res_init = init_heap_information(heap1, heap2, s1->to_ignore, s2->to_ignore); if (res_init == -1) { #ifdef MC_DEBUG @@ -578,15 +589,14 @@ int snapshot_compare(void *state1, void *state2) mc_mem_region_t region2 = s2->snapshot_regions[k]; // Preconditions: - if (region1->region_type != MC_REGION_TYPE_DATA) + if (region1->region_type() != simgrid::mc::RegionType::Data) continue; - xbt_assert(region1->region_type == region2->region_type); - xbt_assert(region1->object_info == region2->object_info); - - xbt_assert(region1->object_info); + 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; + const char* name = region1->object_info()->file_name; #ifdef MC_DEBUG if (is_diff == 0) @@ -596,7 +606,7 @@ int snapshot_compare(void *state1, void *state2) /* Compare global variables */ is_diff = - compare_global_variables(region1->object_info, MC_ADDRESS_SPACE_READ_FLAGS_NONE, + compare_global_variables(region1->object_info( ), simgrid::mc::AddressSpace::Normal, region1, region2, s1, s2); @@ -713,20 +723,4 @@ void print_comparison_times() XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time); } -/**************************** MC snapshot compare simcall **************************/ -/***********************************************************************************/ - -int simcall_HANDLER_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); - -} - }