src/mc/mc_request.c
src/mc/mc_state.c
src/mc/memory_map.c
+ src/mc/mc_pair.c
)
set(headers_to_install
SG_BEGIN_DECL()
-typedef struct xbt_state {
+typedef struct xbt_automaton_state {
char* id;
int type; /* -1 = init, 0 = inter, 1 = final */
xbt_dynar_t in;
xbt_dynar_t out;
-} s_xbt_state;
+} s_xbt_automaton_state;
-typedef struct xbt_state* xbt_state_t;
+typedef struct xbt_automaton_state* xbt_automaton_state_t;
typedef struct xbt_automaton {
xbt_dynar_t propositional_symbols;
xbt_dynar_t transitions;
xbt_dynar_t states;
- xbt_state_t current_state;
+ xbt_automaton_state_t current_state;
} s_xbt_automaton;
typedef struct xbt_automaton* xbt_automaton_t;
-typedef struct xbt_exp_label{
+typedef struct xbt_automaton_exp_label{
enum{or=0, and=1, not=2, predicat=3, one=4} type;
union{
struct{
- struct xbt_exp_label* left_exp;
- struct xbt_exp_label* right_exp;
+ struct xbt_automaton_exp_label* left_exp;
+ struct xbt_automaton_exp_label* right_exp;
}or_and;
- struct xbt_exp_label* exp_not;
+ struct xbt_automaton_exp_label* exp_not;
char* predicat;
}u;
-} s_xbt_exp_label;
+} s_xbt_automaton_exp_label;
-typedef struct xbt_exp_label* xbt_exp_label_t;
+typedef struct xbt_automaton_exp_label* xbt_automaton_exp_label_t;
-typedef struct xbt_transition {
- xbt_state_t src;
- xbt_state_t dst;
- xbt_exp_label_t label;
-} s_xbt_transition;
+typedef struct xbt_automaton_transition {
+ xbt_automaton_state_t src;
+ xbt_automaton_state_t dst;
+ xbt_automaton_exp_label_t label;
+} s_xbt_automaton_transition;
-typedef struct xbt_transition* xbt_transition_t;
+typedef struct xbt_automaton_transition* xbt_automaton_transition_t;
-typedef struct xbt_propositional_symbol{
+typedef struct xbt_automaton_propositional_symbol{
char* pred;
void* function;
-} s_xbt_propositional_symbol;
+} s_xbt_automaton_propositional_symbol;
-typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t;
+typedef struct xbt_automaton_propositional_symbol* xbt_automaton_propositional_symbol_t;
XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void);
XBT_PUBLIC(void) xbt_automaton_load(xbt_automaton_t automaton, const char *file);
-XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_state_new(xbt_automaton_t a, int type, char* id);
-XBT_PUBLIC(xbt_transition_t) xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label);
+XBT_PUBLIC(xbt_automaton_transition_t) xbt_automaton_transition_new(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst, xbt_automaton_exp_label_t label);
-XBT_PUBLIC(xbt_exp_label_t) xbt_automaton_new_label(int type, ...);
+XBT_PUBLIC(xbt_automaton_exp_label_t) xbt_automaton_exp_label_new(int type, ...);
XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_states(xbt_automaton_t a);
XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_transitions(xbt_automaton_t a);
-XBT_PUBLIC(xbt_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst);
+XBT_PUBLIC(xbt_automaton_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst);
-XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_source(xbt_transition_t t);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_transition_get_source(xbt_automaton_transition_t t);
-XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_destination(xbt_transition_t t);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_transition_get_destination(xbt_automaton_transition_t t);
-XBT_PUBLIC(void) xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src);
+XBT_PUBLIC(void) xbt_automaton_transition_set_source(xbt_automaton_transition_t t, xbt_automaton_state_t src);
-XBT_PUBLIC(void) xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst);
+XBT_PUBLIC(void) xbt_automaton_transition_set_destination(xbt_automaton_transition_t t, xbt_automaton_state_t dst);
-XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_out_transitions(xbt_state_t s);
+XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_out_transitions(xbt_automaton_state_t s);
-XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_in_transitions(xbt_state_t s);
+XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_in_transitions(xbt_automaton_state_t s);
-XBT_PUBLIC(xbt_state_t) xbt_automaton_state_exists(xbt_automaton_t a, char *id);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_state_exists(xbt_automaton_t a, char *id);
XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a);
-XBT_PUBLIC(void) xbt_automaton_display_exp(xbt_exp_label_t l);
+XBT_PUBLIC(void) xbt_automaton_exp_label_display(xbt_automaton_exp_label_t l);
-XBT_PUBLIC(xbt_propositional_symbol_t) xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct);
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct);
-XBT_PUBLIC(xbt_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
-XBT_PUBLIC(int) automaton_state_compare(xbt_state_t s1, xbt_state_t s2);
+XBT_PUBLIC(int) xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2);
-XBT_PUBLIC(int) propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2);
+XBT_PUBLIC(int) xbt_automaton_propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2);
-XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2);
+XBT_PUBLIC(int) xbt_automaton_transition_compare(const void *t1, const void *t2);
-XBT_PUBLIC(int) automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2);
+XBT_PUBLIC(int) xbt_automaton_exp_label_compare(xbt_automaton_exp_label_t l1, xbt_automaton_exp_label_t l2);
-XBT_PUBLIC(void) xbt_state_free_voidp(void *s);
+XBT_PUBLIC(void) xbt_automaton_state_free_voidp(void *s);
-XBT_PUBLIC(void) xbt_state_free(xbt_state_t s);
+XBT_PUBLIC(void) xbt_automaton_state_free(xbt_automaton_state_t s);
-XBT_PUBLIC(void) xbt_transition_free_voidp(void *t);
+XBT_PUBLIC(void) xbt_automaton_transition_free_voidp(void *t);
-XBT_PUBLIC(void) xbt_exp_label_free_voidp(void *e);
+XBT_PUBLIC(void) xbt_automaton_exp_label_free_voidp(void *e);
-XBT_PUBLIC(void) xbt_propositional_symbol_free_voidp(void *ps);
+XBT_PUBLIC(void) xbt_automaton_propositional_symbol_free_voidp(void *ps);
XBT_PUBLIC(void) xbt_automaton_free(xbt_automaton_t a);
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013 Da 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. */
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2012-2013 Da 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. */
return 0;
}
-static int compare_global_variables(int region_type, void *d1, void *d2){
+static int compare_global_variables(int region_type, void *d1, void *d2){ /* region_type = 1 -> libsimgrid, region_type = 2 -> binary */
unsigned int cursor = 0;
size_t offset;
#ifdef MC_VERBOSE
XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
#endif
-
+
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
#ifdef MC_VERBOSE
XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
#endif
-
+
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
#ifdef MC_VERBOSE
XBT_VERB("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global);
#endif
-
+
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
#ifdef MC_VERBOSE
XBT_VERB("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local);
#endif
-
+
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
#ifdef MC_VERBOSE
XBT_VERB("Different global variables in binary");
#endif
-
+
reset_heap_information();
xbt_os_timer_free(timer);
xbt_os_timer_stop(global_timer);
#ifdef MC_DEBUG
XBT_DEBUG("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
#endif
+
xbt_dynar_free(&s_tokens1);
xbt_dynar_free(&s_tokens2);
xbt_dynar_free(&tokens1);
-/* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013. Da 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. */
xbt_dynar_t visited_states;
static int is_visited_state(void);
-static void visited_state_free(mc_safety_visited_state_t state);
+static void visited_state_free(mc_visited_state_t state);
static void visited_state_free_voidp(void *s);
-static void visited_state_free(mc_safety_visited_state_t state){
+static void visited_state_free(mc_visited_state_t state){
if(state){
MC_free_snapshot(state->system_state);
xbt_free(state);
}
static void visited_state_free_voidp(void *s){
- visited_state_free((mc_safety_visited_state_t) * (void **) s);
+ visited_state_free((mc_visited_state_t) * (void **) s);
}
static int is_visited_state(){
MC_SET_RAW_MEM;
- mc_safety_visited_state_t new_state = NULL;
- new_state = xbt_new0(s_mc_safety_visited_state_t, 1);
+ mc_visited_state_t new_state = NULL;
+ new_state = xbt_new0(s_mc_visited_state_t, 1);
new_state->system_state = MC_take_snapshot();
new_state->num = mc_stats->expanded_states;
int start = 0;
int end = xbt_dynar_length(visited_states) - 1;
- mc_safety_visited_state_t state_test = NULL;
+ mc_visited_state_t state_test = NULL;
size_t bytes_used_test;
int same_bytes_not_found = 1;
while(start <= end && same_bytes_not_found){
cursor = (start + end) / 2;
- state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
+ state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
bytes_used_test = state_test->system_state->heap_bytes_used;
if(bytes_used_test < current_bytes_used)
start = cursor + 1;
/* Search another state with same number of bytes used */
previous_cursor = cursor - 1;
while(previous_cursor >= 0){
- state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
+ state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_visited_state_t);
bytes_used_test = state_test->system_state->heap_bytes_used;
if(bytes_used_test != current_bytes_used)
break;
}
next_cursor = cursor + 1;
while(next_cursor < xbt_dynar_length(visited_states)){
- state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
+ state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_visited_state_t);
bytes_used_test = state_test->system_state->heap_bytes_used;
if(bytes_used_test != current_bytes_used)
break;
}
}
- state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
+ state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
bytes_used_test = state_test->system_state->heap_bytes_used;
if(bytes_used_test < current_bytes_used)
MC_SET_RAW_MEM;
initial_state = MC_state_new();
- visited_states = xbt_dynar_new(sizeof(mc_safety_visited_state_t), visited_state_free_voidp);
+ visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
MC_UNSET_RAW_MEM;
}
-
-
xbt_fifo_unshift(mc_stack_safety, next_state);
MC_UNSET_RAW_MEM;
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013 Da 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. */
double *mc_time = NULL;
mc_comparison_times_t mc_comp_times = NULL;
double mc_snapshot_comparison_time;
+mc_stats_t mc_stats = NULL;
/* Safety */
xbt_fifo_t mc_stack_safety = NULL;
-mc_stats_t mc_stats = NULL;
mc_global_t initial_state_safety = NULL;
/* Liveness */
-mc_stats_pair_t mc_stats_pair = NULL;
xbt_fifo_t mc_stack_liveness = NULL;
mc_global_t initial_state_liveness = NULL;
int compare;
MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
MC_SET_RAW_MEM;
-
+
/* Initialize statistics */
- mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
+ mc_stats = xbt_new0(s_mc_stats_t, 1);
+ mc_stats->state_size = 1;
/* Create exploration stack */
mc_stack_liveness = xbt_fifo_new();
+ /* Create the initial state */
initial_state_liveness = xbt_new0(s_mc_global_t, 1);
MC_UNSET_RAW_MEM;
MC_ddfs_init();
/* We're done */
- MC_print_statistics_pairs(mc_stats_pair);
+ MC_print_statistics(mc_stats);
xbt_free(mc_time);
if(raw_mem_set)
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item;
mc_state_t state;
- mc_pair_stateless_t pair;
+ mc_pair_t pair;
int depth = 1;
XBT_DEBUG("**** Begin Replay ****");
while(depth <= xbt_fifo_size(stack)){
- pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
+ pair = (mc_pair_t) xbt_fifo_get_item_content(item);
state = (mc_state_t) pair->graph_state;
if(pair->requests > 0){
depth++;
/* Update statistics */
- mc_stats_pair->visited_pairs++;
+ mc_stats->visited_states++;
+ mc_stats->executed_transitions++;
item = xbt_fifo_get_prev_item(item);
}
item != xbt_fifo_get_first_item(stack);
item = xbt_fifo_get_prev_item(item)) {
- pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
+ pair = (mc_pair_t) xbt_fifo_get_item_content(item);
state = (mc_state_t) pair->graph_state;
if(pair->requests > 0){
depth++;
/* Update statistics */
- mc_stats_pair->visited_pairs++;
+ mc_stats->visited_states++;
+ mc_stats->executed_transitions++;
}
}
void MC_show_stack_liveness(xbt_fifo_t stack){
int value;
- mc_pair_stateless_t pair;
+ mc_pair_t pair;
xbt_fifo_item_t item;
smx_simcall_t req;
char *req_str = NULL;
for (item = xbt_fifo_get_last_item(stack);
- (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
+ (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
: (NULL)); item = xbt_fifo_get_prev_item(item)) {
req = MC_state_get_executed_request(pair->graph_state, &value);
if(req){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- mc_pair_stateless_t pair;
+ mc_pair_t pair;
MC_SET_RAW_MEM;
- while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
- pair_stateless_free(pair);
+ while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
+ MC_pair_delete(pair);
MC_UNSET_RAW_MEM;
if(raw_mem_set)
(double)stats->expanded_states / stats->state_size); */
}
-void MC_print_statistics_pairs(mc_stats_pair_t stats)
-{
- 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_pairs / stats->expanded_pairs);
-
- if(mmalloc_get_current_heap() == raw_heap)
- MC_UNSET_RAW_MEM;
-}
-
void MC_assert(int prop)
{
if (MC_is_active() && !prop){
//XBT_INFO("Counter-example execution trace:");
MC_show_stack_liveness(mc_stack_liveness);
//MC_dump_snapshot_stack(mc_snapshot_stack);
- MC_print_statistics_pairs(mc_stats_pair);
+ MC_print_statistics(mc_stats);
xbt_abort();
}
}
if (_mc_property_automaton == NULL)
_mc_property_automaton = xbt_automaton_new();
- xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
+ xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
MC_UNSET_RAW_MEM;
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
-
+
unsigned int cursor = 0;
int start = 0;
int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2011-2013 Da 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. */
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
-xbt_dynar_t reached_pairs;
+/********* Global variables *********/
+
+xbt_dynar_t acceptance_pairs;
xbt_dynar_t visited_pairs;
xbt_dynar_t successors;
-int create_dump(int pair)
-{
- // Try to enable core dumps
- struct rlimit core_limit;
- core_limit.rlim_cur = RLIM_INFINITY;
- core_limit.rlim_max = RLIM_INFINITY;
-
- if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
- fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
-
- int status;
- switch(fork()){
- case 0:
- // We are the child process -- run the actual program
- xbt_abort();
- break;
-
- case -1:
- // An error occurred, shouldn't happen
- perror("fork");
- return -1;
-
- default:
- // We are the parent process -- wait for the child process to exit
- if(wait(&status) < 0)
- perror("wait");
- if(WIFSIGNALED(status) && WCOREDUMP(status)){
- char *core_name = xbt_malloc(20);
- sprintf(core_name,"core_%d", pair);
- rename("core", core_name);
- free(core_name);
- }
- }
- return 0;
-}
+/********* Static functions *********/
-int reached(xbt_state_t st){
+static int is_reached_acceptance_pair(xbt_automaton_state_t st){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
- mc_pair_reached_t new_pair = NULL;
- new_pair = xbt_new0(s_mc_pair_reached_t, 1);
- new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
+ mc_acceptance_pair_t new_pair = NULL;
+ new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
+ new_pair->num = xbt_dynar_length(acceptance_pairs) + 1;
new_pair->automaton_state = st;
new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
new_pair->system_state = MC_take_snapshot();
int res;
int_f_void_t f;
unsigned int cursor = 0;
- xbt_propositional_symbol_t ps = NULL;
+ xbt_automaton_propositional_symbol_t ps = NULL;
xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
f = (int_f_void_t)ps->function;
res = f();
MC_UNSET_RAW_MEM;
- if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
+ if(xbt_dynar_is_empty(acceptance_pairs)){
MC_SET_RAW_MEM;
- /* New pair reached */
- xbt_dynar_push(reached_pairs, &new_pair);
+ /* New acceptance pair */
+ xbt_dynar_push(acceptance_pairs, &new_pair);
MC_UNSET_RAW_MEM;
if(raw_mem_set)
MC_SET_RAW_MEM;
cursor = 0;
- mc_pair_reached_t pair_test = NULL;
+ mc_acceptance_pair_t pair_test = NULL;
- xbt_dynar_foreach(reached_pairs, cursor, pair_test){
+ xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
- XBT_DEBUG("****** Pair reached #%d ******", pair_test->nb);
- if(automaton_state_compare(pair_test->automaton_state, st) == 0){
- if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+ XBT_DEBUG("****** Pair reached #%d ******", pair_test->num);
+ if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
+ if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
if(raw_mem_set)
}
}
- /* New pair reached */
- xbt_dynar_push(reached_pairs, &new_pair);
+ /* New acceptance pair */
+ xbt_dynar_push(acceptance_pairs, &new_pair);
MC_UNSET_RAW_MEM;
}
-void set_pair_reached(xbt_state_t st){
+static void set_acceptance_pair_reached(xbt_automaton_state_t st){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
- mc_pair_reached_t pair = NULL;
- pair = xbt_new0(s_mc_pair_reached_t, 1);
- pair->nb = xbt_dynar_length(reached_pairs) + 1;
+ mc_acceptance_pair_t pair = NULL;
+ pair = xbt_new0(s_mc_acceptance_pair_t, 1);
+ pair->num = xbt_dynar_length(acceptance_pairs) + 1;
pair->automaton_state = st;
pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
pair->system_state = MC_take_snapshot();
/* Get values of propositional symbols */
unsigned int cursor = 0;
- xbt_propositional_symbol_t ps = NULL;
+ xbt_automaton_propositional_symbol_t ps = NULL;
int res;
int_f_void_t f;
xbt_dynar_push_as(pair->prop_ato, int, res);
}
- xbt_dynar_push(reached_pairs, &pair);
+ xbt_dynar_push(acceptance_pairs, &pair);
MC_UNSET_RAW_MEM;
}
-int visited(xbt_state_t st){
+static int is_visited_pair(xbt_automaton_state_t st){
if(_sg_mc_visited == 0)
return 0;
MC_SET_RAW_MEM;
- mc_pair_visited_t new_pair = NULL;
- new_pair = xbt_new0(s_mc_pair_visited_t, 1);
+ mc_visited_pair_t new_pair = NULL;
+ new_pair = xbt_new0(s_mc_visited_pair_t, 1);
new_pair->automaton_state = st;
new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
new_pair->system_state = MC_take_snapshot();
int res;
int_f_void_t f;
unsigned int cursor = 0;
- xbt_propositional_symbol_t ps = NULL;
+ xbt_automaton_propositional_symbol_t ps = NULL;
xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
f = (int_f_void_t)ps->function;
res = f();
MC_SET_RAW_MEM;
cursor = 0;
- mc_pair_visited_t pair_test = NULL;
+ mc_visited_pair_t pair_test = NULL;
xbt_dynar_foreach(visited_pairs, cursor, pair_test){
if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
- if(automaton_state_compare(pair_test->automaton_state, st) == 0){
- if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+ if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
+ if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
if(raw_mem_set)
MC_SET_RAW_MEM;
}
}
-void MC_pair_delete(mc_pair_t pair){
- xbt_free(pair->graph_state->proc_status);
- xbt_free(pair->graph_state);
- xbt_free(pair);
-}
-
-
-
-int MC_automaton_evaluate_label(xbt_exp_label_t l){
+static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
switch(l->type){
case 0 : {
}
case 3 : {
unsigned int cursor = 0;
- xbt_propositional_symbol_t p = NULL;
+ xbt_automaton_propositional_symbol_t p = NULL;
int_f_void_t f;
xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
if(strcmp(p->pred, l->u.predicat) == 0){
}
-/********************* Double-DFS stateless *******************/
+/********* Free functions *********/
-void pair_visited_free(mc_pair_visited_t pair){
+static void visited_pair_free(mc_visited_pair_t pair){
if(pair){
xbt_dynar_free(&(pair->prop_ato));
MC_free_snapshot(pair->system_state);
}
}
-void pair_visited_free_voidp(void *p){
- pair_visited_free((mc_pair_visited_t) * (void **) p);
+static void visited_pair_free_voidp(void *p){
+ visited_pair_free((mc_visited_pair_t) * (void **) p);
}
-void pair_stateless_free(mc_pair_stateless_t pair){
- xbt_free(pair->graph_state->system_state);
- xbt_free(pair->graph_state->proc_status);
- xbt_free(pair->graph_state);
- xbt_free(pair);
-}
-
-void pair_stateless_free_voidp(void *p){
- pair_stateless_free((mc_pair_stateless_t) * (void **) p);
-}
-
-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
- mc_pair_stateless_t p = NULL;
- p = xbt_new0(s_mc_pair_stateless_t, 1);
- p->automaton_state = st;
- p->graph_state = sg;
- p->requests = r;
- mc_stats_pair->expanded_pairs++;
- return p;
-}
-
-void pair_reached_free(mc_pair_reached_t pair){
+static void acceptance_pair_free(mc_acceptance_pair_t pair){
if(pair){
xbt_dynar_free(&(pair->prop_ato));
MC_free_snapshot(pair->system_state);
}
}
-void pair_reached_free_voidp(void *p){
- pair_reached_free((mc_pair_reached_t) * (void **) p);
+static void acceptance_pair_free_voidp(void *p){
+ acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);
}
+
+/********* DDFS Algorithm *********/
+
+
void MC_ddfs_init(void){
initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
XBT_DEBUG("Double-DFS init");
XBT_DEBUG("**************************************************");
- mc_pair_stateless_t mc_initial_pair = NULL;
+ mc_pair_t mc_initial_pair = NULL;
mc_state_t initial_graph_state = NULL;
smx_process_t process;
MC_SET_RAW_MEM;
- initial_graph_state = MC_state_pair_new();
+ initial_graph_state = MC_state_new();
xbt_swag_foreach(process, simix_global->process_list){
if(MC_process_is_enabled(process)){
MC_state_interleave_process(initial_graph_state, process);
}
}
- reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
- visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), pair_visited_free_voidp);
- successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+ acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp);
+ visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp);
+ successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
/* Save the initial state */
initial_state_liveness->snapshot = MC_take_snapshot();
MC_UNSET_RAW_MEM;
unsigned int cursor = 0;
- xbt_state_t state;
+ xbt_automaton_state_t automaton_state;
- xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
- if(state->type == -1){
+ xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
+ if(automaton_state->type == -1){
MC_SET_RAW_MEM;
- mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+ mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
MC_UNSET_RAW_MEM;
MC_ddfs(0);
}else{
- if(state->type == 2){
+ if(automaton_state->type == 2){
MC_SET_RAW_MEM;
- mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+ mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
MC_UNSET_RAW_MEM;
- set_pair_reached(state);
+ set_acceptance_pair_reached(automaton_state);
if(cursor != 0){
MC_restore_snapshot(initial_state_liveness->snapshot);
void MC_ddfs(int search_cycle){
- //initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
smx_process_t process;
- mc_pair_stateless_t current_pair = NULL;
+ mc_pair_t current_pair = NULL;
if(xbt_fifo_size(mc_stack_liveness) == 0)
return;
/* Get current pair */
- current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
+ current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
/* Update current state in buchi automaton */
_mc_property_automaton->current_state = current_pair->automaton_state;
XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
- mc_stats_pair->visited_pairs++;
-
- //sleep(1);
+ mc_stats->visited_states++;
int value;
mc_state_t next_graph_state = NULL;
smx_simcall_t req = NULL;
char *req_str;
- xbt_transition_t transition_succ;
+ xbt_automaton_transition_t transition_succ;
unsigned int cursor = 0;
int res;
- mc_pair_stateless_t next_pair = NULL;
- mc_pair_stateless_t pair_succ;
+ mc_pair_t next_pair = NULL;
+ mc_pair_t pair_succ;
- mc_pair_stateless_t remove_pair;
- mc_pair_reached_t remove_pair_reached;
+ mc_pair_t pair_to_remove;
+ mc_acceptance_pair_t acceptance_pair_to_remove;
if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
MC_SET_RAW_MEM;
/* Create the new expanded graph_state */
- next_graph_state = MC_state_pair_new();
+ next_graph_state = MC_state_new();
/* Get enabled process and insert it in the interleave set of the next graph_state */
xbt_swag_foreach(process, simix_global->process_list){
if(res == 1){ // enabled transition in automaton
MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
xbt_dynar_push(successors, &next_pair);
MC_UNSET_RAW_MEM;
}
if(res == 2){ // true transition in automaton
MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
xbt_dynar_push(successors, &next_pair);
MC_UNSET_RAW_MEM;
}
if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
- if(reached(pair_succ->automaton_state)){
+ if(is_reached_acceptance_pair(pair_succ->automaton_state)){
XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
XBT_INFO("Counter-example that violates formula :");
MC_show_stack_liveness(mc_stack_liveness);
MC_dump_stack_liveness(mc_stack_liveness);
- MC_print_statistics_pairs(mc_stats_pair);
+ MC_print_statistics(mc_stats);
xbt_abort();
}else{
- if(visited(pair_succ->automaton_state)){
+ if(is_visited_pair(pair_succ->automaton_state)){
XBT_DEBUG("Next pair already visited !");
break;
XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
- XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
MC_SET_RAW_MEM;
xbt_fifo_unshift(mc_stack_liveness, pair_succ);
}else{
- if(visited(pair_succ->automaton_state)){
+ if(is_visited_pair(pair_succ->automaton_state)){
XBT_DEBUG("Next pair already visited !");
break;
}else{
- if(visited(pair_succ->automaton_state)){
+ if(is_visited_pair(pair_succ->automaton_state)){
XBT_DEBUG("Next pair already visited !");
break;
XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
- set_pair_reached(pair_succ->automaton_state);
+ set_acceptance_pair_reached(pair_succ->automaton_state);
search_cycle = 1;
- XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
}
MC_SET_RAW_MEM;
/* Create the new expanded graph_state */
- next_graph_state = MC_state_pair_new();
+ next_graph_state = MC_state_new();
xbt_dynar_reset(successors);
if(res == 1){ // enabled transition in automaton
MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
xbt_dynar_push(successors, &next_pair);
MC_UNSET_RAW_MEM;
}
if(res == 2){ // true transition in automaton
MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
xbt_dynar_push(successors, &next_pair);
MC_UNSET_RAW_MEM;
}
if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
- if(reached(pair_succ->automaton_state)){
+ if(is_reached_acceptance_pair(pair_succ->automaton_state)){
XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
XBT_INFO("Counter-example that violates formula :");
MC_show_stack_liveness(mc_stack_liveness);
MC_dump_stack_liveness(mc_stack_liveness);
- MC_print_statistics_pairs(mc_stats_pair);
+ MC_print_statistics(mc_stats);
xbt_abort();
}else{
- if(visited(pair_succ->automaton_state)){
+ if(is_visited_pair(pair_succ->automaton_state)){
XBT_DEBUG("Next pair already visited !");
break;
XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
- XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
MC_SET_RAW_MEM;
xbt_fifo_unshift(mc_stack_liveness, pair_succ);
}else{
- if(visited(pair_succ->automaton_state)){
+ if(is_visited_pair(pair_succ->automaton_state)){
XBT_DEBUG("Next pair already visited !");
break;
}else{
- if(visited(pair_succ->automaton_state)){
+ if(is_visited_pair(pair_succ->automaton_state)){
XBT_DEBUG("Next pair already visited !");
break;
if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
- set_pair_reached(pair_succ->automaton_state);
+ set_acceptance_pair_reached(pair_succ->automaton_state);
search_cycle = 1;
- XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
}
}else{
XBT_WARN("/!\\ Max depth reached ! /!\\ ");
- if(current_pair->requests > 0){
+ if(MC_state_interleave_size(current_pair->graph_state) > 0){
XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
}
MC_SET_RAW_MEM;
- remove_pair = xbt_fifo_shift(mc_stack_liveness);
- xbt_fifo_remove(mc_stack_liveness, remove_pair);
- remove_pair = NULL;
+ pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
+ xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
+ pair_to_remove = NULL;
if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
- remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
- pair_reached_free(remove_pair_reached);
- remove_pair_reached = NULL;
+ acceptance_pair_to_remove = xbt_dynar_pop_as(acceptance_pairs, mc_acceptance_pair_t);
+ acceptance_pair_free(acceptance_pair_to_remove);
+ acceptance_pair_to_remove = NULL;
}
MC_UNSET_RAW_MEM;
- /*if(initial_state_liveness->raw_mem_set)
- MC_SET_RAW_MEM;*/
-
}
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013 Da 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. */
--- /dev/null
+/* Copyright (c) 2013 Da 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. */
+
+#include "mc_private.h"
+
+mc_pair_t MC_pair_new(mc_state_t gs, xbt_automaton_state_t as, int r){
+ mc_pair_t p = NULL;
+ p = xbt_new0(s_mc_pair_t, 1);
+ p->automaton_state = as;
+ p->graph_state = gs;
+ p->system_state = NULL;
+ p->requests = r;
+ return p;
+}
+
+void MC_pair_delete(mc_pair_t p){
+ p->automaton_state = NULL;
+ if(p->system_state)
+ MC_free_snapshot(p->system_state);
+ MC_state_delete(p->graph_state);
+ xbt_free(p);
+}
-/* Copyright (c) 2007-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2007-2013 Da 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 is_stack_ignore_variable(char *frame, char *var_name);
/********************************* MC Global **********************************/
+
extern double *mc_time;
extern FILE *dot_output;
extern const char* colors[10];
void MC_init_dot_output(void);
int SIMIX_pre_mc_random(smx_simcall_t simcall);
+
/********************************* Requests ***********************************/
+
int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
char* MC_request_to_string(smx_simcall_t req, int value);
unsigned int MC_request_testany_fail(smx_simcall_t req);
/******************************** States **************************************/
+
/* Possible exploration status of a process in a state */
typedef enum {
MC_NOT_INTERLEAVE=0, /* Do not interleave (do not execute) */
smx_simcall_t MC_state_get_request(mc_state_t state, int *value);
void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process);
+
/****************************** Statistics ************************************/
+
typedef struct mc_stats {
unsigned long state_size;
unsigned long visited_states;
unsigned long executed_transitions;
} s_mc_stats_t, *mc_stats_t;
-typedef struct mc_stats_pair {
- //unsigned long pair_size;
- unsigned long visited_pairs;
- unsigned long expanded_pairs;
- unsigned long executed_transitions;
-} s_mc_stats_pair_t, *mc_stats_pair_t;
-
extern mc_stats_t mc_stats;
-extern mc_stats_pair_t mc_stats_pair;
void MC_print_statistics(mc_stats_t);
-void MC_print_statistics_pairs(mc_stats_pair_t);
+
/********************************** MEMORY ******************************/
/* The possible memory modes for the modelchecker are standard and raw. */
#define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap)
#define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap)
+
/******************************* MEMORY MAPPINGS ***************************/
/* These functions and data structures implements a binary interface for */
/* the proc maps ascii interface */
} s_memory_map_t, *memory_map_t;
+
+void MC_init_memory_map_info(void);
memory_map_t get_memory_map(void);
void free_memory_map(memory_map_t map);
void get_libsimgrid_plt_section(void);
extern void *start_got_plt_binary;
extern void *end_got_plt_binary;
+
/********************************** Snapshot comparison **********************************/
typedef struct s_mc_comparison_times{
void print_comparison_times(void);
//#define MC_DEBUG 1
-//#define MC_VERBOSE 1
+#define MC_VERBOSE 1
+
+
+/********************************** DPOR for safety property **************************************/
-/********************************** DPOR for safety **************************************/
typedef enum {
e_mc_reduce_unset,
e_mc_reduce_none,
extern e_mc_reduce_t mc_reduce_kind;
extern mc_global_t initial_state_safety;
+extern xbt_fifo_t mc_stack_safety;
void MC_dpor_init(void);
void MC_dpor(void);
-typedef struct s_mc_safety_visited_state{
+typedef struct s_mc_visited_state{
mc_snapshot_t system_state;
int num;
-}s_mc_safety_visited_state_t, *mc_safety_visited_state_t;
+}s_mc_visited_state_t, *mc_visited_state_t;
-/********************************** Double-DFS for liveness property**************************************/
+/********************************** Double-DFS for liveness property **************************************/
extern xbt_fifo_t mc_stack_liveness;
extern mc_global_t initial_state_liveness;
extern xbt_dynar_t mc_stack_comparison_ignore;
extern xbt_dynar_t mc_data_bss_comparison_ignore;
-
typedef struct s_mc_pair{
mc_snapshot_t system_state;
mc_state_t graph_state;
- xbt_state_t automaton_state;
+ xbt_automaton_state_t automaton_state;
+ int requests;
}s_mc_pair_t, *mc_pair_t;
-typedef struct s_mc_pair_reached{
- int nb;
- xbt_state_t automaton_state;
+typedef struct s_mc_acceptance_pair{
+ int num;
+ xbt_automaton_state_t automaton_state;
xbt_dynar_t prop_ato;
mc_snapshot_t system_state;
-}s_mc_pair_reached_t, *mc_pair_reached_t;
+}s_mc_acceptance_pair_t, *mc_acceptance_pair_t;
-typedef struct s_mc_pair_visited{
- xbt_state_t automaton_state;
+typedef struct s_mc_visited_pair{
+ xbt_automaton_state_t automaton_state;
xbt_dynar_t prop_ato;
mc_snapshot_t system_state;
-}s_mc_pair_visited_t, *mc_pair_visited_t;
-
-int MC_automaton_evaluate_label(xbt_exp_label_t l);
-
-int reached(xbt_state_t st);
-void set_pair_reached(xbt_state_t st);
-int visited(xbt_state_t st);
-
-void MC_pair_delete(mc_pair_t pair);
-mc_state_t MC_state_pair_new(void);
-void pair_reached_free(mc_pair_reached_t pair);
-void pair_reached_free_voidp(void *p);
-void pair_visited_free(mc_pair_visited_t pair);
-void pair_visited_free_voidp(void *p);
-void MC_init_memory_map_info(void);
-
-int get_heap_region_index(mc_snapshot_t s);
-
-/* **** Double-DFS stateless **** */
+ int num;
+}s_mc_visited_pair_t, *mc_visited_pair_t;
-typedef struct s_mc_pair_stateless{
- mc_state_t graph_state;
- xbt_state_t automaton_state;
- int requests;
-}s_mc_pair_stateless_t, *mc_pair_stateless_t;
+mc_pair_t MC_pair_new(mc_state_t sg, xbt_automaton_state_t st, int r);
+void MC_pair_delete(mc_pair_t);
-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r);
void MC_ddfs_init(void);
void MC_ddfs(int search_cycle);
void MC_show_stack_liveness(xbt_fifo_t stack);
void MC_dump_stack_liveness(xbt_fifo_t stack);
-void pair_stateless_free(mc_pair_stateless_t pair);
-void pair_stateless_free_voidp(void *p);
-/********************************** Configuration of MC **************************************/
-extern xbt_fifo_t mc_stack_safety;
-
-/****** Core dump ******/
-int create_dump(int pair);
-
-/****** Local variables with DWARF ******/
+/********************************** Local variables with DWARF **********************************/
typedef enum {
e_dw_loclist,
void print_local_variables(xbt_dict_t list);
xbt_dict_t MC_get_location_list(const char *elf_file);
-/**** Global variables ****/
+
+/********************************** Global variables with objdump **********************************/
typedef struct s_global_variable{
char *name;
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013 Da 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. */
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013 Da 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. */
return state;
}
-mc_state_t MC_state_pair_new(void)
-{
- mc_state_t state = NULL;
-
- state = xbt_new0(s_mc_state_t, 1);
- state->max_pid = simix_process_maxpid;
- state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
-
- //mc_stats->expanded_states++;
- return state;
-}
-
/**
* \brief Deletes a state data structure
* \param trans The state to be deleted
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013 Da 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. */
xbt_automaton_t xbt_automaton_new(){
xbt_automaton_t automaton = NULL;
automaton = xbt_new0(struct xbt_automaton, 1);
- automaton->states = xbt_dynar_new(sizeof(xbt_state_t), xbt_state_free_voidp);
- automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
- automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), xbt_propositional_symbol_free_voidp);
+ automaton->states = xbt_dynar_new(sizeof(xbt_automaton_state_t), xbt_automaton_state_free_voidp);
+ automaton->transitions = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp);
+ automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_automaton_propositional_symbol_t), xbt_automaton_propositional_symbol_free_voidp);
return automaton;
}
-xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){
- xbt_state_t state = NULL;
- state = xbt_new0(struct xbt_state, 1);
+xbt_automaton_state_t xbt_automaton_state_new(xbt_automaton_t a, int type, char* id){
+ xbt_automaton_state_t state = NULL;
+ state = xbt_new0(struct xbt_automaton_state, 1);
state->type = type;
state->id = strdup(id);
- state->in = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
- state->out = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
+ state->in = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp);
+ state->out = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp);
xbt_dynar_push(a->states, &state);
return state;
}
-xbt_transition_t xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label){
- xbt_transition_t transition = NULL;
- transition = xbt_new0(struct xbt_transition, 1);
+xbt_automaton_transition_t xbt_automaton_transition_new(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst, xbt_automaton_exp_label_t label){
+ xbt_automaton_transition_t transition = NULL;
+ transition = xbt_new0(struct xbt_automaton_transition, 1);
if(src != NULL){
xbt_dynar_push(src->out, &transition);
transition->src = src;
return transition;
}
-xbt_exp_label_t xbt_automaton_new_label(int type, ...){
- xbt_exp_label_t label = NULL;
- label = xbt_new0(struct xbt_exp_label, 1);
+xbt_automaton_exp_label_t xbt_automaton_exp_label_new(int type, ...){
+ xbt_automaton_exp_label_t label = NULL;
+ label = xbt_new0(struct xbt_automaton_exp_label, 1);
label->type = type;
va_list ap;
va_start(ap, type);
switch(type){
case 0 : {
- xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
- xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
+ xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t);
+ xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t);
label->u.or_and.left_exp = left;
label->u.or_and.right_exp = right;
break;
}
case 1 : {
- xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
- xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
+ xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t);
+ xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t);
label->u.or_and.left_exp = left;
label->u.or_and.right_exp = right;
break;
}
case 2 : {
- xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t);
+ xbt_automaton_exp_label_t exp_not = va_arg(ap, xbt_automaton_exp_label_t);
label->u.exp_not = exp_not;
break;
}
return a->transitions;
}
-xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst){
- xbt_transition_t transition;
+xbt_automaton_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst){
+ xbt_automaton_transition_t transition;
unsigned int cursor;
xbt_dynar_foreach(src->out, cursor, transition){
if((transition->src == src) && (transition->dst == dst))
return NULL;
}
-xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){
+xbt_automaton_state_t xbt_automaton_transition_get_source(xbt_automaton_transition_t t){
return t->src;
}
-xbt_state_t xbt_automaton_transition_get_destination(xbt_transition_t t){
+xbt_automaton_state_t xbt_automaton_transition_get_destination(xbt_automaton_transition_t t){
return t->dst;
}
-void xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src){
+void xbt_automaton_transition_set_source(xbt_automaton_transition_t t, xbt_automaton_state_t src){
t->src = src;
xbt_dynar_push(src->out,&t);
}
-void xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst){
+void xbt_automaton_transition_set_destination(xbt_automaton_transition_t t, xbt_automaton_state_t dst){
t->dst = dst;
xbt_dynar_push(dst->in,&t);
}
-xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_state_t s){
+xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_automaton_state_t s){
return s->out;
}
-xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_state_t s){
+xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_automaton_state_t s){
return s->in;
}
-xbt_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){
- xbt_state_t state = NULL;
+xbt_automaton_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){
+ xbt_automaton_state_t state = NULL;
unsigned int cursor = 0;
xbt_dynar_foreach(a->states, cursor, state){
if(strcmp(state->id, id)==0)
return NULL;
}
-void xbt_automaton_display(xbt_automaton_t a){
+void xbt_automaton_display(xbt_automaton_t a){
unsigned int cursor = 0;
- xbt_state_t state = NULL;
+ xbt_automaton_state_t state = NULL;
printf("\n\nEtat courant : %s\n", a->current_state->id);
}
cursor=0;
- xbt_transition_t transition = NULL;
+ xbt_automaton_transition_t transition = NULL;
printf("\nListe des transitions : %lu\n\n", xbt_dynar_length(a->transitions));
xbt_dynar_foreach(a->transitions, cursor, transition){
printf("label :");
- xbt_automaton_display_exp(transition->label);
+ xbt_automaton_exp_label_display(transition->label);
printf(", %s -> %s\n", transition->src->id, transition->dst->id);
}
}
-void xbt_automaton_display_exp(xbt_exp_label_t label){
+void xbt_automaton_exp_label_display(xbt_automaton_exp_label_t label){
switch(label->type){
case 0 :
printf("(");
- xbt_automaton_display_exp(label->u.or_and.left_exp);
+ xbt_automaton_exp_label_display(label->u.or_and.left_exp);
printf(" || ");
- xbt_automaton_display_exp(label->u.or_and.right_exp);
+ xbt_automaton_exp_label_display(label->u.or_and.right_exp);
printf(")");
break;
case 1 :
printf("(");
- xbt_automaton_display_exp(label->u.or_and.left_exp);
+ xbt_automaton_exp_label_display(label->u.or_and.left_exp);
printf(" && ");
- xbt_automaton_display_exp(label->u.or_and.right_exp);
+ xbt_automaton_exp_label_display(label->u.or_and.right_exp);
printf(")");
break;
case 2 :
printf("(!");
- xbt_automaton_display_exp(label->u.exp_not);
+ xbt_automaton_exp_label_display(label->u.exp_not);
printf(")");
break;
case 3 :
}
-xbt_state_t xbt_automaton_get_current_state(xbt_automaton_t a){
+xbt_automaton_state_t xbt_automaton_get_current_state(xbt_automaton_t a){
return a->current_state;
}
-xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct){
- xbt_propositional_symbol_t prop_symb = NULL;
- prop_symb = xbt_new0(struct xbt_propositional_symbol, 1);
+xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct){
+ xbt_automaton_propositional_symbol_t prop_symb = NULL;
+ prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1);
prop_symb->pred = strdup(id);
prop_symb->function = fct;
xbt_dynar_push(a->propositional_symbols, &prop_symb);
return prop_symb;
}
-int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){
+int xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2){
/* single id for each state, id and type sufficient for comparison*/
}
-int automaton_transition_compare(const void *t1, const void *t2){
+int xbt_automaton_transition_compare(const void *t1, const void *t2){
- if(automaton_state_compare(((xbt_transition_t)t1)->src, ((xbt_transition_t)t2)->src))
+ if(xbt_automaton_state_compare(((xbt_automaton_transition_t)t1)->src, ((xbt_automaton_transition_t)t2)->src))
return 1;
- if(automaton_state_compare(((xbt_transition_t)t1)->dst, ((xbt_transition_t)t2)->dst))
+ if(xbt_automaton_state_compare(((xbt_automaton_transition_t)t1)->dst, ((xbt_automaton_transition_t)t2)->dst))
return 1;
- if(automaton_label_transition_compare(((xbt_transition_t)t1)->label,((xbt_transition_t)t2)->label))
+ if(xbt_automaton_exp_label_compare(((xbt_automaton_transition_t)t1)->label,((xbt_automaton_transition_t)t2)->label))
return 1;
return 0;
}
-int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
+int xbt_automaton_exp_label_compare(xbt_automaton_exp_label_t l1, xbt_automaton_exp_label_t l2){
if(l1->type != l2->type)
return 1;
case 0 : // OR
case 1 : // AND
- if(automaton_label_transition_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp))
+ if(xbt_automaton_exp_label_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp))
return 1;
else
- return automaton_label_transition_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp);
+ return xbt_automaton_exp_label_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp);
break;
case 2 : // NOT
- return automaton_label_transition_compare(l1->u.exp_not, l2->u.exp_not);
+ return xbt_automaton_exp_label_compare(l1->u.exp_not, l2->u.exp_not);
break;
case 3 : // predicat
}
-int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
+int xbt_automaton_propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
int *iptr1, *iptr2;
unsigned int cursor;
/************ Free functions ****************/
-static void xbt_transition_free(xbt_transition_t t);
-static void xbt_exp_label_free(xbt_exp_label_t e);
-static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps);
+static void xbt_automaton_transition_free(xbt_automaton_transition_t t);
+static void xbt_automaton_exp_label_free(xbt_automaton_exp_label_t e);
+static void xbt_automaton_propositional_symbol_free(xbt_automaton_propositional_symbol_t ps);
-void xbt_state_free(xbt_state_t s){
+void xbt_automaton_state_free(xbt_automaton_state_t s){
if(s){
xbt_free(s->id);
xbt_dynar_free(&(s->in));
}
}
-void xbt_state_free_voidp(void *s){
- xbt_state_free((xbt_state_t) * (void **) s);
+void xbt_automaton_state_free_voidp(void *s){
+ xbt_automaton_state_free((xbt_automaton_state_t) * (void **) s);
}
-static void xbt_transition_free(xbt_transition_t t){
+static void xbt_automaton_transition_free(xbt_automaton_transition_t t){
if(t){
- xbt_exp_label_free(t->label);
+ xbt_automaton_exp_label_free(t->label);
xbt_free(t);
t = NULL;
}
}
-void xbt_transition_free_voidp(void *t){
- xbt_transition_free((xbt_transition_t) * (void **) t);
+void xbt_automaton_transition_free_voidp(void *t){
+ xbt_automaton_transition_free((xbt_automaton_transition_t) * (void **) t);
}
-static void xbt_exp_label_free(xbt_exp_label_t e){
+static void xbt_automaton_exp_label_free(xbt_automaton_exp_label_t e){
if(e){
switch(e->type){
case 0:
case 1:
- xbt_exp_label_free(e->u.or_and.left_exp);
- xbt_exp_label_free(e->u.or_and.right_exp);
+ xbt_automaton_exp_label_free(e->u.or_and.left_exp);
+ xbt_automaton_exp_label_free(e->u.or_and.right_exp);
break;
case 2:
- xbt_exp_label_free(e->u.exp_not);
+ xbt_automaton_exp_label_free(e->u.exp_not);
break;
case 3:
xbt_free(e->u.predicat);
}
}
-void xbt_exp_label_free_voidp(void *e){
- xbt_exp_label_free((xbt_exp_label_t) * (void **) e);
+void xbt_automaton_exp_label_free_voidp(void *e){
+ xbt_automaton_exp_label_free((xbt_automaton_exp_label_t) * (void **) e);
}
-static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps){
+static void xbt_automaton_propositional_symbol_free(xbt_automaton_propositional_symbol_t ps){
if(ps){
xbt_free(ps->pred);
xbt_free(ps);
}
}
-void xbt_propositional_symbol_free_voidp(void *ps){
- xbt_propositional_symbol_free((xbt_propositional_symbol_t) * (void **) ps);
+void xbt_automaton_propositional_symbol_free_voidp(void *ps){
+ xbt_automaton_propositional_symbol_free((xbt_automaton_propositional_symbol_t) * (void **) ps);
}
void xbt_automaton_free(xbt_automaton_t a){
xbt_dynar_free(&(a->propositional_symbols));
xbt_dynar_free(&(a->transitions));
xbt_dynar_free(&(a->states));
- xbt_state_free(a->current_state);
+ xbt_automaton_state_free(a->current_state);
xbt_free(a);
a = NULL;
}
}
}
- xbt_state_t state = NULL;
+ xbt_automaton_state_t state = NULL;
state = xbt_automaton_state_exists(parsed_automaton, id_state);
if(state == NULL){
- state = xbt_automaton_new_state(parsed_automaton, type, id_state);
+ state = xbt_automaton_state_new(parsed_automaton, type, id_state);
}
if(type==-1)
}
-static void new_transition(char* id, xbt_exp_label_t label){
+static void new_transition(char* id, xbt_automaton_exp_label_t label){
char* id_state = strdup(id);
- xbt_state_t state_dst = NULL;
+ xbt_automaton_state_t state_dst = NULL;
new_state(id, 0);
state_dst = xbt_automaton_state_exists(parsed_automaton, id_state);
- xbt_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src);
+ xbt_automaton_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src);
//xbt_transition_t trans = NULL;
- xbt_automaton_new_transition(parsed_automaton, state_src, state_dst, label);
+ xbt_automaton_transition_new(parsed_automaton, state_src, state_dst, label);
}
-static xbt_exp_label_t new_label(int type, ...){
- xbt_exp_label_t label = NULL;
+static xbt_automaton_exp_label_t new_label(int type, ...){
+ xbt_automaton_exp_label_t label = NULL;
va_list ap;
va_start(ap,type);
switch(type){
case 0 : {
- xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
- xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
- label = xbt_automaton_new_label(type, left, right);
+ xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t);
+ xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t);
+ label = xbt_automaton_exp_label_new(type, left, right);
break;
}
case 1 : {
- xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
- xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
- label = xbt_automaton_new_label(type, left, right);
+ xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t);
+ xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t);
+ label = xbt_automaton_exp_label_new(type, left, right);
break;
}
case 2 : {
- xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t);
- label = xbt_automaton_new_label(type, exp_not);
+ xbt_automaton_exp_label_t exp_not = va_arg(ap, xbt_automaton_exp_label_t);
+ label = xbt_automaton_exp_label_new(type, exp_not);
break;
}
case 3 : {
char* p = va_arg(ap, char*);
- label = xbt_automaton_new_label(type, p);
+ label = xbt_automaton_exp_label_new(type, p);
break;
}
case 4 : {
- label = xbt_automaton_new_label(type);
+ label = xbt_automaton_exp_label_new(type);
break;
}
}
double real;
int integer;
char* string;
- xbt_exp_label_t label;
+ xbt_automaton_exp_label_t label;
double real;
int integer;
char* string;
- xbt_exp_label_t label;
+ xbt_automaton_exp_label_t label;
}
%token NEVER