model-checker : non-progressive cycle detection (enabled with --cfg=model-check/termi...

diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt
index 8effff1..191d4e7 100644 (file)
--- a/examples/smpi/CMakeLists.txt
+++ b/examples/smpi/CMakeLists.txt
@@ -32,6 +32,10 @@ if(enable_smpi)
     add_executable(smpi_send_deterministic mc/send_deterministic.c)
     add_executable(smpi_non_deterministic mc/non_deterministic.c)
     add_executable(smpi_mutual_exclusion mc/mutual_exclusion.c)
+    add_executable(smpi_non_termination1 mc/non_termination1.c)
+    add_executable(smpi_non_termination2 mc/non_termination2.c)
+    add_executable(smpi_non_termination3 mc/non_termination3.c)
+    add_executable(smpi_non_termination4 mc/non_termination4.c)
 
     target_link_libraries(smpi_bugged1 simgrid)
     target_link_libraries(smpi_bugged2 simgrid)
@@ -39,6 +43,10 @@ if(enable_smpi)
     target_link_libraries(smpi_send_deterministic simgrid)
     target_link_libraries(smpi_non_deterministic simgrid)
     target_link_libraries(smpi_mutual_exclusion simgrid)
+    target_link_libraries(smpi_non_termination1 simgrid)
+    target_link_libraries(smpi_non_termination2 simgrid)
+    target_link_libraries(smpi_non_termination3 simgrid)
+    target_link_libraries(smpi_non_termination4 simgrid)
     
     set_target_properties(smpi_bugged1 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     set_target_properties(smpi_bugged2 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
@@ -46,6 +54,10 @@ if(enable_smpi)
     set_target_properties(smpi_send_deterministic PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     set_target_properties(smpi_non_deterministic PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     set_target_properties(smpi_mutual_exclusion PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
+    set_target_properties(smpi_non_termination1 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
+    set_target_properties(smpi_non_termination2 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
+    set_target_properties(smpi_non_termination3 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
+    set_target_properties(smpi_non_termination4 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     
   endif()
   
@@ -74,6 +86,10 @@ set(examples_src
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/send_deterministic.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_deterministic.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/mutual_exclusion.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination1.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination2.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination3.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination4.c
   PARENT_SCOPE
   )
 set(bin_files
@@ -86,6 +102,7 @@ set(bin_files
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_send_deterministic
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_deterministic
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_mutual_exclusion
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_termination
   PARENT_SCOPE
   )
 set(txt_files

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 2bfe7ad..e3fcd97 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -51,6 +51,7 @@ extern int _sg_mc_comms_determinism;
 extern int _sg_mc_send_determinism;
 extern int _sg_mc_safety;
 extern int _sg_mc_liveness;
+extern int _sg_mc_termination;
 
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
@@ -70,6 +71,7 @@ void _mc_cfg_cb_visited(const char *name, int pos);
 void _mc_cfg_cb_dot_output(const char *name, int pos);
 void _mc_cfg_cb_comms_determinism(const char *name, int pos);
 void _mc_cfg_cb_send_determinism(const char *name, int pos);
+void _mc_cfg_cb_termination(const char *name, int pos);
 
 XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
 XBT_PUBLIC(void) MC_init(void);

diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 4745d3a..2eb1d25 100644 (file)
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -366,6 +366,11 @@ int snapshot_compare(void *state1, void *state2)
     s2 = ((mc_visited_pair_t) state2)->graph_state->system_state;
     num1 = ((mc_visited_pair_t) state1)->num;
     num2 = ((mc_visited_pair_t) state2)->num;
+  }else if (_sg_mc_termination) { /* Non-progressive cycle MC */
+    s1 = ((mc_state_t) state1)->system_state;
+    s2 = ((mc_state_t) state2)->system_state;
+    num1 = ((mc_state_t) state1)->num;
+    num2 = ((mc_state_t) state2)->num;
   } else {                      /* Safety or comm determinism MC */
     s1 = ((mc_visited_state_t) state1)->system_state;
     s2 = ((mc_visited_state_t) state2)->system_state;

diff --git a/src/mc/mc_config.c b/src/mc/mc_config.c
index 07c9179..5959b7f 100644 (file)
--- a/src/mc/mc_config.c
+++ b/src/mc/mc_config.c
@@ -58,6 +58,7 @@ int _sg_mc_comms_determinism = 0;
 int _sg_mc_send_determinism = 0;
 int _sg_mc_safety = 0;
 int _sg_mc_liveness = 0;
+int _sg_mc_termination = 0;
 
 
 void _mc_cfg_cb_reduce(const char *name, int pos)
@@ -165,4 +166,14 @@ void _mc_cfg_cb_send_determinism(const char *name, int pos)
   mc_reduce_kind = e_mc_reduce_none;
 }
 
+void _mc_cfg_cb_termination(const char *name, int pos)
+{
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
+    xbt_die
+        ("You are specifying a value to enable/disable the detection of non progressive cycles after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+  }
+  _sg_mc_termination = xbt_cfg_get_boolean(_sg_cfg_set, name);
+  mc_reduce_kind = e_mc_reduce_none;
+}
+
 #endif

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 63ecd05..59425b3 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -173,7 +173,7 @@ void MC_init()
 
   MC_SET_STD_HEAP;
 
-  if (_sg_mc_visited > 0 || _sg_mc_liveness) {
+  if (_sg_mc_visited > 0 || _sg_mc_liveness  || _sg_mc_termination) {
     /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
     MC_ignore_local_variable("e", "*");
     MC_ignore_local_variable("__ex_cleanup", "*");
@@ -333,7 +333,10 @@ void MC_do_the_modelcheck_for_real()
   } else if (!_sg_mc_property_file || _sg_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");
+    if(_sg_mc_termination)
+      XBT_INFO("Check non progressive cycles");
+    else
+      XBT_INFO("Check a safety property");
     MC_modelcheck_safety_init();
   } else {
     if (mc_reduce_kind == e_mc_reduce_unset)
@@ -690,6 +693,15 @@ void MC_show_deadlock(smx_simcall_t req)
   MC_print_statistics(mc_stats);
 }
 
+void MC_show_non_termination(void){
+  XBT_INFO("******************************************");
+  XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+  XBT_INFO("******************************************");
+  XBT_INFO("Counter-example execution trace:");
+  MC_dump_stack_safety(mc_stack);
+  MC_print_statistics(mc_stats);
+}
+
 
 void MC_show_stack_liveness(xbt_fifo_t stack)
 {

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 4a86245..86b7e64 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -56,6 +56,7 @@ void MC_replay_liveness(xbt_fifo_t stack);
 void MC_show_deadlock(smx_simcall_t req);
 void MC_show_stack_safety(xbt_fifo_t stack);
 void MC_dump_stack_safety(xbt_fifo_t stack);
+void MC_show_non_termination(void);
 
 /** Stack (of `mc_state_t`) representing the current position of the
  *  the MC in the exploration graph

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 83460ff..38e0999 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -15,6 +15,20 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 
+static int is_exploration_stack_state(mc_state_t current_state){
+
+  xbt_fifo_item_t item;
+  mc_state_t stack_state;
+  for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
+    stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
+    if(snapshot_compare(stack_state, current_state) == 0){
+      XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
+      return 1;
+    }
+  }
+  return 0;
+}
+
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
@@ -118,6 +132,11 @@ void MC_modelcheck_safety(void)
 
       next_state = MC_state_new();
 
+      if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+          MC_show_non_termination();
+          return;
+      }
+
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 84db3e8..5830913 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -71,7 +71,7 @@ mc_state_t MC_state_new()
   state->in_visited_states = 0;
   state->incomplete_comm_pattern = NULL;
   /* Stateful model checking */
-  if(_sg_mc_checkpoint > 0 && mc_stats->expanded_states % _sg_mc_checkpoint == 0){
+  if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) ||  _sg_mc_termination){
     state->system_state = MC_take_snapshot(state->num);
     if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
       copy_incomplete_communications_pattern(state);

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index 544de00..b2bda9f 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -712,6 +712,12 @@ void sg_config_init(int *argc, char **argv)
                      "Specify the name of dot file corresponding to graph state",
                      xbt_cfgelm_string, 1, 1, _mc_cfg_cb_dot_output, NULL);
     xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/dot_output", "");
+
+     /* Enable/disable non progressive cycles detection with model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/termination",
+                     "Enable/Disable non progressive cycle detection",
+                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_termination, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/termination", "no");
 #endif
 
     /* do verbose-exit */