XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
-XBT_PUBLIC(void) MC_init_safety(void);
+XBT_PUBLIC(void) MC_init(void);
XBT_PUBLIC(void) MC_exit(void);
XBT_PUBLIC(void) MC_exit_liveness(void);
-XBT_PUBLIC(void) MC_modelcheck(void);
+XBT_PUBLIC(void) MC_modelcheck_safety(void);
XBT_PUBLIC(void) MC_modelcheck_liveness(void);
XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
return;
}
-void MC_take_snapshot(mc_snapshot_t snapshot)
-{
- unsigned int i = 0;
- s_map_region_t reg;
- memory_map_t maps = get_memory_map();
-
- /* Save the std heap and the writable mapped pages of libsimgrid */
- while (i < maps->mapsize) {
- reg = maps->regions[i];
- if ((reg.prot & PROT_WRITE)){
- if (maps->regions[i].pathname == NULL){
- if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one)
- MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
- }
- i++;
- } else {
- if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
- MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
- i++;
- reg = maps->regions[i];
- while(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize){
- MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
- i++;
- reg = maps->regions[i];
- }
- }else{
- i++;
- }
- }
- }else{
- i++;
- }
- }
-
- free_memory_map(maps);
-}
+/* void MC_take_snapshot(mc_snapshot_t snapshot) */
+/* { */
+/* unsigned int i = 0; */
+/* s_map_region_t reg; */
+/* memory_map_t maps = get_memory_map(); */
+
+/* /\* Save the std heap and the writable mapped pages of libsimgrid *\/ */
+/* while (i < maps->mapsize) { */
+/* reg = maps->regions[i]; */
+/* if ((reg.prot & PROT_WRITE)){ */
+/* if (maps->regions[i].pathname == NULL){ */
+/* if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one) */
+/* MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); */
+/* } */
+/* i++; */
+/* } else { */
+/* if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){ */
+/* MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); */
+/* i++; */
+/* reg = maps->regions[i]; */
+/* while(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize){ */
+/* MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); */
+/* i++; */
+/* reg = maps->regions[i]; */
+/* } */
+/* }else{ */
+/* i++; */
+/* } */
+/* } */
+/* }else{ */
+/* i++; */
+/* } */
+/* } */
+
+/* free_memory_map(maps); */
+/* } */
void MC_init_memory_map_info(){
}
-mc_snapshot_t MC_take_snapshot_liveness()
+mc_snapshot_t MC_take_snapshot()
{
int raw_mem = (mmalloc_get_current_heap() == raw_heap);
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
"Logging specific to MC DPOR exploration");
+xbt_dynar_t visited_states;
+
+static int is_visited_state(void);
+
+static int is_visited_state(){
+
+ if(_surf_mc_stateful == 0)
+ return 0;
+
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ mc_snapshot_t new_state = NULL;
+ new_state = MC_take_snapshot();
+
+ MC_UNSET_RAW_MEM;
+
+ if(xbt_dynar_is_empty(visited_states)){
+
+ MC_SET_RAW_MEM;
+ xbt_dynar_push(visited_states, &new_state);
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+ return 0;
+
+ }else{
+
+ MC_SET_RAW_MEM;
+
+ unsigned int cursor = 0;
+ mc_snapshot_t state_test = NULL;
+
+ xbt_dynar_foreach(visited_states, cursor, state_test){
+ if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug))
+ XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
+ if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+
+ return 1;
+ }
+ }
+
+ if(xbt_dynar_length(visited_states) == _surf_mc_stateful){
+ mc_snapshot_t state_to_remove = NULL;
+ xbt_dynar_shift(visited_states, &state_to_remove);
+ MC_free_snapshot(state_to_remove);
+ }
+
+ xbt_dynar_push(visited_states, &new_state);
+
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+ return 0;
+
+ }
+}
+
/**
* \brief Initialize the DPOR exploration algorithm
*/
/* Create the initial state and push it into the exploration stack */
MC_SET_RAW_MEM;
+
initial_state = MC_state_new();
+ visited_states = xbt_dynar_new(sizeof(mc_snapshot_t), NULL);
+
MC_UNSET_RAW_MEM;
XBT_DEBUG("**************************************************");
next_state = MC_state_new();
- xbt_swag_foreach(process, simix_global->process_list){
- if(MC_process_is_enabled(process)){
- XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
+ if(!is_visited_state()){
+
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
+ }
}
- }
-
- /* Get an enabled process and insert it in the interleave set of the next state */
- xbt_swag_foreach(process, simix_global->process_list){
- if(MC_process_is_enabled(process)){
- MC_state_interleave_process(next_state, process);
- break;
+
+ /* Get an enabled process and insert it in the interleave set of the next state */
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ MC_state_interleave_process(next_state, process);
+ break;
+ }
+ }
+
+ if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
+ next_state->system_state = MC_take_snapshot();
}
- }
- if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
- next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot(next_state->system_state);
}
xbt_fifo_unshift(mc_stack_safety, next_state);
mc_state_t mc_current_state = NULL;
char mc_replay_mode = FALSE;
double *mc_time = NULL;
-mc_snapshot_t initial_snapshot = NULL;
/* Safety */
xbt_fifo_t mc_stack_safety = NULL;
mc_stats_t mc_stats = NULL;
+mc_global_t initial_state_safety = NULL;
/* Liveness */
mc_reduce_kind=e_mc_reduce_dpor;
XBT_INFO("Check a safety property");
- MC_modelcheck();
+ MC_modelcheck_safety();
} else {
}
}
-/**
- * \brief Initialize the model-checker data structures
- */
-void MC_init_safety(void)
-{
-
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
- /* Check if MC is already initialized */
- if (initial_snapshot)
- return;
-
- mc_time = xbt_new0(double, simix_process_maxpid);
-
- /* Initialize the data structures that must be persistent across every
- iteration of the model-checker (in RAW memory) */
-
- MC_SET_RAW_MEM;
-
- /* Initialize statistics */
- mc_stats = xbt_new0(s_mc_stats_t, 1);
- mc_stats->state_size = 1;
-
- /* Create exploration stack */
- mc_stack_safety = xbt_fifo_new();
-
- MC_UNSET_RAW_MEM;
-
- MC_dpor_init();
-
- MC_SET_RAW_MEM;
- /* Save the initial state */
- initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot(initial_snapshot);
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
-
-}
void MC_compare(void){
compare = 1;
}
-
-void MC_modelcheck(void)
-{
- MC_init_safety();
- MC_dpor();
- MC_exit();
-}
-
-void MC_init_liveness(){
+void MC_init(){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
xbt_dict_t libsimgrid_location_list = MC_get_location_list(ls_path);
MC_get_local_variables(ls_path, libsimgrid_location_list, &mc_local_variables);
- initial_state_liveness = xbt_new0(s_mc_global_t, 1);
-
MC_UNSET_RAW_MEM;
MC_init_memory_map_info();
}
+void MC_modelcheck_safety(void)
+{
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ /* Check if MC is already initialized */
+ if (initial_state_safety)
+ return;
+
+ mc_time = xbt_new0(double, simix_process_maxpid);
+
+ /* Initialize the data structures that must be persistent across every
+ iteration of the model-checker (in RAW memory) */
+
+ MC_SET_RAW_MEM;
+
+ /* Initialize statistics */
+ mc_stats = xbt_new0(s_mc_stats_t, 1);
+ mc_stats->state_size = 1;
+
+ /* Create exploration stack */
+ mc_stack_safety = xbt_fifo_new();
+
+ MC_UNSET_RAW_MEM;
+
+ if(_surf_mc_stateful > 0)
+ MC_init();
+
+ MC_dpor_init();
+
+ MC_SET_RAW_MEM;
+ /* Save the initial state */
+ initial_state_safety = xbt_new0(s_mc_global_t, 1);
+ initial_state_safety->snapshot = MC_take_snapshot();
+ //MC_take_snapshot(initial_snapshot);
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+ MC_dpor();
+
+ MC_exit();
+}
+
void MC_modelcheck_liveness(){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- MC_init_liveness();
+ MC_init();
MC_SET_RAW_MEM;
/* Initialize statistics */
mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
- XBT_DEBUG("Creating stack");
-
/* Create exploration stack */
mc_stack_liveness = xbt_fifo_new();
+ initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+
MC_UNSET_RAW_MEM;
MC_ddfs_init();
if(start == -1){
/* Restore the initial state */
- MC_restore_snapshot(initial_snapshot);
+ MC_restore_snapshot(initial_state_safety->snapshot);
/* At the moment of taking the snapshot the raw heap was set, so restoring
* it will set it back again, we have to unset it to continue */
MC_UNSET_RAW_MEM;
new_pair->automaton_state = st;
new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
new_pair->comparison_times = new_comparison_times();
- new_pair->system_state = MC_take_snapshot_liveness();
+ new_pair->system_state = MC_take_snapshot();
/* Get values of propositional symbols */
int res;
pair->automaton_state = st;
pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
pair->comparison_times = new_comparison_times();
- pair->system_state = MC_take_snapshot_liveness();
+ pair->system_state = MC_take_snapshot();
/* Get values of propositional symbols */
unsigned int cursor = 0;
new_pair = xbt_new0(s_mc_pair_visited_t, 1);
new_pair->automaton_state = st;
new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- new_pair->system_state = MC_take_snapshot_liveness();
+ new_pair->system_state = MC_take_snapshot();
/* Get values of propositional symbols */
int res;
successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
/* Save the initial state */
- initial_state_liveness->snapshot = MC_take_snapshot_liveness();
+ initial_state_liveness->snapshot = MC_take_snapshot();
MC_UNSET_RAW_MEM;
int raw_mem_set;
}s_mc_global_t, *mc_global_t;
-void MC_take_snapshot(mc_snapshot_t);
-mc_snapshot_t MC_take_snapshot_liveness(void);
+//void MC_take_snapshot(mc_snapshot_t);
+mc_snapshot_t MC_take_snapshot(void);
void MC_restore_snapshot(mc_snapshot_t);
void MC_free_snapshot(mc_snapshot_t);
void snapshot_stack_free_voidp(void *s);
} e_mc_reduce_t;
extern e_mc_reduce_t mc_reduce_kind;
+extern mc_global_t initial_state_safety;
void MC_dpor_init(void);
void MC_dpor(void);
void MC_dpor_exit(void);
-void MC_init_safety(void);
+void MC_init(void);
/********************************** Double-DFS for liveness property**************************************/
#ifdef HAVE_MC
case SIMCALL_MC_SNAPSHOT:
- simcall->mc_snapshot.s = MC_take_snapshot_liveness();
+ simcall->mc_snapshot.s = MC_take_snapshot();
SIMIX_simcall_answer(simcall);
break;
