model-checker : cleanups in mc_snapshot structure

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index f4ec6ef..46b7096 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -42,7 +42,6 @@ static xbt_dynar_t take_snapshot_ignore(void);
 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);
 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);
   new_reg->start_addr = start_addr;
   new_reg->size = size;
   new_reg->data = xbt_malloc0(size);


@@ -72,10 +71,7 @@ static void MC_region_destroy(mc_mem_region_t reg)
 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(type, start_addr, 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(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->region_type[snapshot->num_reg] = type;
-  snapshot->num_reg++;
+  snapshot->regions[type] = new_reg;

   return;
 } 
 
   return;
 } 
 


@@ -163,7 +159,7 @@ mc_snapshot_t MC_take_snapshot()
         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);
           snapshot->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
         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);
           snapshot->heap_bytes_used = mmalloc_get_bytes_used(std_heap);

-          heap = snapshot->regions[snapshot->num_reg - 1]->data;
+          heap = snapshot->regions[0]->data;

         }
         i++;
       } else{ 
         }
         i++;
       } else{ 


@@ -221,7 +217,7 @@ mc_snapshot_t MC_take_snapshot()
 void MC_restore_snapshot(mc_snapshot_t snapshot)
 {
   unsigned int i;
 void MC_restore_snapshot(mc_snapshot_t snapshot)
 {
   unsigned int i;

-  for(i=0; i < snapshot->num_reg; i++){
+  for(i=0; i < NB_REGIONS; i++){

     MC_region_restore(snapshot->regions[i]);
   }
 
     MC_region_restore(snapshot->regions[i]);
   }
 


@@ -230,10 +226,9 @@ void MC_restore_snapshot(mc_snapshot_t snapshot)
 void MC_free_snapshot(mc_snapshot_t snapshot)
 {
   unsigned int i;
 void MC_free_snapshot(mc_snapshot_t snapshot)
 {
   unsigned int i;

-  for(i=0; i < snapshot->num_reg; i++)
+  for(i=0; i < NB_REGIONS; i++)

     MC_region_destroy(snapshot->regions[i]);
 
     MC_region_destroy(snapshot->regions[i]);
 

-  xbt_free(snapshot->regions);

   xbt_dynar_free(&(snapshot->stacks));
   xbt_dynar_free(&(snapshot->to_ignore));
   xbt_free(snapshot);
   xbt_dynar_free(&(snapshot->stacks));
   xbt_dynar_free(&(snapshot->to_ignore));
   xbt_free(snapshot);

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 6aa0777..005381c 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -167,21 +167,6 @@ int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
   return snapshot_compare(s1, s2);
 }
 
   return snapshot_compare(s1, s2);
 }
 

-int get_heap_region_index(mc_snapshot_t s){
-  int i = 0;
-  while(i < s->num_reg){
-    switch(s->regions[i]->type){
-    case 0:
-      return i;
-      break;
-    default:
-      i++;
-      break;
-    }
-  }
-  return -1;
-}
-

 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
   int raw_mem = (mmalloc_get_current_heap() == raw_heap);


@@ -300,36 +285,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     xbt_os_timer_start(timer);
   #endif
 
     xbt_os_timer_start(timer);
   #endif
 

-  int heap_index = 0, data_libsimgrid_index = 0, data_program_index = 0;
-  i = 0;
-  
-  /* Get index of regions */
-  while(i < s1->num_reg){
-    switch(s1->region_type[i]){
-    case 0:
-      heap_index = i;
-      i++;
-      break;
-    case 1:
-      data_libsimgrid_index = i;
-      i++;
-      while( i < s1->num_reg && s1->region_type[i] == 1)
-        i++;
-      break;
-    case 2:
-      data_program_index = i;
-      i++;
-      while( i < s1->num_reg && s1->region_type[i] == 2)
-        i++;
-      break;
-    }
-  }
-

   /* Init heap information used in heap comparison algorithm */
   /* Init heap information used in heap comparison algorithm */

-  init_heap_information((xbt_mheap_t)s1->regions[heap_index]->data, (xbt_mheap_t)s2->regions[heap_index]->data, s1->to_ignore, s2->to_ignore);
+  init_heap_information((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data, s1->to_ignore, s2->to_ignore);

 
   /* Compare binary global variables */
 
   /* Compare binary global variables */

-  is_diff = compare_global_variables(s1->region_type[data_program_index], s1->regions[data_program_index]->data, s2->regions[data_program_index]->data);
+  is_diff = compare_global_variables(2, s1->regions[2]->data, s2->regions[2]->data);

   if(is_diff != 0){
     #ifdef MC_DEBUG
       xbt_os_timer_stop(timer);
   if(is_diff != 0){
     #ifdef MC_DEBUG
       xbt_os_timer_stop(timer);


@@ -360,7 +320,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   #endif
 
   /* Compare libsimgrid global variables */
   #endif
 
   /* Compare libsimgrid global variables */

-    is_diff = compare_global_variables(s1->region_type[data_libsimgrid_index], s1->regions[data_libsimgrid_index]->data, s2->regions[data_libsimgrid_index]->data);
+  is_diff = compare_global_variables(1, s1->regions[1]->data, s2->regions[1]->data);

   if(is_diff != 0){
     #ifdef MC_DEBUG
       xbt_os_timer_stop(timer);
   if(is_diff != 0){
     #ifdef MC_DEBUG
       xbt_os_timer_stop(timer);


@@ -433,7 +393,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
   /* Compare heap */
  
 
   /* Compare heap */
  

-  if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[heap_index]->data, (xbt_mheap_t)s2->regions[heap_index]->data)){
+  if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data)){

 
     #ifdef MC_DEBUG
       xbt_os_timer_stop(timer);
 
     #ifdef MC_DEBUG
       xbt_os_timer_stop(timer);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 699a467..c0b6287 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -26,23 +26,20 @@
 
 /****************************** Snapshots ***********************************/
 
 
 /****************************** Snapshots ***********************************/
 

-#define nb_regions 3 /* binary data (data + BSS), libsimgrid data (data + BSS), std_heap */ 
+#define NB_REGIONS 3 /* binary data (data + BSS) (type = 2), libsimgrid data (data + BSS) (type = 1), std_heap (type = 0)*/ 

 
 typedef struct s_mc_mem_region{
 
 typedef struct s_mc_mem_region{

-  int type;

   void *start_addr;
   void *data;
   size_t size;
 } s_mc_mem_region_t, *mc_mem_region_t;
 
 typedef struct s_mc_snapshot{
   void *start_addr;
   void *data;
   size_t size;
 } s_mc_mem_region_t, *mc_mem_region_t;
 
 typedef struct s_mc_snapshot{

-  unsigned int num_reg;
-  int region_type[nb_regions];

   size_t heap_bytes_used;
   size_t heap_bytes_used;

-  mc_mem_region_t *regions;
+  mc_mem_region_t regions[NB_REGIONS];
+  int nb_processes;

   size_t *stack_sizes;
   xbt_dynar_t stacks;
   size_t *stack_sizes;
   xbt_dynar_t stacks;

-  int nb_processes;

   xbt_dynar_t to_ignore;
 } s_mc_snapshot_t, *mc_snapshot_t;
 
   xbt_dynar_t to_ignore;
 } s_mc_snapshot_t, *mc_snapshot_t;