Revert "[mc] Enable MC specific behaviour in replay mode"

This reverts commit 33eca433c4f055cdfcc55e46d125f8708e1848c7.

Build is broken.

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 12f4fb1..2e3344e 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -589,7 +589,6 @@ 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
@@ -604,6 +603,7 @@ 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 96105a8..a64b03a 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 */
-  if(MC_is_active() || MC_record_replay_is_active()){
+  if(MC_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() || MC_record_replay_is_active()){
-          if(MC_is_active() && !MC_visited_reduction() && no_op){
+        if(MC_is_active()){
+          if(!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 6fe5c2c..974165d 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -6,8 +6,6 @@
 /* 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"
@@ -48,17 +46,6 @@ 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 126622e..4614ac9 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -27,15 +27,12 @@
 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;
@@ -765,6 +762,18 @@ 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)
 {
 
@@ -832,16 +841,3 @@ 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 b898e56..47dd8e3 100644 (file)
--- a/src/mc/mc_record.c
+++ b/src/mc/mc_record.c
@@ -137,8 +137,3 @@ 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 3ea2d77..3257703 100644 (file)
--- a/src/mc/mc_record.h
+++ b/src/mc/mc_record.h
@@ -20,9 +20,16 @@
 #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
@@ -30,6 +37,11 @@ SG_BEGIN_DECL()
  */
 #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
@@ -76,8 +88,6 @@ 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 eb50d4d..75ab8dc 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");
 
-  if (MC_is_active() || MC_record_replay_is_active()) {
+  if (MC_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() || MC_record_replay_is_active()) {
+  if (MC_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 6e3dac7..6d52482 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)
 {
-  if(MC_is_active() || MC_record_replay_is_active()){
+  if(MC_is_active()){
     return MC_process_clock_get(SIMIX_process_self());
   }else{
     return surf_get_clock();
@@ -308,7 +308,6 @@ 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 d05a6be..30043b0 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 */
-  if (!MC_is_active() && !MC_record_replay_is_active()) {
+  if (!MC_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() && !MC_record_replay_is_active()) {
+  if (!MC_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() || MC_record_replay_is_active()) {
+  if (MC_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 9f47c97..089c68e 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;
 
 
-  if (MC_is_active() || MC_record_replay_is_active()) {
+  if (MC_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() || MC_record_replay_is_active()) {
+  if (MC_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() || MC_record_replay_is_active()) {
+  if (MC_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() || MC_record_replay_is_active()){
+  if(MC_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() || MC_record_replay_is_active()){
+  if (MC_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() || MC_record_replay_is_active()){
+  if (MC_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() && !MC_record_replay_is_active())
+      if (!MC_is_active())
         simcall_comm_waitany__set__result(simcall, xbt_dynar_search(simcall_comm_waitany__get__comms(simcall), &synchro));
     }
 
@@ -945,7 +945,6 @@ 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 d2e80ba..a0bcac1 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)
 {
-  if (MC_is_active() || MC_record_replay_is_active()) {
+  if (MC_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 dba43c9..8b60d82 100644 (file)
--- a/src/smpi/smpi_base.c
+++ b/src/smpi/smpi_base.c
@@ -905,9 +905,10 @@ 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((MC_is_active() || MC_record_replay_is_active()) && (*request)->action)
+#ifdef HAVE_MC
+  if(MC_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);
@@ -992,7 +993,7 @@ int smpi_mpi_waitall(int count, MPI_Request requests[],
   }
   for(c = 0; c < count; c++) {
 
-    if (MC_is_active() || MC_record_replay_is_active()) {
+    if (MC_is_active()) {
       smpi_mpi_wait(&requests[c], pstat);
       index = c;
     } else {
@@ -1586,3 +1587,4 @@ 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 72230db..55970de 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());
 
-  if (MC_is_active() || MC_record_replay_is_active())
+  if(MC_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() || MC_record_replay_is_active())
+  if(MC_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 1b2d38c..16899d1 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:
-    if(MC_is_active() || MC_record_is_active())
+    if(MC_is_active())
       return;
 
     int index = smpi_process_index();