-/* 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
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include <assert.h>
+#include <cassert>
-#include "mc_state.h"
-#include "mc_request.h"
-#include "mc_safety.h"
-#include "mc_private.h"
-#include "mc_record.h"
-#include "mc_smx.h"
-#include "mc_client.h"
+#include <cstdio>
-#include "xbt/mmalloc/mmprivate.h"
+#include <xbt/log.h>
+#include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
+#include <xbt/fifo.h>
+#include <xbt/sysdep.h>
+
+#include "src/mc/mc_state.h"
+#include "src/mc/mc_request.h"
+#include "src/mc/mc_safety.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_record.h"
+#include "src/mc/mc_smx.h"
+#include "src/mc/mc_client.h"
+#include "src/mc/mc_exit.h"
+
+#include "src/xbt/mmalloc/mmprivate.h"
extern "C" {
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
+}
+
+namespace simgrid {
+namespace mc {
+
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)) {
+ for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; 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 0;
}
+static void modelcheck_safety_init(void);
+
/**
* \brief Initialize the DPOR exploration algorithm
*/
-static void MC_pre_modelcheck_safety()
+static void 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);
+ simgrid::mc::visited_states = simgrid::xbt::newDeleteDynar<simgrid::mc::VisitedState>();
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;
+ mc_model_checker->wait_for_requests();
/* Get an enabled process and insert it in the interleave set of the initial state */
- smx_process_t process;
- MC_EACH_SIMIX_PROCESS(process,
- if (MC_process_is_enabled(process)) {
- MC_state_interleave_process(initial_state, process);
- if (mc_reduce_kind != e_mc_reduce_none)
+ for (auto& p : mc_model_checker->process().simix_processes())
+ if (simgrid::mc::process_is_enabled(&p.copy)) {
+ MC_state_interleave_process(initial_state, &p.copy);
+ if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
break;
}
- );
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)
+int modelcheck_safety(void)
{
- char *req_str = NULL;
+ modelcheck_safety_init();
+
+ char *req_str = nullptr;
int value;
- smx_simcall_t req = NULL;
- mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
- xbt_fifo_item_t item = NULL;
- mc_visited_state_t visited_state = NULL;
+ smx_simcall_t req = nullptr;
+ mc_state_t state = nullptr, prev_state = NULL, next_state = NULL;
+ xbt_fifo_item_t item = nullptr;
+ simgrid::mc::VisitedState* visited_state = nullptr;
while (xbt_fifo_size(mc_stack) > 0) {
/* If there are processes to interleave and the maximum depth has not been reached
then perform one step of the exploration algorithm */
if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
- && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
+ && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
- req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+ req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
XBT_DEBUG("Execute: %s", req_str);
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;
- }
+ if (dot_output != nullptr)
+ req_str = simgrid::mc::request_get_dot_output(req, value);
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
// MC_execute_transition(req, value)
/* Answer the request */
- MC_simcall_handle(req, value);
- MC_wait_for_requests();
+ simgrid::mc::handle_simcall(req, value);
+ mc_model_checker->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;
+ return SIMGRID_MC_EXIT_NON_TERMINATION;
}
- if ((visited_state = is_visited_state(next_state)) == NULL) {
+ if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
- smx_process_t process = NULL;
- MC_EACH_SIMIX_PROCESS(process,
- if (MC_process_is_enabled(process)) {
- MC_state_interleave_process(next_state, process);
- if (mc_reduce_kind != e_mc_reduce_none)
+ for (auto& p : mc_model_checker->process().simix_processes())
+ if (simgrid::mc::process_is_enabled(&p.copy)) {
+ MC_state_interleave_process(next_state, &p.copy);
+ if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
break;
}
- );
- if (dot_output != NULL)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
+ if (dot_output != nullptr)
+ std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
- } else {
+ } else if (dot_output != nullptr)
+ std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
- if (dot_output != NULL)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
-
- }
xbt_fifo_unshift(mc_stack, next_state);
- if (dot_output != NULL)
+ if (dot_output != nullptr)
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 */
} else {
- if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
+ if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
- if (user_max_depth_reached && visited_state == NULL)
+ if (user_max_depth_reached && visited_state == nullptr)
XBT_DEBUG("User max depth reached !");
- else if (visited_state == NULL)
+ else if (visited_state == nullptr)
XBT_WARN("/!\\ Max depth reached ! /!\\ ");
else
XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
- } else {
-
+ } else
XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
- }
-
- 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;
+ visited_state = nullptr;
/* Check for deadlocks */
if (MC_deadlock_check()) {
- MC_show_deadlock(NULL);
- return;
+ MC_show_deadlock(nullptr);
+ return SIMGRID_MC_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
state that executed that previous request. */
while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
- if (mc_reduce_kind == e_mc_reduce_dpor) {
+ if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::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))) {
+ if (simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
- req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
+ req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
xbt_free(req_str);
prev_req = MC_state_get_executed_request(state, &value);
- req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
+ req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
XBT_DEBUG("%s (state=%d)", req_str, state->num);
xbt_free(req_str);
}
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);
+ return SIMGRID_MC_EXIT_SUCCESS;
}
-void MC_modelcheck_safety(void)
+static void 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;
+ simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
+ else if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
+ simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::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();
+ mc_model_checker->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();
+ 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();
+ initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
}
}
+}
