#include <libgen.h>
#include "private.h"
-static mc_mem_region_t MC_region_new(void *start_addr, size_t size);
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
+ "Logging specific to mc_checkpoint");
+
+static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size);
static void MC_region_restore(mc_mem_region_t reg);
static void MC_region_destroy(mc_mem_region_t reg);
-static void MC_snapshot_add_region(mc_snapshot_t snapshot, void *start_addr, size_t size);
+static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start_addr, size_t size);
-static mc_mem_region_t MC_region_new(void *start_addr, size_t size)
+static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size)
{
mc_mem_region_t new_reg = xbt_new0(s_mc_mem_region_t, 1);
+ new_reg->type = type;
new_reg->start_addr = start_addr;
new_reg->size = size;
new_reg->data = xbt_malloc0(size);
xbt_free(reg);
}
-static void MC_snapshot_add_region(mc_snapshot_t snapshot, void *start_addr, size_t size)
+static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start_addr, size_t size)
{
- mc_mem_region_t new_reg = MC_region_new(start_addr, size);
+ mc_mem_region_t new_reg = MC_region_new(type, start_addr, size);
snapshot->regions = xbt_realloc(snapshot->regions, (snapshot->num_reg + 1) * sizeof(mc_mem_region_t));
snapshot->regions[snapshot->num_reg] = new_reg;
snapshot->num_reg++;
s_map_region reg;
memory_map_t maps = get_memory_map();
+ XBT_DEBUG("Take snapshot");
+
/* 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, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
+ MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
}
} else {
if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
- MC_snapshot_add_region(snapshot, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
+ MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
}
}
}
int i;
for(i=0 ; i< s1->num_reg ; i++){
-
+
if(s1->regions[i]->size != s2->regions[i]->size)
return 1;
-
+
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
return 1;
-
- if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0)
+
+ XBT_DEBUG("(%d) Snapshot ok before memcmp on data", i);
+
+ if(s1->regions[i]->type != s2->regions[i]->type)
return 1;
+
+ if(s1->regions[i]->type == 0){
+ if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0)
+ return 1;
+ }
}
}
-int reached(xbt_automaton_t a){
+int reached(xbt_automaton_t a, mc_snapshot_t s){
if(xbt_dynar_is_empty(reached_pairs)){
return 0;
pair = xbt_new0(s_mc_pair_reached_t, 1);
pair->automaton_state = a->current_state;
pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot(pair->system_state);
+ pair->system_state = s;
/* Get values of propositional symbols */
unsigned int cursor = 0;
}
}
-int set_pair_reached(xbt_automaton_t a){
+int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s){
- if(reached(a) == 0){
+ if(reached(a, s) == 0){
MC_SET_RAW_MEM;
pair = xbt_new0(s_mc_pair_reached_t, 1);
pair->automaton_state = a->current_state;
pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot(pair->system_state);
+ pair->system_state = s;
/* Get values of propositional symbols */
unsigned int cursor = 0;
//XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
- if((search_cycle == 1) && (reached(a) == 1)){
+ if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
- int res = set_pair_reached(a);
+ int res = set_pair_reached(a, next_snapshot);
XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
MC_SET_RAW_MEM;
mc_pair_stateless_t next_pair = NULL;
mc_pair_stateless_t pair_succ;
+ mc_snapshot_t next_snapshot = NULL;
xbt_dynar_t successors = NULL;
MC_state_interleave_process(next_graph_state, process);
}
}
+
+ next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot(next_snapshot);
xbt_dynar_reset(successors);
xbt_dynar_foreach(successors, cursor, pair_succ){
- if((search_cycle == 1) && (reached(a) == 1)){
+ if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
XBT_DEBUG("Acceptance pair %p : graph=%p, automaton=%p(%s)", pair_succ, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
- int res = set_pair_reached(a);
+ int res = set_pair_reached(a, next_snapshot);
MC_SET_RAW_MEM;
xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
char *lfields[6], *tok, *endptr;
int i;
+ char *backup_line = NULL;
+
/* Open the actual process's proc maps file and create the memory_map_t */
/* to be returned. */
fp = fopen("/proc/self/maps", "r");
/* Read one line at the time, parse it and add it to the memory map to be returned */
while ((read = getline(&line, &n, fp)) != -1) {
- //XBT_DEBUG("%s", line);
+ //XBT_INFO("%s", line);
+ if(XBT_LOG_ISENABLED(mc_memory_map, xbt_log_priority_debug))
+ backup_line = strdup(line);
/* Wipeout the new line character */
line[read - 1] = '\0';
xbt_realloc(ret->regions, sizeof(memreg) * (ret->mapsize + 1));
memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg));
ret->mapsize++;
+
+ if(XBT_LOG_ISENABLED(mc_memory_map, xbt_log_priority_debug)){
+
+ if (memreg.pathname == NULL){
+ if (memreg.start_addr == std_heap){
+ XBT_DEBUG("New region in snapshot : %s", backup_line);
+ }
+ } else {
+ if (!memcmp(basename(memreg.pathname), "libsimgrid", 10)){
+ XBT_DEBUG("New region in snapshot : %s", backup_line);
+ }
+ }
+ }
+
+
}
if (line)
/****************************** Snapshots ***********************************/
typedef struct s_mc_mem_region{
+ int type;
void *start_addr;
void *data;
size_t size;
memory_map_t get_memory_map(void);
+/********************************** DPOR for safety (stateless) **************************************/
+void MC_dpor_init(void);
+void MC_dpor(void);
+void MC_dpor_exit(void);
+
+/***** DPOR for safety (stateful) **** */
+
+typedef struct s_mc_state_with_snapshot{
+ mc_snapshot_t system_state;
+ mc_state_t graph_state;
+}s_mc_state_ws_t, *mc_state_ws_t;
+
+extern xbt_fifo_t mc_stack_safety_stateful;
+
+void MC_init_stateful(void);
+void MC_modelcheck_stateful(void);
+mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs);
+void MC_dpor_stateful_init(void);
+void MC_dpor_stateful(void);
+void MC_exit_stateful(void);
+
+
/********************************** Double-DFS for liveness property**************************************/
typedef struct s_mc_pair{
int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l);
mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st);
-int reached(xbt_automaton_t a);
-int set_pair_reached(xbt_automaton_t a);
+int reached(xbt_automaton_t a, mc_snapshot_t s);
+int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s);
int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2);
void MC_show_stack_liveness_stateful(xbt_fifo_t stack);
void MC_dump_stack_liveness_stateful(xbt_fifo_t stack);
void MC_dump_stack_liveness_stateless(xbt_fifo_t stack);
void MC_pair_stateless_delete(mc_pair_stateless_t pair);
-/********************************** DPOR for safety (stateless) **************************************/
-void MC_dpor_init(void);
-void MC_dpor(void);
-void MC_dpor_exit(void);
-
-/***** DPOR for safety (stateful) **** */
-
-typedef struct s_mc_state_with_snapshot{
- mc_snapshot_t system_state;
- mc_state_t graph_state;
-}s_mc_state_ws_t, *mc_state_ws_t;
-
-extern xbt_fifo_t mc_stack_safety_stateful;
-void MC_init_stateful(void);
-void MC_modelcheck_stateful(void);
-mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs);
-void MC_dpor_stateful_init(void);
-void MC_dpor_stateful(void);
-void MC_exit_stateful(void);
#endif