From: Martin Quinson <martin.quinson@loria.fr>
Date: Thu, 21 Jun 2012 15:17:50 +0000 (+0200)
Subject: Cleanups in the --cfg options regarding model-checking
X-Git-Tag: v3_8~518
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/be647c10d0b1d760b036f1205f314002637d9876

Cleanups in the --cfg options regarding model-checking

plus, various internal cleanups. Also, we broke the liveness checking
for some obscure reason that we fail to see right now...
---

diff --git a/examples/msg/mc/bugged1_for_liveness.c b/examples/msg/mc/bugged1_for_liveness.c
index b1f2112af6..3aa5b55e29 100644
--- a/examples/msg/mc/bugged1_for_liveness.c
+++ b/examples/msg/mc/bugged1_for_liveness.c
@@ -128,16 +128,17 @@ int client(int argc, char *argv[])
 
 int main(int argc, char *argv[])
 {
-  MC_automaton_load("promela1_bugged1_liveness");
+  MSG_init(&argc, argv);
+
+  MSG_config("model-check/property","promela1_bugged1_liveness");
   MC_automaton_new_propositional_symbol("r", &predR);
   MC_automaton_new_propositional_symbol("cs", &predCS);
   
-  MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_bugged1_liveness.xml");
-  MSG_main_liveness();
+  MSG_main();
 
   return 0;
 }
diff --git a/examples/msg/mc/bugged1_while_liveness.c b/examples/msg/mc/bugged1_while_liveness.c
index b8da0a149a..5f50a5968e 100644
--- a/examples/msg/mc/bugged1_while_liveness.c
+++ b/examples/msg/mc/bugged1_while_liveness.c
@@ -119,16 +119,17 @@ int client(int argc, char *argv[])
 int main(int argc, char *argv[])
 {
 
-  MC_automaton_load("promela1_bugged1_liveness");
+  MSG_init(&argc, argv);
+
+  MSG_config("model-check/property","promela1_bugged1_liveness");
   MC_automaton_new_propositional_symbol("r", &predR);
   MC_automaton_new_propositional_symbol("cs", &predCS);
   
-  MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_bugged1_liveness.xml");
-  MSG_main_liveness();
+  MSG_main();
 
   return 0;
 }
diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index 3209cff42b..c3337a4dc7 100644
--- a/examples/msg/mc/bugged2_liveness.c
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -172,19 +172,20 @@ int main(int argc, char *argv[])
   buffer = malloc(8*sizeof(char));
   buffer[0]='\0';
 
-  MC_automaton_load("promela2_bugged2_liveness");
+  MSG_init(&argc, argv);
+
+  MSG_config("model-check/property","promela2_bugged2_liveness");
   MC_automaton_new_propositional_symbol("pready", &predPready);
   MC_automaton_new_propositional_symbol("cready", &predCready);
   MC_automaton_new_propositional_symbol("consume", &predConsume);
   MC_automaton_new_propositional_symbol("produce", &predProduce);
   
-  MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("consumer", consumer);
   MSG_function_register("producer", producer);
   MSG_launch_application("deploy_bugged2_liveness.xml");
-  MSG_main_liveness();
+  MSG_main();
 
   return 0;
 
diff --git a/examples/msg/mc/centralized_liveness.c b/examples/msg/mc/centralized_liveness.c
index b031038971..238dd45665 100644
--- a/examples/msg/mc/centralized_liveness.c
+++ b/examples/msg/mc/centralized_liveness.c
@@ -99,15 +99,16 @@ int client(int argc, char *argv[])
 int main(int argc, char *argv[])
 {
   
-  MC_automaton_load("promela_centralized_liveness");
+  MSG_init(&argc, argv);
+
+  MSG_config("model-check/property","promela_centralized_liveness");
   MC_automaton_new_propositional_symbol("cs", &predCS);
   
-  MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_centralized_liveness.xml");
-  MSG_main_liveness();
+  MSG_main();
 
   return 0;
 
diff --git a/examples/msg/mc/centralized_liveness_deadlock.c b/examples/msg/mc/centralized_liveness_deadlock.c
index 6d1e175fcf..b3c9d40e23 100644
--- a/examples/msg/mc/centralized_liveness_deadlock.c
+++ b/examples/msg/mc/centralized_liveness_deadlock.c
@@ -96,15 +96,16 @@ int client(int argc, char *argv[])
 int main(int argc, char *argv[])
 {
 
-  MC_automaton_load("promela_centralized_liveness");
+  MSG_init(&argc, argv);
+
+  MSG_config("model-check/property","promela_centralized_liveness");
   MC_automaton_new_propositional_symbol("cs", &predCS);
   
-  MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_centralized_liveness.xml");
-  MSG_main_liveness();
+  MSG_main();
 
   return 0;
 
diff --git a/examples/msg/mc/test_snapshot.c b/examples/msg/mc/test_snapshot.c
index 59c7fc6495..32de8df2b2 100644
--- a/examples/msg/mc/test_snapshot.c
+++ b/examples/msg/mc/test_snapshot.c
@@ -120,8 +120,9 @@ int client(int argc, char *argv[])
   return 0;
 }
 
-int main(int argc, char *argv[])
-{
+int main(int argc, char *argv[]) {
+
+  MSG_init(&argc, argv);
 
   d1 = xbt_dynar_new(sizeof(char *), NULL);
   XBT_DEBUG("Dynar d1 : %p -> %p", &d1, d1);
@@ -129,16 +130,15 @@ int main(int argc, char *argv[])
   xbt_dynar_push(d1, &c1);
   xbt_dynar_push(d1, &c1);
 
-  MC_automaton_load("promela_test_snapshot");
+  MSG_config("model-check/property","promela_test_snapshot");
   MC_automaton_new_propositional_symbol("r", &predR);
   MC_automaton_new_propositional_symbol("cs", &predCS);
   
-  MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_test_snapshot.xml");
-  MSG_main_liveness();
+  MSG_main();
 
   return 0;
 }
diff --git a/include/msg/msg.h b/include/msg/msg.h
index da0fca17c2..a947576db3 100644
--- a/include/msg/msg.h
+++ b/include/msg/msg.h
@@ -57,7 +57,6 @@ XBT_PUBLIC(void) MSG_config(const char *name, ...);
 
 XBT_PUBLIC(void) MSG_init_nocheck(int *argc, char **argv);
 XBT_PUBLIC(MSG_error_t) MSG_main(void);
-XBT_PUBLIC(MSG_error_t) MSG_main_liveness(void);
 XBT_PUBLIC(MSG_error_t) MSG_clean(void);
 XBT_PUBLIC(void) MSG_function_register(const char *name,
                                        xbt_main_func_t code);
diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index da83b88a29..bd966e6243 100644
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -20,7 +20,6 @@ extern int _surf_do_model_check;
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(int) MC_random(int min, int max);
 XBT_PUBLIC(void) MC_diff(void);
-XBT_PUBLIC(void) MC_automaton_load(const char *file);
 XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct);
 
 
diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 52c568de92..eca3d4246d 100644
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -19,7 +19,15 @@
 
 SG_BEGIN_DECL()
 
+extern char*_surf_mc_property_file; /* fixme: better location? */
+
 /********************************* Global *************************************/
+void _mc_cfg_cb_reduce(const char *name, int pos);
+void _mc_cfg_cb_checkpoint(const char *name, int pos);
+void _mc_cfg_cb_property(const char *name, int pos);
+
+XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
+
 XBT_PUBLIC(void) MC_init_safety(void);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_exit_liveness(void);
@@ -27,6 +35,7 @@ XBT_PUBLIC(void) MC_modelcheck(void);
 XBT_PUBLIC(void) MC_modelcheck_liveness(void);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
+void MC_automaton_load(const char *file);
 
 /********************************* Memory *************************************/
 XBT_PUBLIC(void) MC_memory_init(void);  /* Initialize the memory subsystem */
diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index dd0aba395d..707ed9b102 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -111,7 +111,7 @@ void MC_dpor(void)
         }
       }
 
-      if(_surf_do_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_do_mc_checkpoint == 0)){
+      if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
         next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
         MC_take_snapshot(next_state->system_state);
       }
@@ -174,7 +174,7 @@ void MC_dpor(void)
         }
         if (MC_state_interleave_size(state)) {
           /* We found a back-tracking point, let's loop */
-          if(_surf_do_mc_checkpoint){
+          if(_surf_mc_checkpoint){
             if(state->system_state != NULL){
               MC_restore_snapshot(state->system_state);
               xbt_fifo_unshift(mc_stack_safety, state);
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index f62e2f7230..4876944315 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -18,6 +18,31 @@ XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
                                 "Logging specific to MC (global)");
 
+/* Configuration support */
+e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
+
+void _mc_cfg_cb_reduce(const char *name, int pos) {
+  char *val= xbt_cfg_get_string(_surf_cfg_set, name);
+  if (!strcasecmp(val,"none")) {
+    mc_reduce_kind = e_mc_reduce_none;
+  } else if (!strcasecmp(val,"dpor")) {
+    mc_reduce_kind = e_mc_reduce_dpor;
+  } else {
+    xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
+  }
+  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+
+void _mc_cfg_cb_checkpoint(const char *name, int pos) {
+  _surf_mc_checkpoint = xbt_cfg_get_int(_surf_cfg_set, name);
+  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+void _mc_cfg_cb_property(const char *name, int pos) {
+  _surf_mc_property_file= xbt_cfg_get_string(_surf_cfg_set, name);
+  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+
+
 /* MC global data structures */
 
 mc_state_t mc_current_state = NULL;
@@ -40,6 +65,24 @@ xbt_automaton_t _mc_property_automaton = NULL;
 
 static void MC_assert_pair(int prop);
 
+void MC_do_the_modelcheck_for_real() {
+  if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
+    if (mc_reduce_kind==e_mc_reduce_unset)
+      mc_reduce_kind=e_mc_reduce_dpor;
+
+    XBT_INFO("Check a safety property");
+    MC_modelcheck();
+
+  } else  {
+
+    if (mc_reduce_kind==e_mc_reduce_unset)
+      mc_reduce_kind=e_mc_reduce_none;
+
+    XBT_INFO("Check the liveness property %s",_surf_mc_property_file);
+    MC_automaton_load(_surf_mc_property_file);
+    MC_modelcheck_liveness();
+  }
+}
 
 /**
  *  \brief Initialize the model-checker data structures
@@ -77,7 +120,6 @@ void MC_init_safety(void)
 }
 
 
-
 void MC_modelcheck(void)
 {
   MC_init_safety();
@@ -343,7 +385,7 @@ void MC_dump_stack_safety(xbt_fifo_t stack)
 
   MC_show_stack_safety(stack);
 
-  if(!_surf_do_mc_checkpoint){
+  if(!_surf_mc_checkpoint){
 
     mc_state_t state;
 
@@ -520,9 +562,11 @@ void MC_diff(void){
 
 void MC_automaton_load(const char *file){
   MC_SET_RAW_MEM;
+
   if (_mc_property_automaton == NULL)
     _mc_property_automaton = xbt_automaton_new();
   xbt_automaton_load(_mc_property_automaton,file);
+
   MC_UNSET_RAW_MEM;
 }
 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 77d842da75..02aa05a8f7 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -182,6 +182,12 @@ memory_map_t get_memory_map(void);
 
 
 /********************************** DPOR for safety  **************************************/
+typedef enum {
+  e_mc_reduce_unset,
+  e_mc_reduce_none,
+  e_mc_reduce_dpor
+} e_mc_reduce_t;
+extern e_mc_reduce_t mc_reduce_kind;
 
 void MC_dpor_init(void);
 void MC_dpor(void);
@@ -268,9 +274,10 @@ void MC_dump_stack_liveness(xbt_fifo_t stack);
 void MC_pair_stateless_delete(mc_pair_stateless_t pair);
 
 /********************************** Configuration of MC **************************************/
-
-extern int _surf_do_mc_checkpoint;
 extern xbt_fifo_t mc_stack_safety;
 
+extern int _surf_mc_checkpoint;
+extern char* _surf_mc_property_file;
+
 
 #endif
diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 3d89d84e47..ec73bfd36f 100644
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -11,11 +11,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
 static char* pointer_to_string(void* pointer);
 static char* buff_size_to_string(size_t size);
 
-int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
-{
-  if(_surf_do_model_check == 2)
+int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) {
+  if(mc_reduce_kind == e_mc_reduce_none)
     return TRUE;
-  
+
 
   if (r1->issuer == r2->issuer)
     return FALSE;
diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c
index 681bdef8b9..9012803624 100644
--- a/src/msg/msg_global.c
+++ b/src/msg/msg_global.c
@@ -108,26 +108,9 @@ MSG_error_t MSG_main(void)
   fflush(stdout);
   fflush(stderr);
 
-  if (MC_IS_ENABLED) {
-    MC_modelcheck();
-  }
-  else {
-    SIMIX_run();
-  }
-  return MSG_OK;
-}
-
-
-MSG_error_t MSG_main_liveness()
-{
-  /* Clean IO before the run */
-  fflush(stdout);
-  fflush(stderr);
-
-  if (MC_IS_ENABLED) {
-    MC_modelcheck_liveness();
-  }
-  else {
+  if (MC_IS_ENABLED && (_surf_do_model_check == 1)) {
+    MC_do_the_modelcheck_for_real();
+  } else {
     SIMIX_run();
   }
   return MSG_OK;
diff --git a/src/surf/surf_config.c b/src/surf/surf_config.c
index 830675d845..299219f4e1 100644
--- a/src/surf/surf_config.c
+++ b/src/surf/surf_config.c
@@ -12,6 +12,7 @@
 #include "surf/surf_private.h"
 #include "surf/surf_routing.h"  /* COORD_HOST_LEVEL and COORD_ASR_LEVEL */
 #include "simgrid/simix.h"
+#include "mc/mc.h" /* configuration callbacks of model-checking */
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_config, surf,
                                 "About the configuration of surf (and the rest of the simulation)");
@@ -240,14 +241,6 @@ static void _surf_cfg_cb_model_check(const char *name, int pos)
   }
 }
 
-extern int _surf_do_mc_checkpoint;   /* this variable lives in xbt_main until I find a right location for it */
-
-static void _surf_cfg_cb_mc_checkpoint(const char *name, int pos)
-{
-  _surf_do_mc_checkpoint = xbt_cfg_get_int(_surf_cfg_set, name);
-  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
-}
-
 extern int _surf_do_verbose_exit;
 
 static void _surf_cfg_cb_verbose_exit(const char *name, int pos)
@@ -256,8 +249,7 @@ static void _surf_cfg_cb_verbose_exit(const char *name, int pos)
 }
 
 
-static void _surf_cfg_cb_context_factory(const char *name, int pos)
-{
+static void _surf_cfg_cb_context_factory(const char *name, int pos) {
   smx_context_factory_name = xbt_cfg_get_string(_surf_cfg_set, name);
 }
 
@@ -482,27 +474,35 @@ void surf_config_init(int *argc, char **argv)
                      xbt_cfgelm_int, &default_value_int, 0, 1,
                      NULL, NULL);
 
-    /* do model-check */
+    /* do model-checking */
     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)",
+                     "Verify the system through model-checking instead of simulating it (EXPERIMENTAL)",
                      xbt_cfgelm_int, &default_value_int, 0, 1,
                      _surf_cfg_cb_model_check, NULL);
-    
-    /*
-       FIXME: this function is not setting model-check to it's default value because
-       internally it calls to variable->cb_set that in this case is the function 
-       _surf_cfg_cb_model_check which sets it's value to 1 (instead of the default value 0)
-       xbt_cfg_set_int(_surf_cfg_set, "model-check", default_value_int); */
 
-
-    /* do stateful model-check */
+    /* do stateful model-checking */
     default_value_int = 0;
-    xbt_cfg_register(&_surf_cfg_set, "mc-checkpoint",
-                     "Activate the stateful model-checking of the \"simulated\" system (EXPERIMENTAL -- msg only for now), value corresponding to steps between each checkpoint",
+    xbt_cfg_register(&_surf_cfg_set, "model-check/checkpoint",
+                     "Specify the amount of steps between checkpoints during stateful model-checking (default: 0 => stateless verification). "
+                     "If value=1, one checkpoint is saved for each step => faster verification, but huge memory consumption; higher values are good compromises between speed and memory consumption.",
                      xbt_cfgelm_int, &default_value_int, 0, 1,
-                     _surf_cfg_cb_mc_checkpoint, NULL);
+                     _mc_cfg_cb_checkpoint, NULL);
     
+    /* do liveness model-checking */
+    default_value = xbt_strdup("");
+    xbt_cfg_register(&_surf_cfg_set, "model-check/property",
+                     "Specify the name of the file containing the property. It must be the result of the ltl2ba program.",
+                     xbt_cfgelm_string, &default_value, 0, 1,
+                     _mc_cfg_cb_property, NULL);
+
+    /* Specify the kind of model-checking reduction */
+    default_value = xbt_strdup("unset");
+    xbt_cfg_register(&_surf_cfg_set, "model-check/reduction",
+                     "Specify the kind of exploration reduction (either none or DPOR)",
+                     xbt_cfgelm_string, &default_value, 0, 1,
+                     _mc_cfg_cb_reduce, NULL);
+
     /* do verbose-exit */
     default_value_int = 1;
     xbt_cfg_register(&_surf_cfg_set, "verbose-exit",
diff --git a/src/xbt/xbt_main.c b/src/xbt/xbt_main.c
index 892fd30d4b..2ca0ed635a 100644
--- a/src/xbt/xbt_main.c
+++ b/src/xbt/xbt_main.c
@@ -26,8 +26,9 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(module, xbt, "module handling");
 char *xbt_binary_name = NULL;   /* Mandatory to retrieve neat backtraces */
 int xbt_initialized = 0;
 
-int _surf_do_model_check = 0;   /* this variable is used accros the libraries, and must be declared in XBT so that it's also defined in GRAS (not only in libsimgrid) */
-int _surf_do_mc_checkpoint = 0;   /* this variable is used accros the libraries, and must be declared in XBT so that it's also defined in GRAS (not only in libsimgrid) */
+int _surf_do_model_check = 0;
+int _surf_mc_checkpoint=0;
+char* _surf_mc_property_file=NULL;
 
 /* Declare xbt_preinit and xbt_postexit as constructor/destructor of the library.
  * This is crude and rather compiler-specific, unfortunately.