/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
+#include "mc_base.h"
+
+#ifndef _XBT_WIN32
#include <unistd.h>
-#include <sys/types.h>
#include <sys/wait.h>
#include <sys/time.h>
-#include <sys/mman.h>
-#include <libgen.h>
-
-#define UNW_LOCAL_ONLY
-#include <libunwind.h>
+#endif
#include "simgrid/sg_config.h"
#include "../surf/surf_private.h"
#include "../simix/smx_private.h"
-#include "../xbt/mmalloc/mmprivate.h"
#include "xbt/fifo.h"
-#include "mc_private.h"
-#include "mc_record.h"
#include "xbt/automaton.h"
#include "xbt/dict.h"
+#ifdef HAVE_MC
+#define UNW_LOCAL_ONLY
+#include <libunwind.h>
+
+#include "../xbt/mmalloc/mmprivate.h"
+#include "mc_object_info.h"
+#include "mc_comm_pattern.h"
+#include "mc_request.h"
+#include "mc_safety.h"
+#include "mc_memory_map.h"
+#include "mc_snapshot.h"
+#include "mc_liveness.h"
+#include "mc_private.h"
+#endif
+#include "mc_record.h"
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
/* Liveness */
xbt_automaton_t _mc_property_automaton = NULL;
-/* Variables */
-mc_object_info_t mc_libsimgrid_info = NULL;
-mc_object_info_t mc_binary_info = NULL;
-
-mc_object_info_t mc_object_infos[2] = { NULL, NULL };
-
-size_t mc_object_infos_size = 2;
-
/* Dot output */
FILE *dot_output = NULL;
const char *colors[13];
}
-static void MC_init_debug_info(void)
-{
- XBT_INFO("Get debug information ...");
-
- memory_map_t maps = MC_get_memory_map();
-
- /* Get local variables for state equality detection */
- mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
- mc_object_infos[0] = mc_binary_info;
-
- mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0);
- mc_object_infos[1] = mc_libsimgrid_info;
-
- // Use information of the other objects:
- MC_post_process_object_info(mc_binary_info);
- MC_post_process_object_info(mc_libsimgrid_info);
-
- MC_free_memory_map(maps);
- XBT_INFO("Get debug information done !");
-}
-
-
mc_model_checker_t mc_model_checker = NULL;
mc_model_checker_t MC_model_checker_new()
mc->pages = mc_pages_store_new();
mc->fd_clear_refs = -1;
mc->fd_pagemap = -1;
+ MC_process_init(&mc->process, getpid());
return mc;
}
mc_pages_store_delete(mc->pages);
if(mc->record)
xbt_dynar_free(&mc->record);
+ MC_process_clear(&mc->process);
}
void MC_init()
mc_stats = xbt_new0(s_mc_stats_t, 1);
mc_stats->state_size = 1;
- MC_init_memory_map_info();
- MC_init_debug_info(); /* FIXME : get debug information only if liveness verification or visited state reduction */
-
if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0'))
MC_init_dot_output();
/* Ignore local variable about time used for tracing */
MC_ignore_local_variable("start_time", "*");
+ /* Main MC state: */
MC_ignore_global_variable("mc_model_checker");
+ MC_ignore_global_variable("communications_pattern");
+ MC_ignore_global_variable("initial_communications_pattern");
+ MC_ignore_global_variable("incomplete_communications_pattern");
- // Mot of those things could be moved into mc_model_checker:
- MC_ignore_global_variable("compared_pointers");
+ /* MC __thread variables: */
+ MC_ignore_global_variable("mc_diff_info");
MC_ignore_global_variable("mc_comp_times");
MC_ignore_global_variable("mc_snapshot_comparison_time");
+
+ /* This MC state is used in MC replay as well: */
MC_ignore_global_variable("mc_time");
- MC_ignore_global_variable("smpi_current_rank");
- MC_ignore_global_variable("counter"); /* Static variable used for tracing */
- MC_ignore_global_variable("maestro_stack_start");
- MC_ignore_global_variable("maestro_stack_end");
+
+ /* Static variable used for tracing */
+ MC_ignore_global_variable("counter");
+
+ /* SIMIX */
MC_ignore_global_variable("smx_total_comms");
- MC_ignore_global_variable("communications_pattern");
- MC_ignore_global_variable("initial_communications_pattern");
- MC_ignore_global_variable("incomplete_communications_pattern");
- MC_ignore_global_variable("mc_diff_info");
MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
user_max_depth_reached = 1;
}
-void MC_process_clock_add(smx_process_t process, double amount)
-{
- mc_time[process->pid] += amount;
-}
-
void MC_automaton_load(const char *file)
{
return 0;
}
}
+
+void MC_process_clock_add(smx_process_t process, double amount)
+{
+ mc_time[process->pid] += amount;
+}