A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
[surf] Move the host ns3 hook to routingEdgeCreatedCallbacks
[simgrid.git]
/
src
/
mc
/
mc_safety.cpp
diff --git
a/src/mc/mc_safety.cpp
b/src/mc/mc_safety.cpp
index
f05de06
..
1642b3a
100644
(file)
--- a/
src/mc/mc_safety.cpp
+++ b/
src/mc/mc_safety.cpp
@@
-1,4
+1,4
@@
-/* Copyright (c) 2008-201
4
. The SimGrid Team.
+/* Copyright (c) 2008-201
5
. The SimGrid Team.
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
@@
-6,21
+6,24
@@
#include <assert.h>
#include <assert.h>
-#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 "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 "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 ");
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;
static int is_exploration_stack_state(mc_state_t current_state){
xbt_fifo_item_t item;
@@
-35,26
+38,23
@@
static int is_exploration_stack_state(mc_state_t current_state){
return 0;
}
return 0;
}
+static void MC_modelcheck_safety_init(void);
+
/**
* \brief Initialize the DPOR exploration algorithm
*/
static void MC_pre_modelcheck_safety()
{
/**
* \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();
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) */
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;
/* Get an enabled process and insert it in the interleave set of the initial state */
smx_process_t process;
@@
-67,15
+67,16
@@
static void MC_pre_modelcheck_safety()
);
xbt_fifo_unshift(mc_stack, initial_state);
);
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)
*/
}
/** \brief Model-check the application using a DFS exploration
* with DPOR (Dynamic Partial Order Reductions)
*/
-
static void MC_modelcheck_safety_main
(void)
+
int MC_modelcheck_safety
(void)
{
{
+ MC_modelcheck_safety_init();
+
char *req_str = NULL;
int value;
smx_simcall_t req = NULL;
char *req_str = NULL;
int value;
smx_simcall_t req = NULL;
@@
-107,9
+108,7
@@
static void MC_modelcheck_safety_main(void)
xbt_free(req_str);
if (dot_output != NULL) {
xbt_free(req_str);
if (dot_output != NULL) {
- MC_SET_MC_HEAP;
req_str = MC_request_get_dot_output(req, value);
req_str = MC_request_get_dot_output(req, value);
- MC_SET_STD_HEAP;
}
MC_state_set_executed_request(state, req, value);
}
MC_state_set_executed_request(state, req, value);
@@
-120,16
+119,14
@@
static void MC_modelcheck_safety_main(void)
/* Answer the request */
MC_simcall_handle(req, value);
/* Answer the request */
MC_simcall_handle(req, value);
-
MC_
wait_for_requests();
+
mc_model_checker->
wait_for_requests();
/* Create the new expanded state */
/* 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();
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 = is_visited_state(next_state)) == NULL) {
@@
-159,8
+156,6
@@
static void MC_modelcheck_safety_main(void)
if (dot_output != NULL)
xbt_free(req_str);
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 */
/* Let's loop again */
/* The interleave set is empty or the maximum depth is reached, let's back-track */
@@
-181,24
+176,19
@@
static void MC_modelcheck_safety_main(void)
}
}
- 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);
/* 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);
visited_state = NULL;
/* Check for deadlocks */
if (MC_deadlock_check()) {
MC_show_deadlock(NULL);
- return;
+ 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
/* 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
@@
-209,6
+199,9
@@
static void MC_modelcheck_safety_main(void)
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);
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))) {
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))) {
@@
-261,16
+254,15
@@
static void MC_modelcheck_safety_main(void)
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
}
}
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 MC_modelcheck_safety_init
(void)
{
if(_sg_mc_termination)
mc_reduce_kind = e_mc_reduce_none;
{
if(_sg_mc_termination)
mc_reduce_kind = e_mc_reduce_none;
@@
-281,33
+273,18
@@
void MC_modelcheck_safety(void)
XBT_INFO("Check non progressive cycles");
else
XBT_INFO("Check a safety property");
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_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();
/* Create exploration stack */
mc_stack = xbt_fifo_new();
- MC_SET_STD_HEAP;
-
MC_pre_modelcheck_safety();
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);
/* 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();
-}
-
}
}