// Parent (model-checker):
::close(sockets[0]);
- auto memory = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid);
- checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(sockets[1], std::move(memory));
+ checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(sockets[1], pid);
start();
int status;
// The model-checked process SIGSTOP itself to signal it's ready:
- const pid_t pid = get_remote_process_memory().pid();
+ const pid_t pid = checker_side_->get_pid();
xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
"Could not wait model-checked process");
throw xbt::errno_error();
get_remote_process_memory().clear_cache();
- if (this->get_remote_process_memory().running())
+ if (checker_side_->running())
checker_side_->dispatch_events();
}
{
XBT_DEBUG("Shutting down model-checker");
- RemoteProcessMemory& process = get_remote_process_memory();
- if (process.running()) {
+ if (checker_side_->running()) {
XBT_DEBUG("Killing process");
finalize_app(true);
- kill(process.pid(), SIGKILL);
- process.terminate();
+ kill(checker_side_->get_pid(), SIGKILL);
+ checker_side_->terminate();
}
}
checker_side_->get_channel().send(m);
get_remote_process_memory().clear_cache();
- if (this->get_remote_process_memory().running())
+ if (checker_side_->running())
checker_side_->dispatch_events(); // The app may send messages while processing the transition
s_mc_message_simcall_execute_answer_t answer;
/** High-level view of the verified application, from the model-checker POV
*
- * This is expected to become the interface used by model-checking
- * algorithms to control the execution of the model-checked process
- * and the exploration of the execution graph. Model-checking
- * algorithms should be able to be written in high-level languages
- * (e.g. Python) using bindings on this interface.
+ * This is expected to become the interface used by model-checking algorithms to control the execution of
+ * the application process during the exploration of the execution graph.
+ *
+ * One day, this will allow parallel exploration, ie, the handling of several application processes (each encapsulated
+ * in a separate CheckerSide objects) that explore several parts of the exploration graph.
*/
class XBT_PUBLIC RemoteApp {
private:
get_remote_app().get_remote_process_memory().dump_stack();
}
- get_remote_app().get_remote_process_memory().terminate();
system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
}
void Exploration::report_assertion_failure()
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkerside, mc, "MC communication with the application");
namespace simgrid::mc {
-CheckerSide::CheckerSide(int sockfd, std::unique_ptr<RemoteProcessMemory> memory)
- : remote_memory_(std::move(memory)), channel_(sockfd)
+CheckerSide::CheckerSide(int sockfd, pid_t pid)
+ : remote_memory_(std::make_unique<simgrid::mc::RemoteProcessMemory>(pid))
+ , channel_(sockfd)
+ , running_(true)
+ , pid_(pid)
{
auto* base = event_base_new();
base_.reset(base);
while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
if (pid == -1) {
if (errno == ECHILD) { // No more children:
- xbt_assert(not get_remote_memory().running(), "Inconsistent state");
+ xbt_assert(not this->running(), "Inconsistent state");
break;
} else {
XBT_ERROR("Could not wait for pid");
}
}
- if (pid == get_remote_memory().pid()) {
+ if (pid == get_pid()) {
// From PTRACE_O_TRACEEXIT:
#ifdef __linux__
if (status >> 8 == (SIGTRAP | (PTRACE_EVENT_EXIT << 8))) {
unsigned long eventmsg;
xbt_assert(ptrace(PTRACE_GETEVENTMSG, pid, 0, &eventmsg) != -1, "Could not get exit status");
status = static_cast<int>(eventmsg);
- if (WIFSIGNALED(status))
+ if (WIFSIGNALED(status)) {
+ this->terminate();
Exploration::get_instance()->report_crash(status);
+ }
}
#endif
}
else if (WIFSIGNALED(status)) {
+ this->terminate();
Exploration::get_instance()->report_crash(status);
} else if (WIFEXITED(status)) {
XBT_DEBUG("Child process is over");
- get_remote_memory().terminate();
+ this->terminate();
}
}
}
namespace simgrid::mc {
+/* CheckerSide: All what the checker needs to interact with a given application process */
+
class CheckerSide {
std::unique_ptr<event_base, decltype(&event_base_free)> base_{nullptr, &event_base_free};
std::unique_ptr<event, decltype(&event_free)> socket_event_{nullptr, &event_free};
std::unique_ptr<RemoteProcessMemory> remote_memory_;
Channel channel_;
+ bool running_ = false;
+ pid_t pid_;
+
public:
- explicit CheckerSide(int sockfd, std::unique_ptr<RemoteProcessMemory> mem);
+ explicit CheckerSide(int sockfd, pid_t pid);
// No copy:
CheckerSide(CheckerSide const&) = delete;
CheckerSide& operator=(CheckerSide const&) = delete;
CheckerSide& operator=(CheckerSide&&) = delete;
+ /* Communicating with the application */
Channel const& get_channel() const { return channel_; }
Channel& get_channel() { return channel_; }
- RemoteProcessMemory& get_remote_memory() { return *remote_memory_.get(); }
+ bool handle_message(const char* buffer, ssize_t size);
void dispatch_events() const;
void break_loop() const;
+ /* Interacting with the application process */
+ pid_t get_pid() const { return pid_; }
+ bool running() const { return running_; }
+ void terminate() { running_ = false; }
+ RemoteProcessMemory& get_remote_memory() { return *remote_memory_.get(); }
void handle_waitpid();
- bool handle_message(const char* buffer, ssize_t size);
};
} // namespace simgrid::mc
// ***** RemoteProcessMemory
-RemoteProcessMemory::RemoteProcessMemory(pid_t pid) : AddressSpace(this), pid_(pid), running_(true) {}
+RemoteProcessMemory::RemoteProcessMemory(pid_t pid) : AddressSpace(this), pid_(pid) {}
void RemoteProcessMemory::init(xbt_mheap_t mmalloc_default_mdp)
{
std::size_t size;
};
-/** The Application's process memory, seen from the Checker perspective
+/** The Application's process memory, seen from the Checker perspective. This class is not needed if you don't need to
+ * introspect the application process.
*
- * Responsibilities:
- *
- * - reading from the process memory (`AddressSpace`);
- * - accessing the system state of the process (heap, …);
- * - stack unwinding;
- * - etc.
+ * Responsabilities:
+ * - reading from the process memory (`AddressSpace`);
+ * - accessing the system state of the process (heap, …);
+ * - stack unwinding;
+ * - etc.
*/
class RemoteProcessMemory final : public AddressSpace {
private:
RemoteProcessMemory& operator=(RemoteProcessMemory const&) = delete;
RemoteProcessMemory& operator=(RemoteProcessMemory&&) = delete;
- pid_t pid() const { return pid_; }
- bool running() const { return running_; }
- void terminate() { running_ = false; }
-
/* ************* */
/* Low-level API */
/* ************* */
void refresh_heap();
void refresh_malloc_info();
- pid_t pid_ = -1;
- bool running_ = false;
+ pid_t pid_ = -1;
std::vector<xbt::VmMap> memory_map_;
RemotePtr<void> maestro_stack_start_;
RemotePtr<void> maestro_stack_end_;
