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
[mc] Fix the hash computation
[simgrid.git]
/
src
/
mc
/
mc_safety.cpp
diff --git
a/src/mc/mc_safety.cpp
b/src/mc/mc_safety.cpp
index
7336489
..
1642b3a
100644
(file)
--- a/
src/mc/mc_safety.cpp
+++ b/
src/mc/mc_safety.cpp
@@
-6,16
+6,16
@@
#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 "mc_exit.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" {
extern "C" {
@@
-54,7
+54,7
@@
static void MC_pre_modelcheck_safety()
XBT_DEBUG("Initial state");
/* Wait for requests (schedules processes) */
XBT_DEBUG("Initial state");
/* Wait for requests (schedules processes) */
-
MC_
wait_for_requests();
+
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;
@@
-73,7
+73,7
@@
static void MC_pre_modelcheck_safety()
/** \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)
*/
-
void
MC_modelcheck_safety(void)
+
int
MC_modelcheck_safety(void)
{
MC_modelcheck_safety_init();
{
MC_modelcheck_safety_init();
@@
-119,14
+119,14
@@
void MC_modelcheck_safety(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 */
next_state = MC_state_new();
if(_sg_mc_termination && is_exploration_stack_state(next_state)){
MC_show_non_termination();
/* Create the new expanded state */
next_state = MC_state_new();
if(_sg_mc_termination && is_exploration_stack_state(next_state)){
MC_show_non_termination();
-
exit(SIMGRID_EXIT_NON_TERMINATION)
;
+
return SIMGRID_MC_EXIT_NON_TERMINATION
;
}
if ((visited_state = is_visited_state(next_state)) == NULL) {
}
if ((visited_state = is_visited_state(next_state)) == NULL) {
@@
-186,7
+186,7
@@
void MC_modelcheck_safety(void)
/* Check for deadlocks */
if (MC_deadlock_check()) {
MC_show_deadlock(NULL);
/* Check for deadlocks */
if (MC_deadlock_check()) {
MC_show_deadlock(NULL);
-
exit(SIMGRID_EXIT_DEADLOCK)
;
+
return SIMGRID_MC_EXIT_DEADLOCK
;
}
/* Traverse the stack backwards until a state with a non empty interleave
}
/* Traverse the stack backwards until a state with a non empty interleave
@@
-201,7
+201,7
@@
void MC_modelcheck_safety(void)
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, "
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
");
+ "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))) {
@@
-259,7
+259,7
@@
void MC_modelcheck_safety(void)
XBT_INFO("No property violation found.");
MC_print_statistics(mc_stats);
XBT_INFO("No property violation found.");
MC_print_statistics(mc_stats);
-
exit(SIMGRID_EXIT_SUCCESS)
;
+
return SIMGRID_MC_EXIT_SUCCESS
;
}
static void MC_modelcheck_safety_init(void)
}
static void MC_modelcheck_safety_init(void)
@@
-273,7
+273,7
@@
static void MC_modelcheck_safety_init(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");
XBT_DEBUG("Starting the safety algorithm");