X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/38d1cfd08cf30b0da496b20dfa8b849cbfdb7ab4..89df17fd2f872e224e49bbdeeba43ca76a5b7d71:/src/mc/mc_server.cpp diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index 12ca0a89a3..9ea15bd0ba 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -15,11 +15,16 @@ #include -#include "mc_model_checker.h" +#include "ModelChecker.hpp" #include "mc_protocol.h" #include "mc_server.h" #include "mc_private.h" #include "mc_ignore.h" +#include "mcer_ignore.h" + +using simgrid::mc::remote; + +extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); @@ -39,8 +44,7 @@ static int mc_symbol_pointer_callback_evaluate(void* p) { struct mc_symbol_pointer_callback* callback = (struct mc_symbol_pointer_callback*) p; int value; - MC_process_read(callback->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE, - &value, callback->value, sizeof(value), MC_PROCESS_INDEX_ANY); + callback->process->read_bytes(&value, sizeof(value), remote(callback->value)); return value; } @@ -55,11 +59,9 @@ void s_mc_server::start() /* Wait for the target process to initialize and exchange a HELLO messages * before trying to look at its memory map. */ - XBT_DEBUG("Greeting the MC client"); int res = MC_protocol_hello(socket); if (res != 0) throw std::system_error(res, std::system_category()); - XBT_DEBUG("Greeted the MC client"); // Block SIGCHLD (this will be handled with accept/signalfd): sigset_t set; @@ -92,28 +94,28 @@ void s_mc_server::shutdown() { XBT_DEBUG("Shuting down model-checker"); - mc_process_t process = &mc_model_checker->process; - int status = process->status; - if (process->running) { + mc_process_t process = &mc_model_checker->process(); + int status = process->status(); + if (process->running()) { XBT_DEBUG("Killing process"); - kill(process->pid, SIGTERM); - if (waitpid(process->pid, &status, 0) == -1) + kill(process->pid(), SIGTERM); + if (waitpid(process->pid(), &status, 0) == -1) throw std::system_error(errno, std::system_category()); // TODO, handle the case when the process does not want to die with a timeout - process->status = status; + process->terminate(status); } } void s_mc_server::exit() { // Finished: - int status = mc_model_checker->process.status; + int status = mc_model_checker->process().status(); if (WIFEXITED(status)) ::exit(WEXITSTATUS(status)); else if (WIFSIGNALED(status)) { // Try to uplicate the signal of the model-checked process. // This is a temporary hack so we don't try too hard. - kill(mc_model_checker->process.pid, WTERMSIG(status)); + kill(mc_model_checker->process().pid(), WTERMSIG(status)); abort(); } else { xbt_die("Unexpected status from model-checked process"); @@ -126,6 +128,7 @@ void s_mc_server::resume(mc_process_t process) int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE); if (res) throw std::system_error(res, std::system_category()); + process->cache_flags = (mc_process_cache_flags_t) 0; } static @@ -138,7 +141,7 @@ void throw_socket_error(int fd) throw std::system_error(error, std::system_category()); } -void s_mc_server::handle_events() +bool s_mc_server::handle_events() { char buffer[MC_MESSAGE_LENGTH]; struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX]; @@ -156,7 +159,7 @@ void s_mc_server::handle_events() if (socket_pollfd->revents) { if (socket_pollfd->revents & POLLIN) { - ssize_t size = recv(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT); + ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT); if (size == -1 && errno != EAGAIN) throw std::system_error(errno, std::system_category()); @@ -169,7 +172,6 @@ void s_mc_server::handle_events() case MC_MESSAGE_IGNORE_HEAP: { - XBT_DEBUG("Received ignored region"); s_mc_ignore_heap_message_t message; if (size != sizeof(message)) xbt_die("Broken messsage"); @@ -180,33 +182,29 @@ void s_mc_server::handle_events() break; } - case MC_MESSAGE_UNIGNORE_HEAP: { - XBT_DEBUG("Received unignored region"); s_mc_ignore_memory_message_t message; if (size != sizeof(message)) xbt_die("Broken messsage"); memcpy(&message, buffer, sizeof(message)); - MC_remove_ignore_heap(message.addr, message.size); + MC_heap_region_ignore_remove(message.addr, message.size); break; } case MC_MESSAGE_IGNORE_MEMORY: { - XBT_DEBUG("Received ignored memory"); s_mc_ignore_memory_message_t message; if (size != sizeof(message)) xbt_die("Broken messsage"); memcpy(&message, buffer, sizeof(message)); - MC_process_ignore_memory(&mc_model_checker->process, - message.addr, message.size); + mc_model_checker->process().ignore_region( + (std::uint64_t)message.addr, message.size); break; } case MC_MESSAGE_STACK_REGION: { - XBT_DEBUG("Received stack area"); s_mc_stack_region_message_t message; if (size != sizeof(message)) xbt_die("Broken messsage"); @@ -228,7 +226,7 @@ void s_mc_server::handle_events() XBT_DEBUG("Received symbol: %s", message.name); struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1); - callback->process = &mc_model_checker->process; + callback->process = &mc_model_checker->process(); callback->value = message.data; MC_automaton_new_propositional_symbol_callback(message.name, @@ -236,11 +234,19 @@ void s_mc_server::handle_events() break; } + case MC_MESSAGE_WAITING: + return false; + + case MC_MESSAGE_ASSERTION_FAILED: + MC_report_assertion_error(); + xbt_abort(); + break; + default: xbt_die("Unexpected message from model-checked application"); } - return; + return true; } if (socket_pollfd->revents & POLLERR) { throw_socket_error(socket_pollfd->fd); @@ -252,7 +258,7 @@ void s_mc_server::handle_events() if (signalfd_pollfd->revents) { if (signalfd_pollfd->revents & POLLIN) { this->handle_signals(); - return; + return true; } if (signalfd_pollfd->revents & POLLERR) { throw_socket_error(signalfd_pollfd->fd); @@ -260,11 +266,13 @@ void s_mc_server::handle_events() if (signalfd_pollfd->revents & POLLHUP) xbt_die("Signalfd hang up?"); } + + return true; } void s_mc_server::loop() { - while (mc_model_checker->process.running) + while (mc_model_checker->process().running()) this->handle_events(); } @@ -297,21 +305,20 @@ void s_mc_server::handle_waitpid() if (pid == -1) { if (errno == ECHILD) { // No more children: - if (mc_model_checker->process.running) + if (mc_model_checker->process().running()) xbt_die("Inconsistent state"); else break; } else { - XBT_ERROR("Could not wait for pid: %s", strerror(errno)); + XBT_ERROR("Could not wait for pid"); throw std::system_error(errno, std::system_category()); } } - if (pid == mc_model_checker->process.pid) { + if (pid == mc_model_checker->process().pid()) { if (WIFEXITED(status) || WIFSIGNALED(status)) { XBT_DEBUG("Child process is over"); - mc_model_checker->process.status = status; - mc_model_checker->process.running = false; + mc_model_checker->process().terminate(status); } } } @@ -327,3 +334,34 @@ void s_mc_server::on_signal(const struct signalfd_siginfo* info) break; } } + +void MC_server_wait_client(mc_process_t process) +{ + mc_server->resume(process); + while (mc_model_checker->process().running()) { + if (!mc_server->handle_events()) + return; + } +} + +void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value) +{ + s_mc_simcall_handle_message m; + memset(&m, 0, sizeof(m)); + m.type = MC_MESSAGE_SIMCALL_HANDLE; + m.pid = pid; + m.value = value; + MC_protocol_send(mc_model_checker->process().socket, &m, sizeof(m)); + process->cache_flags = (mc_process_cache_flags_t) 0; + while (mc_model_checker->process().running()) { + if (!mc_server->handle_events()) + return; + } +} + +void MC_server_loop(mc_server_t server) +{ + server->loop(); +} + +}