X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b16f029ad88f7238b6c86111eea5efc8eed32095..162424b0ac640baa56b0ca9bc158ef9743f0c4ac:/src/mc/mc_global.cpp diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 4ab05de085..51c4074fed 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -1,54 +1,36 @@ -/* Copyright (c) 2008-2017. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -#include -#include -#include -#include - -#include - -#include - -#include "xbt/automaton.h" -#include "xbt/backtrace.hpp" -#include "xbt/dynar.h" - -#include "mc_base.h" - #include "mc/mc.h" - -#ifndef _WIN32 -#include -#include -#include -#endif - -#include "src/simix/ActorImpl.hpp" +#include "src/kernel/actor/ActorImpl.hpp" #if SIMGRID_HAVE_MC +#include "src/mc/Session.hpp" #include "src/mc/checker/Checker.hpp" -#include "src/mc/mc_comm_pattern.hpp" +#include "src/mc/inspect/mc_unw.hpp" +#include "src/mc/mc_config.hpp" #include "src/mc/mc_private.hpp" -#include "src/mc/mc_request.hpp" #include "src/mc/mc_safety.hpp" -#include "src/mc/mc_smx.hpp" -#include "src/mc/mc_snapshot.hpp" -#include "src/mc/mc_unw.hpp" +#include "src/mc/remote/AppSide.hpp" +#include "src/mc/sosp/Snapshot.hpp" + +#include +#include +#include +#include #include #endif -#include "src/mc/Transition.hpp" -#include "src/mc/mc_record.hpp" -#include "src/mc/remote/Client.hpp" -#include "src/mc/remote/mc_protocol.h" +#ifndef _WIN32 +#include +#include +#include +#endif XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); -extern std::string _sg_mc_dot_output_file; - namespace simgrid { namespace mc { @@ -78,16 +60,11 @@ FILE *dot_output = nullptr; void MC_init_dot_output() { - dot_output = fopen(_sg_mc_dot_output_file.c_str(), "w"); - - if (dot_output == nullptr) { - perror("Error open dot output file"); - xbt_abort(); - } + dot_output = fopen(_sg_mc_dot_output_file.get().c_str(), "w"); + xbt_assert(dot_output != nullptr, "Error open dot output file: %s", strerror(errno)); fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n"); - } /******************************* Core of MC *******************************/ @@ -95,93 +72,55 @@ void MC_init_dot_output() void MC_run() { - simgrid::mc::processes_time.resize(SIMIX_process_get_maxpid()); + simgrid::mc::processes_time.resize(simgrid::kernel::actor::get_maxpid()); MC_ignore_heap(simgrid::mc::processes_time.data(), simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0])); - simgrid::mc::Client::get()->mainLoop(); - simgrid::mc::processes_time.clear(); -} - -void MC_show_deadlock() -{ - XBT_INFO("**************************"); - XBT_INFO("*** DEAD-LOCK DETECTED ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - for (auto const& s : mc_model_checker->getChecker()->getTextualTrace()) - XBT_INFO("%s", s.c_str()); - simgrid::mc::session->logState(); -} - -void MC_automaton_load(const char *file) -{ - if (simgrid::mc::property_automaton == nullptr) - simgrid::mc::property_automaton = xbt_automaton_new(); - - xbt_automaton_load(simgrid::mc::property_automaton, file); + simgrid::mc::AppSide::get()->main_loop(); } namespace simgrid { namespace mc { -void dumpStack(FILE* file, unw_cursor_t cursor) +void dumpStack(FILE* file, unw_cursor_t* cursor) { int nframe = 0; - char buffer[100]; + std::array buffer; unw_word_t off; do { - const char* name = not unw_get_proc_name(&cursor, buffer, 100, &off) ? buffer : "?"; + const char* name = not unw_get_proc_name(cursor, buffer.data(), buffer.size(), &off) ? buffer.data() : "?"; // Unmangle C++ names: - auto realname = simgrid::xbt::demangle(name); + std::string realname = boost::core::demangle(name); #if defined(__x86_64__) unw_word_t rip = 0; unw_word_t rsp = 0; - unw_get_reg(&cursor, UNW_X86_64_RIP, &rip); - unw_get_reg(&cursor, UNW_X86_64_RSP, &rsp); - fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n", nframe, realname.get(), (std::uint64_t)rip, + unw_get_reg(cursor, UNW_X86_64_RIP, &rip); + unw_get_reg(cursor, UNW_X86_64_RSP, &rsp); + fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n", nframe, realname.c_str(), (std::uint64_t)rip, (std::uint64_t)rsp); #else - fprintf(file, " %i: %s\n", nframe, realname.get()); + fprintf(file, " %i: %s\n", nframe, realname.c_str()); #endif ++nframe; - } while(unw_step(&cursor)); + } while (unw_step(cursor)); } } } - -static void MC_dump_stacks(FILE* file) -{ - int nstack = 0; - for (auto const& stack : mc_model_checker->process().stack_areas()) { - fprintf(file, "Stack %i:\n", nstack); - nstack++; - - simgrid::mc::UnwindContext context; - unw_context_t raw_context = - (unw_context_t) mc_model_checker->process().read( - simgrid::mc::remote((unw_context_t *)stack.context)); - context.initialize(&mc_model_checker->process(), &raw_context); - - unw_cursor_t cursor = context.cursor(); - simgrid::mc::dumpStack(file, cursor); - } -} #endif -double MC_process_clock_get(smx_actor_t process) +double MC_process_clock_get(const simgrid::kernel::actor::ActorImpl* process) { if (simgrid::mc::processes_time.empty()) return 0; if (process != nullptr) - return simgrid::mc::processes_time[process->pid]; + return simgrid::mc::processes_time[process->get_pid()]; return -1; } -void MC_process_clock_add(smx_actor_t process, double amount) +void MC_process_clock_add(const simgrid::kernel::actor::ActorImpl* process, double amount) { - simgrid::mc::processes_time[process->pid] += amount; + simgrid::mc::processes_time[process->get_pid()] += amount; }