X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/983883d65cbcf86c675a323208f9dd15ffbbf583..46448320f12d59d0a5efc015ec51ec6ebba525c6:/src/mc/mc_server.cpp diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index c9dc25f939..b869b19f7e 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -14,12 +14,21 @@ #include #include +#include +#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" +#include "mc_exit.h" +#include "mc/mc_liveness.h" + +using simgrid::mc::remote; + +extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); @@ -40,11 +49,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; @@ -77,40 +84,40 @@ 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) { + simgrid::mc::Process* 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"); } } -void s_mc_server::resume(mc_process_t process) +void s_mc_server::resume(simgrid::mc::Process* process) { - int socket = process->socket; - int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE); + int res = process->send_message(MC_MESSAGE_CONTINUE); if (res) throw std::system_error(res, std::system_category()); + process->cache_flags = (mc_process_cache_flags_t) 0; } static @@ -123,7 +130,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]; @@ -141,7 +148,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()); @@ -154,7 +161,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"); @@ -165,33 +171,30 @@ 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( + (void *)(std::uintptr_t) 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, + mc_model_checker->process().ignore_region( 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"); @@ -202,11 +205,43 @@ void s_mc_server::handle_events() } break; + case MC_MESSAGE_REGISTER_SYMBOL: + { + s_mc_register_symbol_message_t message; + if (size != sizeof(message)) + xbt_die("Broken message"); + memcpy(&message, buffer, sizeof(message)); + if (message.callback) + xbt_die("Support for client-side function proposition is not implemented."); + XBT_DEBUG("Received symbol: %s", message.name); + + if (_mc_property_automaton == NULL) + _mc_property_automaton = xbt_automaton_new(); + + simgrid::mc::Process* process = &mc_model_checker->process(); + simgrid::mc::remote_ptr address + = simgrid::mc::remote((int*) message.data); + simgrid::xbt::add_proposition(_mc_property_automaton, + message.name, + [process, address]() { return process->read(address); } + ); + + break; + } + + case MC_MESSAGE_WAITING: + return false; + + case MC_MESSAGE_ASSERTION_FAILED: + MC_report_assertion_error(); + ::exit(SIMGRID_EXIT_SAFETY); + break; + default: xbt_die("Unexpected message from model-checked application"); } - return; + return true; } if (socket_pollfd->revents & POLLERR) { throw_socket_error(socket_pollfd->fd); @@ -218,7 +253,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); @@ -226,11 +261,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(); } @@ -263,21 +300,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); } } } @@ -293,3 +329,34 @@ void s_mc_server::on_signal(const struct signalfd_siginfo* info) break; } } + +void MC_server_wait_client(simgrid::mc::Process* process) +{ + mc_server->resume(process); + while (mc_model_checker->process().running()) { + if (!mc_server->handle_events()) + return; + } +} + +void MC_server_simcall_handle(simgrid::mc::Process* 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_model_checker->process().send_message(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(); +} + +}