X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/38d1cfd08cf30b0da496b20dfa8b849cbfdb7ab4..923896223efc203372ce0a7435cbdb7b539149f6:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 5c5fb92f92..9d7bd56181 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -35,6 +35,7 @@ #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" @@ -115,14 +116,22 @@ void MC_init_pid(pid_t pid, int socket) } } - 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) */ 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) { + int maxpid; + MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid", + &maxpid, sizeof(maxpid)); + simix_process_maxpid = maxpid; + } + + 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); @@ -138,7 +147,7 @@ void MC_init_pid(pid_t pid, int socket) 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", "*"); @@ -159,9 +168,9 @@ void MC_init_pid(pid_t pid, int socket) /* 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"); + MC_ignore_global_variable("nb_comm_pattern"); /* MC __thread variables: */ MC_ignore_global_variable("mc_diff_info"); @@ -178,13 +187,17 @@ void MC_init_pid(pid_t pid, int socket) MC_ignore_global_variable("smx_total_comms"); if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) { - MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); + /* Those requests are handled on the client side and propagated by message + * to the server: */ + + MC_ignore_heap(mc_time, MC_smx_get_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)); - } + MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); + } } + } mmalloc_set_current_heap(heap); @@ -216,8 +229,11 @@ 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; + initial_global_state->recv_diff = NULL; + initial_global_state->send_diff = NULL; + MC_SET_STD_HEAP; MC_modelcheck_comm_determinism(); @@ -285,11 +301,15 @@ void MC_do_the_modelcheck_for_real() 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) - mc_reduce_kind = e_mc_reduce_dpor; - XBT_INFO("Check a safety property"); + if(_sg_mc_termination){ + XBT_INFO("Check non progressive cycles"); + mc_reduce_kind = e_mc_reduce_none; + }else{ + XBT_INFO("Check a safety property"); + } MC_modelcheck_safety_init(); } else { if (mc_reduce_kind == e_mc_reduce_unset) @@ -311,43 +331,100 @@ 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)); + if (s == -1) + xbt_die("Could not receive message"); + else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) { + xbt_die("Unexpected message, expected MC_MESSAGE_DEADLOCK_CHECK_REPLY %i %i vs %i %i", + (int) s, (int) message.type, (int) sizeof(message), (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY + ); + } + 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 mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value, xbt_dynar_t pattern) { +void 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); + get_comm_pattern(pattern, req, call_type, backtracking); break; case MC_CALL_TYPE_WAIT: + case MC_CALL_TYPE_WAITANY: { smx_synchro_t current_comm = NULL; if (call_type == MC_CALL_TYPE_WAIT) 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); - break; + 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; i < MC_smx_get_maxpid(); i++){ + initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t); + xbt_dynar_reset(initial_incomplete_process_comms); + incomplete_process_comms = xbt_dynar_get_as(state->incomplete_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); + } + } } /** @@ -355,63 +432,47 @@ void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value * a given model-checker stack. * \param stack The stack with the transitions to execute. * \param start Start index to begin the re-execution. - * - * If start==-1, restore the initial state and replay the actions the - * the transitions in the stack. - * - * Otherwise, we only replay a part of the transitions of the stacks - * without restoring the state: it is assumed that the current state - * match with the transitions to execute. */ -void MC_replay(xbt_fifo_t stack, int start) +void MC_replay(xbt_fifo_t stack) { xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - int value, i = 1, count = 1, j; + int value, count = 1, j; char *req_str; smx_simcall_t req = NULL, saved_req = NULL; xbt_fifo_item_t item, start_item; mc_state_t state; - smx_process_t process = NULL; - + XBT_DEBUG("**** Begin Replay ****"); - if (start == -1) { - /* Restore the initial state */ - MC_restore_snapshot(initial_global_state->snapshot); - /* At the moment of taking the snapshot the raw heap was set, so restoring - * it will set it back again, we have to unset it to continue */ - MC_SET_STD_HEAP; - } - - start_item = xbt_fifo_get_last_item(stack); - if (start != -1) { - while (i != start) { - start_item = xbt_fifo_get_prev_item(start_item); - i++; + /* Intermediate backtracking */ + 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; } } - MC_SET_MC_HEAP; - if (mc_reduce_kind == e_mc_reduce_dpor) { - xbt_dict_reset(first_enabled_state); - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_process_is_enabled(process)) { - char *key = bprintf("%lu", process->pid); - char *data = bprintf("%d", count); - xbt_dict_set(first_enabled_state, key, data, NULL); - xbt_free(key); - } - } - } + /* Restore the initial state */ + MC_restore_snapshot(initial_global_state->snapshot); + /* At the moment of taking the snapshot the raw heap was set, so restoring + * it will set it back again, we have to unset it to continue */ + MC_SET_STD_HEAP; + + start_item = xbt_fifo_get_last_item(stack); + + MC_SET_MC_HEAP; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - for (j=0; jindex_comm = 0; } } @@ -424,20 +485,13 @@ void MC_replay(xbt_fifo_t stack, int start) state = (mc_state_t) xbt_fifo_get_item_content(item); saved_req = MC_state_get_executed_request(state, &value); - - if (mc_reduce_kind == e_mc_reduce_dpor) { - MC_SET_MC_HEAP; - char *key = bprintf("%lu", saved_req->issuer->pid); - if(xbt_dict_get_or_null(first_enabled_state, key)) - xbt_dict_remove(first_enabled_state, key); - xbt_free(key); - MC_SET_STD_HEAP; - } - + 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)) { @@ -447,38 +501,20 @@ void MC_replay(xbt_fifo_t stack, int start) } /* TODO : handle test and testany simcalls */ - mc_call_type call = MC_CALL_TYPE_NONE; - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { + 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); - } - - SIMIX_simcall_handle(req, value); - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - MC_SET_MC_HEAP; - mc_update_comm_pattern(call, req, value, communications_pattern); - MC_SET_STD_HEAP; - } + 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_SET_STD_HEAP; + MC_wait_for_requests(); count++; - - if (mc_reduce_kind == e_mc_reduce_dpor) { - MC_SET_MC_HEAP; - /* Insert in dict all enabled processes */ - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_process_is_enabled(process) ) { - char *key = bprintf("%lu", process->pid); - if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) { - char *data = bprintf("%d", count); - xbt_dict_set(first_enabled_state, key, data, NULL); - } - xbt_free(key); - } - } - MC_SET_STD_HEAP; - } } /* Update statistics */ @@ -491,16 +527,31 @@ void MC_replay(xbt_fifo_t stack, int start) mmalloc_set_current_heap(heap); } -void MC_replay_liveness(xbt_fifo_t stack, int all_stack) +void MC_replay_liveness(xbt_fifo_t stack) { initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap); xbt_fifo_item_t item; - int depth = 1; + mc_pair_t pair = NULL; + mc_state_t state = NULL; + smx_simcall_t req = NULL, saved_req = NULL; + int value, depth = 1; + char *req_str; XBT_DEBUG("**** Begin Replay ****"); + /* Intermediate backtracking */ + 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 */ MC_restore_snapshot(initial_global_state->snapshot); @@ -511,26 +562,22 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) /* Traverse the stack from the initial state and re-execute the transitions */ for (item = xbt_fifo_get_last_item(stack); - all_stack ? depth <= xbt_fifo_size(stack) : item != xbt_fifo_get_first_item(stack); + item != xbt_fifo_get_first_item(stack); item = xbt_fifo_get_prev_item(item)) { - mc_pair_t pair = (mc_pair_t) xbt_fifo_get_item_content(item); + pair = (mc_pair_t) xbt_fifo_get_item_content(item); - mc_state_t state = (mc_state_t) pair->graph_state; - smx_simcall_t req = NULL, saved_req = NULL; - int value; - char *req_str; + state = (mc_state_t) pair->graph_state; - if (pair->requests > 0) { + if (pair->exploration_started) { saved_req = MC_state_get_executed_request(state, &value); - //XBT_DEBUG("SavedReq->call %u", saved_req->call); 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; - //XBT_DEBUG("Req->call %u", req->call); + 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)) { @@ -541,7 +588,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) } - SIMIX_simcall_handle(req, value); + MC_simcall_handle(req, value); MC_wait_for_requests(); } @@ -550,7 +597,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) mc_stats->executed_transitions++; depth++; - + } XBT_DEBUG("**** End Replay ****"); @@ -572,18 +619,12 @@ void MC_dump_stack_safety(xbt_fifo_t stack) xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); MC_show_stack_safety(stack); - - if (!_sg_mc_checkpoint) { - - mc_state_t state; - - MC_SET_MC_HEAP; - while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) - MC_state_delete(state); - MC_SET_STD_HEAP; - - } - + + mc_state_t state; + + MC_SET_MC_HEAP; + while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) + MC_state_delete(state, !state->in_visited_states ? 1 : 0); mmalloc_set_current_heap(heap); } @@ -627,6 +668,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) { @@ -637,21 +687,18 @@ void MC_show_stack_liveness(xbt_fifo_t stack) char *req_str = NULL; for (item = xbt_fifo_get_last_item(stack); - (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item))) - : (NULL)); item = xbt_fifo_get_prev_item(item)) { + (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item))) : (NULL)); + item = xbt_fifo_get_prev_item(item)) { req = MC_state_get_executed_request(pair->graph_state, &value); - if (req) { - if (pair->requests > 0) { - req_str = MC_request_to_string(req, value); - XBT_INFO("%s", req_str); - xbt_free(req_str); - } else { - XBT_INFO("End of system requests but evolution in Büchi automaton"); - } + if (req && req->call != SIMCALL_NONE) { + req_str = MC_request_to_string(req, value); + XBT_INFO("%s", req_str); + xbt_free(req_str); } } } + void MC_dump_stack_liveness(xbt_fifo_t stack) { xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); @@ -661,9 +708,22 @@ void MC_dump_stack_liveness(xbt_fifo_t stack) mmalloc_set_current_heap(heap); } - void MC_print_statistics(mc_stats_t stats) { + 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); XBT_INFO("Visited states = %lu", stats->visited_states); @@ -677,13 +737,10 @@ void MC_print_statistics(mc_stats_t stats) 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(heap); }