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)
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")
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()
${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
${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
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;
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);
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;
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)
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
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", "*");
} 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)
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)
{
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
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
*/
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 */
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);
"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 */