}
}
+ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
+
+ mc_list_comm_pattern_t list_comm_pattern = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
+
+ if(!backtracking){
+ mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, comm->index, mc_comm_pattern_t);
+ e_mc_comm_pattern_difference_t diff;
+
+ if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){
+ if (comm->type == SIMIX_COMM_SEND)
+ initial_global_state->send_deterministic = 0;
+ initial_global_state->comm_deterministic = 0;
+ print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+ }
+ }
+
+ list_comm_pattern->index_comm++;
+ comm_pattern_free(comm);
+
+ }
+
/********** Non Static functions ***********/
- void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, mc_call_type call_type)
+ void comm_pattern_free_voidp(void *p) {
+ comm_pattern_free((mc_comm_pattern_t) * (void **) p);
+ }
+
+ void list_comm_pattern_free_voidp(void *p) {
+ list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
+ }
+
+ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type)
{
-
+ mc_process_t process = &mc_model_checker->process;
mc_comm_pattern_t pattern = NULL;
pattern = xbt_new0(s_mc_comm_pattern_t, 1);
- pattern->num = ++nb_comm_pattern;
pattern->data_size = -1;
+ pattern->data = NULL;
+
+ pattern->index = ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, request->issuer->pid, mc_list_comm_pattern_t))->index_comm + xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t));
+
void *addr_pointed;
- if (call_type == MC_CALL_TYPE_SEND) { // ISEND
+
+ if (call_type == MC_CALL_TYPE_SEND) {
+ /* Create comm pattern */
pattern->type = SIMIX_COMM_SEND;
pattern->comm = simcall_comm_isend__get__result(request);
+ pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
pattern->src_proc = pattern->comm->comm.src_proc->pid;
pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
- pattern->data_size = pattern->comm->comm.src_buff_size;
- pattern->data = xbt_malloc0(pattern->data_size);
- addr_pointed = *(void **) pattern->comm->comm.src_buff;
- if (addr_pointed > (void*) process->heap_address
- && addr_pointed < MC_process_get_heap(process)->breakval)
- memcpy(pattern->data, addr_pointed, pattern->data_size);
- else
- memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
- } else if (call_type == MC_CALL_TYPE_RECV) { // IRECV
+ if(pattern->comm->comm.src_buff != NULL){
+ pattern->data_size = pattern->comm->comm.src_buff_size;
+ pattern->data = xbt_malloc0(pattern->data_size);
+ addr_pointed = *(void **) pattern->comm->comm.src_buff;
- if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval)
++ if (addr_pointed > (void*) process->heap_address
++ && addr_pointed < MC_process_get_heap(process)->breakval)
+ memcpy(pattern->data, addr_pointed, pattern->data_size);
+ else
+ memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
+ }
+ } else if (call_type == MC_CALL_TYPE_RECV) {
pattern->type = SIMIX_COMM_RECEIVE;
pattern->comm = simcall_comm_irecv__get__result(request);
+ pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
} else {
/* SIMIX */
MC_ignore_global_variable("smx_total_comms");
- MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+ if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
+ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+
- smx_process_t process;
- xbt_swag_foreach(process, simix_global->process_list) {
- MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
+ smx_process_t process;
+ xbt_swag_foreach(process, simix_global->process_list) {
- MC_ignore_heap(&(process->process_hookup),
- sizeof(process->process_hookup));
- }
++ MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
++ }
}
}
* a given model-checker stack.
* \param stack The stack with the transitions to execute.
* \param start Start index to begin the re-execution.
- *
- * If start==-1, restore the initial state and replay the actions the
- * the transitions in the stack.
- *
- * Otherwise, we only replay a part of the transitions of the stacks
- * without restoring the state: it is assumed that the current state
- * match with the transitions to execute.
*/
- void MC_replay(xbt_fifo_t stack, int start)
+ void MC_replay(xbt_fifo_t stack)
{
- int raw_mem = (mmalloc_get_current_heap() == mc_heap);
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- int value, i = 1, count = 1, j;
+ int value, count = 1, j;
char *req_str;
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item, start_item;
}
XBT_DEBUG("**** End Replay ****");
-
- if (raw_mem)
- MC_SET_MC_HEAP;
- else
- MC_SET_STD_HEAP;
-
-
+ mmalloc_set_current_heap(heap);
}
- void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
+ void MC_replay_liveness(xbt_fifo_t stack)
{
initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
*/
void MC_dump_stack_safety(xbt_fifo_t stack)
{
-
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
MC_show_stack_safety(stack);
-
- if (!_sg_mc_checkpoint) {
-
- mc_state_t state;
-
- MC_SET_MC_HEAP;
- while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
- MC_state_delete(state);
- MC_SET_STD_HEAP;
-
- }
-
+
+ mc_state_t state;
+
+ MC_SET_MC_HEAP;
+ while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+ MC_state_delete(state, !state->in_visited_states ? 1 : 0);
- MC_SET_STD_HEAP;
-
- if (raw_mem_set)
- MC_SET_MC_HEAP;
- else
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
}
}
}
+
void MC_dump_stack_liveness(xbt_fifo_t stack)
{
-
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
mc_pair_t pair;
-
- MC_SET_MC_HEAP;
while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
MC_pair_delete(pair);
- MC_SET_STD_HEAP;
-
- if (raw_mem_set)
- MC_SET_MC_HEAP;
-
+ mmalloc_set_current_heap(heap);
}
}
if (initial_global_state != NULL) {
if (_sg_mc_comms_determinism)
- XBT_INFO("Communication-deterministic : %s",
- !initial_global_state->comm_deterministic ? "No" : "Yes");
+ XBT_INFO("Communication-deterministic : %s", !initial_global_state->comm_deterministic ? "No" : "Yes");
if (_sg_mc_send_determinism)
- XBT_INFO("Send-deterministic : %s",
- !initial_global_state->send_deterministic ? "No" : "Yes");
+ XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes");
}
- mmalloc_set_current_heap(previous_heap);
-}
-
-void MC_assert(int prop)
-{
- if (MC_is_active() && !prop) {
- XBT_INFO("**************************");
- XBT_INFO("*** PROPERTY NOT VALID ***");
- XBT_INFO("**************************");
- XBT_INFO("Counter-example execution trace:");
- MC_record_dump_path(mc_stack);
- MC_dump_stack_safety(mc_stack);
- MC_print_statistics(mc_stats);
- xbt_abort();
- }
-}
-
-void MC_cut(void)
-{
- user_max_depth_reached = 1;
+ mmalloc_set_current_heap(heap);
}
void MC_automaton_load(const char *file)
return values;
}
--
- static mc_visited_pair_t is_reached_acceptance_pair(int pair_num,
- xbt_automaton_state_t
- automaton_state,
- xbt_dynar_t
- atomic_propositions)
- {
-static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair){
-
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
++static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) {
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- mc_visited_pair_t pair = NULL;
- pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
- pair->acceptance_pair = 1;
+ mc_visited_pair_t new_pair = NULL;
+ new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
+ new_pair->acceptance_pair = 1;
if (xbt_dynar_is_empty(acceptance_pairs)) {
} */
cursor = min;
- while (cursor <= max) {
- pair_test =
- (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, cursor,
- mc_visited_pair_t);
- if (xbt_automaton_state_compare
- (pair_test->automaton_state, pair->automaton_state) == 0) {
- if (xbt_automaton_propositional_symbols_compare_value
- (pair_test->atomic_propositions,
- pair->atomic_propositions) == 0) {
- if (snapshot_compare(pair_test, pair) == 0) {
- XBT_INFO("Pair %d already reached (equal to pair %d) !",
- pair->num, pair_test->num);
-
- xbt_fifo_shift(mc_stack);
- if (dot_output != NULL)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- initial_global_state->prev_pair, pair_test->num,
- initial_global_state->prev_req);
- mmalloc_set_current_heap(heap);
- return NULL;
+ if(pair->search_cycle == 1){
+ while (cursor <= max) {
+ pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_pair->atomic_propositions) == 0) {
+ if (snapshot_compare(pair_test, new_pair) == 0) {
+ XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
+ xbt_fifo_shift(mc_stack);
+ if (dot_output != NULL)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
-
- if (!raw_mem_set)
- MC_SET_STD_HEAP;
-
++ mmalloc_set_current_heap(heap);
+ return NULL;
+ }
}
}
+ cursor++;
}
- cursor++;
}
- xbt_dynar_insert_at(acceptance_pairs, min, &pair);
+ xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
} else {
- pair_test =
- (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index,
- mc_visited_pair_t);
- if (pair_test->nb_processes < pair->nb_processes) {
- xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
+ pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
+ if (pair_test->nb_processes < new_pair->nb_processes) {
+ xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
} else {
- if (pair_test->heap_bytes_used < pair->heap_bytes_used)
- xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
+ if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
+ xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
else
- xbt_dynar_insert_at(acceptance_pairs, index, &pair);
+ xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
}
}
}
-
- if (!raw_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
- return pair;
+ return new_pair;
-
}
-static void remove_acceptance_pair(int pair_num) {
-
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+static void remove_acceptance_pair(int pair_num)
+{
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
unsigned int cursor = 0;
mc_visited_pair_t pair_test = NULL;
}
}
- xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
+ if(pair_found == 1) {
+ xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
+
+ pair_test->acceptance_removed = 1;
- pair_test->acceptance_removed = 1;
+ if (_sg_mc_visited == 0 || pair_test->visited_removed == 1)
+ MC_visited_pair_delete(pair_test);
- if (_sg_mc_visited == 0) {
- MC_visited_pair_delete(pair_test);
- } else if (pair_test->visited_removed == 1) {
- MC_visited_pair_delete(pair_test);
}
- if (!raw_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
}
case 3:{
unsigned int cursor = 0;
xbt_automaton_propositional_symbol_t p = NULL;
- xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor,
- p) {
+ xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p) {
- if (strcmp(p->pred, l->u.predicat) == 0)
+ if (strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
- return (int) xbt_dynar_get_as(atomic_propositions_values, cursor,
- int);
+ return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int);
}
return -1;
}
}
}
+ MC_SET_STD_HEAP;
+
+ MC_modelcheck_liveness();
+
if (initial_global_state->raw_mem_set)
MC_SET_MC_HEAP;
- else
- MC_SET_STD_HEAP;
-
-
}
-void MC_modelcheck_liveness() {
--
+void MC_modelcheck_liveness()
+{
- smx_process_t process;
+ smx_process_t process = NULL;
mc_pair_t current_pair = NULL;
-
- if (xbt_fifo_size(mc_stack) == 0)
- return;
-
- /* Get current pair */
- current_pair =
- (mc_pair_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
-
- /* Update current state in buchi automaton */
- _mc_property_automaton->current_state = current_pair->automaton_state;
-
- XBT_DEBUG
- ("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)",
- xbt_fifo_size(mc_stack), current_pair->search_cycle,
- MC_state_interleave_size(current_pair->graph_state), current_pair->num);
-
- mc_stats->visited_pairs++;
-
- int value;
+ int value, res, visited_num = -1;
smx_simcall_t req = NULL;
-
- xbt_automaton_transition_t transition_succ;
- unsigned int cursor = 0;
- int res;
- int visited_num;
-
+ xbt_automaton_transition_t transition_succ = NULL;
+ int cursor = 0;
mc_pair_t next_pair = NULL;
xbt_dynar_t prop_values = NULL;
mc_visited_pair_t reached_pair = NULL;
mc_state_t initial_state = NULL;
smx_process_t process;
- /* Create the initial state and push it into the exploration stack */
- if (!mc_mem_set)
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if (_sg_mc_visited > 0)
- visited_states =
- xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
-
- if (mc_reduce_kind == e_mc_reduce_dpor)
- first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
+ visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
initial_state = MC_state_new();
}
xbt_fifo_unshift(mc_stack, initial_state);
--
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- /* To ensure the soundness of DPOR, we have to keep a list of
- processes which are still enabled at each step of the exploration.
- If max depth is reached, we interleave them in the state in which they have
- been enabled for the first time. */
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- char *key = bprintf("%lu", process->pid);
- char *data = bprintf("%d", xbt_fifo_size(mc_stack));
- xbt_dict_set(first_enabled_state, key, data, NULL);
- xbt_free(key);
- }
- }
- }
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
}
return new_state;
}
-
- mc_visited_pair_t MC_visited_pair_new(int pair_num,
- xbt_automaton_state_t automaton_state,
- xbt_dynar_t atomic_propositions)
+ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
{
+ mc_process_t process = &(mc_model_checker->process);
mc_visited_pair_t pair = NULL;
pair = xbt_new0(s_mc_visited_pair_t, 1);
- pair->graph_state = MC_state_new();
- pair->graph_state->system_state = MC_take_snapshot(pair_num);
+ pair->graph_state = graph_state;
+ if(pair->graph_state->system_state == NULL)
+ pair->graph_state->system_state = MC_take_snapshot(pair_num);
- pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+ pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
+ MC_process_get_heap(process)->heaplimit,
+ MC_process_get_malloc_info(process));
pair->nb_processes = xbt_swag_size(simix_global->process_list);
pair->automaton_state = automaton_state;
pair->num = pair_num;
}
}
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
mc_visited_state_t new_state = visited_state_new();
+ graph_state->system_state = new_state->system_state;
+ graph_state->in_visited_states = 1;
+ XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
if (xbt_dynar_is_empty(visited_states)) {
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
- new_state->other_num = state_test->other_num;
- if (dot_output == NULL)
- 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 (with a bigger num)
- (when the max number of visited states is reached, the oldest
- one is removed according to its number (= with the min number) */
- xbt_dynar_remove_at(visited_states, cursor, NULL);
- xbt_dynar_insert_at(visited_states, cursor, &new_state);
-
- mmalloc_set_current_heap(heap);
- return state_test;
+ if(!partial_comm && initial_global_state->initial_communications_pattern_done){
+
+ 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
+ new_state->other_num = state_test->other_num;
+ if (dot_output == NULL)
+ 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 (with a bigger num)
+ (when the max number of visited states is reached, the oldest
+ one is removed according to its number (= with the min number) */
+ xbt_dynar_remove_at(visited_states, cursor, NULL);
+ xbt_dynar_insert_at(visited_states, cursor, &new_state);
+ XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
+
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
++ mmalloc_set_current_heap(heap);
+ return state_test;
+ }
+ cursor++;
}
- cursor++;
}
-
- // The state has not been visited: insert the state in the dynamic array.
+
xbt_dynar_insert_at(visited_states, min, &new_state);
-
+ XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
+
} else {
// The state has not been visited: insert the state in the dynamic array.
// and drop it:
xbt_dynar_remove_at(visited_states, index2, NULL);
+ XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return NULL;
-
}
}
if (_sg_mc_visited == 0)
return -1;
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- mc_visited_pair_t new_pair = NULL;
+ mc_visited_pair_t new_visited_pair = NULL;
- if (pair == NULL) {
- new_pair =
- MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+ if (visited_pair == NULL) {
+ new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
} else {
- new_pair = pair;
+ new_visited_pair = visited_pair;
}
if (xbt_dynar_is_empty(visited_pairs)) {
} else {
MC_visited_pair_delete(pair_test);
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
- return new_pair->other_num;
+ return new_visited_pair->other_num;
}
}
}
