[mc] Enable MC specific behaviour in replay mode

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 2e3344e..12f4fb1 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -589,6 +589,7 @@ set(MC_SRC_BASE
   src/mc/mc_base.h
   src/mc/mc_record.c
   src/mc/mc_config.c
   src/mc/mc_base.h
   src/mc/mc_record.c
   src/mc/mc_config.c

+  src/mc/mc_global.c

   )
 
 set(MC_SRC
   )
 
 set(MC_SRC


@@ -603,7 +604,6 @@ set(MC_SRC
   src/mc/mc_dwarf_attrnames.h
   src/mc/mc_dwarf_expression.c
   src/mc/mc_dwarf_tagnames.h
   src/mc/mc_dwarf_attrnames.h
   src/mc/mc_dwarf_expression.c
   src/mc/mc_dwarf_tagnames.h

-  src/mc/mc_global.c

   src/mc/mc_hash.c
   src/mc/mc_ignore.c
   src/mc/mc_interface.h
   src/mc/mc_hash.c
   src/mc/mc_ignore.c
   src/mc/mc_interface.h

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index a64b03a..96105a8 100644 (file)
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -297,7 +297,7 @@ int node(int argc, char *argv[])
 {
 
   /* Reduce the run size for the MC */
 {
 
   /* Reduce the run size for the MC */

-  if(MC_is_active()){
+  if(MC_is_active() || MC_record_replay_is_active()){

     periodic_stabilize_delay = 8;
     periodic_fix_fingers_delay = 8;
     periodic_check_predecessor_delay = 8;
     periodic_stabilize_delay = 8;
     periodic_fix_fingers_delay = 8;
     periodic_check_predecessor_delay = 8;


@@ -371,8 +371,8 @@ int node(int argc, char *argv[])
 
         // no task was received: make some periodic calls
 
 
         // no task was received: make some periodic calls
 

-        if(MC_is_active()){
-          if(!MC_visited_reduction() && no_op){
+        if(MC_is_active() || MC_record_replay_is_active()){
+          if(MC_is_active() && !MC_visited_reduction() && no_op){

               MC_cut();
           }
           if(listen == 0 && (sub_protocol = MC_random(0, 4)) > 0){
               MC_cut();
           }
           if(listen == 0 && (sub_protocol = MC_random(0, 4)) > 0){

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 974165d..6fe5c2c 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -6,6 +6,8 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 

+#include <stdbool.h>
+

 #include <simgrid_config.h> /* HAVE_MC ? */
 #include <xbt.h>
 #include "xbt/automaton.h"
 #include <simgrid_config.h> /* HAVE_MC ? */
 #include <xbt.h>
 #include "xbt/automaton.h"


@@ -46,6 +48,17 @@ XBT_PUBLIC(void) MC_ignore(void *addr, size_t size);
 
 #endif
 
 
 #endif
 

+/** Replay path (if any) in string representation
+ *
+ *  This is a path as generated by `MC_record_stack_to_string()`.
+ */
+extern char* MC_record_path;
+
+/** Whether the replay mode is enabled */
+static inline bool MC_record_replay_is_active(void) {
+  return MC_record_path;
+}
+

 SG_END_DECL()
 
 #endif /* SIMGRID_MODELCHECKER_H */
 SG_END_DECL()
 
 #endif /* SIMGRID_MODELCHECKER_H */

diff --git a/src/mc/mc_base.h b/src/mc/mc_base.h
index 39a62e0..34852e4 100644 (file)
--- a/src/mc/mc_base.h
+++ b/src/mc/mc_base.h
@@ -18,6 +18,8 @@ int MC_request_is_enabled(smx_simcall_t req);
 int MC_request_is_visible(smx_simcall_t req);
 void MC_wait_for_requests(void);
 
 int MC_request_is_visible(smx_simcall_t req);
 void MC_wait_for_requests(void);
 

+extern double *mc_time;
+

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 4614ac9..66e8f81 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -17,22 +17,28 @@
 #include "simgrid/sg_config.h"
 #include "../surf/surf_private.h"
 #include "../simix/smx_private.h"
 #include "simgrid/sg_config.h"
 #include "../surf/surf_private.h"
 #include "../simix/smx_private.h"

-#include "../xbt/mmalloc/mmprivate.h"

 #include "xbt/fifo.h"
 #include "xbt/fifo.h"

-#include "mc_private.h"
-#include "mc_record.h"

 #include "xbt/automaton.h"
 #include "xbt/dict.h"
 
 #include "xbt/automaton.h"
 #include "xbt/dict.h"
 

+#ifdef HAVE_MC
+#include "../xbt/mmalloc/mmprivate.h"
+#include "mc_private.h"
+#endif
+#include "mc_record.h"
+

 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
                                 "Logging specific to MC (global)");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
                                 "Logging specific to MC (global)");
 

+double *mc_time = NULL;
+
+#ifdef HAVE_MC

 int user_max_depth_reached = 0;
 
 /* MC global data structures */
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 int user_max_depth_reached = 0;
 
 /* MC global data structures */
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;

-double *mc_time = NULL;
+

 __thread mc_comparison_times_t mc_comp_times = NULL;
 __thread double mc_snapshot_comparison_time;
 mc_stats_t mc_stats = NULL;
 __thread mc_comparison_times_t mc_comp_times = NULL;
 __thread double mc_snapshot_comparison_time;
 mc_stats_t mc_stats = NULL;


@@ -757,23 +763,6 @@ void MC_cut(void)
   user_max_depth_reached = 1;
 }
 
   user_max_depth_reached = 1;
 }
 

-void MC_process_clock_add(smx_process_t process, double amount)
-{
-  mc_time[process->pid] += amount;
-}
-
-double MC_process_clock_get(smx_process_t process)
-{
-  if (mc_time) {
-    if (process != NULL)
-      return mc_time[process->pid];
-    else
-      return -1;
-  } else {
-    return 0;
-  }
-}
-

 void MC_automaton_load(const char *file)
 {
 
 void MC_automaton_load(const char *file)
 {
 


@@ -841,3 +830,21 @@ void MC_dump_stacks(FILE* file)
   if (raw_mem_set)
     MC_SET_MC_HEAP;
 }
   if (raw_mem_set)
     MC_SET_MC_HEAP;
 }

+#endif
+
+double MC_process_clock_get(smx_process_t process)
+{
+  if (mc_time) {
+    if (process != NULL)
+      return mc_time[process->pid];
+    else
+      return -1;
+  } else {
+    return 0;
+  }
+}
+
+void MC_process_clock_add(smx_process_t process, double amount)
+{
+  mc_time[process->pid] += amount;
+}

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 1348243..78b4c26 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -235,7 +235,6 @@ extern xbt_dynar_t mc_checkpoint_ignore;
 
 /********************************* MC Global **********************************/
 
 
 /********************************* MC Global **********************************/
 

-extern double *mc_time;

 extern FILE *dot_output;
 extern const char* colors[13];
 extern xbt_parmap_t parmap;
 extern FILE *dot_output;
 extern const char* colors[13];
 extern xbt_parmap_t parmap;

diff --git a/src/mc/mc_record.c b/src/mc/mc_record.c
index 47dd8e3..b898e56 100644 (file)
--- a/src/mc/mc_record.c
+++ b/src/mc/mc_record.c
@@ -137,3 +137,8 @@ void MC_record_replay_from_string(const char* path_string)
   MC_record_replay(start, xbt_dynar_length(path));
   xbt_dynar_free(&path);
 }
   MC_record_replay(start, xbt_dynar_length(path));
   xbt_dynar_free(&path);
 }

+
+void MC_record_replay_init()
+{
+  mc_time = xbt_new0(double, simix_process_maxpid);
+}

diff --git a/src/mc/mc_record.h b/src/mc/mc_record.h
index 3257703..3ea2d77 100644 (file)
--- a/src/mc/mc_record.h
+++ b/src/mc/mc_record.h
@@ -20,16 +20,9 @@
 #include <stdbool.h>
 
 #include "simgrid_config.h"
 #include <stdbool.h>
 
 #include "simgrid_config.h"

-#include "mc_record.h"

 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 

-/** Replay path (if any) in string representation
- *
- *  This is a path as generated by `MC_record_stack_to_string()`.
- */
-extern char* MC_record_path;
-

 /** Whether the MC record mode is enabled
  *
  *  The behaviour is not changed. The only real difference is that
 /** Whether the MC record mode is enabled
  *
  *  The behaviour is not changed. The only real difference is that


@@ -37,11 +30,6 @@ extern char* MC_record_path;
  */
 #define MC_record_is_active() _sg_do_model_check_record
 
  */
 #define MC_record_is_active() _sg_do_model_check_record
 

-/** Whether the replay mode is enabled */
-static inline bool MC_record_replay_is_active(void) {
-  return MC_record_path;
-}
-

 // **** Data conversion
 
 /** An element in the recorded path
 // **** Data conversion
 
 /** An element in the recorded path


@@ -88,6 +76,8 @@ void MC_record_replay(mc_record_item_t start, size_t count);
  */
 void MC_record_replay_from_string(const char* data);
 
  */
 void MC_record_replay_from_string(const char* data);
 

+void MC_record_replay_init(void);
+

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/simix/libsmx.c b/src/simix/libsmx.c
index 75ab8dc..eb50d4d 100644 (file)
--- a/src/simix/libsmx.c
+++ b/src/simix/libsmx.c
@@ -928,7 +928,7 @@ void simcall_comm_send(smx_process_t src, smx_rdv_t rdv, double task_size, doubl
 
   xbt_assert(rdv, "No rendez-vous point defined for send");
 
 
   xbt_assert(rdv, "No rendez-vous point defined for send");
 

-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {

     /* the model-checker wants two separate simcalls */
     smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simcall */
     comm = simcall_comm_isend(src, rdv, task_size, rate,
     /* the model-checker wants two separate simcalls */
     smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simcall */
     comm = simcall_comm_isend(src, rdv, task_size, rate,


@@ -975,7 +975,7 @@ void simcall_comm_recv(smx_rdv_t rdv, void *dst_buff, size_t * dst_buff_size,
   xbt_assert(isfinite(timeout), "timeout is not finite!");
   xbt_assert(rdv, "No rendez-vous point defined for recv");
 
   xbt_assert(isfinite(timeout), "timeout is not finite!");
   xbt_assert(rdv, "No rendez-vous point defined for recv");
 

-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {

     /* the model-checker wants two separate simcalls */
     smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simcall */
     comm = simcall_comm_irecv(rdv, dst_buff, dst_buff_size,
     /* the model-checker wants two separate simcalls */
     smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simcall */
     comm = simcall_comm_irecv(rdv, dst_buff, dst_buff_size,

diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c
index 6d52482..6e3dac7 100644 (file)
--- a/src/simix/smx_global.c
+++ b/src/simix/smx_global.c
@@ -281,7 +281,7 @@ void SIMIX_clean(void)
  */
 XBT_INLINE double SIMIX_get_clock(void)
 {
  */
 XBT_INLINE double SIMIX_get_clock(void)
 {

-  if(MC_is_active()){
+  if(MC_is_active() || MC_record_replay_is_active()){

     return MC_process_clock_get(SIMIX_process_self());
   }else{
     return surf_get_clock();
     return MC_process_clock_get(SIMIX_process_self());
   }else{
     return surf_get_clock();


@@ -308,6 +308,7 @@ static int process_syscall_color(void *p)
 void SIMIX_run(void)
 {
   if(MC_record_path) {
 void SIMIX_run(void)
 {
   if(MC_record_path) {

+    MC_record_replay_init();

     MC_record_replay_from_string(MC_record_path);
     return;
   }
     MC_record_replay_from_string(MC_record_path);
     return;
   }

diff --git a/src/simix/smx_host.c b/src/simix/smx_host.c
index 30043b0..d05a6be 100644 (file)
--- a/src/simix/smx_host.c
+++ b/src/simix/smx_host.c
@@ -377,7 +377,7 @@ smx_synchro_t SIMIX_host_execute(const char *name,
 #endif
 
   /* set surf's action */
 #endif
 
   /* set surf's action */

-  if (!MC_is_active()) {
+  if (!MC_is_active() && !MC_record_replay_is_active()) {

 
     synchro->execution.surf_exec = surf_workstation_execute(host, computation_amount);
     surf_action_set_data(synchro->execution.surf_exec, synchro);
 
     synchro->execution.surf_exec = surf_workstation_execute(host, computation_amount);
     surf_action_set_data(synchro->execution.surf_exec, synchro);


@@ -441,7 +441,7 @@ smx_synchro_t SIMIX_host_parallel_execute(const char *name,
   }
 
   /* set surf's synchro */
   }
 
   /* set surf's synchro */

-  if (!MC_is_active()) {
+  if (!MC_is_active() && !MC_record_replay_is_active()) {

     synchro->execution.surf_exec =
       surf_workstation_model_execute_parallel_task((surf_workstation_model_t)surf_workstation_model,
                  host_nb, workstation_list, computation_amount, communication_amount, rate);
     synchro->execution.surf_exec =
       surf_workstation_model_execute_parallel_task((surf_workstation_model_t)surf_workstation_model,
                  host_nb, workstation_list, computation_amount, communication_amount, rate);


@@ -515,7 +515,7 @@ void simcall_HANDLER_host_execution_wait(smx_simcall_t simcall, smx_synchro_t sy
   simcall->issuer->waiting_synchro = synchro;
 
   /* set surf's synchro */
   simcall->issuer->waiting_synchro = synchro;
 
   /* set surf's synchro */

-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {

     synchro->state = SIMIX_DONE;
     SIMIX_execution_finish(synchro);
     return;
     synchro->state = SIMIX_DONE;
     SIMIX_execution_finish(synchro);
     return;

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 089c68e..9f47c97 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -423,7 +423,7 @@ smx_synchro_t SIMIX_comm_isend(smx_process_t src_proc, smx_rdv_t rdv,
   other_synchro->comm.copy_data_fun = copy_data_fun;
 
 
   other_synchro->comm.copy_data_fun = copy_data_fun;
 
 

-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {

     other_synchro->state = SIMIX_RUNNING;
     return (detached ? NULL : other_synchro);
   }
     other_synchro->state = SIMIX_RUNNING;
     return (detached ? NULL : other_synchro);
   }


@@ -532,7 +532,7 @@ smx_synchro_t SIMIX_comm_irecv(smx_process_t dst_proc, smx_rdv_t rdv,
     SIMIX_comm_copy_data(other_synchro);*/
 
 
     SIMIX_comm_copy_data(other_synchro);*/
 
 

-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {

     other_synchro->state = SIMIX_RUNNING;
     return other_synchro;
   }
     other_synchro->state = SIMIX_RUNNING;
     return other_synchro;
   }


@@ -593,7 +593,7 @@ void simcall_HANDLER_comm_wait(smx_simcall_t simcall, smx_synchro_t synchro, dou
   xbt_fifo_push(synchro->simcalls, simcall);
   simcall->issuer->waiting_synchro = synchro;
 
   xbt_fifo_push(synchro->simcalls, simcall);
   simcall->issuer->waiting_synchro = synchro;
 

-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {

     int idx = SIMCALL_GET_MC_VALUE(simcall);
     if (idx == 0) {
       synchro->state = SIMIX_DONE;
     int idx = SIMCALL_GET_MC_VALUE(simcall);
     if (idx == 0) {
       synchro->state = SIMIX_DONE;


@@ -630,7 +630,7 @@ void simcall_HANDLER_comm_wait(smx_simcall_t simcall, smx_synchro_t synchro, dou
 
 void simcall_HANDLER_comm_test(smx_simcall_t simcall, smx_synchro_t synchro)
 {
 
 void simcall_HANDLER_comm_test(smx_simcall_t simcall, smx_synchro_t synchro)
 {

-  if(MC_is_active()){
+  if(MC_is_active() || MC_record_replay_is_active()){

     simcall_comm_test__set__result(simcall, synchro->comm.src_proc && synchro->comm.dst_proc);
     if(simcall_comm_test__get__result(simcall)){
       synchro->state = SIMIX_DONE;
     simcall_comm_test__set__result(simcall, synchro->comm.src_proc && synchro->comm.dst_proc);
     if(simcall_comm_test__get__result(simcall)){
       synchro->state = SIMIX_DONE;


@@ -657,7 +657,7 @@ void simcall_HANDLER_comm_testany(smx_simcall_t simcall, xbt_dynar_t synchros)
   smx_synchro_t synchro;
   simcall_comm_testany__set__result(simcall, -1);
 
   smx_synchro_t synchro;
   simcall_comm_testany__set__result(simcall, -1);
 

-  if (MC_is_active()){
+  if (MC_is_active() || MC_record_replay_is_active()){

     int idx = SIMCALL_GET_MC_VALUE(simcall);
     if(idx == -1){
       SIMIX_simcall_answer(simcall);
     int idx = SIMCALL_GET_MC_VALUE(simcall);
     if(idx == -1){
       SIMIX_simcall_answer(simcall);


@@ -687,7 +687,7 @@ void simcall_HANDLER_comm_waitany(smx_simcall_t simcall, xbt_dynar_t synchros)
   smx_synchro_t synchro;
   unsigned int cursor = 0;
 
   smx_synchro_t synchro;
   unsigned int cursor = 0;
 

-  if (MC_is_active()){
+  if (MC_is_active() || MC_record_replay_is_active()){

     int idx = SIMCALL_GET_MC_VALUE(simcall);
     synchro = xbt_dynar_get_as(synchros, idx, smx_synchro_t);
     xbt_fifo_push(synchro->simcalls, simcall);
     int idx = SIMCALL_GET_MC_VALUE(simcall);
     synchro = xbt_dynar_get_as(synchros, idx, smx_synchro_t);
     xbt_fifo_push(synchro->simcalls, simcall);


@@ -791,7 +791,7 @@ void SIMIX_comm_finish(smx_synchro_t synchro)
       continue; // if process handling comm is killed
     if (simcall->call == SIMCALL_COMM_WAITANY) {
       SIMIX_waitany_remove_simcall_from_actions(simcall);
       continue; // if process handling comm is killed
     if (simcall->call == SIMCALL_COMM_WAITANY) {
       SIMIX_waitany_remove_simcall_from_actions(simcall);

-      if (!MC_is_active())
+      if (!MC_is_active() && !MC_record_replay_is_active())

         simcall_comm_waitany__set__result(simcall, xbt_dynar_search(simcall_comm_waitany__get__comms(simcall), &synchro));
     }
 
         simcall_comm_waitany__set__result(simcall, xbt_dynar_search(simcall_comm_waitany__get__comms(simcall), &synchro));
     }
 


@@ -945,6 +945,7 @@ void SIMIX_comm_cancel(smx_synchro_t synchro)
     synchro->state = SIMIX_CANCELED;
   }
   else if (!MC_is_active() /* when running the MC there are no surf actions */
     synchro->state = SIMIX_CANCELED;
   }
   else if (!MC_is_active() /* when running the MC there are no surf actions */

+           && !MC_record_replay_is_active()

            && (synchro->state == SIMIX_READY || synchro->state == SIMIX_RUNNING)) {
 
     surf_action_cancel(synchro->comm.surf_comm);
            && (synchro->state == SIMIX_READY || synchro->state == SIMIX_RUNNING)) {
 
     surf_action_cancel(synchro->comm.surf_comm);

diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c
index a0bcac1..d2e80ba 100644 (file)
--- a/src/simix/smx_process.c
+++ b/src/simix/smx_process.c
@@ -714,7 +714,7 @@ smx_synchro_t SIMIX_process_join(smx_process_t issuer, smx_process_t process, do
 
 void simcall_HANDLER_process_sleep(smx_simcall_t simcall, double duration)
 {
 
 void simcall_HANDLER_process_sleep(smx_simcall_t simcall, double duration)
 {

-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {

     MC_process_clock_add(simcall->issuer, duration);
     simcall_process_sleep__set__result(simcall, SIMIX_DONE);
     SIMIX_simcall_answer(simcall);
     MC_process_clock_add(simcall->issuer, duration);
     simcall_process_sleep__set__result(simcall, SIMIX_DONE);
     SIMIX_simcall_answer(simcall);

diff --git a/src/smpi/smpi_base.c b/src/smpi/smpi_base.c
index 8b60d82..dba43c9 100644 (file)
--- a/src/smpi/smpi_base.c
+++ b/src/smpi/smpi_base.c
@@ -905,10 +905,9 @@ void smpi_mpi_wait(MPI_Request * request, MPI_Status * status)
 
   if ((*request)->action != NULL) { // this is not a detached send
     simcall_comm_wait((*request)->action, -1.0);
 
   if ((*request)->action != NULL) { // this is not a detached send
     simcall_comm_wait((*request)->action, -1.0);

-#ifdef HAVE_MC
-  if(MC_is_active() && (*request)->action)
+
+  if((MC_is_active() || MC_record_replay_is_active()) && (*request)->action)

     (*request)->action->comm.dst_data = NULL; // dangling pointer : dst_data is freed with a wait, need to set it to NULL for system state comparison
     (*request)->action->comm.dst_data = NULL; // dangling pointer : dst_data is freed with a wait, need to set it to NULL for system state comparison

-#endif

   }
 
   finish_wait(request, status);
   }
 
   finish_wait(request, status);


@@ -993,7 +992,7 @@ int smpi_mpi_waitall(int count, MPI_Request requests[],
   }
   for(c = 0; c < count; c++) {
 
   }
   for(c = 0; c < count; c++) {
 

-    if (MC_is_active()) {
+    if (MC_is_active() || MC_record_replay_is_active()) {

       smpi_mpi_wait(&requests[c], pstat);
       index = c;
     } else {
       smpi_mpi_wait(&requests[c], pstat);
       index = c;
     } else {


@@ -1587,4 +1586,3 @@ void smpi_mpi_exscan(void *sendbuf, void *recvbuf, int count,
   xbt_free(tmpbufs);
   xbt_free(requests);
 }
   xbt_free(tmpbufs);
   xbt_free(requests);
 }

-

diff --git a/src/smpi/smpi_bench.c b/src/smpi/smpi_bench.c
index 55970de..72230db 100644 (file)
--- a/src/smpi/smpi_bench.c
+++ b/src/smpi/smpi_bench.c
@@ -195,7 +195,7 @@ void smpi_bench_begin(void)
 {
   smpi_switch_data_segment(smpi_process_index());
 
 {
   smpi_switch_data_segment(smpi_process_index());
 

-  if(MC_is_active())
+  if (MC_is_active() || MC_record_replay_is_active())

     return;
 
   xbt_os_threadtimer_start(smpi_process_timer());
     return;
 
   xbt_os_threadtimer_start(smpi_process_timer());


@@ -204,7 +204,7 @@ void smpi_bench_begin(void)
 void smpi_bench_end(void)
 {
 
 void smpi_bench_end(void)
 {
 

-  if(MC_is_active())
+  if (MC_is_active() || MC_record_replay_is_active())

     return;
 
   xbt_os_timer_t timer = smpi_process_timer();
     return;
 
   xbt_os_timer_t timer = smpi_process_timer();

diff --git a/src/smpi/smpi_global.c b/src/smpi/smpi_global.c
index 16899d1..8a39d33 100644 (file)
--- a/src/smpi/smpi_global.c
+++ b/src/smpi/smpi_global.c
@@ -136,7 +136,7 @@ void smpi_process_finalize(void)
 {
     // This leads to an explosion of the search graph
     // which cannot be reduced:
 {
     // This leads to an explosion of the search graph
     // which cannot be reduced:

-    if(MC_is_active())
+    if(MC_is_active() || MC_record_replay_is_active())

       return;
 
     int index = smpi_process_index();
       return;
 
     int index = smpi_process_index();