From fec07ddcf333c9cc6e00b9cb60c5245b4c5b6700 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 13 May 2014 15:23:13 +0200 Subject: [PATCH] [mc] Rename raw_heap into mc_heap --- src/mc/mc_dpor.c | 66 +++++++++---------- src/mc/mc_global.c | 154 +++++++++++++++++++++---------------------- src/mc/mc_liveness.c | 78 +++++++++++----------- src/mc/mc_memory.c | 14 ++-- src/mc/mc_private.h | 6 +- 5 files changed, 159 insertions(+), 159 deletions(-) diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 6c22b82738..c4ccb59628 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -230,9 +230,9 @@ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu", state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used); - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; int cursor = 0, previous_cursor, next_cursor; mc_visited_state_t state_test; @@ -270,14 +270,14 @@ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, next_cursor++; } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; } } } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return cursor; } @@ -291,9 +291,9 @@ static int is_visited_state(){ if(_sg_mc_visited == 0) return -1; - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_visited_state_t new_state = visited_state_new(); @@ -302,7 +302,7 @@ static int is_visited_state(){ xbt_dynar_push(visited_states, &new_state); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; @@ -332,7 +332,7 @@ static int is_visited_state(){ xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL); xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return new_state->other_num; }*/ @@ -356,7 +356,7 @@ static int is_visited_state(){ xbt_dynar_insert_at(visited_states, cursor, &new_state); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return new_state->other_num; } cursor++; @@ -399,7 +399,7 @@ static int is_visited_state(){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; @@ -412,13 +412,13 @@ static int is_visited_state(){ void MC_dpor_init() { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); mc_state_t initial_state = NULL; smx_process_t process; /* Create the initial state and push it into the exploration stack */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(_sg_mc_visited > 0) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); @@ -435,7 +435,7 @@ void MC_dpor_init() initial_state = MC_state_new(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); @@ -446,7 +446,7 @@ void MC_dpor_init() MC_ignore_heap(simix_global->process_to_run->data, 0); MC_ignore_heap(simix_global->process_that_ran->data, 0); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Get an enabled process and insert it in the interleave set of the initial state */ xbt_swag_foreach(process, simix_global->process_list){ @@ -474,12 +474,12 @@ void MC_dpor_init() } } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -531,20 +531,20 @@ void MC_dpor(void) xbt_free(req_str); } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(dot_output != NULL) req_str = MC_request_get_dot_output(req, value); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; if(mc_reduce_kind == e_mc_reduce_dpor){ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; char *key = bprintf("%lu", req->issuer->pid); xbt_dict_remove(first_enabled_state, key); xbt_free(key); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ @@ -558,14 +558,14 @@ void MC_dpor(void) SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(comm_pattern != 0){ if(!initial_state_safety->initial_communications_pattern_done) get_comm_pattern(initial_communications_pattern, req, comm_pattern); else get_comm_pattern(communications_pattern, req, comm_pattern); } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; comm_pattern = 0; } @@ -573,7 +573,7 @@ void MC_dpor(void) MC_wait_for_requests(); /* Create the new expanded state */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; next_state = MC_state_new(); @@ -621,7 +621,7 @@ void MC_dpor(void) if(dot_output != NULL) xbt_free(req_str); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Let's loop again */ @@ -664,7 +664,7 @@ void MC_dpor(void) } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(initial_state_safety->initial_communications_pattern_done){ @@ -703,7 +703,7 @@ void MC_dpor(void) MC_state_delete(state); XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Check for deadlocks */ if(MC_deadlock_check()){ @@ -711,7 +711,7 @@ void MC_dpor(void) return; } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that have it empty in the way. For each deleted state, check if the request that has generated it @@ -763,7 +763,7 @@ void MC_dpor(void) if(state->system_state != NULL){ MC_restore_snapshot(state->system_state); xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; }else{ pos = xbt_fifo_size(mc_stack_safety); item = xbt_fifo_get_first_item(mc_stack_safety); @@ -778,12 +778,12 @@ void MC_dpor(void) } MC_restore_snapshot(restored_state->system_state); xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_replay(mc_stack_safety, pos); } }else{ xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_replay(mc_stack_safety, -1); } XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety)); @@ -800,11 +800,11 @@ void MC_dpor(void) MC_state_delete(state); } } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } } MC_print_statistics(mc_stats); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 89b98559a9..265f54f210 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -472,9 +472,9 @@ static void checkpoint_ignore_region_free_voidp(void *r){ void MC_ignore_heap(void *address, size_t size){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_heap_ignore_region_t region = NULL; region = xbt_new0(s_mc_heap_ignore_region_t, 1); @@ -495,7 +495,7 @@ void MC_ignore_heap(void *address, size_t size){ mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp); xbt_dynar_push(mc_heap_comparison_ignore, ®ion); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; } @@ -510,7 +510,7 @@ void MC_ignore_heap(void *address, size_t size){ if(current_region->address == address){ heap_ignore_region_free(region); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; }else if(current_region->address < address){ start = cursor + 1; @@ -525,14 +525,14 @@ void MC_ignore_heap(void *address, size_t size){ xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_remove_ignore_heap(void *address, size_t size){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; unsigned int cursor = 0; int start = 0; @@ -564,15 +564,15 @@ void MC_remove_ignore_heap(void *address, size_t size){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_ignore_global_variable(const char *name){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized"); @@ -596,7 +596,7 @@ void MC_ignore_global_variable(const char *name){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } /** \brief Ignore a local variable in a scope @@ -667,27 +667,27 @@ static void MC_ignore_local_variable_in_object(const char *var_name, const char void MC_ignore_local_variable(const char *var_name, const char *frame_name){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); if(strcmp(frame_name, "*") == 0) frame_name = NULL; - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; MC_ignore_local_variable_in_object(var_name, frame_name, mc_libsimgrid_info); if(frame_name!=NULL) MC_ignore_local_variable_in_object(var_name, frame_name, mc_binary_info); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_new_stack_area(void *stack, char *name, void* context, size_t size){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(stacks_areas == NULL) stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL); @@ -702,14 +702,14 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){ xbt_dynar_push(stacks_areas, ®ion); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_ignore(void *addr, size_t size){ - int raw_mem_set= (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set= (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(mc_checkpoint_ignore == NULL) mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp); @@ -734,7 +734,7 @@ void MC_ignore(void *addr, size_t size){ if(current_region->size == size){ checkpoint_ignore_region_free(region); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; }else if(current_region->size < size){ start = cursor + 1; @@ -762,7 +762,7 @@ void MC_ignore(void *addr, size_t size){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } /******************************* Initialisation of MC *******************************/ @@ -810,14 +810,14 @@ static void MC_init_debug_info(void) { void MC_init(){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); compare = 0; /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; MC_init_memory_map_info(); MC_init_debug_info(); @@ -825,7 +825,7 @@ void MC_init(){ /* Init parmap */ parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ MC_ignore_local_variable("e", "*"); @@ -865,7 +865,7 @@ void MC_init(){ } if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } @@ -901,9 +901,9 @@ static void MC_init_dot_output(){ /* FIXME : more colors */ void MC_do_the_modelcheck_for_real() { - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') { if (mc_reduce_kind==e_mc_reduce_unset) @@ -925,7 +925,7 @@ void MC_do_the_modelcheck_for_real() { void MC_modelcheck_safety(void) { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); /* Check if MC is already initialized */ if (initial_state_safety) @@ -939,7 +939,7 @@ void MC_modelcheck_safety(void) /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Initialize statistics */ mc_stats = xbt_new0(s_mc_stats_t, 1); @@ -951,32 +951,32 @@ void MC_modelcheck_safety(void) if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')) MC_init_dot_output(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(_sg_mc_visited > 0){ MC_init(); }else{ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; MC_init_memory_map_info(); MC_init_debug_info(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } MC_dpor_init(); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Save the initial state */ initial_state_safety = xbt_new0(s_mc_global_t, 1); initial_state_safety->snapshot = MC_take_snapshot(0); initial_state_safety->initial_communications_pattern_done = 0; initial_state_safety->comm_deterministic = 1; initial_state_safety->send_deterministic = 1; - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_dpor(); if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; xbt_abort(); //MC_exit(); @@ -984,7 +984,7 @@ void MC_modelcheck_safety(void) void MC_modelcheck_liveness(){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); MC_init(); @@ -993,7 +993,7 @@ void MC_modelcheck_liveness(){ /* mc_time refers to clock for each process -> ignore it for heap comparison */ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Initialize statistics */ mc_stats = xbt_new0(s_mc_stats_t, 1); @@ -1008,7 +1008,7 @@ void MC_modelcheck_liveness(){ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')) MC_init_dot_output(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_ddfs_init(); @@ -1017,7 +1017,7 @@ void MC_modelcheck_liveness(){ xbt_free(mc_time); if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } @@ -1086,7 +1086,7 @@ int MC_deadlock_check() */ void MC_replay(xbt_fifo_t stack, int start) { - int raw_mem = (mmalloc_get_current_heap() == raw_heap); + int raw_mem = (mmalloc_get_current_heap() == mc_heap); int value, i = 1, count = 1; char *req_str; @@ -1103,7 +1103,7 @@ void MC_replay(xbt_fifo_t stack, int start) MC_restore_snapshot(initial_state_safety->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_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } start_item = xbt_fifo_get_last_item(stack); @@ -1114,7 +1114,7 @@ void MC_replay(xbt_fifo_t stack, int start) } } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(mc_reduce_kind == e_mc_reduce_dpor){ xbt_dict_reset(first_enabled_state); @@ -1133,7 +1133,7 @@ void MC_replay(xbt_fifo_t stack, int start) xbt_dynar_reset(incomplete_communications_pattern); } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Traverse the stack from the state at position start and re-execute the transitions */ @@ -1145,11 +1145,11 @@ void MC_replay(xbt_fifo_t stack, int start) saved_req = MC_state_get_executed_request(state, &value); if(mc_reduce_kind == e_mc_reduce_dpor){ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; char *key = bprintf("%lu", saved_req->issuer->pid); xbt_dict_remove(first_enabled_state, key); xbt_free(key); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } if(saved_req){ @@ -1175,11 +1175,11 @@ void MC_replay(xbt_fifo_t stack, int start) SIMIX_simcall_pre(req, value); if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(comm_pattern != 0){ get_comm_pattern(communications_pattern, req, comm_pattern); } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; comm_pattern = 0; } @@ -1188,7 +1188,7 @@ void MC_replay(xbt_fifo_t stack, int start) count++; if(mc_reduce_kind == e_mc_reduce_dpor){ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Insert in dict all enabled processes */ xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){ @@ -1200,7 +1200,7 @@ void MC_replay(xbt_fifo_t stack, int start) xbt_free(key); } } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } /* Update statistics */ @@ -1212,9 +1212,9 @@ void MC_replay(xbt_fifo_t stack, int start) XBT_DEBUG("**** End Replay ****"); if(raw_mem) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -1222,7 +1222,7 @@ void MC_replay(xbt_fifo_t stack, int start) void MC_replay_liveness(xbt_fifo_t stack, int all_stack) { - initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == mc_heap); int value; char *req_str; @@ -1240,7 +1240,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) /* 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 */ if(!initial_state_liveness->raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(all_stack){ @@ -1329,9 +1329,9 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) XBT_DEBUG("**** End Replay ****"); if(initial_state_liveness->raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -1343,7 +1343,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) void MC_dump_stack_safety(xbt_fifo_t stack) { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); MC_show_stack_safety(stack); @@ -1351,17 +1351,17 @@ void MC_dump_stack_safety(xbt_fifo_t stack) mc_state_t state; - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) MC_state_delete(state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -1369,9 +1369,9 @@ void MC_dump_stack_safety(xbt_fifo_t stack) void MC_show_stack_safety(xbt_fifo_t stack) { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; int value; mc_state_t state; @@ -1391,7 +1391,7 @@ void MC_show_stack_safety(xbt_fifo_t stack) } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_show_deadlock(smx_simcall_t req) @@ -1435,17 +1435,17 @@ void MC_show_stack_liveness(xbt_fifo_t stack){ void MC_dump_stack_liveness(xbt_fifo_t stack){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); mc_pair_t pair; - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL) MC_pair_delete(pair); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } @@ -1460,7 +1460,7 @@ void MC_print_statistics(mc_stats_t stats) XBT_INFO("Visited pairs = %lu", stats->visited_pairs); } XBT_INFO("Executed transitions = %lu", stats->executed_transitions); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){ fprintf(dot_output, "}\n"); fclose(dot_output); @@ -1471,7 +1471,7 @@ void MC_print_statistics(mc_stats_t stats) if (_sg_mc_send_determinism) XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_assert(int prop) @@ -1510,37 +1510,37 @@ double MC_process_clock_get(smx_process_t process) void MC_automaton_load(const char *file){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); xbt_automaton_load(_mc_property_automaton,file); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } void MC_automaton_new_propositional_symbol(const char* id, void* fct) { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 96e6513669..cd1603bbc8 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -42,9 +42,9 @@ static xbt_dynar_t get_atomic_propositions_values(){ */ static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; int cursor = 0, previous_cursor, next_cursor; mc_visited_pair_t pair_test; @@ -82,23 +82,23 @@ static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, in next_cursor++; } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; } } } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return cursor; } static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_visited_pair_t pair = NULL; pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions); @@ -123,7 +123,7 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_ /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair); if(res != -1){ if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num; }*/ @@ -140,7 +140,7 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, pair_test->num, initial_state_liveness->prev_req); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return NULL; } @@ -164,7 +164,7 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return pair; @@ -172,9 +172,9 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_ static void remove_acceptance_pair(int pair_num){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; unsigned int cursor = 0; mc_visited_pair_t pair_test = NULL; @@ -196,7 +196,7 @@ static void remove_acceptance_pair(int pair_num){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } /** \brief Checks whether a given state has already been visited by the algorithm. @@ -207,9 +207,9 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s if(_sg_mc_visited == 0) return -1; - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_visited_pair_t new_pair = NULL; @@ -257,7 +257,7 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s } } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return pair->other_num; }*/ cursor = min; @@ -285,7 +285,7 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s MC_visited_pair_delete(pair_test); } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return new_pair->other_num; } } @@ -329,7 +329,7 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; } @@ -374,7 +374,7 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t void MC_ddfs_init(void){ - initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == mc_heap); XBT_DEBUG("**************************************************"); XBT_DEBUG("Double-DFS init"); @@ -388,7 +388,7 @@ void MC_ddfs_init(void){ MC_ignore_heap(simix_global->process_to_run->data, 0); MC_ignore_heap(simix_global->process_that_ran->data, 0); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); @@ -397,7 +397,7 @@ void MC_ddfs_init(void){ initial_state_liveness->snapshot = MC_take_snapshot(0); initial_state_liveness->prev_pair = 0; - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; unsigned int cursor = 0; xbt_automaton_state_t automaton_state; @@ -405,7 +405,7 @@ void MC_ddfs_init(void){ xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){ if(automaton_state->type == -1){ /* Initial automaton state */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; initial_pair = MC_pair_new(); initial_pair->automaton_state = automaton_state; @@ -424,21 +424,21 @@ void MC_ddfs_init(void){ xbt_fifo_unshift(mc_stack_liveness, initial_pair); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_ddfs(); if(cursor != 0){ MC_restore_snapshot(initial_state_liveness->snapshot); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } } } if(initial_state_liveness->raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -502,16 +502,16 @@ void MC_ddfs(){ if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(dot_output != NULL) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; }else{ while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(dot_output != NULL){ if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req); @@ -519,7 +519,7 @@ void MC_ddfs(){ } initial_state_liveness->prev_pair = current_pair->num; } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Debug information */ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ @@ -528,13 +528,13 @@ void MC_ddfs(){ xbt_free(req_str); } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(dot_output != NULL){ initial_state_liveness->prev_req = MC_request_get_dot_output(req, value); if(current_pair->search_cycle) fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_state_set_executed_request(current_pair->graph_state, req, value); mc_stats->executed_transitions++; @@ -545,9 +545,9 @@ void MC_ddfs(){ /* Wait for requests (schedules processes) */ MC_wait_for_requests(); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; prop_values = get_atomic_propositions_values(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; int new_pair = 0; @@ -562,7 +562,7 @@ void MC_ddfs(){ if(new_pair) MC_replay_liveness(mc_stack_liveness, 1); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; next_pair = MC_pair_new(); next_pair->graph_state = MC_state_new(); @@ -586,7 +586,7 @@ void MC_ddfs(){ if(mc_stats->expanded_pairs%1000000 == 0) XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; new_pair = 1; @@ -607,7 +607,7 @@ void MC_ddfs(){ if(new_pair) MC_replay_liveness(mc_stack_liveness, 1); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; next_pair = MC_pair_new(); next_pair->graph_state = MC_state_new(); @@ -631,7 +631,7 @@ void MC_ddfs(){ if(mc_stats->expanded_pairs%1000000 == 0) XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; new_pair = 1; @@ -670,7 +670,7 @@ void MC_ddfs(){ } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; xbt_dynar_free(&prop_values); current_pair = xbt_fifo_shift(mc_stack_liveness); if(xbt_fifo_size(mc_stack_liveness) != _sg_mc_max_depth -1 && current_pair->requests > 0 && current_pair->search_cycle){ @@ -678,6 +678,6 @@ void MC_ddfs(){ } MC_pair_delete(current_pair); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } diff --git a/src/mc/mc_memory.c b/src/mc/mc_memory.c index f734ec70ad..b2e53d01de 100644 --- a/src/mc/mc_memory.c +++ b/src/mc/mc_memory.c @@ -15,10 +15,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc, /* Pointers to each of the heap regions to use */ void *std_heap = NULL; /* memory erased each time the MC stuff rollbacks to the beginning. Almost everything goes here */ -void *raw_heap = NULL; /* memory persistent over the MC rollbacks. Only MC stuff should go there */ +void *mc_heap = NULL; /* memory persistent over the MC rollbacks. Only MC stuff should go there */ /* Initialize the model-checker memory subsystem */ -/* It creates the two heap regions: std_heap and raw_heap */ +/* It creates the two heap regions: std_heap and mc_heap */ void MC_memory_init() { /* Create the first region HEAP_OFFSET bytes after the heap break address */ @@ -27,11 +27,11 @@ void MC_memory_init() #if defined HAVE_GNU_LD && !defined MMALLOC_WANT_OVERRIDE_LEGACY /* use the system malloc for the model-checker data */ - raw_heap = NULL; + mc_heap = NULL; #else /* Create the second region a page after the first one ends + safety gap */ - raw_heap = xbt_mheap_new(-1, (char*)(std_heap) + STD_HEAP_SIZE + xbt_pagesize); - xbt_assert(raw_heap != NULL); + mc_heap = xbt_mheap_new(-1, (char*)(std_heap) + STD_HEAP_SIZE + xbt_pagesize); + xbt_assert(mc_heap != NULL); #endif } @@ -42,6 +42,6 @@ void MC_memory_exit(void) MC_free_object_info(&mc_binary_info); MC_free_object_info(&mc_libsimgrid_info); - if (raw_heap) - xbt_mheap_destroy(raw_heap); + if (mc_heap) + xbt_mheap_destroy(mc_heap); } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 0d45e7484b..7090eebc2c 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -221,7 +221,7 @@ void MC_print_statistics(mc_stats_t); /* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE */ extern void *std_heap; -extern void *raw_heap; +extern void *mc_heap; /* FIXME: Horrible hack! because the mmalloc library doesn't provide yet of */ @@ -236,8 +236,8 @@ extern void *raw_heap; /* size_t bytes_free; /\* Byte total of chunks in the free list. *\/ */ /* }; */ -#define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap) -#define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap) +#define MC_SET_MC_HEAP mmalloc_set_current_heap(mc_heap) +#define MC_SET_STD_HEAP mmalloc_set_current_heap(std_heap) /******************************* MEMORY MAPPINGS ***************************/ -- 2.20.1