X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e47b3e4c9b5ea0bd18d8c088320844200e4ff07e..e0300cbd373040c590de77e64cc6c6e5fc3c28bb:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 56ad792d39..c867495992 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -116,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); @@ -139,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", "*"); @@ -182,13 +190,14 @@ void MC_init_pid(pid_t pid, int socket) /* Those requests are handled on the client side and propagated by message * to the server: */ - MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); + 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)); } } + } mmalloc_set_current_heap(heap); @@ -220,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(); @@ -289,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) @@ -354,7 +370,7 @@ void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int valu 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: @@ -364,55 +380,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; + 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. @@ -432,7 +408,7 @@ void MC_replay(xbt_fifo_t stack) XBT_DEBUG("**** Begin Replay ****"); /* Intermediate backtracking */ - if(_sg_mc_checkpoint > 0) { + 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){ @@ -456,7 +432,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; } @@ -654,6 +630,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) { @@ -685,9 +670,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); @@ -701,11 +699,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); }