From: cristianrosa <cristianrosa@48e7efb5-ca39-0410-a469-dd3cf9ba447f>
Date: Thu, 20 Jan 2011 15:46:02 +0000 (+0000)
Subject: Add a clock per process when running in MC mode.
X-Git-Tag: v3.6_beta2~463
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/208924f0b511eb55c98c74a56a9d9e6b7430c370?hp=76cf83f4634017a34173bbceb819b99d77ac7ba7

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 bf7593a923..d4c01ffd6b 100644
--- 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 4ac7758bd9..6c4c2b23be 100644
--- 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 359560edab..733a7269a6 100644
--- 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 d0e2c53314..059130d929 100644
--- 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 ccd61f541b..eff7ab721b 100644
--- 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;