model-checker : add type in s_mc_mem_region (0=std_heap, 1=libsimgrid)

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index dc85a3b..a2bb87b 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -1,15 +1,20 @@
 #include <libgen.h>
 #include "private.h"
 
 #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_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);
 {
   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);
   new_reg->start_addr = start_addr;
   new_reg->size = size;
   new_reg->data = xbt_malloc0(size);


@@ -30,9 +35,9 @@ static void MC_region_destroy(mc_mem_region_t reg)
   xbt_free(reg);
 }
 
   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++;
   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++;


@@ -45,17 +50,19 @@ void MC_take_snapshot(mc_snapshot_t snapshot)
   s_map_region reg;
   memory_map_t maps = get_memory_map();
 
   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)
   /* 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)){
         }
       } 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);

         }
       }
     }
         }
       }
     }

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 74086a1..c377374 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -26,15 +26,22 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
   int i;
   for(i=0 ; i< s1->num_reg ; i++){
 
   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]->size != s2->regions[i]->size)
       return 1;

-
+    

     if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
       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;
       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;
+    }

     
   }
 
     
   }
 


@@ -42,7 +49,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
 }
 
 
 }
 

-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;
 
   if(xbt_dynar_is_empty(reached_pairs)){
     return 0;


@@ -53,8 +60,7 @@ int reached(xbt_automaton_t a){
     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 = 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;
     
     /* Get values of propositional symbols */
     unsigned int cursor = 0;


@@ -85,9 +91,9 @@ int reached(xbt_automaton_t a){
   }
 }
 
   }
 }
 

-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;
 
 
     MC_SET_RAW_MEM;
 


@@ -95,8 +101,7 @@ int set_pair_reached(xbt_automaton_t a){
     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 = 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;
     
     /* Get values of propositional symbols */
     unsigned int cursor = 0;


@@ -381,7 +386,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 
       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 
 
       //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("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("|             ACCEPTANCE CYCLE            |");
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");


@@ -403,7 +408,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
     
       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
     
       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;
        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;


@@ -567,6 +572,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 
   mc_pair_stateless_t next_pair = NULL;
   mc_pair_stateless_t pair_succ;
 
   mc_pair_stateless_t next_pair = NULL;
   mc_pair_stateless_t pair_succ;

+  mc_snapshot_t next_snapshot = NULL;

   
   xbt_dynar_t successors = NULL;
   
   
   xbt_dynar_t successors = NULL;
   


@@ -606,6 +612,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
        MC_state_interleave_process(next_graph_state, process);
       }
     }
        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_reset(successors);
 


@@ -653,7 +662,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 
     xbt_dynar_foreach(successors, cursor, pair_succ){
      
 
     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("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("|             ACCEPTANCE CYCLE            |");
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");


@@ -674,7 +683,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
       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);
       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);
 
        MC_SET_RAW_MEM;
        xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);

diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c
index d1f279e..fa49689 100644 (file)
--- a/src/mc/memory_map.c
+++ b/src/mc/memory_map.c
@@ -18,6 +18,8 @@ memory_map_t get_memory_map(void)
   char *lfields[6], *tok, *endptr;
   int i;
 
   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");
 /* Open the actual process's proc maps file and create the memory_map_t */
 /* to be returned. */
   fp = fopen("/proc/self/maps", "r");


@@ -32,7 +34,9 @@ memory_map_t get_memory_map(void)
   /* 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) {
 
   /* 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';
 
     /* Wipeout the new line character */
     line[read - 1] = '\0';


@@ -138,6 +142,21 @@ memory_map_t get_memory_map(void)
         xbt_realloc(ret->regions, sizeof(memreg) * (ret->mapsize + 1));
     memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg));
     ret->mapsize++;
         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)
   }
 
   if (line)

diff --git a/src/mc/private.h b/src/mc/private.h
index 3ea8ad9..839f1ae 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -24,6 +24,7 @@
 /****************************** Snapshots ***********************************/
 
 typedef struct s_mc_mem_region{
 /****************************** Snapshots ***********************************/
 
 typedef struct s_mc_mem_region{

+  int type;

   void *start_addr;
   void *data;
   size_t size;
   void *start_addr;
   void *data;
   size_t size;


@@ -180,6 +181,28 @@ typedef struct s_memory_map {
 memory_map_t get_memory_map(void);
 
 
 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{
 /********************************** Double-DFS for liveness property**************************************/
 
 typedef struct s_mc_pair{


@@ -199,8 +222,8 @@ extern xbt_fifo_t mc_stack_liveness_stateful;
 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 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);
 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);


@@ -229,25 +252,6 @@ void MC_show_stack_liveness_stateless(xbt_fifo_t stack);
 void MC_dump_stack_liveness_stateless(xbt_fifo_t stack);
 void MC_pair_stateless_delete(mc_pair_stateless_t pair);
 
 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
 
 #endif