Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add a flag --cfg=contexts/stacksize and rename other context flags to be
[simgrid.git] / src / mc / mc_global.c
index 7c77d37..6c4c2b2 100644 (file)
@@ -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();
 }
 
@@ -78,7 +81,7 @@ void MC_wait_for_requests(void)
   do {
     SIMIX_context_runall(simix_global->process_to_run);
     while((req = SIMIX_request_pop())){
-      if(!SIMIX_request_is_visible(req))
+      if(!MC_request_is_visible(req))
         SIMIX_request_pre(req, 0);
       else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
         req_str = MC_request_to_string(req);
@@ -97,7 +100,7 @@ int MC_deadlock_check()
     deadlock = TRUE;
     xbt_swag_foreach(process, simix_global->process_list){
       if(process->request.call != REQ_NO_REQ
-         && SIMIX_request_is_enabled(&process->request)){
+         && MC_request_is_enabled(&process->request)){
         deadlock = FALSE;
         break;
       }
@@ -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;
+}