#include "mc_record.h"
#include "mc_smx.h"
#include "mc_client.h"
+#include "mc_exit.h"
#include "xbt/mmalloc/mmprivate.h"
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;
return 0;
}
+static void MC_modelcheck_safety_init(void);
+
/**
* \brief Initialize the DPOR exploration algorithm
*/
static void MC_pre_modelcheck_safety()
{
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
if (_sg_mc_visited > 0)
visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
mc_state_t initial_state = MC_state_new();
- MC_SET_STD_HEAP;
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
- MC_SET_MC_HEAP;
-
/* Get an enabled process and insert it in the interleave set of the initial state */
smx_process_t process;
MC_EACH_SIMIX_PROCESS(process,
);
xbt_fifo_unshift(mc_stack, initial_state);
- mmalloc_set_current_heap(heap);
}
/** \brief Model-check the application using a DFS exploration
* with DPOR (Dynamic Partial Order Reductions)
*/
-static void MC_modelcheck_safety_main(void)
+void MC_modelcheck_safety(void)
{
+ MC_modelcheck_safety_init();
+
char *req_str = NULL;
int value;
smx_simcall_t req = NULL;
xbt_free(req_str);
if (dot_output != NULL) {
- MC_SET_MC_HEAP;
req_str = MC_request_get_dot_output(req, value);
- MC_SET_STD_HEAP;
}
MC_state_set_executed_request(state, req, value);
MC_wait_for_requests();
/* Create the new expanded state */
- MC_SET_MC_HEAP;
-
next_state = MC_state_new();
if(_sg_mc_termination && is_exploration_stack_state(next_state)){
MC_show_non_termination();
- return;
+ exit(SIMGRID_EXIT_NON_TERMINATION);
}
if ((visited_state = is_visited_state(next_state)) == NULL) {
if (dot_output != NULL)
xbt_free(req_str);
- MC_SET_STD_HEAP;
-
/* Let's loop again */
/* The interleave set is empty or the maximum depth is reached, let's back-track */
}
- MC_SET_MC_HEAP;
-
/* Trash the current state, no longer needed */
xbt_fifo_shift(mc_stack);
XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
- MC_SET_STD_HEAP;
-
visited_state = NULL;
/* Check for deadlocks */
if (MC_deadlock_check()) {
MC_show_deadlock(NULL);
- return;
+ exit(SIMGRID_EXIT_DEADLOCK);
}
- MC_SET_MC_HEAP;
/* Traverse the stack backwards until a state with a non empty interleave
set is found, deleting all the states that have it empty in the way.
For each deleted state, check if the request that has generated it
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
}
}
- MC_SET_STD_HEAP;
}
}
- MC_print_statistics(mc_stats);
- MC_SET_STD_HEAP;
- return;
+ XBT_INFO("No property violation found.");
+ MC_print_statistics(mc_stats);
+ exit(SIMGRID_EXIT_SUCCESS);
}
-void MC_modelcheck_safety(void)
+static void MC_modelcheck_safety_init(void)
{
+ if(_sg_mc_termination)
+ mc_reduce_kind = e_mc_reduce_none;
+ else if (mc_reduce_kind == e_mc_reduce_unset)
+ mc_reduce_kind = e_mc_reduce_dpor;
+ _sg_mc_safety = 1;
+ if (_sg_mc_termination)
+ XBT_INFO("Check non progressive cycles");
+ else
+ XBT_INFO("Check a safety property");
+ MC_wait_for_requests();
+
XBT_DEBUG("Starting the safety algorithm");
_sg_mc_safety = 1;
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
/* Create exploration stack */
mc_stack = xbt_fifo_new();
- MC_SET_STD_HEAP;
-
MC_pre_modelcheck_safety();
- MC_SET_MC_HEAP;
/* Save the initial state */
initial_global_state = xbt_new0(s_mc_global_t, 1);
initial_global_state->snapshot = MC_take_snapshot(0);
- MC_SET_STD_HEAP;
-
- MC_modelcheck_safety_main();
-
- mmalloc_set_current_heap(heap);
-
- xbt_abort();
- //MC_exit();
-}
-
}