src/mc/mc_smx.cpp
src/mc/mc_xbt.hpp
src/mc/mc_xbt.cpp
+ src/mc/mc_exit.h
)
set(MC_SIMGRID_MC_SRC
#! ./tesh
-! expect signal SIGABRT
+! expect return 1
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
> [ 0.000000] (0:@) Check a safety property
#! ./tesh
-! expect signal SIGABRT
+! expect return 2
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
#! ./tesh
-! expect signal SIGABRT
+! expect return 2
! timeout 60
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
#! ./tesh
-! expect signal SIGABRT
+! expect return 2
! timeout 90
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
#! ./tesh
-! expect signal SIGABRT
+! expect return 2
! timeout 90
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
#! ./tesh
-! expect signal SIGABRT
+! expect return 1
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
> [ 0.000000] (0:@) Check a safety property
#include "mc_record.h"
#include "mc_smx.h"
#include "mc_client.h"
+#include "mc_exit.h"
using simgrid::mc::remote;
xbt_free(initial_global_state->send_diff);
initial_global_state->send_diff = NULL;
MC_print_statistics(mc_stats);
- xbt_abort();
+ exit(SIMGRID_EXIT_NON_DETERMINISM);
}else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
XBT_INFO("****************************************************");
XBT_INFO("***** Non-deterministic communications pattern *****");
xbt_free(initial_global_state->recv_diff);
initial_global_state->recv_diff = NULL;
MC_print_statistics(mc_stats);
- xbt_abort();
+ exit(SIMGRID_EXIT_NON_DETERMINISM);
}
}
}
--- /dev/null
+#ifndef SIMGRID_MC_EXIT_HPP
+#define SIMGRID_MC_EXIT_HPP
+
+#define SIMGRID_EXIT_SUCCESS 0
+#define SIMGRID_EXIT_SAFETY 1
+#define SIMGRID_EXIT_LIVENESS 2
+#define SIMGRID_EXIT_DEADLOCK 3
+#define SIMGRID_EXIT_NON_TERMINATION 4
+#define SIMGRID_EXIT_NON_DETERMINISM 5
+
+#define SIMGRID_ERROR 63
+
+#endif
#include "mc_client.h"
#include "mc_replay.h"
#include "mc_safety.h"
+#include "mc_exit.h"
extern "C" {
MC_dump_stack_liveness(mc_stack);
MC_print_statistics(mc_stats);
XBT_INFO("Counter-example depth : %d", counter_example_depth);
- xbt_abort();
+ exit(SIMGRID_EXIT_LIVENESS);
}
}
#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
*/
/** \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
}
}
}
+
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();
-}
-
}
#include "mc_private.h"
#include "mc_ignore.h"
#include "mcer_ignore.h"
+#include "mc_exit.h"
using simgrid::mc::remote;
case MC_MESSAGE_ASSERTION_FAILED:
MC_report_assertion_error();
- xbt_abort();
+ ::exit(SIMGRID_EXIT_SAFETY);
break;
default:
#include <xbt/misc.h>
#include "mc_process.h"
+#include "mc_exit.h"
SG_BEGIN_DECL()
-#define MC_SERVER_ERROR 127
+#define MC_SERVER_ERROR SIMGRID_ERROR
typedef struct s_mc_server s_mc_server_t, *mc_server_t;
#!/usr/bin/env tesh
-!expect signal SIGABRT
+! expect return 1
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random_bug ${srcdir:=.}/../../../examples/platforms/small_platform.xml ${srcdir:=.}/random_bug.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/record:1
> [ 0.000000] (0:@) Check a safety property
> [ 0.000000] (0:@) **************************