-/* Copyright (c) 2011-2013. The SimGrid Team.
+/* Copyright (c) 2011-2014. The SimGrid Team.
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
return values;
}
+/** \brief Find a suitable subrange of candidate duplicates for a given state
+ *
+ * See mc_dpor.c with a similar (same?) function.
+ */
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;
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);
index = get_search_interval(acceptance_pairs, pair, &min, &max);
if(min != -1 && max != -1){ // Acceptance pair with same number of processes and same heap bytes used exists
+
+ // Parallell implementation
/*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;
}*/
+
cursor = min;
while(cursor <= max){
pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
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;
}
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return pair;
static void remove_acceptance_pair(int pair_num){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
- fprintf(stderr, "Search acceptance pair %d\n", pair_num);
+ 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;
}
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.
+ *
+ */
static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
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;
}
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return pair->other_num;
}*/
cursor = min;
if(dot_output == NULL)
XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
else
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, pair->other_num);
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, new_pair->other_num);
xbt_dynar_remove_at(visited_pairs, cursor, NULL);
xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
pair_test->visited_removed = 1;
MC_visited_pair_delete(pair_test);
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return new_pair->other_num;
}
}
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return -1;
}
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");
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);
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;
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;
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;
}
mc_pair_t next_pair = NULL;
xbt_dynar_t prop_values = NULL;
mc_visited_pair_t reached_pair = NULL;
+ int counter_example_depth = 0;
if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
if((reached_pair = is_reached_acceptance_pair(current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) == NULL){
+ counter_example_depth = xbt_fifo_size(mc_stack_liveness);
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
MC_show_stack_liveness(mc_stack_liveness);
MC_dump_stack_liveness(mc_stack_liveness);
MC_print_statistics(mc_stats);
+ XBT_INFO("Counter-example depth : %d", counter_example_depth);
xbt_abort();
}
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);
}
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)){
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++;
/* 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;
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();
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;
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();
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;
}
- 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){
}
MC_pair_delete(current_pair);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
