-/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013. The SimGrid Team.
+ * All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
int user_max_depth_reached = 0;
-extern int _sg_init_status;
void _mc_cfg_cb_reduce(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
char *val= xbt_cfg_get_string(_sg_cfg_set, name);
}
void _mc_cfg_cb_checkpoint(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
- _sg_mc_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
+ _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_property(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
}
void _mc_cfg_cb_timeout(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
}
void _mc_cfg_cb_max_depth(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_visited(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_dot_output(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
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;
+__thread mc_comparison_times_t mc_comp_times = NULL;
+__thread double mc_snapshot_comparison_time;
mc_stats_t mc_stats = NULL;
/* Safety */
/******************************* Ignore mechanism *******************************/
/*********************************************************************************/
+xbt_dynar_t mc_checkpoint_ignore;
+
typedef struct s_mc_stack_ignore_variable{
- int in_libsimgrid;
char *var_name;
char *frame;
}s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
typedef struct s_mc_data_bss_ignore_variable{
- int in_libsimgrid;
char *name;
}s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
}
+static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){
+ xbt_free(r);
+}
+
+static void checkpoint_ignore_region_free_voidp(void *r){
+ checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
+}
+
/***********************************************************************/
void MC_ignore_heap(void *address, size_t size){
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
return;
- }
- if(current_region->address < address)
+ }else if(current_region->address < address){
start = cursor + 1;
- if(current_region->address > address)
- end = cursor - 1;
+ }else{
+ end = cursor - 1;
+ }
}
if(current_region->address < address)
else
xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
void MC_remove_ignore_heap(void *address, size_t size){
if(region->address == address){
ignore_found = 1;
break;
- }
- if(region->address < address)
+ }else if(region->address < address){
start = cursor + 1;
- if(region->address > address){
+ }else{
if((char * )region->address <= ((char *)address + size)){
ignore_found = 1;
break;
- }else
+ }else{
end = cursor - 1;
+ }
}
}
MC_remove_ignore_heap(address, size);
}
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
-void MC_ignore_global_variable(const char *name, ...){
+void MC_ignore_global_variable(const char *name){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
- va_list ap;
- va_start(ap, name);
- int in_libsimgrid = va_arg(ap, int);
- va_end(ap);
-
- xbt_dynar_t variables = NULL;
-
- if(in_libsimgrid == 1){
- variables = mc_global_variables_libsimgrid;
- }else{
- variables = mc_global_variables_binary;
- }
-
- if(variables){
+ if(mc_global_variables_libsimgrid){
unsigned int cursor = 0;
dw_variable_t current_var;
int start = 0;
- int end = xbt_dynar_length(variables) - 1;
- int var_found;
+ int end = xbt_dynar_length(mc_global_variables_libsimgrid) - 1;
while(start <= end){
cursor = (start + end) /2;
- current_var = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
+ current_var = (dw_variable_t)xbt_dynar_get_as(mc_global_variables_libsimgrid, cursor, dw_variable_t);
if(strcmp(current_var->name, name) == 0){
- xbt_dynar_remove_at(variables, cursor, NULL);
- var_found = 1;
- break;
+ xbt_dynar_remove_at(mc_global_variables_libsimgrid, cursor, NULL);
+ start = 0;
+ end = xbt_dynar_length(mc_global_variables_libsimgrid) - 1;
}else if(strcmp(current_var->name, name) < 0){
start = cursor + 1;
}else{
end = cursor - 1;
}
}
-
- if(var_found){
- if(in_libsimgrid == 1)
- MC_ignore_global_variable(name, 1);
- else
- MC_ignore_global_variable(name);
- }
-
+
}else{
if(mc_data_bss_comparison_ignore == NULL)
mc_data_bss_ignore_variable_t var = NULL;
var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
var->name = strdup(name);
- var->in_libsimgrid = (in_libsimgrid == 1);
if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
}
}
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
-void MC_ignore_local_variable(const char *var_name, const char *frame_name, ...){
+void MC_ignore_local_variable(const char *var_name, const char *frame_name){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
- va_list ap;
- va_start(ap, frame_name);
- int in_libsimgrid = va_arg(ap, int);
- va_end(ap);
-
- xbt_dict_t variables = NULL;
-
- if(in_libsimgrid == 1){
- variables = mc_local_variables_libsimgrid;
- }else{
- variables = mc_local_variables_binary;
- }
-
- if(variables){
+ if(mc_local_variables_libsimgrid){
unsigned int cursor = 0;
dw_variable_t current_var;
int start, end;
- if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames (binary and libsimgrid) */
- xbt_dict_cursor_t dict_cursor, dict_cursor2;
+ if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */
+ xbt_dict_cursor_t dict_cursor;
char *current_frame_name;
dw_frame_t frame;
xbt_dict_foreach(mc_local_variables_libsimgrid, dict_cursor, current_frame_name, frame){
end = xbt_dynar_length(frame->variables) - 1;
while(start <= end){
cursor = (start + end) / 2;
- current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
+ current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
if(strcmp(current_var->name, var_name) == 0){
xbt_dynar_remove_at(frame->variables, cursor, NULL);
start = 0;
}
}
}
- xbt_dict_foreach(mc_local_variables_binary, dict_cursor2, current_frame_name, frame){
+ xbt_dict_foreach(mc_local_variables_binary, dict_cursor, current_frame_name, frame){
start = 0;
end = xbt_dynar_length(frame->variables) - 1;
while(start <= end){
cursor = (start + end) / 2;
- current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
+ current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
if(strcmp(current_var->name, var_name) == 0){
xbt_dynar_remove_at(frame->variables, cursor, NULL);
start = 0;
}
}
}else{
- xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(variables, frame_name))->variables;
+ xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(mc_local_variables_libsimgrid, frame_name))->variables;
start = 0;
end = xbt_dynar_length(variables_list) - 1;
while(start <= end){
mc_stack_ignore_variable_t var = NULL;
var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
- var->in_libsimgrid = (in_libsimgrid == 1);
var->var_name = strdup(var_name);
var->frame = strdup(frame_name);
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
return;
- }
- if(strcmp(current_var->var_name, var_name) < 0)
+ }else if(strcmp(current_var->var_name, var_name) < 0){
start = cursor + 1;
- if(strcmp(current_var->var_name, var_name) > 0)
+ }else{
end = cursor - 1;
- }
- if(strcmp(current_var->frame, frame_name) < 0)
+ }
+ }else if(strcmp(current_var->frame, frame_name) < 0){
start = cursor + 1;
- if(strcmp(current_var->frame, frame_name) > 0)
+ }else{
end = cursor - 1;
+ }
}
- if(strcmp(current_var->frame, frame_name) < 0)
+ if(strcmp(current_var->frame, frame_name) == 0){
+ if(strcmp(current_var->var_name, var_name) < 0){
+ xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
+ }else{
+ xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
+ }
+ }else if(strcmp(current_var->frame, frame_name) < 0){
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
- else
+ }else{
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
-
+ }
}
}
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
+
if(stacks_areas == NULL)
stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
region->size = size;
region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
xbt_dynar_push(stacks_areas, ®ion);
-
- MC_UNSET_RAW_MEM;
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
+}
+
+void MC_ignore(void *addr, size_t size){
+
+ int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ if(mc_checkpoint_ignore == NULL)
+ mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
+
+ mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
+ region->addr = addr;
+ region->size = size;
+
+ if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
+ xbt_dynar_push(mc_checkpoint_ignore, ®ion);
+ }else{
+
+ unsigned int cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
+ mc_checkpoint_ignore_region_t current_region = NULL;
+
+ while(start <= end){
+ cursor = (start + end) / 2;
+ current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
+ if(current_region->addr == addr){
+ if(current_region->size == size){
+ checkpoint_ignore_region_free(region);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
+ return;
+ }else if(current_region->size < size){
+ start = cursor + 1;
+ }else{
+ end = cursor - 1;
+ }
+ }else if(current_region->addr < addr){
+ start = cursor + 1;
+ }else{
+ end = cursor - 1;
+ }
+ }
+
+ if(current_region->addr == addr){
+ if(current_region->size < size){
+ xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, ®ion);
+ }else{
+ xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, ®ion);
+ }
+ }else if(current_region->addr < addr){
+ xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, ®ion);
+ }else{
+ xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, ®ion);
+ }
+ }
+
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
/******************************* Initialisation of MC *******************************/
unsigned int cursor = 0;
mc_stack_ignore_variable_t current_var;
- xbt_dict_t variables;
xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){
-
- if(current_var->in_libsimgrid == 1){
- variables = mc_local_variables_libsimgrid;
- }else{
- variables = mc_local_variables_binary;
- }
-
- unsigned int cursor2 = 0;
- dw_variable_t var;
- int start, end;
-
- if(strcmp(current_var->frame, "*") == 0){
- xbt_dict_cursor_t dict_cursor;
- char *frame_name;
- dw_frame_t frame;
- xbt_dict_foreach(variables, dict_cursor, frame_name, frame){
- start = 0;
- end = xbt_dynar_length(frame->variables) - 1;
- while(start <= end){
- cursor2 = (start + end) / 2;
- var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor2, dw_variable_t);
- if(strcmp(var->name, current_var->var_name) == 0){
- xbt_dynar_remove_at(frame->variables, cursor2, NULL);
- start = 0;
- end = xbt_dynar_length(frame->variables) - 1;
- }else if(strcmp(var->name, current_var->var_name) < 0){
- start = cursor2 + 1;
- }else{
- end = cursor2 - 1;
- }
- }
- }
- }else{
- xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(variables, current_var->frame))->variables;
- start = 0;
- end = xbt_dynar_length(variables_list) - 1;
- while(start <= end){
- cursor2 = (start + end) / 2;
- var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor2, dw_variable_t);
- if(strcmp(var->name, current_var->var_name) == 0){
- xbt_dynar_remove_at(variables_list, cursor2, NULL);
- start = 0;
- end = xbt_dynar_length(variables_list) - 1;
- }else if(strcmp(var->name, current_var->var_name) < 0){
- start = cursor2 + 1;
- }else{
- end = cursor2 - 1;
- }
- }
- }
+ MC_ignore_local_variable(current_var->var_name, current_var->frame);
}
xbt_dynar_free(&mc_stack_comparison_ignore);
unsigned int cursor = 0;
mc_data_bss_ignore_variable_t current_var;
- xbt_dynar_t variables;
-
- unsigned int cursor2 = 0;
- dw_variable_t var;
- int start, end;
xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){
-
- if(current_var->in_libsimgrid == 1){
- variables = mc_global_variables_libsimgrid;
- }else{
- variables = mc_global_variables_binary;
- }
-
- cursor2 = 0;
- start = 0;
- end = xbt_dynar_length(variables) - 1;
-
- while(start <= end){
- cursor2 = (start + end) / 2;
- var = (dw_variable_t)xbt_dynar_get_as(variables, cursor2, dw_variable_t);
- if(strcmp(var->name, current_var->name) == 0){
- xbt_dynar_remove_at(variables, cursor2, NULL);
- return;
- }else if(strcmp(var->name, current_var->name) < 0){
- start = cursor2 + 1;
- }else{
- end = cursor2 - 1;
- }
- }
+ MC_ignore_global_variable(current_var->name);
}
xbt_dynar_free(&mc_data_bss_comparison_ignore);
mc_data_bss_comparison_ignore = NULL;
-
}
xbt_dict_free(&libsimgrid_location_list);
xbt_dict_free(&binary_location_list);
+ XBT_INFO("Get debug information done !");
+
/* Remove variables ignored before getting list of variables */
MC_dump_ignored_local_variables();
MC_dump_ignored_global_variables();
MC_get_libsimgrid_plt_section();
MC_get_binary_plt_section();
+ /* Init parmap */
+ parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
+
MC_UNSET_RAW_MEM;
/* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
MC_ignore_local_variable("e", "*");
- MC_ignore_local_variable("__ex_cleanup", "*", 1);
- MC_ignore_local_variable("__ex_mctx_en", "*", 1);
- MC_ignore_local_variable("__ex_mctx_me", "*", 1);
- MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*", 1);
- MC_ignore_local_variable("_log_ev", "*", 1);
- MC_ignore_local_variable("_throw_ctx", "*", 1);
- MC_ignore_local_variable("ctx", "*", 1);
+ MC_ignore_local_variable("__ex_cleanup", "*");
+ MC_ignore_local_variable("__ex_mctx_en", "*");
+ MC_ignore_local_variable("__ex_mctx_me", "*");
+ MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
+ MC_ignore_local_variable("_log_ev", "*");
+ MC_ignore_local_variable("_throw_ctx", "*");
+ MC_ignore_local_variable("ctx", "*");
- MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial", 1);
- MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial", 1);
+ MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
+ MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
/* Ignore local variable about time used for tracing */
- MC_ignore_local_variable("start_time", "*", 1);
-
- MC_ignore_global_variable("mc_comp_times", 1);
- MC_ignore_global_variable("mc_snapshot_comparison_time", 1);
- MC_ignore_global_variable("mc_time", 1);
- MC_ignore_global_variable("smpi_current_rank", 1);
- MC_ignore_global_variable("smx_current_context_serial", 1);
- MC_ignore_global_variable("smx_current_context_key", 1);
- MC_ignore_global_variable("sysv_maestro_context", 1);
- MC_ignore_global_variable("counter", 1); /* Static variable used for tracing */
+ MC_ignore_local_variable("start_time", "*");
+
+ MC_ignore_global_variable("mc_comp_times");
+ MC_ignore_global_variable("mc_snapshot_comparison_time");
+ MC_ignore_global_variable("mc_time");
+ MC_ignore_global_variable("smpi_current_rank");
+ MC_ignore_global_variable("counter"); /* Static variable used for tracing */
+ MC_ignore_global_variable("maestro_stack_start");
+ MC_ignore_global_variable("maestro_stack_end");
+
+ MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
+ MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
+ MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
+ MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
+
+ smx_process_t process;
+ xbt_swag_foreach(process, simix_global->process_list){
+ MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
+ }
if(raw_mem_set)
MC_SET_RAW_MEM;
- XBT_INFO("Get debug information done !");
-
}
static void MC_init_dot_output(){ /* FIXME : more colors */
MC_SET_RAW_MEM;
/* Save the initial state */
initial_state_safety = xbt_new0(s_mc_global_t, 1);
- initial_state_safety->snapshot = MC_take_snapshot();
+ initial_state_safety->snapshot = MC_take_snapshot(0);
MC_UNSET_RAW_MEM;
MC_dpor();
