if (_sg_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_int(_sg_cfg_set, name);
+ _sg_mc_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
void _mc_cfg_cb_property(const char *name, int pos) {
if (_sg_init_status && !_sg_do_model_check) {
if (_sg_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_int(_sg_cfg_set, name);
+ _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
}
void _mc_cfg_cb_max_depth(const char *name, int pos) {
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
MC_UNSET_RAW_MEM;
- if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
- MC_init_dot_output();
-
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;
MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
+ /* Ignore local variable about time used for tracing */
+ MC_ignore_stack("start_time", "*");
+
MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time));
MC_ignore_data_bss(&mc_time, sizeof(mc_time));
xbt_abort();
}
- fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.20; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
+ fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
}
/* Create exploration stack */
mc_stack_safety = xbt_fifo_new();
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+ MC_init_dot_output();
+
MC_UNSET_RAW_MEM;
if(_sg_mc_visited > 0){
/* Create the initial state */
initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+ MC_init_dot_output();
+
MC_UNSET_RAW_MEM;
MC_ddfs_init();
void MC_exit(void)
{
- MC_SET_RAW_MEM;
- if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
- fprintf(dot_output, "}\n");
- fclose(dot_output);
- }
- MC_UNSET_RAW_MEM;
-
xbt_free(mc_time);
MC_memory_exit();
xbt_abort();
{
int raw_mem = (mmalloc_get_current_heap() == raw_heap);
- int value, i = 1;
+ int value, i = 1, count = 1;
char *req_str;
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item, start_item;
mc_state_t state;
+ smx_process_t process = NULL;
XBT_DEBUG("**** Begin Replay ****");
}
}
+ MC_SET_RAW_MEM;
+ xbt_dict_reset(first_enabled_state);
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ char *key = bprintf("%lu", process->pid);
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
+
+
/* Traverse the stack from the state at position start and re-execute the transitions */
for (item = start_item;
item != xbt_fifo_get_first_item(stack);
state = (mc_state_t) xbt_fifo_get_item_content(item);
saved_req = MC_state_get_executed_request(state, &value);
+ MC_SET_RAW_MEM;
+ char *key = bprintf("%lu", saved_req->issuer->pid);
+ xbt_dict_remove(first_enabled_state, key);
+ xbt_free(key);
+ MC_UNSET_RAW_MEM;
+
if(saved_req){
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
xbt_free(req_str);
}
}
-
+
SIMIX_simcall_pre(req, value);
MC_wait_for_requests();
+
+ count++;
+
+ MC_SET_RAW_MEM;
+ /* 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)*/){
+ char *key = bprintf("%lu", process->pid);
+ if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ }
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
/* Update statistics */
mc_stats->visited_states++;
mc_stats->executed_transitions++;
+
}
+
XBT_DEBUG("**** End Replay ****");
if(raw_mem)
depth++;
/* Update statistics */
- mc_stats->visited_states++;
+ mc_stats->visited_pairs++;
mc_stats->executed_transitions++;
item = xbt_fifo_get_prev_item(item);
depth++;
/* Update statistics */
- mc_stats->visited_states++;
+ mc_stats->visited_pairs++;
mc_stats->executed_transitions++;
}
}
void MC_print_statistics(mc_stats_t stats)
{
- //XBT_INFO("State space size ~= %lu", stats->state_size);
- XBT_INFO("Expanded states = %lu", stats->expanded_states);
- XBT_INFO("Visited states = %lu", stats->visited_states);
+ if(stats->expanded_pairs == 0){
+ XBT_INFO("Expanded states = %lu", stats->expanded_states);
+ XBT_INFO("Visited states = %lu", stats->visited_states);
+ }else{
+ XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
+ XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
+ }
XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
- XBT_INFO("Expanded / Visited = %lf",
- (double) stats->visited_states / stats->expanded_states);
- /*XBT_INFO("Exploration coverage = %lf",
- (double)stats->expanded_states / stats->state_size); */
+ MC_SET_RAW_MEM;
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+ fprintf(dot_output, "}\n");
+ fclose(dot_output);
+ }
+ MC_UNSET_RAW_MEM;
}
void MC_assert(int prop)
if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
region->fragment = -1;
- ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore = 1;
+ ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
}else{
region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
- ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment] = 1;
+ ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
}
if(mc_heap_comparison_ignore == NULL){
}
unsigned int cursor = 0;
- mc_heap_ignore_region_t current_region;
+ mc_heap_ignore_region_t current_region = NULL;
int start = 0;
int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
}
+void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
+ xbt_free(v);
+}
+
+void data_bss_ignore_variable_free_voidp(void *v){
+ data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
+}
+
void MC_ignore_data_bss(void *address, size_t size){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
if(mc_data_bss_comparison_ignore == NULL)
- mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), 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);
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(current_var->address == address){
+ data_bss_ignore_variable_free(var);
MC_UNSET_RAW_MEM;
if(raw_mem_set)
MC_SET_RAW_MEM;
return 0;
}
+void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
+ xbt_free(v->var_name);
+ xbt_free(v->frame);
+ xbt_free(v);
+}
+void stack_ignore_variable_free_voidp(void *v){
+ stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
+}
void MC_ignore_stack(const char *var_name, const char *frame_name){
MC_SET_RAW_MEM;
if(mc_stack_comparison_ignore == NULL)
- mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), 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)){
- 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);
-
xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
}else{
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);
MC_UNSET_RAW_MEM;
if(raw_mem_set)
MC_SET_RAW_MEM;
end = cursor - 1;
}
- 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(strcmp(current_var->frame, frame_name) < 0)
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
else
