static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start_addr, size_t size);
static void add_value(xbt_dynar_t *list, const char *type, unsigned long int val);
-static xbt_dynar_t take_snapshot_stacks(void *heap);
+static xbt_dynar_t take_snapshot_stacks(mc_snapshot_t *s, void *heap);
static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap);
static void print_local_variables_values(xbt_dynar_t all_variables);
static void *get_stack_pointer(void *stack_context, void *heap);
mc_mem_region_t new_reg = MC_region_new(type, start_addr, size);
snapshot->regions = xbt_realloc(snapshot->regions, (snapshot->num_reg + 1) * sizeof(mc_mem_region_t));
snapshot->regions[snapshot->num_reg] = new_reg;
+ snapshot->region_type[snapshot->num_reg] = type;
snapshot->num_reg++;
return;
}
}
if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,""))
- snapshot->stacks = take_snapshot_stacks(heap);
+ snapshot->stacks = take_snapshot_stacks(&snapshot, heap);
free_memory_map(maps);
xbt_dynar_push(*list, &value);
}
-static xbt_dynar_t take_snapshot_stacks(void *heap){
+static xbt_dynar_t take_snapshot_stacks(mc_snapshot_t *snapshot, void *heap){
xbt_dynar_t res = xbt_dynar_new(sizeof(s_mc_snapshot_stack_t), snapshot_stack_free_voidp);
- unsigned int cursor1 = 0;
+ unsigned int cursor = 0;
stack_region_t current_stack;
- xbt_dynar_foreach(stacks_areas, cursor1, current_stack){
+ xbt_dynar_foreach(stacks_areas, cursor, current_stack){
mc_snapshot_stack_t st = xbt_new(s_mc_snapshot_stack_t, 1);
st->local_variables = get_local_variables_values(current_stack->context, heap);
st->stack_pointer = get_stack_pointer(current_stack->context, heap);
- st->size_used = current_stack->size - ((char *)st->stack_pointer - (char *)((char *)heap + ((char *)current_stack->address - (char *)std_heap)));
xbt_dynar_push(res, &st);
+ (*snapshot)->stack_sizes = xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t));
+ (*snapshot)->stack_sizes[cursor] = current_stack->size - ((char *)st->stack_pointer - (char *)((char *)heap + ((char *)current_stack->address - (char *)std_heap)));
}
return res;
int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
mc_snapshot_t s1, mc_snapshot_t s2){
- return snapshot_compare(s1, s2, NULL, NULL);
+ return snapshot_compare(s1, s2);
}
int get_heap_region_index(mc_snapshot_t s){
return -1;
}
-int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t ct1, mc_comparison_times_t ct2){
+int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
int raw_mem = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
- int errors = 0, i = 0;
-
- if(ct1 != NULL)
- ct1->nb_comparisons++;
- if(ct2 != NULL)
- ct2->nb_comparisons++;
+ int errors = 0;
xbt_os_timer_t global_timer = xbt_os_timer_new();
xbt_os_timer_t timer = xbt_os_timer_new();
xbt_os_timer_start(global_timer);
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
+ #ifdef MC_DEBUG
xbt_os_timer_start(timer);
+ #endif
/* Compare number of processes */
if(s1->nb_processes != s2->nb_processes){
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
- xbt_os_timer_stop(timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
- XBT_DEBUG("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
- errors++;
- }else{
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
- XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
+ #ifdef MC_DEBUG
+ xbt_os_timer_stop(timer);
+ mc_comp_times->nb_processes_comparison_time = xbt_os_timer_elapsed(timer);
+ XBT_DEBUG("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
+ errors++;
+ #else
+ #ifdef MC_VERBOSE
+ XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
+ #endif
- xbt_os_timer_free(timer);
- xbt_os_timer_stop(global_timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- xbt_os_timer_free(global_timer);
+ xbt_os_timer_free(timer);
+ xbt_os_timer_stop(global_timer);
+ mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
+ xbt_os_timer_free(global_timer);
- if(!raw_mem)
- MC_UNSET_RAW_MEM;
+ if(!raw_mem)
+ MC_UNSET_RAW_MEM;
- return 1;
- }
+ return 1;
+ #endif
}
/* Compare number of blocks/fragments used in each heap */
-
if(s1->heap_chunks_used != s2->heap_chunks_used){
-
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_DEBUG
xbt_os_timer_stop(timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
+ mc_comp_times->chunks_used_comparison_time = xbt_os_timer_elapsed(timer);
XBT_DEBUG("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used);
errors++;
- }else{
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ #else
+ #ifdef MC_VERBOSE
XBT_VERB("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used);
-
+ #endif
+
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
+ mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
xbt_os_timer_free(global_timer);
if(!raw_mem)
MC_UNSET_RAW_MEM;
return 1;
- }
+ #endif
}else{
-
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
+ #ifdef MC_DEBUG
xbt_os_timer_stop(timer);
+ #endif
}
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
+ #ifdef MC_DEBUG
xbt_os_timer_start(timer);
+ #endif
/* Compare size of stacks */
-
- unsigned int cursor = 0;
+ int i = 0;
size_t size_used1, size_used2;
int is_diff = 0;
- while(cursor < xbt_dynar_length(stacks_areas)){
- size_used1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->size_used;
- size_used2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->size_used;
+ while(i < xbt_dynar_length(s1->stacks)){
+ size_used1 = s1->stack_sizes[i];
+ size_used2 = s2->stack_sizes[i];
if(size_used1 != size_used2){
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
- if(is_diff == 0){
- xbt_os_timer_stop(timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->stacks_sizes_comparison_times, double, xbt_os_timer_elapsed(timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->stacks_sizes_comparison_times, double, xbt_os_timer_elapsed(timer));
- }
- XBT_DEBUG("Different size used in stacks : %zu - %zu", size_used1, size_used2);
- errors++;
- is_diff = 1;
- }else{
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
- XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
+ #ifdef MC_DEBUG
+ if(is_diff == 0){
+ xbt_os_timer_stop(timer);
+ mc_comp_times->stacks_sizes_comparison_time = xbt_os_timer_elapsed(timer);
+ }
+ XBT_DEBUG("Different size used in stacks : %zu - %zu", size_used1, size_used2);
+ errors++;
+ is_diff = 1;
+ #else
+ #ifdef MC_VERBOSE
+ XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
+ #endif
- xbt_os_timer_free(timer);
- xbt_os_timer_stop(global_timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- xbt_os_timer_free(global_timer);
+ xbt_os_timer_free(timer);
+ xbt_os_timer_stop(global_timer);
+ mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
+ xbt_os_timer_free(global_timer);
- if(!raw_mem)
- MC_UNSET_RAW_MEM;
+ if(!raw_mem)
+ MC_UNSET_RAW_MEM;
- return 1;
- }
+ return 1;
+ #endif
}
- cursor++;
+ i++;
}
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_DEBUG
if(is_diff == 0)
xbt_os_timer_stop(timer);
xbt_os_timer_start(timer);
- }
+ #endif
int heap_index = 0, data_libsimgrid_index = 0, data_program_index = 0;
+ i = 0;
/* Get index of regions */
while(i < s1->num_reg){
- switch(s1->regions[i]->type){
+ switch(s1->region_type[i]){
case 0:
heap_index = i;
i++;
case 1:
data_libsimgrid_index = i;
i++;
- while( i < s1->num_reg && s1->regions[i]->type == 1)
+ while( i < s1->num_reg && s1->region_type[i] == 1)
i++;
break;
case 2:
data_program_index = i;
i++;
- while( i < s1->num_reg && s1->regions[i]->type == 2)
+ while( i < s1->num_reg && s1->region_type[i] == 2)
i++;
break;
}
}
/* Compare binary global variables */
-
- is_diff = compare_global_variables(s1->regions[data_program_index]->type, s1->regions[data_program_index]->data, s2->regions[data_program_index]->data);
+ is_diff = compare_global_variables(s1->region_type[data_program_index], s1->regions[data_program_index]->data, s2->regions[data_program_index]->data);
if(is_diff != 0){
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_DEBUG
xbt_os_timer_stop(timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->binary_global_variables_comparison_times, double, xbt_os_timer_elapsed(timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->binary_global_variables_comparison_times, double, xbt_os_timer_elapsed(timer));
+ mc_comp_times->binary_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
XBT_DEBUG("Different global variables in binary");
errors++;
- }else{
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ #else
+ #ifdef MC_VERBOSE
XBT_VERB("Different global variables in binary");
+ #endif
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
+ mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
xbt_os_timer_free(global_timer);
if(!raw_mem)
MC_UNSET_RAW_MEM;
return 1;
- }
+ #endif
}
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_VERBOSE
if(is_diff == 0)
xbt_os_timer_stop(timer);
xbt_os_timer_start(timer);
- }
+ #endif
/* Compare libsimgrid global variables */
-
- is_diff = compare_global_variables(s1->regions[data_libsimgrid_index]->type, s1->regions[data_libsimgrid_index]->data, s2->regions[data_libsimgrid_index]->data);
+ is_diff = compare_global_variables(s1->region_type[data_libsimgrid_index], s1->regions[data_libsimgrid_index]->data, s2->regions[data_libsimgrid_index]->data);
if(is_diff != 0){
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_DEBUG
xbt_os_timer_stop(timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->libsimgrid_global_variables_comparison_times, double, xbt_os_timer_elapsed(timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->libsimgrid_global_variables_comparison_times, double, xbt_os_timer_elapsed(timer));
+ mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
XBT_DEBUG("Different global variables in libsimgrid");
errors++;
- }else{
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ #else
+ #ifdef MC_VERBOSE
XBT_VERB("Different global variables in libsimgrid");
+ #endif
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
+ mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
xbt_os_timer_free(global_timer);
if(!raw_mem)
MC_UNSET_RAW_MEM;
return 1;
- }
+ #endif
}
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_DEBUG
if(is_diff == 0)
xbt_os_timer_stop(timer);
xbt_os_timer_start(timer);
- }
+ #endif
/* Compare heap */
-
xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp);
if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[heap_index]->data, (xbt_mheap_t)s2->regions[heap_index]->data, &stacks1, &stacks2, &equals)){
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_DEBUG
xbt_os_timer_stop(timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->heap_comparison_times, double, xbt_os_timer_elapsed(timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->heap_comparison_times, double, xbt_os_timer_elapsed(timer));
+ mc_comp_times->heap_comparison_time = xbt_os_timer_elapsed(timer);
XBT_DEBUG("Different heap (mmalloc_compare)");
errors++;
- }else{
+ #else
xbt_os_timer_free(timer);
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ #ifdef MC_VERBOSE
XBT_VERB("Different heap (mmalloc_compare)");
+ #endif
xbt_os_timer_stop(global_timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
+ mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
xbt_os_timer_free(global_timer);
if(!raw_mem)
MC_UNSET_RAW_MEM;
return 1;
- }
+ #endif
}else{
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
+ #ifdef MC_DEBUG
xbt_os_timer_stop(timer);
+ #endif
}
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
+ #ifdef MC_DEBUG
xbt_os_timer_start(timer);
+ #endif
/* Stacks comparison */
-
- cursor = 0;
+ unsigned int cursor = 0;
stack_region_t stack_region1, stack_region2;
int diff = 0, diff_local = 0;
void *sp1, *sp2;
if(diff > 0){ /* Differences may be due to padding */
diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, equals);
if(diff_local > 0){
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_DEBUG
if(is_diff == 0){
xbt_os_timer_stop(timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->stacks_comparison_times, double, xbt_os_timer_elapsed(timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->stacks_comparison_times, double, xbt_os_timer_elapsed(timer));
+ mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer);
}
XBT_DEBUG("Different local variables between stacks %d", cursor + 1);
errors++;
is_diff = 1;
- }else{
+ #else
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ #ifdef MC_VERBOSE
XBT_VERB("Different local variables between stacks %d", cursor + 1);
+ #endif
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
+ mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
xbt_os_timer_free(global_timer);
if(!raw_mem)
MC_UNSET_RAW_MEM;
return 1;
- }
+ #endif
}
}
cursor++;
xbt_os_timer_free(timer);
- if(!XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ #ifdef MC_VERBOSE
xbt_os_timer_stop(global_timer);
- if(ct1 != NULL)
- xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- if(ct2 != NULL)
- xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
- }
+ mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
+ #endif
+
xbt_os_timer_free(global_timer);
+ #ifdef MC_DEBUG
+ print_comparison_times();
+ #endif
+
if(!raw_mem)
MC_UNSET_RAW_MEM;
return simcall_mc_compare_snapshots(s1, s2);
}
+
+void print_comparison_times(){
+ XBT_DEBUG("*** Comparison times ***");
+ XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time);
+ XBT_DEBUG("- Nb chunks used : %f", mc_comp_times->chunks_used_comparison_time);
+ XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time);
+ XBT_DEBUG("- Binary global variables : %f", mc_comp_times->binary_global_variables_comparison_time);
+ XBT_DEBUG("- Libsimgrid global variables : %f", mc_comp_times->libsimgrid_global_variables_comparison_time);
+ XBT_DEBUG("- Heap : %f", mc_comp_times->heap_comparison_time);
+ XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time);
+}
end = cursor - 1;
if(chunks_used_test == current_chunks_used){
same_chunks_not_found = 0;
- if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
+ if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
xbt_dynar_remove_at(visited_states, cursor, NULL);
xbt_dynar_insert_at(visited_states, cursor, &new_state);
if(raw_mem_set)
chunks_used_test = state_test->system_state->heap_chunks_used;
if(chunks_used_test != current_chunks_used)
break;
- if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
+ if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
if(raw_mem_set)
chunks_used_test = state_test->system_state->heap_chunks_used;
if(chunks_used_test != current_chunks_used)
break;
- if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
+ if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
xbt_dynar_remove_at(visited_states, next_cursor, NULL);
xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
if(raw_mem_set)
mc_state_t mc_current_state = NULL;
char mc_replay_mode = FALSE;
double *mc_time = NULL;
+mc_comparison_times_t mc_comp_times = NULL;
+double mc_snapshot_comparison_time;
/* Safety */
static void MC_get_global_variables(char *elf_file);
void MC_do_the_modelcheck_for_real() {
+
+ MC_SET_RAW_MEM;
+ mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
+ MC_UNSET_RAW_MEM;
+
if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
if (mc_reduce_kind==e_mc_reduce_unset)
mc_reduce_kind=e_mc_reduce_dpor;
get_binary_plt_section();
MC_ignore_data_bss(&end_raw_heap, sizeof(end_raw_heap));
-
+ MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
+ MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time));
+
/* Get global variables */
MC_get_global_variables(xbt_binary_name);
MC_get_global_variables(libsimgrid_path);
return 0;
}
-void MC_print_comparison_times_statistics(mc_comparison_times_t ct){
-
- XBT_DEBUG("Comparisons done : %d", ct->nb_comparisons);
-
- double total, min, max;
- unsigned int cursor;
-
- if(xbt_dynar_length(ct->chunks_used_comparison_times) > 0){
- cursor = 0;
- total = 0.0;
- max = 0.0;
- min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
- while(cursor < xbt_dynar_length(ct->chunks_used_comparison_times) - 1){
- total += xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) > max)
- max = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) < min)
- min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
- cursor++;
- }
- XBT_DEBUG("Chunks used comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->chunks_used_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->chunks_used_comparison_times), max, min);
- }
-
- if(xbt_dynar_length(ct->stacks_sizes_comparison_times) > 0){
- cursor = 0;
- total = 0.0;
- max = 0.0;
- min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
- while(cursor < xbt_dynar_length(ct->stacks_sizes_comparison_times) - 1){
- total += xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) > max)
- max = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) < min)
- min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
- cursor++;
- }
- XBT_DEBUG("Stacks sizes comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_sizes_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_sizes_comparison_times), max, min);
- }
-
- if(xbt_dynar_length(ct->binary_global_variables_comparison_times) > 0){
- cursor = 0;
- total = 0.0;
- max = 0.0;
- min = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double);
- while(cursor < xbt_dynar_length(ct->binary_global_variables_comparison_times) - 1){
- total += xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double) > max)
- max = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double) < min)
- min = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double);
- cursor++;
- }
- XBT_DEBUG("Binary global variables comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->binary_global_variables_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->binary_global_variables_comparison_times), max, min);
- }
-
- if(xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times) > 0){
- cursor = 0;
- total = 0.0;
- max = 0.0;
- min = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double);
- while(cursor < xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times) - 1){
- total += xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double) > max)
- max = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double) < min)
- min = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double);
- cursor++;
- }
- XBT_DEBUG("Libsimgrid global variables comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times), max, min);
- }
-
- if(xbt_dynar_length(ct->heap_comparison_times) > 0){
- cursor = 0;
- total = 0.0;
- max = 0.0;
- min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
- while(cursor < xbt_dynar_length(ct->heap_comparison_times) - 1){
- total += xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) > max)
- max = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) < min)
- min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
- cursor++;
- }
- XBT_DEBUG("Heap comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->heap_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->heap_comparison_times), max, min);
- }
-
- if(xbt_dynar_length(ct->stacks_comparison_times) > 0){
- cursor = 0;
- total = 0.0;
- max = 0.0;
- min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
- while(cursor < xbt_dynar_length(ct->stacks_comparison_times) - 1){
- total += xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) > max)
- max = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) < min)
- min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
- cursor++;
- }
- XBT_DEBUG("Stacks comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_comparison_times), max, min);
- }
-
- if(xbt_dynar_length(ct->snapshot_comparison_times) > 0){
- cursor = 0;
- total = 0.0;
- max = 0.0;
- min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
- while(cursor < xbt_dynar_length(ct->snapshot_comparison_times) - 1){
- total += xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) > max)
- max = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
- if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) < min)
- min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
- cursor++;
- }
- XBT_DEBUG("Snapshot comparison (Whole funnel) -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->snapshot_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->snapshot_comparison_times), max, min);
- }
-
-}
-
-mc_comparison_times_t new_comparison_times(){
- mc_comparison_times_t ct = NULL;
- ct = xbt_new0(s_mc_comparison_times_t, 1);
- ct->nb_comparisons = 0;
- ct->snapshot_comparison_times = xbt_dynar_new(sizeof(double), NULL);
- ct->chunks_used_comparison_times = xbt_dynar_new(sizeof(double), NULL);
- ct->stacks_sizes_comparison_times = xbt_dynar_new(sizeof(double), NULL);
- ct->binary_global_variables_comparison_times = xbt_dynar_new(sizeof(double), NULL);
- ct->libsimgrid_global_variables_comparison_times = xbt_dynar_new(sizeof(double), NULL);
- ct->heap_comparison_times = xbt_dynar_new(sizeof(double), NULL);
- ct->stacks_comparison_times = xbt_dynar_new(sizeof(double), NULL);
- return ct;
-}
-
int reached(xbt_state_t st){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
new_pair->automaton_state = st;
new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- new_pair->comparison_times = new_comparison_times();
new_pair->system_state = MC_take_snapshot();
/* Get values of propositional symbols */
XBT_DEBUG("****** 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, new_pair->prop_ato) == 0){
- if(snapshot_compare(new_pair->system_state, pair_test->system_state, new_pair->comparison_times, pair_test->comparison_times) == 0){
+ if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
if(raw_mem_set)
MC_SET_RAW_MEM;
MC_UNSET_RAW_MEM;
return 1;
- }
+ }
}else{
XBT_DEBUG("Different values of propositional symbols");
}
}else{
XBT_DEBUG("Different automaton state");
}
- if(pair_test->comparison_times != NULL && XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
- XBT_DEBUG("*** Comparison times statistics ***");
- MC_print_comparison_times_statistics(pair_test->comparison_times);
- }
}
/* New pair reached */
pair->nb = xbt_dynar_length(reached_pairs) + 1;
pair->automaton_state = st;
pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- pair->comparison_times = new_comparison_times();
pair->system_state = MC_take_snapshot();
/* Get values of propositional symbols */
XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
if(automaton_state_compare(pair_test->automaton_state, st) == 0){
if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
- if(snapshot_compare(new_pair->system_state, pair_test->system_state, NULL, NULL) == 0){
+ if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
if(raw_mem_set)
MC_SET_RAW_MEM;
else
if(pair){
pair->automaton_state = NULL;
xbt_dynar_free(&(pair->prop_ato));
- if(pair->comparison_times != NULL){
- xbt_dynar_free(&(pair->comparison_times->snapshot_comparison_times));
- xbt_dynar_free(&(pair->comparison_times->chunks_used_comparison_times));
- xbt_dynar_free(&(pair->comparison_times->stacks_sizes_comparison_times));
- xbt_dynar_free(&(pair->comparison_times->binary_global_variables_comparison_times));
- xbt_dynar_free(&(pair->comparison_times->libsimgrid_global_variables_comparison_times));
- xbt_dynar_free(&(pair->comparison_times->heap_comparison_times));
- xbt_dynar_free(&(pair->comparison_times->stacks_comparison_times));
- }
MC_free_snapshot(pair->system_state);
xbt_free(pair);
}
/****************************** Snapshots ***********************************/
+#define nb_regions 3 /* binary data (data + BSS), libsimgrid data (data + BSS), std_heap */
+
typedef struct s_mc_mem_region{
int type;
void *start_addr;
typedef struct s_mc_snapshot{
unsigned int num_reg;
+ int region_type[nb_regions];
size_t heap_chunks_used;
mc_mem_region_t *regions;
+ size_t *stack_sizes;
xbt_dynar_t stacks;
int nb_processes;
} s_mc_snapshot_t, *mc_snapshot_t;
typedef struct s_mc_snapshot_stack{
xbt_strbuff_t local_variables;
void *stack_pointer;
- size_t size_used;
}s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
typedef struct s_mc_global_t{
extern void *start_got_plt_binary;
extern void *end_got_plt_binary;
+/********************************** Snapshot comparison **********************************/
+
+typedef struct s_mc_comparison_times{
+ double nb_processes_comparison_time;
+ double chunks_used_comparison_time;
+ double stacks_sizes_comparison_time;
+ double binary_global_variables_comparison_time;
+ double libsimgrid_global_variables_comparison_time;
+ double heap_comparison_time;
+ double stacks_comparison_time;
+}s_mc_comparison_times_t, *mc_comparison_times_t;
+
+extern mc_comparison_times_t mc_comp_times;
+extern double mc_snapshot_comparison_time;
+
+int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2);
+int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_snapshot_t s2);
+void print_comparison_times(void);
+
+//#define MC_DEBUG 1
+//#define MC_VERBOSE 1
/********************************** DPOR for safety **************************************/
typedef enum {
xbt_state_t automaton_state;
}s_mc_pair_t, *mc_pair_t;
-typedef struct s_mc_comparison_times{
- int nb_comparisons;
- xbt_dynar_t snapshot_comparison_times;
- xbt_dynar_t chunks_used_comparison_times;
- xbt_dynar_t stacks_sizes_comparison_times;
- xbt_dynar_t binary_global_variables_comparison_times;
- xbt_dynar_t libsimgrid_global_variables_comparison_times;
- xbt_dynar_t heap_comparison_times;
- xbt_dynar_t stacks_comparison_times;
-}s_mc_comparison_times_t, *mc_comparison_times_t;
-
typedef struct s_mc_pair_reached{
int nb;
xbt_state_t automaton_state;
xbt_dynar_t prop_ato;
mc_snapshot_t system_state;
- mc_comparison_times_t comparison_times;
}s_mc_pair_reached_t, *mc_pair_reached_t;
typedef struct s_mc_pair_visited{
int MC_automaton_evaluate_label(xbt_exp_label_t l);
mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st);
-mc_comparison_times_t new_comparison_times(void);
int reached(xbt_state_t st);
void set_pair_reached(xbt_state_t st);
int visited(xbt_state_t st);
-int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
- mc_snapshot_t s1, mc_snapshot_t s2);
-int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t ct1, mc_comparison_times_t ct2);
+
void MC_pair_delete(mc_pair_t pair);
void MC_exit_liveness(void);
mc_state_t MC_state_pair_new(void);
void pair_visited_free_voidp(void *p);
void MC_init_liveness(void);
void MC_init_memory_map_info(void);
-void MC_print_comparison_times_statistics(mc_comparison_times_t ct);
int get_heap_region_index(mc_snapshot_t s);
