From: Marion Guthmuller <marion.guthmuller@inria.fr>
Date: Wed, 4 Jun 2014 15:08:47 +0000 (+0200)
Subject: model-checker : compare the pid of enabled processes before memory introspection
X-Git-Tag: v3_12~956^2~10
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/b77d16c5d011f3c04ab6dcc2c4d5d2f865fd9415

model-checker : compare the pid of enabled processes before memory introspection
---

diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh
index fce5786e53..dfa372b1d4 100644
--- a/examples/msg/mc/bugged1_liveness.tesh
+++ b/examples/msg/mc/bugged1_liveness.tesh
@@ -15,7 +15,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../msg_platform.xml ${srcdir:=.}/de
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (3:client@Fafard) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [  0.000000] (0:@) Pair 22 already reached (equal to pair 10) !
+> [  0.000000] (0:@) Pair 21 already reached (equal to pair 9) !
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
@@ -40,8 +40,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../msg_platform.xml ${srcdir:=.}/de
 > [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
 > [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:@) Expanded pairs = 22
-> [  0.000000] (0:@) Visited pairs = 22
-> [  0.000000] (0:@) Executed transitions = 21
-> [  0.000000] (0:@) Counter-example depth : 21
+> [  0.000000] (0:@) Expanded pairs = 21
+> [  0.000000] (0:@) Visited pairs = 21
+> [  0.000000] (0:@) Executed transitions = 20
+> [  0.000000] (0:@) Counter-example depth : 20
diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 211d99dd31..ba9b772e91 100644
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -74,7 +74,7 @@ void MC_free_snapshot(mc_snapshot_t snapshot)
   xbt_dynar_free(&(snapshot->to_ignore));
 
   if (snapshot->privatization_regions) {
-    size_t n = snapshot->nb_processes;
+    size_t n = xbt_dynar_length(snapshot->enabled_processes);
     for (i = 0; i != n; ++i) {
       MC_region_destroy(snapshot->privatization_regions[i]);
     }
@@ -538,7 +538,11 @@ mc_snapshot_t MC_take_snapshot(int num_state)
 {
 
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
-  snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
+  snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL);
+  smx_process_t process;
+  xbt_swag_foreach(process, simix_global->process_list) {
+    xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid); 
+  }
 
   /* Save the std heap and the writable mapped pages of libsimgrid and binary */
   MC_get_memory_regions(snapshot);
diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 819ccaad49..0e14bab653 100644
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -461,11 +461,18 @@ int snapshot_compare(void *state1, void *state2)
     }
   }
 
+  /* Compare enabled processes */
+  unsigned int cursor;
+  int pid;
+  xbt_dynar_foreach(s1->enabled_processes, cursor, pid){
+    if(!xbt_dynar_member(s2->enabled_processes, &pid))
+      XBT_VERB("(%d - %d) Different enabled processes", num1, num2);
+  }
+
   int i = 0;
   size_t size_used1, size_used2;
   int is_diff = 0;
 
-
   /* Compare size of stacks */
   while (i < xbt_dynar_length(s1->stacks)) {
     size_used1 = s1->stack_sizes[i];
@@ -531,7 +538,7 @@ int snapshot_compare(void *state1, void *state2)
 #endif
 
   /* Stacks comparison */
-  unsigned int cursor = 0;
+  cursor = 0;
   int diff_local = 0;
 #ifdef MC_DEBUG
   is_diff = 0;
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index df7636397e..809f87797a 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -280,11 +280,11 @@ void MC_init()
 
     MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
-    /*smx_process_t process;
+    smx_process_t process;
     xbt_swag_foreach(process, simix_global->process_list) {
       MC_ignore_heap(&(process->process_hookup),
                      sizeof(process->process_hookup));
-                     }*/
+                     }
   }
 
   if (raw_mem_set)
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 3ff124f0c1..d1e1b1910f 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -48,7 +48,7 @@ typedef struct s_mc_mem_region{
 typedef struct s_mc_snapshot{
   size_t heap_bytes_used;
   mc_mem_region_t regions[NB_REGIONS];
-  int nb_processes;
+  xbt_dynar_t enabled_processes;
   mc_mem_region_t* privatization_regions;
   int privatization_index;
   size_t *stack_sizes;