From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Mon, 1 Dec 2014 12:47:04 +0000 (+0100)
Subject: [mc] Enable MC specific behaviour in replay mode
X-Git-Tag: v3_12~732^2~175
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/33eca433c4f055cdfcc55e46d125f8708e1848c7

[mc] Enable MC specific behaviour in replay mode
---

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 2e3344ef45..12f4fb1ee8 100644
--- 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_global.c
   )
 
 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_global.c
   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 a64b03a158..96105a851e 100644
--- 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 */
-  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;
@@ -371,8 +371,8 @@ int node(int argc, char *argv[])
 
         // 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){
diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 974165d740..6fe5c2c5a2 100644
--- 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. */
 
+#include <stdbool.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
 
+/** 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 */
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 4614ac9c77..126622e77f 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -27,12 +27,15 @@
 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;
-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;
@@ -762,18 +765,6 @@ 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)
 {
 
@@ -841,3 +832,16 @@ void MC_dump_stacks(FILE* file)
   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;
+  }
+}
diff --git a/src/mc/mc_record.c b/src/mc/mc_record.c
index 47dd8e3a32..b898e566d7 100644
--- 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);
 }
+
+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 32577039d0..3ea2d77dff 100644
--- a/src/mc/mc_record.h
+++ b/src/mc/mc_record.h
@@ -20,16 +20,9 @@
 #include <stdbool.h>
 
 #include "simgrid_config.h"
-#include "mc_record.h"
 
 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
@@ -37,11 +30,6 @@ extern char* MC_record_path;
  */
 #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
@@ -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_init(void);
+
 SG_END_DECL()
 
 #endif
diff --git a/src/simix/libsmx.c b/src/simix/libsmx.c
index 75ab8dca8c..eb50d4df4c 100644
--- 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");
 
-  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,
@@ -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");
 
-  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,
diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c
index 6d52482a29..6e3dac7a8f 100644
--- 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)
 {
-  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();
@@ -308,6 +308,7 @@ static int process_syscall_color(void *p)
 void SIMIX_run(void)
 {
   if(MC_record_path) {
+    MC_record_replay_init();
     MC_record_replay_from_string(MC_record_path);
     return;
   }
diff --git a/src/simix/smx_host.c b/src/simix/smx_host.c
index 30043b08f4..d05a6be7b3 100644
--- 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 */
-  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);
@@ -441,7 +441,7 @@ smx_synchro_t SIMIX_host_parallel_execute(const char *name,
   }
 
   /* 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);
@@ -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 */
-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {
     synchro->state = SIMIX_DONE;
     SIMIX_execution_finish(synchro);
     return;
diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 089c68e151..9f47c97395 100644
--- 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;
 
 
-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {
     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);*/
 
 
-  if (MC_is_active()) {
+  if (MC_is_active() || MC_record_replay_is_active()) {
     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;
 
-  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;
@@ -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)
 {
-  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;
@@ -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);
 
-  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);
@@ -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;
 
-  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);
@@ -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);
-      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));
     }
 
@@ -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 */
+           && !MC_record_replay_is_active()
            && (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 a0bcac1e15..d2e80ba4fe 100644
--- 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)
 {
-  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);
diff --git a/src/smpi/smpi_base.c b/src/smpi/smpi_base.c
index 8b60d8274d..dba43c97c7 100644
--- 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);
-#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
-#endif
   }
 
   finish_wait(request, status);
@@ -993,7 +992,7 @@ int smpi_mpi_waitall(int count, MPI_Request requests[],
   }
   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 {
@@ -1587,4 +1586,3 @@ void smpi_mpi_exscan(void *sendbuf, void *recvbuf, int count,
   xbt_free(tmpbufs);
   xbt_free(requests);
 }
-
diff --git a/src/smpi/smpi_bench.c b/src/smpi/smpi_bench.c
index 55970de52b..72230dba95 100644
--- 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());
 
-  if(MC_is_active())
+  if (MC_is_active() || MC_record_replay_is_active())
     return;
 
   xbt_os_threadtimer_start(smpi_process_timer());
@@ -204,7 +204,7 @@ void smpi_bench_begin(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();
diff --git a/src/smpi/smpi_global.c b/src/smpi/smpi_global.c
index 16899d192c..1b2d38c07c 100644
--- 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:
-    if(MC_is_active())
+    if(MC_is_active() || MC_record_is_active())
       return;
 
     int index = smpi_process_index();