-/* 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"
+#include "src/xbt/mmalloc/mmprivate.h"
extern "C" {
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
*/
/** \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;
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) {
/* Check for deadlocks */
if (MC_deadlock_check()) {
MC_show_deadlock(NULL);
- return;
+ exit(SIMGRID_EXIT_DEADLOCK);
}
/* Traverse the stack backwards until a state with a non empty interleave
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:none");
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))) {
}
}
}
+
+ XBT_INFO("No property violation found.");
MC_print_statistics(mc_stats);
- return;
+ 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;
/* Save the initial state */
initial_global_state = xbt_new0(s_mc_global_t, 1);
initial_global_state->snapshot = MC_take_snapshot(0);
-
- MC_modelcheck_safety_main();
-
- xbt_abort();
- //MC_exit();
-}
-
}