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;
}
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;
}
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;
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;
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;
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);
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;
}
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);
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);
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);
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 */
}
}
- 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);
}
}
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);
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;
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
}
-
void MC_modelcheck(void)
{
MC_init_safety();
MC_show_stack_safety(stack);
- if(!_surf_do_mc_checkpoint){
+ if(!_surf_mc_checkpoint){
mc_state_t state;
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) {
/********************************** 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);
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
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;
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;
#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)");
}
}
-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)
}
-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);
}
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",
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.
