Add a clock per process when running in MC mode.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@9466 48e7efb5-ca39-0410-a469-dd3cf9ba447f

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index bf7593a..d4c01ff 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -32,6 +32,8 @@ XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(void) MC_modelcheck(void);
 XBT_PUBLIC(int) MC_random(int, int);
+XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
+XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
 
 /********************************* Memory *************************************/
 XBT_PUBLIC(void) MC_memory_init(void);  /* Initialize the memory subsystem */

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 4ac7758..6c4c2b2 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -17,7 +17,7 @@ xbt_fifo_t mc_stack = NULL;
 mc_stats_t mc_stats = NULL;
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
-
+double *mc_time = NULL;
 /**
  *  \brief Initialize the model-checker data structures
  */
@@ -27,6 +27,8 @@ void MC_init(void)
   if (initial_snapshot)
     return;
 
+  mc_time = xbt_new0(double, simix_process_maxpid);
+
   /* Initialize the data structures that must be persistent across every
      iteration of the model-checker (in RAW memory) */
   MC_SET_RAW_MEM;
@@ -58,6 +60,7 @@ void MC_modelcheck(void)
 
 void MC_exit(void)
 {
+  xbt_free(mc_time);
   MC_memory_exit();
 }
 
@@ -234,3 +237,15 @@ void MC_assert(int prop)
   }
 }
 
+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)
+    return mc_time[process->pid];
+  else
+    return 0;
+}

diff --git a/src/mc/private.h b/src/mc/private.h
index 359560e..733a726 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -37,6 +37,7 @@ void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 
 /********************************* MC Global **********************************/
+extern double *mc_time;
 
 /* Bound of the MC depth-first search algorithm */
 #define MAX_DEPTH 1000

diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c
index d0e2c53..059130d 100644 (file)
--- a/src/simix/smx_global.c
+++ b/src/simix/smx_global.c
@@ -10,6 +10,7 @@
 #include "xbt/log.h"
 #include "xbt/str.h"
 #include "xbt/ex.h"             /* ex_backtrace_display */
+#include "mc/mc.h"
 
 XBT_LOG_EXTERNAL_CATEGORY(simix);
 XBT_LOG_EXTERNAL_CATEGORY(simix_action);
@@ -156,7 +157,11 @@ void SIMIX_clean(void)
  */
 XBT_INLINE double SIMIX_get_clock(void)
 {
-  return surf_get_clock();
+  if(MC_IS_ENABLED){
+    return MC_process_clock_get(SIMIX_process_self());
+  }else{
+    return surf_get_clock();
+  }
 }
 
 void SIMIX_run(void)

diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c
index ccd61f5..eff7ab7 100644 (file)
--- a/src/simix/smx_process.c
+++ b/src/simix/smx_process.c
@@ -15,8 +15,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix,
                                 "Logging specific to SIMIX (process)");
 
 unsigned long simix_process_maxpid = 0;
-/* FIXME: Ugly hack!*/
-extern double NOW;
 
 /**
  * \brief Returns the current agent.
@@ -413,7 +411,7 @@ xbt_dict_t SIMIX_process_get_properties(smx_process_t process)
 void SIMIX_pre_process_sleep(smx_req_t req)
 {
   if (MC_IS_ENABLED) {
-    NOW += req->process_sleep.duration;
+    MC_process_clock_add(req->issuer, req->process_sleep.duration);
     req->process_sleep.result = SIMIX_DONE;
     SIMIX_request_answer(req);
     return;