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 fce5786..dfa372b 100644 (file)
--- 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] (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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  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:@) [(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 211d99d..ba9b772 100644 (file)
--- 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) {
   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]);
     }
     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);
 {
 
   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);
 
   /* 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 819ccaa..0e14bab 100644 (file)
--- 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;
 
   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];
   /* 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 */
 #endif
 
   /* Stacks comparison */

-  unsigned int cursor = 0;
+  cursor = 0;

   int diff_local = 0;
 #ifdef MC_DEBUG
   is_diff = 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 df76363..809f877 100644 (file)
--- 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));
 
 
     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));
     xbt_swag_foreach(process, simix_global->process_list) {
       MC_ignore_heap(&(process->process_hookup),
                      sizeof(process->process_hookup));

-                     }*/
+                     }

   }
 
   if (raw_mem_set)
   }
 
   if (raw_mem_set)

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 3ff124f..d1e1b19 100644 (file)
--- 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];
 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;
   mc_mem_region_t* privatization_regions;
   int privatization_index;
   size_t *stack_sizes;