visited_state_free((mc_visited_state_t) * (void **) s);
}
+ /** \brief Save the current state
+ *
+ * \return Snapshot of the current state.
+ */
static mc_visited_state_t visited_state_new(){
mc_visited_state_t new_state = NULL;
}
+ /** \brief Find a suitable subrange of candidate duplicates for a given state
+ *
+ * \param all_ pairs dynamic array of states with candidate duplicates of the current state;
+ * \param pair current state;
+ * \param min (output) index of the beginning of the the subrange
+ * \param max (output) index of the enf of the subrange
+ *
+ * Given a suitably ordered array of state, this function extracts a subrange
+ * (with index *min <= i <= *max) with candidate duplicates of the given state.
+ * This function uses only fast discriminating criterions and does not use the
+ * full state comparison algorithms.
+ *
+ * The states in all_pairs MUST be ordered using a (given) weak order
+ * (based on nb_processes and heap_bytes_used).
+ * The subrange is the subrange of "equivalence" of the given state.
+ */
static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
return cursor;
}
+ /** \brief Take a snapshot the current state and process it.
+ *
+ * \return number of the duplicate state or -1 (not visited)
+ */
static int is_visited_state(){
if(_sg_mc_visited == 0)
index = get_search_interval(visited_states, new_state, &min, &max);
if(min != -1 && max != -1){
+
+ // Parallell implementation
/*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
if(res != -1){
state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
MC_UNSET_RAW_MEM;
return new_state->other_num;
}*/
+
cursor = min;
while(cursor <= max){
state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
if(snapshot_compare(state_test, new_state) == 0){
+ // The state has been visited:
+
if(state_test->other_num == -1)
new_state->other_num = state_test->num;
else
XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
else
XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
+
+ // Replace the old state with the new one (why?):
xbt_dynar_remove_at(visited_states, cursor, NULL);
xbt_dynar_insert_at(visited_states, cursor, &new_state);
+
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
return new_state->other_num;
}
cursor++;
}
+
+ // The state has not been visited, add it to the list:
xbt_dynar_insert_at(visited_states, min, &new_state);
+
}else{
+
+ // The state has not been visited: insert the state in the dynamic array.
state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
if(state_test->nb_processes < new_state->nb_processes){
xbt_dynar_insert_at(visited_states, index+1, &new_state);
else
xbt_dynar_insert_at(visited_states, index, &new_state);
}
+
}
+ // We have reached the maximum number of stored states;
if(xbt_dynar_length(visited_states) > _sg_mc_visited){
+
+ // Find the (index of the) older state:
int min2 = mc_stats->expanded_states;
unsigned int cursor2 = 0;
unsigned int index2 = 0;
min2 = state_test->num;
}
}
+
+ // and drop it:
xbt_dynar_remove_at(visited_states, index2, NULL);
}
}
- /**
- * \brief Perform the model-checking operation using a depth-first search exploration
- * with Dynamic Partial Order Reductions
+ /** \brief Model-check the application using a DFS exploration
+ * with DPOR (Dynamic Partial Order Reductions)
*/
void MC_dpor(void)
{
char *req_str = NULL;
int value;
smx_simcall_t req = NULL, prev_req = NULL;
- mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
+ mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
smx_process_t process = NULL;
xbt_fifo_item_t item = NULL;
mc_state_t state_test = NULL;
int pos;
int visited_state = -1;
int enabled = 0;
- int comm_pattern = 0;
int interleave_size = 0;
+ int comm_pattern = 0;
while (xbt_fifo_size(mc_stack_safety) > 0) {
xbt_dict_remove(first_enabled_state, key);
xbt_free(key);
MC_UNSET_RAW_MEM;
-
- if(req->call == SIMCALL_COMM_ISEND)
- comm_pattern = 1;
- else if(req->call == SIMCALL_COMM_IRECV)
- comm_pattern = 2;
+
+ if(_sg_mc_comms_determinism){
+ if(req->call == SIMCALL_COMM_ISEND)
+ comm_pattern = 1;
+ else if(req->call == SIMCALL_COMM_IRECV)
+ comm_pattern = 2;
+ }
/* Answer the request */
SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
- MC_SET_RAW_MEM;
- 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);
+ if(_sg_mc_comms_determinism){
+ MC_SET_RAW_MEM;
+ 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;
+ comm_pattern = 0;
}
- MC_UNSET_RAW_MEM;
-
- comm_pattern = 0;
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
}
MC_SET_RAW_MEM;
- if(0) {
- if(!initial_state_safety->initial_communications_pattern_done){
- print_communications_pattern(initial_communications_pattern);
- }else{
- if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
- print_communications_pattern(communications_pattern);
- deterministic_pattern(initial_communications_pattern, communications_pattern);
+
+ if(_sg_mc_comms_determinism){
+ if(!initial_state_safety->initial_communications_pattern_done){
+ //print_communications_pattern(initial_communications_pattern);
+ }else{
+ if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
+ //print_communications_pattern(communications_pattern);
+ deterministic_pattern(initial_communications_pattern, communications_pattern);
+ }
}
+ initial_state_safety->initial_communications_pattern_done = 1;
}
- initial_state_safety->initial_communications_pattern_done = 1;
- }
- MC_UNSET_RAW_MEM;
/* Trash the current state, no longer needed */
- MC_SET_RAW_MEM;
xbt_fifo_shift(mc_stack_safety);
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;
/* Check for deadlocks */
pos = xbt_fifo_size(mc_stack_safety);
item = xbt_fifo_get_first_item(mc_stack_safety);
while(pos>0){
- restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
- if(restore_state->system_state != NULL){
+ restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
+ if(restored_state->system_state != NULL){
break;
}else{
item = xbt_fifo_get_next_item(item);
pos--;
}
}
- MC_restore_snapshot(restore_state->system_state);
+ MC_restore_snapshot(restored_state->system_state);
xbt_fifo_unshift(mc_stack_safety, state);
MC_UNSET_RAW_MEM;
MC_replay(mc_stack_safety, pos);
break;
} else {
req = MC_state_get_internal_request(state);
- if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
- // fprintf(stderr, "Remove state with isend or irecv\n");
- if(!xbt_dynar_is_empty(communications_pattern))
- xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
+ if(_sg_mc_comms_determinism){
+ if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
+ if(!xbt_dynar_is_empty(communications_pattern))
+ xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
+ }
}
XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
MC_state_delete(state);
int _sg_mc_checkpoint=0;
char* _sg_mc_property_file=NULL;
int _sg_mc_timeout=0;
+ int _sg_mc_hash=0;
int _sg_mc_max_depth=1000;
int _sg_mc_visited=0;
char *_sg_mc_dot_output_file = NULL;
+int _sg_mc_comms_determinism=0;
int user_max_depth_reached = 0;
_sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
}
+ void _mc_cfg_cb_hash(const char *name, int pos) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _sg_mc_hash= xbt_cfg_get_boolean(_sg_cfg_set, name);
+ }
+
void _mc_cfg_cb_max_depth(const char *name, int pos) {
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_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
}
+void _mc_cfg_cb_comms_determinism(const char *name, int pos) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a value to enable/disable the detection of determinism in the communications schemes 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_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name);
+}
+
/* MC global data structures */
mc_state_t mc_current_state = NULL;
char mc_replay_mode = FALSE;
mc_object_info_t mc_binary_info = NULL;
/* Ignore mechanism */
- xbt_dynar_t mc_stack_comparison_ignore;
- xbt_dynar_t mc_data_bss_comparison_ignore;
extern xbt_dynar_t mc_heap_comparison_ignore;
extern xbt_dynar_t stacks_areas;
dw_variable_free((dw_variable_t) * (void **) t);
}
- // object_info
+ // ***** object_info
mc_object_info_t MC_new_object_info(void) {
mc_object_info_t res = xbt_new0(s_mc_object_info_t, 1);
res->local_variables = xbt_dict_new_homogeneous(NULL);
res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
res->types = xbt_dict_new_homogeneous(NULL);
+ res->types_by_name = xbt_dict_new_homogeneous(NULL);
return res;
}
+
void MC_free_object_info(mc_object_info_t* info) {
xbt_free(&(*info)->file_name);
xbt_dict_free(&(*info)->local_variables);
xbt_dynar_free(&(*info)->global_variables);
xbt_dict_free(&(*info)->types);
+ xbt_dict_free(&(*info)->types_by_name);
xbt_free(info);
+ xbt_dynar_free(&(*info)->functions_index);
*info = NULL;
}
+ // ***** Helpers
+
+ void* MC_object_base_address(mc_object_info_t info) {
+ void* result = info->start_exec;
+ if(info->start_rw!=NULL && result > (void*) info->start_rw) result = info->start_rw;
+ if(info->start_ro!=NULL && result > (void*) info->start_ro) result = info->start_ro;
+ return result;
+ }
+
+ // ***** Functions index
+
+ static int MC_compare_frame_index_items(mc_function_index_item_t a, mc_function_index_item_t b) {
+ if(a->low_pc < b->low_pc)
+ return -1;
+ else if(a->low_pc == b->low_pc)
+ return 0;
+ else
+ return 1;
+ }
+
+ static void MC_make_functions_index(mc_object_info_t info) {
+ xbt_dynar_t index = xbt_dynar_new(sizeof(s_mc_function_index_item_t), NULL);
+
+ // Populate the array:
+ dw_frame_t frame = NULL;
+ xbt_dict_cursor_t cursor = NULL;
+ const char* name = NULL;
+ xbt_dict_foreach(info->local_variables, cursor, name, frame) {
+ if(frame->low_pc==NULL)
+ continue;
+ s_mc_function_index_item_t entry;
+ entry.low_pc = frame->low_pc;
+ entry.high_pc = frame->high_pc;
+ entry.function = frame;
+ xbt_dynar_push(index, &entry);
+ }
+
+ mc_function_index_item_t base = (mc_function_index_item_t) xbt_dynar_get_ptr(index, 0);
+
+ // Sort the array by low_pc:
+ qsort(base,
+ xbt_dynar_length(index),
+ sizeof(s_mc_function_index_item_t),
+ (int (*)(const void *, const void *))MC_compare_frame_index_items);
+
+ info->functions_index = index;
+ }
+
+ mc_object_info_t MC_ip_find_object_info(void* ip) {
+ mc_object_info_t infos[2] = { mc_binary_info, mc_libsimgrid_info };
+ size_t n = 2;
+ size_t i;
+ for(i=0; i!=n; ++i) {
+ if(ip >= (void*)infos[i]->start_exec && ip <= (void*)infos[i]->end_exec) {
+ return infos[i];
+ }
+ }
+ return NULL;
+ }
+
+ static dw_frame_t MC_find_function_by_ip_and_object(void* ip, mc_object_info_t info) {
+ xbt_dynar_t dynar = info->functions_index;
+ mc_function_index_item_t base = (mc_function_index_item_t) xbt_dynar_get_ptr(dynar, 0);
+ int i = 0;
+ int j = xbt_dynar_length(dynar) - 1;
+ while(j>=i) {
+ int k = i + ((j-i)/2);
+ if(ip < base[k].low_pc) {
+ j = k-1;
+ } else if(ip > base[k].high_pc) {
+ i = k+1;
+ } else {
+ return base[k].function;
+ }
+ }
+ return NULL;
+ }
+
+ dw_frame_t MC_find_function_by_ip(void* ip) {
+ mc_object_info_t info = MC_ip_find_object_info(ip);
+ if(info==NULL)
+ return NULL;
+ else
+ return MC_find_function_by_ip_and_object(ip, info);
+ }
+
+ static void MC_post_process_variables(mc_object_info_t info) {
+ unsigned cursor = 0;
+ dw_variable_t variable = NULL;
+ xbt_dynar_foreach(info->global_variables, cursor, variable) {
+ if(variable->type_origin) {
+ variable->type = xbt_dict_get_or_null(info->types, variable->type_origin);
+ }
+ }
+ }
+
+ static void MC_post_process_functions(mc_object_info_t info) {
+ xbt_dict_cursor_t cursor = NULL;
+ char* key = NULL;
+ dw_frame_t function = NULL;
+ xbt_dict_foreach(info->local_variables, cursor, key, function) {
+ unsigned cursor2 = 0;
+ dw_variable_t variable = NULL;
+ xbt_dynar_foreach(function->variables, cursor2, variable) {
+ if(variable->type_origin) {
+ variable->type = xbt_dict_get_or_null(info->types, variable->type_origin);
+ }
+ }
+ }
+ }
+
+ /** \brief Finds informations about a given shared object/executable */
+ mc_object_info_t MC_find_object_info(memory_map_t maps, char* name, int executable) {
+ mc_object_info_t result = MC_new_object_info();
+ if(executable)
+ result->flags |= MC_OBJECT_INFO_EXECUTABLE;
+ result->file_name = xbt_strdup(name);
+ MC_find_object_address(maps, result);
+ MC_dwarf_get_variables(result);
+ MC_post_process_types(result);
+ MC_post_process_variables(result);
+ MC_post_process_functions(result);
+ MC_make_functions_index(result);
+ return result;
+ }
+
/*************************************************************************/
static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
MC_dwarf_register_non_global_variable(info, frame, variable);
}
+
/******************************* Ignore mechanism *******************************/
/*********************************************************************************/
char *frame;
}s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
- typedef struct s_mc_data_bss_ignore_variable{
- char *name;
- }s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
-
/**************************** Free functions ******************************/
static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
}
- static void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
- xbt_free(v->name);
- xbt_free(v);
- }
-
- static void data_bss_ignore_variable_free_voidp(void *v){
- 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);
}
MC_SET_RAW_MEM;
- if(mc_libsimgrid_info){
+ xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized");
unsigned int cursor = 0;
dw_variable_t current_var;
end = cursor - 1;
}
}
-
- }else{
-
- if(mc_data_bss_comparison_ignore == NULL)
- mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
-
- mc_data_bss_ignore_variable_t var = NULL;
- var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
- var->name = strdup(name);
-
- if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
-
- xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
-
- }else{
-
- unsigned int cursor = 0;
- int start = 0;
- int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
- mc_data_bss_ignore_variable_t current_var = NULL;
-
- while(start <= end){
- cursor = (start + end) / 2;
- current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
- if(strcmp(current_var->name, name) == 0){
- data_bss_ignore_variable_free(var);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return;
- }else if(strcmp(current_var->name, name) < 0){
- start = cursor + 1;
- }else{
- end = cursor - 1;
- }
- }
-
- if(strcmp(current_var->name, name) < 0)
- xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
- else
- xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
-
- }
- }
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
MC_SET_RAW_MEM;
- if(mc_libsimgrid_info){
unsigned int cursor = 0;
dw_variable_t current_var;
int start, end;
}
}
}
- }else{
-
- if(mc_stack_comparison_ignore == NULL)
- mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
-
- mc_stack_ignore_variable_t var = NULL;
- var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
- var->var_name = strdup(var_name);
- var->frame = strdup(frame_name);
-
- if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
-
- xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
-
- }else{
-
- unsigned int cursor = 0;
- int start = 0;
- int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
- mc_stack_ignore_variable_t current_var = NULL;
-
- while(start <= end){
- cursor = (start + end) / 2;
- current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
- if(strcmp(current_var->frame, frame_name) == 0){
- if(strcmp(current_var->var_name, var_name) == 0){
- stack_ignore_variable_free(var);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return;
- }else if(strcmp(current_var->var_name, var_name) < 0){
- start = cursor + 1;
- }else{
- end = cursor - 1;
- }
- }else if(strcmp(current_var->frame, frame_name) < 0){
- start = cursor + 1;
- }else{
- end = cursor - 1;
- }
- }
-
- 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{
- xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
- }
- }
- }
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
/******************************* Initialisation of MC *******************************/
/*********************************************************************************/
- static void MC_dump_ignored_local_variables(void){
-
- if(mc_stack_comparison_ignore == NULL || xbt_dynar_is_empty(mc_stack_comparison_ignore))
- return;
-
- unsigned int cursor = 0;
- mc_stack_ignore_variable_t current_var;
-
- xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){
- MC_ignore_local_variable(current_var->var_name, current_var->frame);
+ static void MC_post_process_object_info(mc_object_info_t info) {
+ mc_object_info_t other_info = info == mc_binary_info ? mc_libsimgrid_info : mc_binary_info;
+ xbt_dict_cursor_t cursor = NULL;
+ char* key = NULL;
+ dw_type_t type = NULL;
+ xbt_dict_foreach(info->types, cursor, key, type){
+ if(type->name && type->byte_size == 0) {
+ type->other_object_same_type = xbt_dict_get_or_null(other_info->types_by_name, type->name);
+ }
}
-
- xbt_dynar_free(&mc_stack_comparison_ignore);
- mc_stack_comparison_ignore = NULL;
-
}
- static void MC_dump_ignored_global_variables(void){
-
- if(mc_data_bss_comparison_ignore == NULL || xbt_dynar_is_empty(mc_data_bss_comparison_ignore))
- return;
-
- unsigned int cursor = 0;
- mc_data_bss_ignore_variable_t current_var;
-
- xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){
- MC_ignore_global_variable(current_var->name);
- }
-
- xbt_dynar_free(&mc_data_bss_comparison_ignore);
- mc_data_bss_comparison_ignore = NULL;
-
- }
-
- static void MC_init_debug_info();
- static void MC_init_debug_info() {
+ static void MC_init_debug_info(void) {
XBT_INFO("Get debug information ...");
memory_map_t maps = MC_get_memory_map();
/* Get local variables for state equality detection */
- mc_binary_info = MC_find_object_info(maps, xbt_binary_name);
- mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path);
+ mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
+ mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0);
+
+ // Use information of the other objects:
+ MC_post_process_object_info(mc_binary_info);
+ MC_post_process_object_info(mc_libsimgrid_info);
MC_free_memory_map(maps);
XBT_INFO("Get debug information done !");
MC_init_memory_map_info();
MC_init_debug_info();
- /* Remove variables ignored before getting list of variables */
- MC_dump_ignored_local_variables();
- MC_dump_ignored_global_variables();
-
/* Init parmap */
parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
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_global_variable("smx_total_comms");
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));
xbt_free(key);
}
}
- xbt_dynar_reset(communications_pattern);
+ if(_sg_mc_comms_determinism)
+ xbt_dynar_reset(communications_pattern);
MC_UNSET_RAW_MEM;
}
}
- if(req->call == SIMCALL_COMM_ISEND)
- comm_pattern = 1;
- else if(req->call == SIMCALL_COMM_IRECV)
+ if(_sg_mc_comms_determinism){
+ if(req->call == SIMCALL_COMM_ISEND)
+ comm_pattern = 1;
+ else if(req->call == SIMCALL_COMM_IRECV)
comm_pattern = 2;
-
+ }
+
SIMIX_simcall_pre(req, value);
- MC_SET_RAW_MEM;
- if(comm_pattern != 0){
- get_comm_pattern(communications_pattern, req, comm_pattern);
+ if(_sg_mc_comms_determinism){
+ MC_SET_RAW_MEM;
+ if(comm_pattern != 0){
+ get_comm_pattern(communications_pattern, req, comm_pattern);
+ }
+ MC_UNSET_RAW_MEM;
+ comm_pattern = 0;
}
- MC_UNSET_RAW_MEM;
-
- comm_pattern = 0;
MC_wait_for_requests();
fprintf(dot_output, "}\n");
fclose(dot_output);
}
- if(initial_state_safety != NULL){
- // XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
- // XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
+ if(initial_state_safety != NULL && _sg_mc_comms_determinism){
+ XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
+ XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
}
MC_UNSET_RAW_MEM;
}
