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] Don't leave model-checked processes around
[simgrid.git]
/
src
/
mc
/
ModelChecker.cpp
diff --git
a/src/mc/ModelChecker.cpp
b/src/mc/ModelChecker.cpp
index
6e73a2d
..
1bbf9e6
100644
(file)
--- a/
src/mc/ModelChecker.cpp
+++ b/
src/mc/ModelChecker.cpp
@@
-48,12
+48,13
@@
using simgrid::mc::remote;
namespace simgrid {
namespace mc {
namespace simgrid {
namespace mc {
-ModelChecker::ModelChecker(pid_t pid, int socket) :
- pid_(pid), socket_(socket),
+ModelChecker::ModelChecker(std::unique_ptr<Process> process) :
hostnames_(xbt_dict_new()),
page_store_(500),
hostnames_(xbt_dict_new()),
page_store_(500),
+ process_(std::move(process)),
parent_snapshot_(nullptr)
{
parent_snapshot_(nullptr)
{
+
}
ModelChecker::~ModelChecker()
}
ModelChecker::~ModelChecker()
@@
-63,7
+64,6
@@
ModelChecker::~ModelChecker()
const char* ModelChecker::get_host_name(const char* hostname)
{
const char* ModelChecker::get_host_name(const char* hostname)
{
- // FIXME, simgrid::Host
// Lookup the host name in the dictionary (or create it):
xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
if (!elt) {
// Lookup the host name in the dictionary (or create it):
xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
if (!elt) {
@@
-76,6
+76,8
@@
const char* ModelChecker::get_host_name(const char* hostname)
void ModelChecker::start()
{
void ModelChecker::start()
{
+ const pid_t pid = process_->pid();
+
// Block SIGCHLD (this will be handled with accept/signalfd):
sigset_t set;
sigemptyset(&set);
// Block SIGCHLD (this will be handled with accept/signalfd):
sigset_t set;
sigemptyset(&set);
@@
-89,7
+91,7
@@
void ModelChecker::start()
// Prepare data for poll:
struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
// Prepare data for poll:
struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
- socket_pollfd->fd =
socket_
;
+ socket_pollfd->fd =
process_->socket();
;
socket_pollfd->events = POLLIN;
socket_pollfd->revents = 0;
socket_pollfd->events = POLLIN;
socket_pollfd->revents = 0;
@@
-106,14
+108,11
@@
void ModelChecker::start()
int status;
// The model-checked process SIGSTOP itself to signal it's ready:
int status;
// The model-checked process SIGSTOP itself to signal it's ready:
- pid_t res = waitpid(pid
_
, &status, __WALL);
+ pid_t res = waitpid(pid, &status, __WALL);
if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
xbt_die("Could not wait model-checked process");
if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
xbt_die("Could not wait model-checked process");
- assert(process_ == nullptr);
- process_ = std::unique_ptr<Process>(new Process(pid_, socket_));
- // TODO, avoid direct dependency on sg_cfg
- process_->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
+ process_->init();
/* Initialize statistics */
mc_stats = xbt_new0(s_mc_stats_t, 1);
/* Initialize statistics */
mc_stats = xbt_new0(s_mc_stats_t, 1);
@@
-127,8
+126,8
@@
void ModelChecker::start()
setup_ignore();
setup_ignore();
- ptrace(PTRACE_SETOPTIONS, pid
_
, nullptr, PTRACE_O_TRACEEXIT);
- ptrace(PTRACE_CONT, pid
_
, 0, 0);
+ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
+ ptrace(PTRACE_CONT, pid, 0, 0);
}
static const std::pair<const char*, const char*> ignored_local_variables[] = {
}
static const std::pair<const char*, const char*> ignored_local_variables[] = {
@@
-278,7
+277,7
@@
bool ModelChecker::handle_message(char* buffer, ssize_t size)
case MC_MESSAGE_ASSERTION_FAILED:
MC_report_assertion_error();
case MC_MESSAGE_ASSERTION_FAILED:
MC_report_assertion_error();
-
::
exit(SIMGRID_MC_EXIT_SAFETY);
+
this->
exit(SIMGRID_MC_EXIT_SAFETY);
break;
default:
break;
default:
@@
-288,6
+287,15
@@
bool ModelChecker::handle_message(char* buffer, ssize_t size)
return true;
}
return true;
}
+/** Terminate the model-checker aplication */
+void ModelChecker::exit(int status)
+{
+ // TODO, terminate the model checker politely instead of exiting rudel
+ if (process().running())
+ kill(process().pid(), SIGKILL);
+ ::exit(status);
+}
+
bool ModelChecker::handle_events()
{
char buffer[MC_MESSAGE_LENGTH];
bool ModelChecker::handle_events()
{
char buffer[MC_MESSAGE_LENGTH];
@@
-381,18
+389,18
@@
void ModelChecker::handle_waitpid()
// From PTRACE_O_TRACEEXIT:
if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
// From PTRACE_O_TRACEEXIT:
if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
- if (ptrace(PTRACE_GETEVENTMSG,
pid_
, 0, &status) == -1)
+ if (ptrace(PTRACE_GETEVENTMSG,
this->process().pid()
, 0, &status) == -1)
xbt_die("Could not get exit status");
if (WIFSIGNALED(status)) {
MC_report_crash(status);
xbt_die("Could not get exit status");
if (WIFSIGNALED(status)) {
MC_report_crash(status);
-
::
exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+
mc_model_checker->
exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
}
}
// We don't care about signals, just reinject them:
if (WIFSTOPPED(status)) {
XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
}
}
// We don't care about signals, just reinject them:
if (WIFSTOPPED(status)) {
XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
- if (ptrace(PTRACE_CONT,
pid_
, 0, WSTOPSIG(status)) == -1)
+ if (ptrace(PTRACE_CONT,
this->process().pid()
, 0, WSTOPSIG(status)) == -1)
xbt_die("Could not PTRACE_CONT");
}
xbt_die("Could not PTRACE_CONT");
}