X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0ccbaaa805875e64f29ceb8434e17c7de99b050c..ffe8ce65fd9a8e18a0469f26f067c3ea6d5d60d4:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 63ecd05968..85dacbca78 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -4,15 +4,14 @@ /* 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 + #include "mc_base.h" #ifndef _XBT_WIN32 #include -#include #include #include -#include -#include #endif #include "simgrid/sg_config.h" @@ -23,8 +22,8 @@ #include "xbt/dict.h" #ifdef HAVE_MC -#define UNW_LOCAL_ONLY #include +#include #include "../xbt/mmalloc/mmprivate.h" #include "mc_object_info.h" @@ -35,12 +34,17 @@ #include "mc_snapshot.h" #include "mc_liveness.h" #include "mc_private.h" +#include "mc_unw.h" #endif #include "mc_record.h" +#include "mc_protocol.h" +#include "mc_client.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); +e_mc_mode_t mc_mode; + double *mc_time = NULL; #ifdef HAVE_MC @@ -59,14 +63,6 @@ xbt_fifo_t mc_stack = NULL; /* 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]; @@ -104,57 +100,29 @@ static void MC_init_dot_output() } -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() +void MC_init() { - mc_model_checker_t mc = xbt_new0(s_mc_model_checker_t, 1); - mc->pages = mc_pages_store_new(); - mc->fd_clear_refs = -1; - mc->fd_pagemap = -1; - return mc; + MC_init_pid(getpid(), -1); } -void MC_model_checker_delete(mc_model_checker_t mc) { - mc_pages_store_delete(mc->pages); - if(mc->record) - xbt_dynar_free(&mc->record); -} - -void MC_init() +void MC_init_pid(pid_t pid, int socket) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + if (mc_mode == MC_MODE_NONE) { + if (getenv(MC_ENV_SOCKET_FD)) { + mc_mode = MC_MODE_CLIENT; + } else { + mc_mode = MC_MODE_STANDALONE; + } + } mc_time = xbt_new0(double, simix_process_maxpid); /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - mc_model_checker = MC_model_checker_new(); + mc_model_checker = MC_model_checker_new(pid, socket); mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); @@ -162,9 +130,6 @@ 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(); @@ -212,16 +177,22 @@ void MC_init() /* SIMIX */ MC_ignore_global_variable("smx_total_comms"); - MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); + if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) { + MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); - smx_process_t process; - xbt_swag_foreach(process, simix_global->process_list) { - MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); + smx_process_t process; + xbt_swag_foreach(process, simix_global->process_list) { + MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); + } } } - if (raw_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); + + if (mc_mode == MC_MODE_CLIENT) { + // This will move somehwere else: + MC_client_handle_messages(); + } } @@ -230,13 +201,9 @@ void MC_init() static void MC_modelcheck_comm_determinism_init(void) { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_init(); - if (!mc_mem_set) - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@ -255,21 +222,16 @@ static void MC_modelcheck_comm_determinism_init(void) MC_modelcheck_comm_determinism(); - if(mc_mem_set) - MC_SET_MC_HEAP; - + mmalloc_set_current_heap(heap); } static void MC_modelcheck_safety_init(void) { - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - _sg_mc_safety = 1; MC_init(); - if (!mc_mem_set) - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@ -286,8 +248,7 @@ static void MC_modelcheck_safety_init(void) MC_modelcheck_safety(); - if (mc_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); xbt_abort(); //MC_exit(); @@ -295,15 +256,11 @@ static void MC_modelcheck_safety_init(void) static void MC_modelcheck_liveness_init() { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - _sg_mc_liveness = 1; MC_init(); - if (!mc_mem_set) - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@ -319,8 +276,7 @@ static void MC_modelcheck_liveness_init() MC_print_statistics(mc_stats); xbt_free(mc_time); - if (mc_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); } @@ -443,7 +399,7 @@ static void MC_restore_communications_pattern(mc_state_t state) { */ void MC_replay(xbt_fifo_t stack) { - int raw_mem = (mmalloc_get_current_heap() == mc_heap); + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int value, count = 1, j; char *req_str; @@ -530,13 +486,7 @@ void MC_replay(xbt_fifo_t stack) } XBT_DEBUG("**** End Replay ****"); - - if (raw_mem) - MC_SET_MC_HEAP; - else - MC_SET_STD_HEAP; - - + mmalloc_set_current_heap(heap); } void MC_replay_liveness(xbt_fifo_t stack) @@ -627,8 +577,7 @@ void MC_replay_liveness(xbt_fifo_t stack) */ void MC_dump_stack_safety(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); MC_show_stack_safety(stack); @@ -637,22 +586,13 @@ void MC_dump_stack_safety(xbt_fifo_t stack) MC_SET_MC_HEAP; while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) MC_state_delete(state, !state->in_visited_states ? 1 : 0); - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - else - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); } void MC_show_stack_safety(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int value; mc_state_t state; @@ -671,8 +611,7 @@ void MC_show_stack_safety(xbt_fifo_t stack) } } - if (!raw_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } void MC_show_deadlock(smx_simcall_t req) @@ -714,26 +653,16 @@ void MC_show_stack_liveness(xbt_fifo_t stack) void MC_dump_stack_liveness(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); mc_pair_t pair; - - MC_SET_MC_HEAP; while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL) MC_pair_delete(pair); - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - + mmalloc_set_current_heap(heap); } void MC_print_statistics(mc_stats_t stats) { - xbt_mheap_t previous_heap = mmalloc_get_current_heap(); - if (stats->expanded_pairs == 0) { XBT_INFO("Expanded states = %lu", stats->expanded_states); XBT_INFO("Visited states = %lu", stats->visited_states); @@ -742,7 +671,7 @@ void MC_print_statistics(mc_stats_t stats) XBT_INFO("Visited pairs = %lu", stats->visited_pairs); } XBT_INFO("Executed transitions = %lu", stats->executed_transitions); - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) { fprintf(dot_output, "}\n"); fclose(dot_output); @@ -753,70 +682,73 @@ void MC_print_statistics(mc_stats_t stats) if (_sg_mc_send_determinism) XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); } - mmalloc_set_current_heap(previous_heap); -} - -void MC_assert(int prop) -{ - if (MC_is_active() && !prop) { - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - MC_record_dump_path(mc_stack); - MC_dump_stack_safety(mc_stack); - MC_print_statistics(mc_stats); - xbt_abort(); - } -} - -void MC_cut(void) -{ - user_max_depth_reached = 1; + mmalloc_set_current_heap(heap); } void MC_automaton_load(const char *file) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); xbt_automaton_load(_mc_property_automaton, file); - - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - + mmalloc_set_current_heap(heap); } -void MC_automaton_new_propositional_symbol(const char *id, void *fct) +static void register_symbol(xbt_automaton_propositional_symbol_t symbol) { + if (mc_mode != MC_MODE_CLIENT) + return; + s_mc_register_symbol_message_t message; + message.type = MC_MESSAGE_REGISTER_SYMBOL; + const char* name = xbt_automaton_propositional_symbol_get_name(symbol); + if (strlen(name) + 1 > sizeof(message.name)) + xbt_die("Symbol is too long"); + strncpy(message.name, name, sizeof(message.name)); + message.callback = xbt_automaton_propositional_symbol_get_callback(symbol); + message.data = xbt_automaton_propositional_symbol_get_data(symbol); + MC_client_send_message(&message, sizeof(message)); +} - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; +void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); - xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct); - - MC_SET_STD_HEAP; + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct); + register_symbol(symbol); + mmalloc_set_current_heap(heap); +} - if (raw_mem_set) - MC_SET_MC_HEAP; +void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + if (_mc_property_automaton == NULL) + _mc_property_automaton = xbt_automaton_new(); + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value); + register_symbol(symbol); + mmalloc_set_current_heap(heap); +} +void MC_automaton_new_propositional_symbol_callback(const char* id, + xbt_automaton_propositional_symbol_callback_type callback, + void* data, xbt_automaton_propositional_symbol_free_function_type free_function) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + if (_mc_property_automaton == NULL) + _mc_property_automaton = xbt_automaton_new(); + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_callback( + _mc_property_automaton, id, callback, data, free_function); + register_symbol(symbol); + mmalloc_set_current_heap(heap); } void MC_dump_stacks(FILE* file) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int nstack = 0; stack_region_t current_stack; @@ -838,9 +770,7 @@ void MC_dump_stacks(FILE* file) ++nstack; } - - if (raw_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); } #endif