* under the terms of the license (GNU LGPL) which comes with this package. */
#define __STDC_FORMAT_MACROS
-#include <inttypes.h>
+#include <cinttypes>
#include <boost/unordered_set.hpp>
+#include <xbt/sysdep.h>
+
#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"
#include <xbt/probes.h>
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
- "Logging specific to mc_compare");
-
typedef struct s_pointers_pair {
void *p1;
void *p2;
extern "C" {
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt,
+ "Logging specific to mc_compare in mc");
+
/************************** Free functions ****************************/
/********************************************************************/
static void stack_region_free(stack_region_t s)
{
if (s) {
- xbt_free(s->process_name);
xbt_free(s);
}
}
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;
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 =
return 1;
}
- size_t process_count = smpi_process_count();
+ size_t process_count = MC_smpi_process_count();
xbt_assert(process_count == r1->privatized.regions_count
&& process_count == r2->privatized.regions_count);
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;
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;
cursor++;
}
-
-
- 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
-
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;
+
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];
xbt_assert(region1->object_info == region2->object_info);
xbt_assert(region1->object_info);
+
+ const char* name = region1->object_info->file_name;
+
#ifdef MC_DEBUG
if (is_diff == 0)
xbt_os_walltimer_stop(timer);
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();
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 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);
-
-}
-
}