X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/adcfb1a36dc3a193da6b595829fef2d7f4c9a4dd..c3ac58f9e63770cca194ec50390ac8ccc8e499e8:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 81c594fce9..53235a47d7 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -4,15 +4,15 @@ /* 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 + #include "mc_base.h" #ifndef _XBT_WIN32 #include -#include #include #include -#include -#include #endif #include "simgrid/sg_config.h" @@ -23,8 +23,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 +35,18 @@ #include "mc_snapshot.h" #include "mc_liveness.h" #include "mc_private.h" +#include "mc_unw.h" +#include "mc_smx.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 +65,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 +102,40 @@ static void MC_init_dot_output() } -static void MC_init_debug_info(void) +void MC_init() { - 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_init_pid(getpid(), -1); } - -mc_model_checker_t mc_model_checker = NULL; - -mc_model_checker_t MC_model_checker_new() +static void MC_init_mode(void) { - 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; -} - -void MC_model_checker_delete(mc_model_checker_t mc) { - mc_pages_store_delete(mc->pages); - if(mc->record) - xbt_dynar_free(&mc->record); + if (mc_mode == MC_MODE_NONE) { + if (getenv(MC_ENV_SOCKET_FD)) { + mc_mode = MC_MODE_CLIENT; + } else { + mc_mode = MC_MODE_STANDALONE; + } + } } -void MC_init() +void MC_init_pid(pid_t pid, int socket) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - 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(pid, socket); + if (mc_mode == MC_MODE_SERVER) { + unsigned long maxpid; + MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid", + &maxpid, sizeof(maxpid)); + simix_process_maxpid = maxpid; + } - mc_model_checker = MC_model_checker_new(); + mmalloc_set_current_heap(std_heap); + mc_time = xbt_new0(double, MC_smx_get_maxpid()); + mmalloc_set_current_heap(mc_heap); mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); @@ -162,9 +143,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(); @@ -173,7 +151,7 @@ void MC_init() MC_SET_STD_HEAP; - if (_sg_mc_visited > 0 || _sg_mc_liveness) { + if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination) { /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ MC_ignore_local_variable("e", "*"); MC_ignore_local_variable("__ex_cleanup", "*"); @@ -212,18 +190,21 @@ 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) { + /* Those requests are handled on the client side and propagated by message + * to the server: */ - smx_process_t process; - xbt_swag_foreach(process, simix_global->process_list) { - MC_ignore_heap(&(process->process_hookup), - sizeof(process->process_hookup)); - } - } + MC_ignore_heap(mc_time, MC_smx_get_maxpid() * sizeof(double)); - if (raw_mem_set) - MC_SET_MC_HEAP; + smx_process_t process; + xbt_swag_foreach(process, simix_global->process_list) { + MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); + } + } + } + + mmalloc_set_current_heap(heap); } /******************************* Core of MC *******************************/ @@ -231,13 +212,13 @@ 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_mode == MC_MODE_CLIENT) { + // This will move somehwere else: + MC_client_handle_messages(); + } - 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(); @@ -250,61 +231,29 @@ static void MC_modelcheck_comm_determinism_init(void) initial_global_state = xbt_new0(s_mc_global_t, 1); initial_global_state->snapshot = MC_take_snapshot(0); initial_global_state->initial_communications_pattern_done = 0; - initial_global_state->comm_deterministic = 1; + initial_global_state->recv_deterministic = 1; initial_global_state->send_deterministic = 1; - MC_SET_STD_HEAP; - - MC_modelcheck_comm_determinism(); - - if(mc_mem_set) - MC_SET_MC_HEAP; - -} - -static void MC_modelcheck_safety_init(void) -{ - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - _sg_mc_safety = 1; + initial_global_state->recv_diff = NULL; + initial_global_state->send_diff = NULL; - MC_init(); - - if (!mc_mem_set) - MC_SET_MC_HEAP; - - /* Create exploration stack */ - mc_stack = xbt_fifo_new(); - - MC_SET_STD_HEAP; - - MC_pre_modelcheck_safety(); - - MC_SET_MC_HEAP; - /* Save the initial state */ - initial_global_state = xbt_new0(s_mc_global_t, 1); - initial_global_state->snapshot = MC_take_snapshot(0); MC_SET_STD_HEAP; - MC_modelcheck_safety(); - - if (mc_mem_set) - MC_SET_MC_HEAP; + MC_modelcheck_comm_determinism(); - xbt_abort(); - //MC_exit(); + mmalloc_set_current_heap(heap); } static void MC_modelcheck_liveness_init() { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - _sg_mc_liveness = 1; MC_init(); + if (mc_mode == MC_MODE_CLIENT) { + // This will move somehwere else: + MC_client_handle_messages(); + } - 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(); @@ -320,23 +269,43 @@ 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); } void MC_do_the_modelcheck_for_real() { + MC_init_mode(); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { XBT_INFO("Check communication determinism"); + mc_reduce_kind = e_mc_reduce_none; MC_modelcheck_comm_determinism_init(); - } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') { - if (mc_reduce_kind == e_mc_reduce_unset) + } + + else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') { + if(_sg_mc_termination) + mc_reduce_kind = e_mc_reduce_none; + else if (mc_reduce_kind == e_mc_reduce_unset) mc_reduce_kind = e_mc_reduce_dpor; - XBT_INFO("Check a safety property"); - MC_modelcheck_safety_init(); - } else { + _sg_mc_safety = 1; + if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) { + if (_sg_mc_termination) + XBT_INFO("Check non progressive cycles"); + else + XBT_INFO("Check a safety property"); + MC_wait_for_requests(); + MC_modelcheck_safety(); + } + else { + // Most of this is not needed: + MC_init(); + // Main event loop: + MC_client_main_loop(); + } + } + + else { if (mc_reduce_kind == e_mc_reduce_unset) mc_reduce_kind = e_mc_reduce_none; XBT_INFO("Check the liveness property %s", _sg_mc_property_file); @@ -356,28 +325,49 @@ void MC_exit(void) int MC_deadlock_check() { + if (mc_mode == MC_MODE_SERVER) { + int res; + if ((res = MC_protocol_send_simple_message(mc_model_checker->process.socket, + MC_MESSAGE_DEADLOCK_CHECK))) + xbt_die("Could not check deadlock state"); + s_mc_int_message_t message; + ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message), 0); + if (s == -1) + xbt_die("Could not receive message"); + else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) { + xbt_die("%s received unexpected message %s (%i, size=%i) " + "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)", + MC_mode_name(mc_mode), + MC_message_type_name(message.type), (int) message.type, (int) s, + (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message) + ); + } + else + return message.value; + } + int deadlock = FALSE; smx_process_t process; if (xbt_swag_size(simix_global->process_list)) { deadlock = TRUE; - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_request_is_enabled(&process->simcall)) { + MC_EACH_SIMIX_PROCESS(process, + if (MC_process_is_enabled(process)) { deadlock = FALSE; break; } - } + ); } return deadlock; } -void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) { +void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) { switch(call_type) { case MC_CALL_TYPE_NONE: break; case MC_CALL_TYPE_SEND: case MC_CALL_TYPE_RECV: - get_comm_pattern(pattern, req, call_type); + MC_get_comm_pattern(pattern, req, call_type, backtracking); break; case MC_CALL_TYPE_WAIT: case MC_CALL_TYPE_WAITANY: @@ -387,55 +377,15 @@ void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int valu current_comm = simcall_comm_wait__get__comm(req); else current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t); - // First wait only must be considered: - if (current_comm->comm.refcount == 1) - complete_comm_pattern(pattern, current_comm, backtracking); - break; + MC_complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking); } + break; default: xbt_die("Unexpected call type %i", (int)call_type); } } -static void MC_restore_communications_pattern(mc_state_t state) { - mc_list_comm_pattern_t list_process_comm; - unsigned int cursor, cursor2; - xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){ - list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int); - } - mc_comm_pattern_t comm; - cursor = 0; - xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms; - for(int i=0; iincomplete_comm_pattern, i, xbt_dynar_t); - xbt_dynar_foreach(incomplete_process_comms, cursor2, comm) { - mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1); - copy_comm->index = comm->index; - copy_comm->type = comm->type; - copy_comm->comm = comm->comm; - copy_comm->rdv = strdup(comm->rdv); - copy_comm->data_size = -1; - copy_comm->data = NULL; - if(comm->type == SIMIX_COMM_SEND){ - copy_comm->src_proc = comm->src_proc; - copy_comm->src_host = comm->src_host; - if(comm->data != NULL){ - copy_comm->data_size = comm->data_size; - copy_comm->data = xbt_malloc0(comm->data_size); - memcpy(copy_comm->data, comm->data, comm->data_size); - } - }else{ - copy_comm->dst_proc = comm->dst_proc; - copy_comm->dst_host = comm->dst_host; - } - xbt_dynar_push(initial_incomplete_process_comms, ©_comm); - } - } -} - /** * \brief Re-executes from the state at position start all the transitions indicated by * a given model-checker stack. @@ -444,7 +394,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; @@ -455,14 +405,16 @@ void MC_replay(xbt_fifo_t stack) XBT_DEBUG("**** Begin Replay ****"); /* Intermediate backtracking */ - start_item = xbt_fifo_get_first_item(stack); - state = (mc_state_t)xbt_fifo_get_item_content(start_item); - if(state->system_state){ - MC_restore_snapshot(state->system_state); - if(_sg_mc_comms_determinism || _sg_mc_send_determinism) - MC_restore_communications_pattern(state); - MC_SET_STD_HEAP; - return; + if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) { + start_item = xbt_fifo_get_first_item(stack); + state = (mc_state_t)xbt_fifo_get_item_content(start_item); + if(state->system_state){ + MC_restore_snapshot(state->system_state); + if(_sg_mc_comms_determinism || _sg_mc_send_determinism) + MC_restore_communications_pattern(state); + MC_SET_STD_HEAP; + return; + } } @@ -477,7 +429,7 @@ void MC_replay(xbt_fifo_t stack) MC_SET_MC_HEAP; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - for (j=0; jindex_comm = 0; } @@ -496,11 +448,13 @@ void MC_replay(xbt_fifo_t stack) if (saved_req) { /* because we got a copy of the executed request, we have to fetch the real one, pointed by the request field of the issuer process */ - req = &saved_req->issuer->simcall; + + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + req = &issuer->simcall; /* Debug information */ if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { - req_str = MC_request_to_string(req, value); + req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX); XBT_DEBUG("Replay: %s (%p)", req_str, state); xbt_free(req_str); } @@ -508,13 +462,13 @@ void MC_replay(xbt_fifo_t stack) /* TODO : handle test and testany simcalls */ e_mc_call_type_t call = MC_CALL_TYPE_NONE; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - call = mc_get_call_type(req); + call = MC_get_call_type(req); - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); MC_SET_MC_HEAP; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - handle_comm_pattern(call, req, value, NULL, 1); + MC_handle_comm_pattern(call, req, value, NULL, 1); MC_SET_STD_HEAP; MC_wait_for_requests(); @@ -529,13 +483,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) @@ -553,12 +501,14 @@ void MC_replay_liveness(xbt_fifo_t stack) XBT_DEBUG("**** Begin Replay ****"); /* Intermediate backtracking */ - item = xbt_fifo_get_first_item(stack); - pair = (mc_pair_t) xbt_fifo_get_item_content(item); - if(pair->graph_state->system_state){ - MC_restore_snapshot(pair->graph_state->system_state); - MC_SET_STD_HEAP; - return; + if(_sg_mc_checkpoint > 0) { + item = xbt_fifo_get_first_item(stack); + pair = (mc_pair_t) xbt_fifo_get_item_content(item); + if(pair->graph_state->system_state){ + MC_restore_snapshot(pair->graph_state->system_state); + MC_SET_STD_HEAP; + return; + } } /* Restore the initial state */ @@ -585,18 +535,19 @@ void MC_replay_liveness(xbt_fifo_t stack) if (saved_req != NULL) { /* because we got a copy of the executed request, we have to fetch the real one, pointed by the request field of the issuer process */ - req = &saved_req->issuer->simcall; + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + req = &issuer->simcall; /* Debug information */ if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { - req_str = MC_request_to_string(req, value); + req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX); XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); xbt_free(req_str); } } - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); MC_wait_for_requests(); } @@ -624,8 +575,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); @@ -634,22 +584,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; @@ -662,14 +603,13 @@ void MC_show_stack_safety(xbt_fifo_t stack) : (NULL)); item = xbt_fifo_get_prev_item(item)) { req = MC_state_get_executed_request(state, &value); if (req) { - req_str = MC_request_to_string(req, value); + req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED); XBT_INFO("%s", req_str); xbt_free(req_str); } } - if (!raw_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } void MC_show_deadlock(smx_simcall_t req) @@ -687,6 +627,15 @@ void MC_show_deadlock(smx_simcall_t req) MC_print_statistics(mc_stats); } +void MC_show_non_termination(void){ + XBT_INFO("******************************************"); + XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); + XBT_INFO("******************************************"); + XBT_INFO("Counter-example execution trace:"); + MC_dump_stack_safety(mc_stack); + MC_print_statistics(mc_stats); +} + void MC_show_stack_liveness(xbt_fifo_t stack) { @@ -701,7 +650,7 @@ void MC_show_stack_liveness(xbt_fifo_t stack) item = xbt_fifo_get_prev_item(item)) { req = MC_state_get_executed_request(pair->graph_state, &value); if (req && req->call != SIMCALL_NONE) { - req_str = MC_request_to_string(req, value); + req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED); XBT_INFO("%s", req_str); xbt_free(req_str); } @@ -711,25 +660,28 @@ 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(_sg_mc_comms_determinism) { + if (!initial_global_state->recv_deterministic && initial_global_state->send_deterministic){ + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-send-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", initial_global_state->recv_diff); + }else if(!initial_global_state->send_deterministic && initial_global_state->recv_deterministic) { + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-recv-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", initial_global_state->send_diff); + } + } if (stats->expanded_pairs == 0) { XBT_INFO("Expanded states = %lu", stats->expanded_states); @@ -739,81 +691,84 @@ 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); } - if (initial_global_state != NULL) { + if (initial_global_state != NULL && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) { + XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); if (_sg_mc_comms_determinism) - XBT_INFO("Communication-deterministic : %s", !initial_global_state->comm_deterministic ? "No" : "Yes"); - if (_sg_mc_send_determinism) - XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); + XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_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); } +// TODO, fix cross-process access (this function is not used) 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; @@ -829,15 +784,22 @@ void MC_dump_stacks(FILE* file) unw_word_t off; do { const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?"; +#if defined(__x86_64__) + unw_word_t rip = 0; + unw_word_t rsp = 0; + unw_get_reg(&c, UNW_X86_64_RIP, &rip); + unw_get_reg(&c, UNW_X86_64_RSP, &rsp); + fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n", + nframe, name, rip, rsp); +#else fprintf(file, " %i: %s\n", nframe, name); +#endif ++nframe; } while(unw_step(&c)); ++nstack; } - - if (raw_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); } #endif @@ -857,3 +819,14 @@ void MC_process_clock_add(smx_process_t process, double amount) { mc_time[process->pid] += amount; } + +void MC_report_assertion_error(void) +{ + 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); +}