-/* Copyright (c) 2008-2014. The SimGrid Team.
+/* Copyright (c) 2008-2015. The SimGrid Team.
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
#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
while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
if (mc_reduce_kind == e_mc_reduce_dpor) {
req = MC_state_get_internal_request(state);
+ if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
+ xbt_die("Mutex is currently not supported with DPOR, "
+ "use --cfg=model-check/reduction:dpor");
const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
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;
_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();
-}
-
}