From 3fe1dfd358798ef005607b3118f36adb914375d2 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 20 Jun 2012 13:23:32 +0200 Subject: [PATCH] model-checker : cosmetics reindent --- src/mc/mc_checkpoint.c | 28 +- src/mc/mc_dpor.c | 50 +- src/mc/mc_global.c | 109 ++--- src/mc/mc_liveness.c | 884 ++++++++++++++++++------------------ src/mc/mc_request.c | 278 ++++++------ src/xbt/mmalloc/mm_module.c | 106 ++--- src/xbt/mmalloc/mmorecore.c | 12 +- src/xbt/mmalloc/mmprivate.h | 4 +- src/xbt/mmalloc/mrealloc.c | 8 +- 9 files changed, 741 insertions(+), 738 deletions(-) diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 145af27525..31927b84b5 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -42,15 +42,15 @@ static void MC_region_restore(mc_mem_region_t reg) while(i < maps->mapsize){ r = maps->regions[i]; if (maps->regions[i].pathname != NULL){ - if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){ - size_t diff = (char*)reg->start_addr - (char*)r.start_addr; - void *segment = malloc(reg->size + diff); - XBT_DEBUG("Size of segment : %zu", sizeof(segment)); - memcpy((char *)segment + diff, reg->data, reg->size); - memcpy(r.start_addr, segment, sizeof(segment)); - XBT_DEBUG("Memcpy region ok"); - break; - } + if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){ + size_t diff = (char*)reg->start_addr - (char*)r.start_addr; + void *segment = malloc(reg->size + diff); + XBT_DEBUG("Size of segment : %zu", sizeof(segment)); + memcpy((char *)segment + diff, reg->data, reg->size); + memcpy(r.start_addr, segment, sizeof(segment)); + XBT_DEBUG("Memcpy region ok"); + break; + } } i++; } @@ -134,16 +134,16 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot) if ((reg.prot & PROT_WRITE)){ if (maps->regions[i].pathname == NULL){ if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one) - MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); + MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } } else { if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){ MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } else { - if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){ - MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); - } - } + if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){ + MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); + } + } } } i++; diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index d45cf363ab..6b737a444e 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -39,8 +39,8 @@ void MC_dpor_init() MC_UNSET_RAW_MEM; /* FIXME: Update Statistics - mc_stats->state_size += - xbt_setset_set_size(initial_state->enabled_transitions); */ + mc_stats->state_size += + xbt_setset_set_size(initial_state->enabled_transitions); */ } @@ -65,8 +65,8 @@ void MC_dpor(void) XBT_DEBUG("**************************************************"); XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)", - xbt_fifo_size(mc_stack_safety_stateless), state, - MC_state_interleave_size(state)); + xbt_fifo_size(mc_stack_safety_stateless), state, + MC_state_interleave_size(state)); /* Update statistics */ mc_stats->visited_states++; @@ -107,8 +107,8 @@ void MC_dpor(void) MC_UNSET_RAW_MEM; /* FIXME: Update Statistics - mc_stats->state_size += - xbt_setset_set_size(next_state->enabled_transitions);*/ + mc_stats->state_size += + xbt_setset_set_size(next_state->enabled_transitions);*/ /* Let's loop again */ @@ -258,10 +258,10 @@ void MC_dpor_stateful(){ /* Debug information */ if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req, value); - //XBT_INFO("Visited states = %lu",mc_stats->visited_states ); - XBT_DEBUG("Execute: %s",req_str); - xbt_free(req_str); + req_str = MC_request_to_string(req, value); + //XBT_INFO("Visited states = %lu",mc_stats->visited_states ); + XBT_DEBUG("Execute: %s",req_str); + xbt_free(req_str); } MC_state_set_executed_request(current_state->graph_state, req, value); @@ -280,10 +280,10 @@ void MC_dpor_stateful(){ /* Get an enabled process and insert it in the interleave set of the next graph_state */ xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(next_graph_state, process); - break; - } + if(MC_process_is_enabled(process)){ + MC_state_interleave_process(next_graph_state, process); + break; + } } next_snapshot = xbt_new0(s_mc_snapshot_t, 1); @@ -310,8 +310,8 @@ void MC_dpor_stateful(){ MC_SET_RAW_MEM; while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){ - req = MC_state_get_internal_request(current_state->graph_state); - xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) { + req = MC_state_get_internal_request(current_state->graph_state); + xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) { if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){ if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){ XBT_DEBUG("Dependent Transitions:"); @@ -328,21 +328,21 @@ void MC_dpor_stateful(){ if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){ MC_state_interleave_process(prev_state->graph_state, req->issuer); - } else { + } else { XBT_DEBUG("Process %p is in done set", req->issuer); - } + } break; } } - if(MC_state_interleave_size(current_state->graph_state)){ - MC_restore_snapshot(current_state->system_state); - xbt_fifo_unshift(mc_stack_safety_stateful, current_state); - XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful)); - MC_UNSET_RAW_MEM; - break; - } + if(MC_state_interleave_size(current_state->graph_state)){ + MC_restore_snapshot(current_state->system_state); + xbt_fifo_unshift(mc_stack_safety_stateful, current_state); + XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful)); + MC_UNSET_RAW_MEM; + break; + } } MC_UNSET_RAW_MEM; diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 62accca9ca..f55b44fe1f 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -80,7 +80,7 @@ void MC_init_safety_stateless(void) void MC_init_safety_stateful(void){ - /* Check if MC is already initialized */ + /* Check if MC is already initialized */ if (initial_snapshot) return; @@ -120,7 +120,7 @@ static void MC_init_liveness(xbt_automaton_t a){ XBT_DEBUG("Creating stack"); - /* Create exploration stack */ + /* Create exploration stack */ mc_stack_liveness = xbt_fifo_new(); MC_UNSET_RAW_MEM; @@ -190,7 +190,7 @@ void MC_wait_for_requests(void) xbt_dynar_foreach(simix_global->process_that_ran, iter, process) { req = &process->simcall; if (req->call != SIMCALL_NONE && !MC_request_is_visible(req)) - SIMIX_simcall_pre(req, 0); + SIMIX_simcall_pre(req, 0); } } } @@ -216,7 +216,7 @@ int MC_deadlock_check() * \brief Re-executes from the initial state all the transitions indicated by * a given model-checker stack. * \param stack The stack with the transitions to execute. -*/ + */ void MC_replay(xbt_fifo_t stack) { int value; @@ -293,26 +293,26 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) if(pair->requests > 0){ - saved_req = MC_state_get_executed_request(state, &value); - //XBT_DEBUG("SavedReq->call %u", saved_req->call); + 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); + 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); - /* Debug information */ - if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req, value); - XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); - xbt_free(req_str); - } + /* Debug information */ + if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ + req_str = MC_request_to_string(req, value); + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); + xbt_free(req_str); + } - } + } - SIMIX_simcall_pre(req, value); - MC_wait_for_requests(); + SIMIX_simcall_pre(req, value); + MC_wait_for_requests(); } depth++; @@ -327,34 +327,34 @@ 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); - item != xbt_fifo_get_first_item(stack); - item = xbt_fifo_get_prev_item(item)) { + item != xbt_fifo_get_first_item(stack); + item = xbt_fifo_get_prev_item(item)) { pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item); state = (mc_state_t) pair->graph_state; if(pair->requests > 0){ - saved_req = MC_state_get_executed_request(state, &value); - //XBT_DEBUG("SavedReq->call %u", saved_req->call); + 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); + 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); - /* Debug information */ - if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req, value); - XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); - xbt_free(req_str); - } + /* Debug information */ + if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ + req_str = MC_request_to_string(req, value); + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); + xbt_free(req_str); + } - } + } - SIMIX_simcall_pre(req, value); - MC_wait_for_requests(); + SIMIX_simcall_pre(req, value); + MC_wait_for_requests(); } depth++; @@ -372,7 +372,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) * \brief Dumps the contents of a model-checker's stack and shows the actual * execution trace * \param stack The stack to dump -*/ + */ void MC_dump_stack_safety_stateless(xbt_fifo_t stack) { mc_state_t state; @@ -414,8 +414,8 @@ void MC_show_deadlock(smx_simcall_t req) XBT_INFO("**************************"); XBT_INFO("Locked request:"); /*req_str = MC_request_to_string(req); - XBT_INFO("%s", req_str); - xbt_free(req_str);*/ + XBT_INFO("%s", req_str); + xbt_free(req_str);*/ XBT_INFO("Counter-example execution trace:"); MC_dump_stack_safety_stateless(mc_stack_safety_stateless); } @@ -428,8 +428,8 @@ void MC_show_deadlock_stateful(smx_simcall_t req) XBT_INFO("**************************"); XBT_INFO("Locked request:"); /*req_str = MC_request_to_string(req); - XBT_INFO("%s", req_str); - xbt_free(req_str);*/ + XBT_INFO("%s", req_str); + xbt_free(req_str);*/ XBT_INFO("Counter-example execution trace:"); MC_show_stack_safety_stateful(mc_stack_safety_stateful); } @@ -441,7 +441,7 @@ void MC_dump_stack_safety_stateful(xbt_fifo_t stack) MC_show_stack_safety_stateful(stack); /*MC_SET_RAW_MEM; - while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) + while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) MC_state_delete(state); MC_UNSET_RAW_MEM;*/ } @@ -481,11 +481,11 @@ void MC_show_stack_liveness(xbt_fifo_t stack){ 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); + 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"); + XBT_INFO("End of system requests but evolution in Büchi automaton"); } } } @@ -508,9 +508,9 @@ void MC_print_statistics(mc_stats_t stats) XBT_INFO("Visited states = %lu", stats->visited_states); XBT_INFO("Executed transitions = %lu", stats->executed_transitions); XBT_INFO("Expanded / Visited = %lf", - (double) stats->visited_states / stats->expanded_states); + (double) stats->visited_states / stats->expanded_states); /*XBT_INFO("Exploration coverage = %lf", - (double)stats->expanded_states / stats->state_size); */ + (double)stats->expanded_states / stats->state_size); */ } void MC_print_statistics_pairs(mc_stats_pair_t stats) @@ -519,9 +519,9 @@ void MC_print_statistics_pairs(mc_stats_pair_t stats) XBT_INFO("Visited pairs = %lu", stats->visited_pairs); //XBT_INFO("Executed transitions = %lu", stats->executed_transitions); XBT_INFO("Expanded / Visited = %lf", - (double) stats->visited_pairs / stats->expanded_pairs); + (double) stats->visited_pairs / stats->expanded_pairs); /*XBT_INFO("Exploration coverage = %lf", - (double)stats->expanded_states / stats->state_size); */ + (double)stats->expanded_states / stats->state_size); */ } void MC_assert(int prop) @@ -610,5 +610,8 @@ void MC_diff(void){ } xbt_automaton_t MC_create_automaton(const char *file){ - return xbt_create_automaton(file); + MC_SET_RAW_MEM; + xbt_automaton_t a = xbt_create_automaton(file); + MC_UNSET_RAW_MEM; + return a; } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index b7ad897661..a49dbfbedc 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -79,51 +79,51 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ for(i=0 ; i< s1->num_reg ; i++){ if(s1->regions[i]->type != s2->regions[i]->type){ - XBT_INFO("Different type of region"); - errors++; + XBT_INFO("Different type of region"); + errors++; } switch(s1->regions[i]->type){ - case 0: + case 0: if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; + XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; + XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){ - XBT_INFO("Different heap (mmalloc_compare)"); - errors++; + XBT_INFO("Different heap (mmalloc_compare)"); + errors++; } break; case 1 : if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; + XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; + XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - XBT_INFO("Different memcmp for data in libsimgrid"); - errors++; + XBT_INFO("Different memcmp for data in libsimgrid"); + errors++; } break; case 2 : if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; + XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; + XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - XBT_INFO("Different memcmp for data in program"); - errors++; + XBT_INFO("Different memcmp for data in program"); + errors++; } break; default: @@ -170,27 +170,27 @@ int reached(xbt_state_t st){ xbt_dynar_foreach(reached_pairs, cursor, pair_test){ XBT_INFO("Pair reached #%d", pair_test->nb); if(automaton_state_compare(pair_test->automaton_state, st) == 0){ - if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ - //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points)); - //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){ - //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){ - if(snapshot_compare(pair_test->system_state, sn) == 0){ + if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ + //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points)); + //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){ + //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){ + if(snapshot_compare(pair_test->system_state, sn) == 0){ - MC_free_snapshot(sn); - xbt_dynar_reset(prop_ato); - xbt_free(prop_ato); - MC_UNSET_RAW_MEM; - return 1; - } - /* } - }else{ - XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) ); - }*/ - }else{ - XBT_INFO("Different values of propositional symbols"); - } + MC_free_snapshot(sn); + xbt_dynar_reset(prop_ato); + xbt_free(prop_ato); + MC_UNSET_RAW_MEM; + return 1; + } + /* } + }else{ + XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) ); + }*/ + }else{ + XBT_INFO("Different values of propositional symbols"); + } }else{ - XBT_INFO("Different automaton state"); + XBT_INFO("Different automaton state"); } } @@ -205,162 +205,162 @@ int reached(xbt_state_t st){ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */ - xbt_dict_cursor_t cursor_dict = NULL; - char *key; - char *data; - smx_rdv_t rdv1, rdv2; - xbt_fifo_item_t item1, item2; - smx_action_t action1, action2; - xbt_fifo_item_t item_req1, item_req2; - smx_simcall_t req1, req2; - int i=0; - int j=0; - - xbt_dict_foreach(d1, cursor_dict, key, data){ - rdv1 = (smx_rdv_t)data; - rdv2 = xbt_dict_get_or_null(d2, rdv1->name); - if(rdv2 == NULL){ - XBT_INFO("Rdv point unknown"); - return 1; - }else{ - if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){ - XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) ); - return 1; - }else{ + xbt_dict_cursor_t cursor_dict = NULL; + char *key; + char *data; + smx_rdv_t rdv1, rdv2; + xbt_fifo_item_t item1, item2; + smx_action_t action1, action2; + xbt_fifo_item_t item_req1, item_req2; + smx_simcall_t req1, req2; + int i=0; + int j=0; + + xbt_dict_foreach(d1, cursor_dict, key, data){ + rdv1 = (smx_rdv_t)data; + rdv2 = xbt_dict_get_or_null(d2, rdv1->name); + if(rdv2 == NULL){ + XBT_INFO("Rdv point unknown"); + return 1; + }else{ + if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){ + XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) ); + return 1; + }else{ - XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); + XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); - item1 = xbt_fifo_get_first_item(rdv1->comm_fifo); - item2 = xbt_fifo_get_first_item(rdv2->comm_fifo); + item1 = xbt_fifo_get_first_item(rdv1->comm_fifo); + item2 = xbt_fifo_get_first_item(rdv2->comm_fifo); - while(icomm_fifo)){ - action1 = (smx_action_t) xbt_fifo_get_item_content(item1); - action2 = (smx_action_t) xbt_fifo_get_item_content(item2); + while(icomm_fifo)){ + action1 = (smx_action_t) xbt_fifo_get_item_content(item1); + action2 = (smx_action_t) xbt_fifo_get_item_content(item2); - if(action1->type != action2->type){ - XBT_INFO("Different type of action"); - return 1; - } + if(action1->type != action2->type){ + XBT_INFO("Different type of action"); + return 1; + } - if(action1->state != action2->state){ - XBT_INFO("Different state of action"); - return 1; - } + if(action1->state != action2->state){ + XBT_INFO("Different state of action"); + return 1; + } - if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){ - XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls)); - return 1; - }else{ + if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){ + XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls)); + return 1; + }else{ - item_req1 = xbt_fifo_get_first_item(action1->simcalls); - item_req2 = xbt_fifo_get_first_item(action2->simcalls); + item_req1 = xbt_fifo_get_first_item(action1->simcalls); + item_req2 = xbt_fifo_get_first_item(action2->simcalls); - while(jsimcalls)){ + while(jsimcalls)){ - req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1); - req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2); + req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1); + req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2); - if(req1->call != req2->call){ - XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call); - return 1; - } - if(req1->issuer->pid != req2->issuer->pid){ - XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid); - return 1; - } - - item_req1 = xbt_fifo_get_next_item(item_req1); - item_req2 = xbt_fifo_get_next_item(item_req2); - j++; + if(req1->call != req2->call){ + XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call); + return 1; + } + if(req1->issuer->pid != req2->issuer->pid){ + XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid); + return 1; + } + + item_req1 = xbt_fifo_get_next_item(item_req1); + item_req2 = xbt_fifo_get_next_item(item_req2); + j++; - } - } - - switch(action1->type){ - case 0: /* execution */ - case 1: /* parallel execution */ - if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0) - return 1; - break; - case 2: /* comm */ - if(action1->comm.type != action2->comm.type) - return 1; - //XBT_INFO("Type of comm : %d", action1->comm.type); + } + } + + switch(action1->type){ + case 0: /* execution */ + case 1: /* parallel execution */ + if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0) + return 1; + break; + case 2: /* comm */ + if(action1->comm.type != action2->comm.type) + return 1; + //XBT_INFO("Type of comm : %d", action1->comm.type); - switch(action1->comm.type){ - case 0: /* SEND */ - if(action1->comm.src_proc->pid != action2->comm.src_proc->pid) - return 1; - if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0) - return 1; - break; - case 1: /* RECEIVE */ - if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid) - return 1; - if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0) - return 1; - break; - case 2: /* READY */ - if(action1->comm.src_proc->pid != action2->comm.src_proc->pid) - return 1; - if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0) - return 1; - if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid) - return 1; - if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0) - return 1; - break; - case 3: /* DONE */ - if(action1->comm.src_proc->pid != action2->comm.src_proc->pid) - return 1; - if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0) - return 1; - if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid) - return 1; - if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0) - return 1; - break; + switch(action1->comm.type){ + case 0: /* SEND */ + if(action1->comm.src_proc->pid != action2->comm.src_proc->pid) + return 1; + if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0) + return 1; + break; + case 1: /* RECEIVE */ + if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid) + return 1; + if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0) + return 1; + break; + case 2: /* READY */ + if(action1->comm.src_proc->pid != action2->comm.src_proc->pid) + return 1; + if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0) + return 1; + if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid) + return 1; + if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0) + return 1; + break; + case 3: /* DONE */ + if(action1->comm.src_proc->pid != action2->comm.src_proc->pid) + return 1; + if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0) + return 1; + if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid) + return 1; + if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0) + return 1; + break; - } /* end of switch on type of comm */ + } /* end of switch on type of comm */ - if(action1->comm.refcount != action2->comm.refcount) - return 1; - if(action1->comm.detached != action2->comm.detached) - return 1; - if(action1->comm.rate != action2->comm.rate) - return 1; - if(action1->comm.task_size != action2->comm.task_size) - return 1; - if(action1->comm.src_buff != action2->comm.src_buff) - return 1; - if(action1->comm.dst_buff != action2->comm.dst_buff) - return 1; - if(action1->comm.src_data != action2->comm.src_data) - return 1; - if(action1->comm.dst_data != action2->comm.dst_data) - return 1; + if(action1->comm.refcount != action2->comm.refcount) + return 1; + if(action1->comm.detached != action2->comm.detached) + return 1; + if(action1->comm.rate != action2->comm.rate) + return 1; + if(action1->comm.task_size != action2->comm.task_size) + return 1; + if(action1->comm.src_buff != action2->comm.src_buff) + return 1; + if(action1->comm.dst_buff != action2->comm.dst_buff) + return 1; + if(action1->comm.src_data != action2->comm.src_data) + return 1; + if(action1->comm.dst_data != action2->comm.dst_data) + return 1; - break; - case 3: /* sleep */ - if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0) - return 1; - break; - case 4: /* synchro */ + break; + case 3: /* sleep */ + if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0) + return 1; + break; + case 4: /* synchro */ - break; - default: - break; - } - - item1 = xbt_fifo_get_next_item(item1); - item2 = xbt_fifo_get_next_item(item2); - i++; - } - } - } - } - - return 0; + break; + default: + break; + } + + item1 = xbt_fifo_get_next_item(item1); + item2 = xbt_fifo_get_next_item(item2); + i++; + } + } + } + } + + return 0; } @@ -392,23 +392,23 @@ void set_pair_reached(xbt_state_t st){ /*xbt_dict_t rdv_points = SIMIX_get_rdv_points(); - xbt_dict_cursor_t cursor_dict = NULL; - char *key; - char *data; - xbt_fifo_item_t item; - smx_action_t action; + xbt_dict_cursor_t cursor_dict = NULL; + char *key; + char *data; + xbt_fifo_item_t item; + smx_action_t action; - xbt_dict_foreach(rdv_points, cursor_dict, key, data){ + xbt_dict_foreach(rdv_points, cursor_dict, key, data){ smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1); new_rdv->name = strdup(((smx_rdv_t)data)->name); new_rdv->comm_fifo = xbt_fifo_new(); xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) { - smx_action_t a = xbt_new0(s_smx_action_t, 1); - memcpy(a, action, sizeof(s_smx_action_t)); - xbt_fifo_push(new_rdv->comm_fifo, a); - XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key); - if(action->type==2) - XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount); + smx_action_t a = xbt_new0(s_smx_action_t, 1); + memcpy(a, action, sizeof(s_smx_action_t)); + xbt_fifo_push(new_rdv->comm_fifo, a); + XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key); + if(action->type==2) + XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount); } //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo); xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL); @@ -464,26 +464,26 @@ int reached_hash(xbt_state_t st){ xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){ if(automaton_state_compare(pair_test->automaton_state, st) == 0){ - if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ - for(j=0 ; j< sn->num_reg ; j++){ - if(hash_regions[j] != pair_test->hash_regions[j]){ - region_diff++; - } - } - if(region_diff == 0){ - MC_free_snapshot(sn); - xbt_dynar_reset(prop_ato); - xbt_free(prop_ato); - MC_UNSET_RAW_MEM; - return 1; - }else{ - XBT_INFO("Different snapshot"); - } - }else{ - XBT_INFO("Different values of propositional symbols"); - } + if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ + for(j=0 ; j< sn->num_reg ; j++){ + if(hash_regions[j] != pair_test->hash_regions[j]){ + region_diff++; + } + } + if(region_diff == 0){ + MC_free_snapshot(sn); + xbt_dynar_reset(prop_ato); + xbt_free(prop_ato); + MC_UNSET_RAW_MEM; + return 1; + }else{ + XBT_INFO("Different snapshot"); + } + }else{ + XBT_INFO("Different values of propositional symbols"); + } }else{ - XBT_INFO("Different automaton state"); + XBT_INFO("Different automaton state"); } region_diff = 0; @@ -571,28 +571,28 @@ int visited(xbt_state_t st, int sc){ xbt_dynar_foreach(visited_pairs, cursor, pair_test){ if(pair_test->search_cycle == sc) { - if(automaton_state_compare(pair_test->automaton_state, st) == 0){ - if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ - if(snapshot_compare(pair_test->system_state, sn) == 0){ + if(automaton_state_compare(pair_test->automaton_state, st) == 0){ + if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ + if(snapshot_compare(pair_test->system_state, sn) == 0){ - MC_free_snapshot(sn); - xbt_dynar_reset(prop_ato); - xbt_free(prop_ato); - MC_UNSET_RAW_MEM; + MC_free_snapshot(sn); + xbt_dynar_reset(prop_ato); + xbt_free(prop_ato); + MC_UNSET_RAW_MEM; - return 1; + return 1; + }else{ + XBT_INFO("Different snapshot"); + } + }else{ + XBT_INFO("Different values of propositional symbols"); + } + }else{ + XBT_INFO("Different automaton state"); + } }else{ - XBT_INFO("Different snapshot"); - } - }else{ - XBT_INFO("Different values of propositional symbols"); - } - }else{ - XBT_INFO("Different automaton state"); - } - }else{ - XBT_INFO("Different value of search_cycle"); + XBT_INFO("Different value of search_cycle"); } } @@ -649,30 +649,30 @@ int visited_hash(xbt_state_t st, int sc){ xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){ if(pair_test->search_cycle == sc) { - if(automaton_state_compare(pair_test->automaton_state, st) == 0){ - if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ - for(j=0 ; j< sn->num_reg ; j++){ - if(hash_regions[j] != pair_test->hash_regions[j]){ - region_diff++; + if(automaton_state_compare(pair_test->automaton_state, st) == 0){ + if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ + for(j=0 ; j< sn->num_reg ; j++){ + if(hash_regions[j] != pair_test->hash_regions[j]){ + region_diff++; + } + } + if(region_diff == 0){ + MC_free_snapshot(sn); + xbt_dynar_reset(prop_ato); + xbt_free(prop_ato); + MC_UNSET_RAW_MEM; + return 1; + }else{ + //XBT_INFO("Different snapshot"); + } + }else{ + //XBT_INFO("Different values of propositional symbols"); + } + }else{ + //XBT_INFO("Different automaton state"); } - } - if(region_diff == 0){ - MC_free_snapshot(sn); - xbt_dynar_reset(prop_ato); - xbt_free(prop_ato); - MC_UNSET_RAW_MEM; - return 1; }else{ - //XBT_INFO("Different snapshot"); - } - }else{ - //XBT_INFO("Different values of propositional symbols"); - } - }else{ - //XBT_INFO("Different automaton state"); - } - }else{ - //XBT_INFO("Different value of search_cycle"); + //XBT_INFO("Different value of search_cycle"); } region_diff = 0; @@ -791,8 +791,8 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){ int_f_void_t f; xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){ if(strcmp(p->pred, l->u.predicat) == 0){ - f = (int_f_void_t)p->function; - return (*f)(); + f = (int_f_void_t)p->function; + return (*f)(); } } return -1; @@ -870,8 +870,8 @@ void MC_ddfs_init(void){ MC_UNSET_RAW_MEM; if(cursor != 0){ - MC_restore_snapshot(initial_snapshot_liveness); - MC_UNSET_RAW_MEM; + MC_restore_snapshot(initial_snapshot_liveness); + MC_UNSET_RAW_MEM; } MC_ddfs(0); @@ -879,20 +879,20 @@ void MC_ddfs_init(void){ }else{ if(state->type == 2){ - MC_SET_RAW_MEM; - mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state)); - xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state)); + xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair); + MC_UNSET_RAW_MEM; - set_pair_reached(state); - //set_pair_reached_hash(state); + set_pair_reached(state); + //set_pair_reached_hash(state); - if(cursor != 0){ - MC_restore_snapshot(initial_snapshot_liveness); - MC_UNSET_RAW_MEM; - } + if(cursor != 0){ + MC_restore_snapshot(initial_snapshot_liveness); + MC_UNSET_RAW_MEM; + } - MC_ddfs(1); + MC_ddfs(1); } } @@ -948,171 +948,171 @@ void MC_ddfs(int search_cycle){ while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ - /* Debug information */ + /* Debug information */ - req_str = MC_request_to_string(req, value); - XBT_INFO("Execute: %s", req_str); - xbt_free(req_str); + req_str = MC_request_to_string(req, value); + XBT_INFO("Execute: %s", req_str); + xbt_free(req_str); - MC_state_set_executed_request(current_pair->graph_state, req, value); + MC_state_set_executed_request(current_pair->graph_state, req, value); - /* Answer the request */ - SIMIX_simcall_pre(req, value); + /* Answer the request */ + SIMIX_simcall_pre(req, value); - /* Wait for requests (schedules processes) */ - MC_wait_for_requests(); + /* Wait for requests (schedules processes) */ + MC_wait_for_requests(); - MC_SET_RAW_MEM; + MC_SET_RAW_MEM; - /* Create the new expanded graph_state */ - next_graph_state = MC_state_pair_new(); + /* Create the new expanded graph_state */ + next_graph_state = MC_state_pair_new(); - /* Get enabled process and insert it in the interleave set of the next graph_state */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(next_graph_state, process); - } - } + /* Get enabled process and insert it in the interleave set of the next graph_state */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + MC_state_interleave_process(next_graph_state, process); + } + } - xbt_dynar_reset(successors); + xbt_dynar_reset(successors); - MC_UNSET_RAW_MEM; + MC_UNSET_RAW_MEM; - cursor= 0; - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ + cursor= 0; + xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label); - if(res == 1){ // enabled transition in automaton - MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - } + if(res == 1){ // enabled transition in automaton + MC_SET_RAW_MEM; + next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); + xbt_dynar_push(successors, &next_pair); + MC_UNSET_RAW_MEM; + } - } + } - cursor = 0; + cursor = 0; - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ + xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label); - if(res == 2){ // true transition in automaton - MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - } + if(res == 2){ // true transition in automaton + MC_SET_RAW_MEM; + next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); + xbt_dynar_push(successors, &next_pair); + MC_UNSET_RAW_MEM; + } - } + } - cursor = 0; + cursor = 0; - xbt_dynar_foreach(successors, cursor, pair_succ){ + xbt_dynar_foreach(successors, cursor, pair_succ){ - if(search_cycle == 1){ + if(search_cycle == 1){ - if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ + if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(reached(pair_succ->automaton_state)){ - //if(reached_hash(pair_succ->automaton_state)){ + if(reached(pair_succ->automaton_state)){ + //if(reached_hash(pair_succ->automaton_state)){ - XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state)); + XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state)); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness(mc_stack_liveness); - MC_dump_stack_liveness(mc_stack_liveness); - MC_print_statistics_pairs(mc_stats_pair); - exit(0); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_show_stack_liveness(mc_stack_liveness); + MC_dump_stack_liveness(mc_stack_liveness); + MC_print_statistics_pairs(mc_stats_pair); + exit(0); - }else{ + }else{ - XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(pair_succ->automaton_state); - //set_pair_reached_hash(pair_succ->automaton_state); + set_pair_reached(pair_succ->automaton_state); + //set_pair_reached_hash(pair_succ->automaton_state); - XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); - } + } - }else{ + }else{ - if(!visited_hash(pair_succ->automaton_state, search_cycle)){ - //if(!visited(pair_succ->automaton_state, search_cycle)){ + if(!visited_hash(pair_succ->automaton_state, search_cycle)){ + //if(!visited(pair_succ->automaton_state, search_cycle)){ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); - }else{ + }else{ - XBT_INFO("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); - } + } - } + } - }else{ + }else{ - if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ + if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(pair_succ->automaton_state); - //set_pair_reached_hash(pair_succ->automaton_state); + set_pair_reached(pair_succ->automaton_state); + //set_pair_reached_hash(pair_succ->automaton_state); - search_cycle = 1; + search_cycle = 1; - XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); - } + } - if(!visited_hash(pair_succ->automaton_state, search_cycle)){ - //if(!visited(pair_succ->automaton_state, search_cycle)){ + if(!visited_hash(pair_succ->automaton_state, search_cycle)){ + //if(!visited(pair_succ->automaton_state, search_cycle)){ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); - }else{ + }else{ - XBT_INFO("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); - } + } - } + } - /* Restore system before checking others successors */ - if(cursor != (xbt_dynar_length(successors) - 1)) - MC_replay_liveness(mc_stack_liveness, 1); + /* Restore system before checking others successors */ + if(cursor != (xbt_dynar_length(successors) - 1)) + MC_replay_liveness(mc_stack_liveness, 1); - } + } - if(MC_state_interleave_size(current_pair->graph_state) > 0){ - XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness)); - MC_replay_liveness(mc_stack_liveness, 0); - } + if(MC_state_interleave_size(current_pair->graph_state) > 0){ + XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness)); + MC_replay_liveness(mc_stack_liveness, 0); + } } @@ -1131,14 +1131,14 @@ void MC_ddfs(int search_cycle){ cursor= 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label); - if(res == 1){ // enabled transition in automaton - MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - } + if(res == 1){ // enabled transition in automaton + MC_SET_RAW_MEM; + next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); + xbt_dynar_push(successors, &next_pair); + MC_UNSET_RAW_MEM; + } } @@ -1146,14 +1146,14 @@ void MC_ddfs(int search_cycle){ xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label); - if(res == 2){ // true transition in automaton - MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - } + if(res == 2){ // true transition in automaton + MC_SET_RAW_MEM; + next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); + xbt_dynar_push(successors, &next_pair); + MC_UNSET_RAW_MEM; + } } @@ -1161,95 +1161,95 @@ void MC_ddfs(int search_cycle){ xbt_dynar_foreach(successors, cursor, pair_succ){ - if(search_cycle == 1){ + if(search_cycle == 1){ - if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ + if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(reached(pair_succ->automaton_state)){ - //if(reached_hash(pair_succ->automaton_state)){ + if(reached(pair_succ->automaton_state)){ + //if(reached_hash(pair_succ->automaton_state)){ - XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); + XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness(mc_stack_liveness); - MC_dump_stack_liveness(mc_stack_liveness); - MC_print_statistics_pairs(mc_stats_pair); - exit(0); - - }else{ - - XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_show_stack_liveness(mc_stack_liveness); + MC_dump_stack_liveness(mc_stack_liveness); + MC_print_statistics_pairs(mc_stats_pair); + exit(0); + + }else{ + + XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(pair_succ->automaton_state); - //set_pair_reached_hash(pair_succ->automaton_state); + set_pair_reached(pair_succ->automaton_state); + //set_pair_reached_hash(pair_succ->automaton_state); - XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); - } + } - }else{ + }else{ - if(!visited_hash(pair_succ->automaton_state, search_cycle)){ - //if(!visited(pair_succ->automaton_state, search_cycle)){ + if(!visited_hash(pair_succ->automaton_state, search_cycle)){ + //if(!visited(pair_succ->automaton_state, search_cycle)){ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); - }else{ + }else{ - XBT_INFO("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); - } - } + } + } - }else{ + }else{ - if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ + if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - set_pair_reached(pair_succ->automaton_state); - //set_pair_reached_hash(pair_succ->automaton_state); + set_pair_reached(pair_succ->automaton_state); + //set_pair_reached_hash(pair_succ->automaton_state); - search_cycle = 1; + search_cycle = 1; - XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); - } + } - if(!visited_hash(pair_succ->automaton_state, search_cycle)){ - //if(!visited(pair_succ->automaton_state, search_cycle)){ + if(!visited_hash(pair_succ->automaton_state, search_cycle)){ + //if(!visited(pair_succ->automaton_state, search_cycle)){ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); - }else{ + }else{ - XBT_INFO("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); - } + } - } + } - /* Restore system before checking others successors */ - if(cursor != xbt_dynar_length(successors) - 1) - MC_replay_liveness(mc_stack_liveness, 1); + /* Restore system before checking others successors */ + if(cursor != xbt_dynar_length(successors) - 1) + MC_replay_liveness(mc_stack_liveness, 1); } diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 9a5f74aa40..3d89d84e47 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -27,7 +27,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) return FALSE; if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) - && r2->call == SIMCALL_COMM_WAIT){ + && r2->call == SIMCALL_COMM_WAIT){ if(r2->comm_wait.comm->comm.rdv == NULL) return FALSE; @@ -45,7 +45,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) } if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV) - && r1->call == SIMCALL_COMM_WAIT){ + && r1->call == SIMCALL_COMM_WAIT){ if(r1->comm_wait.comm->comm.rdv != NULL) return FALSE; @@ -66,22 +66,22 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) * isend/irecv call is not stored in a buffer used in the * test call. */ if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) - && r2->call == SIMCALL_COMM_TEST) + && r2->call == SIMCALL_COMM_TEST) return FALSE; /* FIXME: the following rule assumes that the result of the * isend/irecv call is not stored in a buffer used in the * test call.*/ if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV) - && r1->call == SIMCALL_COMM_TEST) + && r1->call == SIMCALL_COMM_TEST) return FALSE; if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND - && r1->comm_isend.rdv != r2->comm_isend.rdv) + && r1->comm_isend.rdv != r2->comm_isend.rdv) return FALSE; if(r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_IRECV - && r1->comm_irecv.rdv != r2->comm_irecv.rdv) + && r1->comm_irecv.rdv != r2->comm_irecv.rdv) return FALSE; if(r1->call == SIMCALL_COMM_WAIT && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST) @@ -95,8 +95,8 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) return FALSE; if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT - && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff - && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff) + && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff + && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff) return FALSE; if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT @@ -110,46 +110,46 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) return FALSE; if(r1->call == SIMCALL_COMM_TEST && - (r1->comm_test.comm == NULL - || r1->comm_test.comm->comm.src_buff == NULL - || r1->comm_test.comm->comm.dst_buff == NULL)) + (r1->comm_test.comm == NULL + || r1->comm_test.comm->comm.src_buff == NULL + || r1->comm_test.comm->comm.dst_buff == NULL)) return FALSE; if(r2->call == SIMCALL_COMM_TEST && - (r2->comm_test.comm == NULL - || r2->comm_test.comm->comm.src_buff == NULL - || r2->comm_test.comm->comm.dst_buff == NULL)) + (r2->comm_test.comm == NULL + || r2->comm_test.comm->comm.src_buff == NULL + || r2->comm_test.comm->comm.dst_buff == NULL)) return FALSE; if(r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT - && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff - && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff) + && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff + && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff) return FALSE; if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST - && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff - && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff) + && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff + && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff) return FALSE; if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST - && r1->comm_wait.comm->comm.src_buff != NULL - && r1->comm_wait.comm->comm.dst_buff != NULL - && r2->comm_test.comm->comm.src_buff != NULL - && r2->comm_test.comm->comm.dst_buff != NULL - && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff - && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff - && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff) + && r1->comm_wait.comm->comm.src_buff != NULL + && r1->comm_wait.comm->comm.dst_buff != NULL + && r2->comm_test.comm->comm.src_buff != NULL + && r2->comm_test.comm->comm.dst_buff != NULL + && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff + && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff + && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff) return FALSE; if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT - && r1->comm_test.comm->comm.src_buff != NULL - && r1->comm_test.comm->comm.dst_buff != NULL - && r2->comm_wait.comm->comm.src_buff != NULL - && r2->comm_wait.comm->comm.dst_buff != NULL - && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff - && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff - && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff) - return FALSE; + && r1->comm_test.comm->comm.src_buff != NULL + && r1->comm_test.comm->comm.dst_buff != NULL + && r2->comm_wait.comm->comm.src_buff != NULL + && r2->comm_wait.comm->comm.dst_buff != NULL + && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff + && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff + && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff) + return FALSE; return TRUE; @@ -179,69 +179,69 @@ char *MC_request_to_string(smx_simcall_t req, int value) size_t size = 0; switch(req->call){ - case SIMCALL_COMM_ISEND: - type = xbt_strdup("iSend"); - p = pointer_to_string(req->comm_isend.src_buff); - bs = buff_size_to_string(req->comm_isend.src_buff_size); - args = bprintf("src=%s, buff=%s, size=%s", req->issuer->name, p, bs); - break; - case SIMCALL_COMM_IRECV: - size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0; - type = xbt_strdup("iRecv"); - p = pointer_to_string(req->comm_irecv.dst_buff); - bs = buff_size_to_string(size); - args = bprintf("dst=%s, buff=%s, size=%s", req->issuer->name, p, bs); - break; - case SIMCALL_COMM_WAIT: - act = req->comm_wait.comm; - if(value == -1){ - type = xbt_strdup("WaitTimeout"); - p = pointer_to_string(act); - args = bprintf("comm=%p", p); - }else{ - type = xbt_strdup("Wait"); - p = pointer_to_string(act); - args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p, - act->comm.src_proc ? act->comm.src_proc->pid : 0, - act->comm.src_proc ? act->comm.src_proc->name : "", - act->comm.dst_proc ? act->comm.dst_proc->pid : 0, - act->comm.dst_proc ? act->comm.dst_proc->name : ""); - } - break; - case SIMCALL_COMM_TEST: - act = req->comm_test.comm; - if(act->comm.src_proc == NULL || act->comm.dst_proc == NULL){ - type = xbt_strdup("Test FALSE"); - p = pointer_to_string(act); - args = bprintf("comm=%s", p); - }else{ - type = xbt_strdup("Test TRUE"); - p = pointer_to_string(act); - args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p, - act->comm.src_proc->pid, act->comm.src_proc->name, - act->comm.dst_proc->pid, act->comm.dst_proc->name); - } - break; - - case SIMCALL_COMM_WAITANY: - type = xbt_strdup("WaitAny"); - p = pointer_to_string(xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t)); - args = bprintf("comm=%s (%d of %lu)", p, - value+1, xbt_dynar_length(req->comm_waitany.comms)); - break; - - case SIMCALL_COMM_TESTANY: - if(value == -1){ - type = xbt_strdup("TestAny FALSE"); - args = xbt_strdup("-"); - }else{ - type = xbt_strdup("TestAny"); - args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms)); - } - break; - - default: - THROW_UNIMPLEMENTED; + case SIMCALL_COMM_ISEND: + type = xbt_strdup("iSend"); + p = pointer_to_string(req->comm_isend.src_buff); + bs = buff_size_to_string(req->comm_isend.src_buff_size); + args = bprintf("src=%s, buff=%s, size=%s", req->issuer->name, p, bs); + break; + case SIMCALL_COMM_IRECV: + size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0; + type = xbt_strdup("iRecv"); + p = pointer_to_string(req->comm_irecv.dst_buff); + bs = buff_size_to_string(size); + args = bprintf("dst=%s, buff=%s, size=%s", req->issuer->name, p, bs); + break; + case SIMCALL_COMM_WAIT: + act = req->comm_wait.comm; + if(value == -1){ + type = xbt_strdup("WaitTimeout"); + p = pointer_to_string(act); + args = bprintf("comm=%p", p); + }else{ + type = xbt_strdup("Wait"); + p = pointer_to_string(act); + args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p, + act->comm.src_proc ? act->comm.src_proc->pid : 0, + act->comm.src_proc ? act->comm.src_proc->name : "", + act->comm.dst_proc ? act->comm.dst_proc->pid : 0, + act->comm.dst_proc ? act->comm.dst_proc->name : ""); + } + break; + case SIMCALL_COMM_TEST: + act = req->comm_test.comm; + if(act->comm.src_proc == NULL || act->comm.dst_proc == NULL){ + type = xbt_strdup("Test FALSE"); + p = pointer_to_string(act); + args = bprintf("comm=%s", p); + }else{ + type = xbt_strdup("Test TRUE"); + p = pointer_to_string(act); + args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p, + act->comm.src_proc->pid, act->comm.src_proc->name, + act->comm.dst_proc->pid, act->comm.dst_proc->name); + } + break; + + case SIMCALL_COMM_WAITANY: + type = xbt_strdup("WaitAny"); + p = pointer_to_string(xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t)); + args = bprintf("comm=%s (%d of %lu)", p, + value+1, xbt_dynar_length(req->comm_waitany.comms)); + break; + + case SIMCALL_COMM_TESTANY: + if(value == -1){ + type = xbt_strdup("TestAny FALSE"); + args = xbt_strdup("-"); + }else{ + type = xbt_strdup("TestAny"); + args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms)); + } + break; + + default: + THROW_UNIMPLEMENTED; } str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args); @@ -268,11 +268,11 @@ unsigned int MC_request_testany_fail(smx_simcall_t req) int MC_request_is_visible(smx_simcall_t req) { return req->call == SIMCALL_COMM_ISEND - || req->call == SIMCALL_COMM_IRECV - || req->call == SIMCALL_COMM_WAIT - || req->call == SIMCALL_COMM_WAITANY - || req->call == SIMCALL_COMM_TEST - || req->call == SIMCALL_COMM_TESTANY; + || req->call == SIMCALL_COMM_IRECV + || req->call == SIMCALL_COMM_WAIT + || req->call == SIMCALL_COMM_WAITANY + || req->call == SIMCALL_COMM_TEST + || req->call == SIMCALL_COMM_TESTANY; } int MC_request_is_enabled(smx_simcall_t req) @@ -282,33 +282,33 @@ int MC_request_is_enabled(smx_simcall_t req) switch (req->call) { - case SIMCALL_COMM_WAIT: - /* FIXME: check also that src and dst processes are not suspended */ + case SIMCALL_COMM_WAIT: + /* FIXME: check also that src and dst processes are not suspended */ + + /* If it has a timeout it will be always be enabled, because even if the + * communication is not ready, it can timeout and won't block. + * On the other hand if it hasn't a timeout, check if the comm is ready.*/ + if(req->comm_wait.timeout >= 0){ + return TRUE; + }else{ + act = req->comm_wait.comm; + return (act->comm.src_proc && act->comm.dst_proc); + } + break; - /* If it has a timeout it will be always be enabled, because even if the - * communication is not ready, it can timeout and won't block. - * On the other hand if it hasn't a timeout, check if the comm is ready.*/ - if(req->comm_wait.timeout >= 0){ + case SIMCALL_COMM_WAITANY: + /* Check if it has at least one communication ready */ + xbt_dynar_foreach(req->comm_waitany.comms, index, act) { + if (act->comm.src_proc && act->comm.dst_proc){ return TRUE; - }else{ - act = req->comm_wait.comm; - return (act->comm.src_proc && act->comm.dst_proc); } - break; - - case SIMCALL_COMM_WAITANY: - /* Check if it has at least one communication ready */ - xbt_dynar_foreach(req->comm_waitany.comms, index, act) { - if (act->comm.src_proc && act->comm.dst_proc){ - return TRUE; - } - } - return FALSE; - break; + } + return FALSE; + break; - default: - /* The rest of the request are always enabled */ - return TRUE; + default: + /* The rest of the request are always enabled */ + return TRUE; } } @@ -318,24 +318,24 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) switch (req->call) { - case SIMCALL_COMM_WAIT: - /* FIXME: check also that src and dst processes are not suspended */ - act = req->comm_wait.comm; - return (act->comm.src_proc && act->comm.dst_proc); - break; + case SIMCALL_COMM_WAIT: + /* FIXME: check also that src and dst processes are not suspended */ + act = req->comm_wait.comm; + return (act->comm.src_proc && act->comm.dst_proc); + break; - case SIMCALL_COMM_WAITANY: - act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t); - return (act->comm.src_proc && act->comm.dst_proc); - break; + case SIMCALL_COMM_WAITANY: + act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t); + return (act->comm.src_proc && act->comm.dst_proc); + break; - case SIMCALL_COMM_TESTANY: - act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t); - return (act->comm.src_proc && act->comm.dst_proc); - break; + case SIMCALL_COMM_TESTANY: + act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t); + return (act->comm.src_proc && act->comm.dst_proc); + break; - default: - return TRUE; + default: + return TRUE; } } diff --git a/src/xbt/mmalloc/mm_module.c b/src/xbt/mmalloc/mm_module.c index b0b2d5d000..1272d4ddb5 100644 --- a/src/xbt/mmalloc/mm_module.c +++ b/src/xbt/mmalloc/mm_module.c @@ -3,22 +3,22 @@ Contributed by Fred Fish at Cygnus Support. fnf@cygnus.com -This file is part of the GNU C Library. + This file is part of the GNU C Library. -The GNU C Library is free software; you can redistribute it and/or -modify it under the terms of the GNU Library General Public License as -published by the Free Software Foundation; either version 2 of the -License, or (at your option) any later version. + The GNU C Library is free software; you can redistribute it and/or + modify it under the terms of the GNU Library General Public License as + published by the Free Software Foundation; either version 2 of the + License, or (at your option) any later version. -The GNU C Library is distributed in the hope that it will be useful, -but WITHOUT ANY WARRANTY; without even the implied warranty of -MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -Library General Public License for more details. + The GNU C Library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Library General Public License for more details. -You should have received a copy of the GNU Library General Public -License along with the GNU C Library; see the file COPYING.LIB. If -not, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330, -Boston, MA 02111-1307, USA. */ + You should have received a copy of the GNU Library General Public + License along with the GNU C Library; see the file COPYING.LIB. If + not, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330, + Boston, MA 02111-1307, USA. */ #include #include /* After sys/types.h, at least for dpx/2. */ @@ -84,56 +84,56 @@ xbt_mheap_t xbt_mheap_new(int fd, void *baseaddr) else if (sbuf.st_size > 0) { /* We were given an valid file descriptor on an open file, so try to remap - it into the current process at the same address to which it was previously - mapped. It naturally have to pass some sanity checks for that. + it into the current process at the same address to which it was previously + mapped. It naturally have to pass some sanity checks for that. - Note that we have to update the file descriptor number in the malloc- - descriptor read from the file to match the current valid one, before - trying to map the file in, and again after a successful mapping and - after we've switched over to using the mapped in malloc descriptor - rather than the temporary one on the stack. + Note that we have to update the file descriptor number in the malloc- + descriptor read from the file to match the current valid one, before + trying to map the file in, and again after a successful mapping and + after we've switched over to using the mapped in malloc descriptor + rather than the temporary one on the stack. - Once we've switched over to using the mapped in malloc descriptor, we - have to update the pointer to the morecore function, since it almost - certainly will be at a different address if the process reusing the - mapped region is from a different executable. + Once we've switched over to using the mapped in malloc descriptor, we + have to update the pointer to the morecore function, since it almost + certainly will be at a different address if the process reusing the + mapped region is from a different executable. - Also note that if the heap being remapped previously used the mmcheckf() - routines, we need to update the hooks since their target functions - will have certainly moved if the executable has changed in any way. - We do this by calling mmcheckf() internally. + Also note that if the heap being remapped previously used the mmcheckf() + routines, we need to update the hooks since their target functions + will have certainly moved if the executable has changed in any way. + We do this by calling mmcheckf() internally. - Returns a pointer to the malloc descriptor if successful, or NULL if - unsuccessful for some reason. */ + Returns a pointer to the malloc descriptor if successful, or NULL if + unsuccessful for some reason. */ struct mdesc newmd; struct mdesc *mdptr = NULL, *mdptemp = NULL; if (lseek(fd, 0L, SEEK_SET) != 0) - return NULL; + return NULL; if (read(fd, (char *) &newmd, sizeof(newmd)) != sizeof(newmd)) - return NULL; + return NULL; if (newmd.headersize != sizeof(newmd)) - return NULL; + return NULL; if (strcmp(newmd.magic, MMALLOC_MAGIC) != 0) - return NULL; + return NULL; if (newmd.version > MMALLOC_VERSION) - return NULL; + return NULL; newmd.fd = fd; if (__mmalloc_remap_core(&newmd) == newmd.base) { - mdptr = (struct mdesc *) newmd.base; - mdptr->fd = fd; - if(!mdptr->refcount){ - sem_init(&mdptr->sem, 0, 1); - mdptr->refcount++; - } + mdptr = (struct mdesc *) newmd.base; + mdptr->fd = fd; + if(!mdptr->refcount){ + sem_init(&mdptr->sem, 0, 1); + mdptr->refcount++; + } } /* Add the new heap to the linked list of heaps attached by mmalloc */ mdptemp = __mmalloc_default_mdp; while(mdptemp->next_mdesc) - mdptemp = mdptemp->next_mdesc; + mdptemp = mdptemp->next_mdesc; LOCK(mdptemp); mdptemp->next_mdesc = mdptr; @@ -193,7 +193,7 @@ xbt_mheap_t xbt_mheap_new(int fd, void *baseaddr) mdp = mdp->next_mdesc; LOCK(mdp); - mdp->next_mdesc = (struct mdesc *)mbase; + mdp->next_mdesc = (struct mdesc *)mbase; UNLOCK(mdp); } @@ -218,18 +218,18 @@ void xbt_mheap_destroy_no_free(xbt_mheap_t md) } /** Terminate access to a mmalloc managed region by unmapping all memory pages - associated with the region, and closing the file descriptor if it is one - that we opened. + associated with the region, and closing the file descriptor if it is one + that we opened. - Returns NULL on success. + Returns NULL on success. - Returns the malloc descriptor on failure, which can subsequently be used - for further action, such as obtaining more information about the nature of - the failure. + Returns the malloc descriptor on failure, which can subsequently be used + for further action, such as obtaining more information about the nature of + the failure. - Note that the malloc descriptor that we are using is currently located in - region we are about to unmap, so we first make a local copy of it on the - stack and use the copy. */ + Note that the malloc descriptor that we are using is currently located in + region we are about to unmap, so we first make a local copy of it on the + stack and use the copy. */ void *xbt_mheap_destroy(xbt_mheap_t mdp) { @@ -324,7 +324,7 @@ void *mmalloc_preinit(void) __mmalloc_default_mdp = xbt_mheap_new(-1, addr); /* Fixme? only the default mdp in protected against forks */ res = xbt_os_thread_atfork(mmalloc_fork_prepare, - mmalloc_fork_parent, mmalloc_fork_child); + mmalloc_fork_parent, mmalloc_fork_child); if (res != 0) THROWF(system_error,0,"xbt_os_thread_atfork() failed: return value %d",res); } diff --git a/src/xbt/mmalloc/mmorecore.c b/src/xbt/mmalloc/mmorecore.c index 339b72c884..d374c7e55d 100644 --- a/src/xbt/mmalloc/mmorecore.c +++ b/src/xbt/mmalloc/mmorecore.c @@ -30,23 +30,23 @@ static size_t pagesize; #define PAGE_ALIGN(addr) (void*) (((long)(addr) + pagesize - 1) & \ - ~(pagesize - 1)) + ~(pagesize - 1)) /* Return MAP_PRIVATE if MDP represents /dev/zero. Otherwise, return MAP_SHARED. */ #define MAP_PRIVATE_OR_SHARED(MDP) (( MDP -> flags & MMALLOC_ANONYMOUS) \ - ? MAP_PRIVATE \ + ? MAP_PRIVATE \ : MAP_SHARED) /* Return MAP_ANONYMOUS if MDP uses anonymous mapping. Otherwise, return 0 */ #define MAP_IS_ANONYMOUS(MDP) (((MDP) -> flags & MMALLOC_ANONYMOUS) \ - ? MAP_ANONYMOUS \ - : 0) + ? MAP_ANONYMOUS \ + : 0) /* Return -1 if MDP uses anonymous mapping. Otherwise, return MDP->FD */ #define MAP_ANON_OR_FD(MDP) (((MDP) -> flags & MMALLOC_ANONYMOUS) \ - ? -1 \ - : (MDP) -> fd) + ? -1 \ + : (MDP) -> fd) /* Get core for the memory region specified by MDP, using SIZE as the amount to either add to or subtract from the existing region. Works diff --git a/src/xbt/mmalloc/mmprivate.h b/src/xbt/mmalloc/mmprivate.h index b68eb49208..ccc667dc8f 100644 --- a/src/xbt/mmalloc/mmprivate.h +++ b/src/xbt/mmalloc/mmprivate.h @@ -134,8 +134,8 @@ struct mstats */ typedef struct { int type; /* 0: busy large block - >0: busy fragmented (fragments of size 2^type bytes) - <0: free block */ + >0: busy fragmented (fragments of size 2^type bytes) + <0: free block */ union { /* Heap information for a busy block. */ struct { diff --git a/src/xbt/mmalloc/mrealloc.c b/src/xbt/mmalloc/mrealloc.c index 7b803fee3c..23d0a1c202 100644 --- a/src/xbt/mmalloc/mrealloc.c +++ b/src/xbt/mmalloc/mrealloc.c @@ -1,6 +1,6 @@ /* Change the size of a block allocated by `mmalloc'. Copyright 1990, 1991 Free Software Foundation - Written May 1989 by Mike Haertel. */ + Written May 1989 by Mike Haertel. */ /* Copyright (c) 2010. The SimGrid Team. * All rights reserved. */ @@ -38,7 +38,7 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size) if ((char *) ptr < (char *) mdp->heapbase || BLOCK(ptr) > mdp->heapsize) { printf - ("FIXME. Ouch, this pointer is not mine, refusing to proceed (another solution would be to malloc it instead of reallocing it, see source code)\n"); + ("FIXME. Ouch, this pointer is not mine, refusing to proceed (another solution would be to malloc it instead of reallocing it, see source code)\n"); result = mmalloc(mdp, size); abort(); return result; @@ -83,10 +83,10 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size) /* The new size is smaller; return excess memory to the free list. */ //printf("(%s) return excess memory...",xbt_thread_self_name()); for (it= block+blocks; it< mdp->heapinfo[block].busy_block.size ; it++) - mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here + mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here mdp->heapinfo[block + blocks].busy_block.size - = mdp->heapinfo[block].busy_block.size - blocks; + = mdp->heapinfo[block].busy_block.size - blocks; mfree(mdp, ADDRESS(block + blocks)); mdp->heapinfo[block].busy_block.size = blocks; -- 2.20.1