new option to any SimGrid-based simulator: --cfg=model-check:1 (for now, that's a...

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

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 064a753..454fc4b 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -31,6 +31,10 @@ XBT_PUBLIC(void) MC_transition_set_comm(mc_transition_t, smx_comm_t);
 XBT_PUBLIC(void) MC_memory_init(void);   /* Initialize the memory subsystem */
 XBT_PUBLIC(void) MC_memory_exit(void);
 
 XBT_PUBLIC(void) MC_memory_init(void);   /* Initialize the memory subsystem */
 XBT_PUBLIC(void) MC_memory_exit(void);
 

+/*
+ * Boolean indicating whether we want to activate the model-checker
+ */
+extern int _surf_do_model_check;

 
 
 SG_END_DECL()
 
 
 SG_END_DECL()

diff --git a/src/msg/global.c b/src/msg/global.c
index a6e0c91..d711b68 100644 (file)
--- a/src/msg/global.c
+++ b/src/msg/global.c
@@ -5,6 +5,7 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "msg/private.h"
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "msg/private.h"

+#include "mc/mc.h"

 #include "xbt/sysdep.h"
 #include "xbt/log.h"
 #include "xbt/virtu.h"
 #include "xbt/sysdep.h"
 #include "xbt/log.h"
 #include "xbt/virtu.h"


@@ -139,7 +140,10 @@ MSG_error_t MSG_main(void)
   fflush(stderr);
   SIMIX_init();
 
   fflush(stderr);
   SIMIX_init();
 

-  while (SIMIX_solve(NULL, NULL) != -1.0);
+  if (_surf_do_model_check)
+    MC_modelcheck(1);
+  else
+    while (SIMIX_solve(NULL, NULL) != -1.0);

   
   return MSG_OK;
 }
   
   return MSG_OK;
 }

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 4987f8f..465fba7 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -6,6 +6,7 @@
 
 #include "private.h"
 #include "xbt/log.h"
 
 #include "private.h"
 #include "xbt/log.h"

+#include "mc/mc.h"

 #include "xbt/dict.h"
 
 /* Pimple to get an histogram of message sizes in the simulation */
 #include "xbt/dict.h"
 
 /* Pimple to get an histogram of message sizes in the simulation */


@@ -83,7 +84,7 @@ smx_comm_t SIMIX_rdv_get_request(smx_rdv_t rdv, smx_comm_type_t type) {
     DEBUG0("Communication request found!");
     xbt_fifo_shift(rdv->comm_fifo);
     SIMIX_communication_use(comm);
     DEBUG0("Communication request found!");
     xbt_fifo_shift(rdv->comm_fifo);
     SIMIX_communication_use(comm);

-    comm->rdv = NULL;    
+    comm->rdv = NULL;

     return comm;
   }
 
     return comm;
   }
 


@@ -200,7 +201,7 @@ static inline void SIMIX_communication_use(smx_comm_t comm)
 
 /**
  *  \brief Start the simulation of a communication request
 
 /**
  *  \brief Start the simulation of a communication request

- *  \param comm The   comm->rdv = NULL;communication request
+ *  \param comm The communication request

  */
 static inline void SIMIX_communication_start(smx_comm_t comm)
 {
  */
 static inline void SIMIX_communication_start(smx_comm_t comm)
 {


@@ -467,7 +468,14 @@ smx_comm_t SIMIX_network_isend(smx_rdv_t rdv, double task_size, double rate,
     void *src_buff, size_t src_buff_size, void *data)
 {
   smx_comm_t comm;
     void *src_buff, size_t src_buff_size, void *data)
 {
   smx_comm_t comm;

+  mc_transition_t trans=NULL;

 
 

+  if (_surf_do_model_check) {
+    /* Let's intercept the communication and control it from the model-checker */
+    trans = MC_create_transition(mc_isend, SIMIX_process_self(), rdv, NULL);
+    SIMIX_process_yield();
+  }
+  

   /* Look for communication request matching our needs.
      If it is not found then create it and push it into the rendez-vous point */
   comm = SIMIX_rdv_get_request(rdv, comm_recv);
   /* Look for communication request matching our needs.
      If it is not found then create it and push it into the rendez-vous point */
   comm = SIMIX_rdv_get_request(rdv, comm_recv);


@@ -485,13 +493,24 @@ smx_comm_t SIMIX_network_isend(smx_rdv_t rdv, double task_size, double rate,
   comm->src_buff_size = src_buff_size;
   comm->data = data;
 
   comm->src_buff_size = src_buff_size;
   comm->data = data;
 

+  /* Associate the simix communication to the mc transition */
+  if (_surf_do_model_check)
+    MC_transition_set_comm(trans, comm);
+  

   SIMIX_communication_start(comm);
   return comm;
 }
 
 smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_size) {
   smx_comm_t comm;
   SIMIX_communication_start(comm);
   return comm;
 }
 
 smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_size) {
   smx_comm_t comm;

-
+  mc_transition_t trans=NULL;
+  
+  if (_surf_do_model_check) {
+    /* Let's intercept the communication and control it from the model-checker */
+    trans = MC_create_transition(mc_irecv, SIMIX_process_self(), rdv, NULL);
+    SIMIX_process_yield();
+  }
+  

   /* Look for communication request matching our needs.
      If it is not found then create it and push it into the rendez-vous point */
   comm = SIMIX_rdv_get_request(rdv, comm_send);
   /* Look for communication request matching our needs.
      If it is not found then create it and push it into the rendez-vous point */
   comm = SIMIX_rdv_get_request(rdv, comm_send);


@@ -506,18 +525,32 @@ smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_s
   comm->dst_buff = dst_buff;
   comm->dst_buff_size = dst_buff_size;
 
   comm->dst_buff = dst_buff;
   comm->dst_buff_size = dst_buff_size;
 

+  /* Associate the simix communication to the mc transition */
+  if (_surf_do_model_check)
+    MC_transition_set_comm(trans, comm);
+ 

   SIMIX_communication_start(comm);
   return comm;
 }
 
 /** @brief blocks until the communication terminates or the timeout occurs */
 XBT_INLINE void SIMIX_network_wait(smx_comm_t comm, double timeout) {
   SIMIX_communication_start(comm);
   return comm;
 }
 
 /** @brief blocks until the communication terminates or the timeout occurs */
 XBT_INLINE void SIMIX_network_wait(smx_comm_t comm, double timeout) {

+  if (_surf_do_model_check) {
+    /* Let's intercept the communication and control it from the model-checker */
+    MC_create_transition(mc_wait, SIMIX_process_self(), comm->rdv, comm);
+    SIMIX_process_yield();
+  }

   /* Wait for communication completion */
   SIMIX_communication_wait_for_completion(comm, timeout);
 }
 
 /** @Returns whether the (asynchronous) communication is done yet or not */
 XBT_INLINE int SIMIX_network_test(smx_comm_t comm) {
   /* Wait for communication completion */
   SIMIX_communication_wait_for_completion(comm, timeout);
 }
 
 /** @Returns whether the (asynchronous) communication is done yet or not */
 XBT_INLINE int SIMIX_network_test(smx_comm_t comm) {

+  if (_surf_do_model_check) {
+    /* Let's intercept the communication and control it from the model-checker */
+    MC_create_transition(mc_test, SIMIX_process_self(), comm->rdv, comm);
+    SIMIX_process_yield();
+  }

   return comm->sem?SIMIX_sem_would_block(comm->sem):0;
 }
 
   return comm->sem?SIMIX_sem_would_block(comm->sem):0;
 }
 


@@ -530,6 +563,12 @@ unsigned int SIMIX_network_waitany(xbt_dynar_t comms) {
   unsigned int cursor, found_comm=-1;
   smx_comm_t comm,comm_finished=NULL;
 
   unsigned int cursor, found_comm=-1;
   smx_comm_t comm,comm_finished=NULL;
 

+  if (_surf_do_model_check) {
+    /* Let's intercept the communication and control it from the model-checker */
+    MC_create_transition(mc_waitany, SIMIX_process_self(), NULL, NULL);
+    SIMIX_process_yield();
+  }
+  

   xbt_dynar_foreach(comms,cursor,comm){
     xbt_dynar_push(sems,&(comm->sem));
   }
   xbt_dynar_foreach(comms,cursor,comm){
     xbt_dynar_push(sems,&(comm->sem));
   }

diff --git a/src/surf/surf.c b/src/surf/surf.c
index 95a6dca..a963b61 100644 (file)
--- a/src/surf/surf.c
+++ b/src/surf/surf.c
@@ -8,6 +8,7 @@
 
 #include "surf_private.h"
 #include "xbt/module.h"
 
 #include "surf_private.h"
 #include "xbt/module.h"

+#include "mc/mc.h"

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_kernel, surf,
                                 "Logging specific to SURF (kernel)");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_kernel, surf,
                                 "Logging specific to SURF (kernel)");


@@ -252,6 +253,10 @@ XBT_LOG_EXTERNAL_CATEGORY(surf_network_gtnets);
 
 void surf_init(int *argc, char **argv)
 {
 
 void surf_init(int *argc, char **argv)
 {

+
+  if (_surf_do_model_check)
+    MC_memory_init();
+  

   /* Connect our log channels: that must be done manually under windows */
   XBT_LOG_CONNECT(surf_cpu, surf);
   XBT_LOG_CONNECT(surf_kernel, surf);
   /* Connect our log channels: that must be done manually under windows */
   XBT_LOG_CONNECT(surf_cpu, surf);
   XBT_LOG_CONNECT(surf_kernel, surf);

diff --git a/src/surf/surf_config.c b/src/surf/surf_config.c
index 7446e4f..68fb17e 100644 (file)
--- a/src/surf/surf_config.c
+++ b/src/surf/surf_config.c
@@ -141,6 +141,12 @@ static void _surf_cfg_cb__surf_path(const char *name, int pos) {
   xbt_dynar_push(surf_path, &path);
 }
 
   xbt_dynar_push(surf_path, &path);
 }
 

+/* callback to decide if we want to use the model-checking */
+int _surf_do_model_check = 0; /* this variable is used accros the lib */
+
+static void _surf_cfg_cb_model_check(const char *name, int pos) {
+  _surf_do_model_check = 1;
+}

 
 #ifdef HAVE_GTNETS
 static void _surf_cfg_cb__gtnets_jitter(const char *name, int pos){
 
 #ifdef HAVE_GTNETS
 static void _surf_cfg_cb__gtnets_jitter(const char *name, int pos){


@@ -245,6 +251,12 @@ void surf_config_init(int *argc, char **argv)
                      "Update the constraint set propagating recursively to others constraints",
                      xbt_cfgelm_int, &default_value_int, 0, 1, _surf_cfg_cb__surf_maxmin_selective_update, NULL);
 
                      "Update the constraint set propagating recursively to others constraints",
                      xbt_cfgelm_int, &default_value_int, 0, 1, _surf_cfg_cb__surf_maxmin_selective_update, NULL);
 

+    /* do model-check */
+    default_value_int = 0;
+    xbt_cfg_register(&_surf_cfg_set, "model-check",
+                     "Activate the model-checking of the \"simulated\" system (EXPERIMENTAL -- msg only for now)",
+                     xbt_cfgelm_int, &default_value_int, 0, 1, _surf_cfg_cb_model_check, NULL);
+

 #ifdef HAVE_GTNETS
     xbt_cfg_register(&_surf_cfg_set, "gtnets_jitter",
                      "Double value to oscillate the link latency, uniformly in random interval [-latency*gtnets_jitter,latency*gtnets_jitter)", xbt_cfgelm_double,
 #ifdef HAVE_GTNETS
     xbt_cfg_register(&_surf_cfg_set, "gtnets_jitter",
                      "Double value to oscillate the link latency, uniformly in random interval [-latency*gtnets_jitter,latency*gtnets_jitter)", xbt_cfgelm_double,

diff --git a/src/xbt/mallocator.c b/src/xbt/mallocator.c
index ebc063b..93e6a5b 100644 (file)
--- a/src/xbt/mallocator.c
+++ b/src/xbt/mallocator.c
@@ -12,6 +12,7 @@
 #include "mallocator_private.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(xbt_mallocator, xbt, "Mallocators");
 #include "mallocator_private.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(xbt_mallocator, xbt, "Mallocators");

+extern int _surf_do_model_check; /* kill mallocators when this is true */

 
 /**
  * \brief Constructor
 
 /**
  * \brief Constructor


@@ -43,12 +44,21 @@ xbt_mallocator_t xbt_mallocator_new(int size,
   xbt_assert0(new_f != NULL && free_f != NULL
               && reset_f != NULL, "invalid parameter");
 
   xbt_assert0(new_f != NULL && free_f != NULL
               && reset_f != NULL, "invalid parameter");
 

+  /* Let's force 0 size mallocator! (Dirty hack, blame Martin :) )*/
+
+  /* mallocators and memory mess introduced by model-checking do not mix well together:
+   *   The mallocator will give standard memory when we are using raw memory (so these blocks are killed on restore)
+   *   and the contrary (so these blocks will leak accross restores)
+   */
+  if (_surf_do_model_check)
+    size = 0;
+  

   m = xbt_new0(s_xbt_mallocator_t, 1);
   VERB1("Create mallocator %p", m);
   if (XBT_LOG_ISENABLED(xbt_mallocator, xbt_log_priority_verbose))
     xbt_backtrace_display_current();
 
   m = xbt_new0(s_xbt_mallocator_t, 1);
   VERB1("Create mallocator %p", m);
   if (XBT_LOG_ISENABLED(xbt_mallocator, xbt_log_priority_verbose))
     xbt_backtrace_display_current();
 

-  m->objects = xbt_new0(void *, size);
+  m->objects = xbt_new0(void *, _surf_do_model_check?1:size);

   m->max_size = size;
   m->current_size = 0;
   m->new_f = new_f;
   m->max_size = size;
   m->current_size = 0;
   m->new_f = new_f;

diff --git a/src/xbt/xbt_rl_time.c b/src/xbt/xbt_rl_time.c
index bd035b1..7d6618e 100644 (file)
--- a/src/xbt/xbt_rl_time.c
+++ b/src/xbt/xbt_rl_time.c
@@ -25,3 +25,8 @@ void xbt_sleep(double sec)
 {
   xbt_os_sleep(sec);
 }
 {
   xbt_os_sleep(sec);
 }

+
+/* This horribly badly placed. I just need to get that symbol with that value into libgras so that the mallocators are happy.
+ * EPR will save us all. One day.
+ */
+int _surf_do_model_check = 0;