-/** Terminate the model-checker application */
-void ModelChecker::exit(int status)
-{
- shutdown();
- ::exit(status);
-}
-
-void ModelChecker::handle_waitpid()
-{
- XBT_DEBUG("Check for wait event");
- int status;
- pid_t pid;
- while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
- if (pid == -1) {
- if (errno == ECHILD) {
- // No more children:
- xbt_assert(not this->get_remote_process().running(), "Inconsistent state");
- break;
- } else {
- XBT_ERROR("Could not wait for pid");
- throw simgrid::xbt::errno_error();
- }
- }
-
- if (pid == this->get_remote_process().pid()) {
- // From PTRACE_O_TRACEEXIT:
-#ifdef __linux__
- if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
- unsigned long eventmsg;
- xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &eventmsg) != -1, "Could not get exit status");
- status = static_cast<int>(eventmsg);
- if (WIFSIGNALED(status)) {
- MC_report_crash(exploration_, status);
- this->get_remote_process().terminate();
- this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
- }
- }
-#endif
-
- // We don't care about signals, just reinject them:
- if (WIFSTOPPED(status)) {
- XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
- errno = 0;
-#ifdef __linux__
- ptrace(PTRACE_CONT, remote_process_->pid(), 0, WSTOPSIG(status));
-#elif defined BSD
- ptrace(PT_CONTINUE, remote_process_->pid(), (caddr_t)1, WSTOPSIG(status));
-#endif
- xbt_assert(errno == 0, "Could not PTRACE_CONT");
- }
-
- else if (WIFSIGNALED(status)) {
- MC_report_crash(exploration_, status);
- this->get_remote_process().terminate();
- this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
- } else if (WIFEXITED(status)) {
- XBT_DEBUG("Child process is over");
- this->get_remote_process().terminate();
- }
- }
- }
-}
-
-void ModelChecker::wait_for_requests()
-{
- this->resume();
- if (this->get_remote_process().running())
- checker_side_.dispatch();
-}
-
-Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
-{
- s_mc_message_simcall_execute_t m = {};
- m.type = MessageType::SIMCALL_EXECUTE;
- m.aid_ = aid;
- m.times_considered_ = times_considered;
- checker_side_.get_channel().send(m);
-
- this->remote_process_->clear_cache();
- if (this->remote_process_->running())
- checker_side_.dispatch(); // The app may send messages while processing the transition
-
- s_mc_message_simcall_execute_answer_t answer;
- ssize_t s = checker_side_.get_channel().receive(answer);
- xbt_assert(s != -1, "Could not receive message");
- xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
- "Received unexpected message %s (%i, size=%i) "
- "expected MessageType::SIMCALL_EXECUTE_ANSWER (%i, size=%i)",
- to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_EXECUTE_ANSWER,
- (int)sizeof(answer));
-
- if (new_transition) {
- std::stringstream stream(answer.buffer.data());
- return deserialize_transition(aid, times_considered, stream);
- } else
- return nullptr;
-}
-
-void ModelChecker::finalize_app(bool terminate_asap)
-{
- s_mc_message_int_t m = {};
- m.type = MessageType::FINALIZE;
- m.value = terminate_asap;
- xbt_assert(checker_side_.get_channel().send(m) == 0, "Could not ask the app to finalize on need");
-
- s_mc_message_t answer;
- ssize_t s = checker_side_.get_channel().receive(answer);
- xbt_assert(s != -1, "Could not receive answer to FINALIZE");
- xbt_assert(s == sizeof(answer) && answer.type == MessageType::FINALIZE_REPLY,
- "Received unexpected message %s (%i, size=%i) expected MessageType::FINALIZE_REPLY (%i, size=%i)",
- to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::FINALIZE_REPLY, (int)sizeof(answer));
-}
-