A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
further simplify the MC initialization
[simgrid.git]
/
src
/
mc
/
mc_global.cpp
diff --git
a/src/mc/mc_global.cpp
b/src/mc/mc_global.cpp
index
b06c18d
..
b9a76cc
100644
(file)
--- a/
src/mc/mc_global.cpp
+++ b/
src/mc/mc_global.cpp
@@
-1,49
+1,33
@@
-/* Copyright (c) 2008-201
7
. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-201
9
. 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. */
/* 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 <cinttypes>
-#include <cassert>
-#include <cstddef>
-#include <cstdint>
-
-#include <cxxabi.h>
-
-#include <vector>
-
-#include "xbt/automaton.h"
-#include "xbt/dynar.h"
-#include "xbt/swag.h"
-
-#include "mc_base.h"
-
#include "mc/mc.h"
#include "mc/mc.h"
-
-#ifndef _WIN32
-#include <unistd.h>
-#include <sys/wait.h>
-#include <sys/time.h>
-#endif
-
-#include "src/simix/ActorImpl.hpp"
+#include "src/kernel/actor/ActorImpl.hpp"
#if SIMGRID_HAVE_MC
#if SIMGRID_HAVE_MC
+#include "src/mc/Session.hpp"
#include "src/mc/checker/Checker.hpp"
#include "src/mc/checker/Checker.hpp"
+#include "src/mc/inspect/mc_unw.hpp"
#include "src/mc/mc_comm_pattern.hpp"
#include "src/mc/mc_comm_pattern.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_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/Client.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
+#include "xbt/backtrace.hpp"
+
#include <libunwind.h>
#endif
#include <libunwind.h>
#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 <sys/time.h>
+#include <sys/wait.h>
+#include <unistd.h>
+#endif
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)");
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)");
@@
-76,7
+60,7
@@
FILE *dot_output = nullptr;
void MC_init_dot_output()
{
void MC_init_dot_output()
{
- dot_output = fopen(_sg_mc_dot_output_file, "w");
+ dot_output = fopen(_sg_mc_dot_output_file
.get().c_str()
, "w");
if (dot_output == nullptr) {
perror("Error open dot output file");
if (dot_output == nullptr) {
perror("Error open dot output file");
@@
-96,12
+80,7
@@
void MC_run()
simgrid::mc::processes_time.resize(SIMIX_process_get_maxpid());
MC_ignore_heap(simgrid::mc::processes_time.data(),
simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0]));
simgrid::mc::processes_time.resize(SIMIX_process_get_maxpid());
MC_ignore_heap(simgrid::mc::processes_time.data(),
simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0]));
- for (auto const& kv : simix_global->process_list) {
- smx_actor_t actor = kv.second;
- MC_ignore_heap(&(actor->process_hookup), sizeof(actor->process_hookup));
- }
- simgrid::mc::Client::get()->mainLoop();
- simgrid::mc::processes_time.clear();
+ simgrid::mc::Client::get()->main_loop();
}
void MC_show_deadlock()
}
void MC_show_deadlock()
@@
-110,9
+89,10
@@
void MC_show_deadlock()
XBT_INFO("*** DEAD-LOCK DETECTED ***");
XBT_INFO("**************************");
XBT_INFO("Counter-example execution trace:");
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();
+ for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
+ XBT_INFO(" %s", s.c_str());
+ simgrid::mc::dumpRecordPath();
+ simgrid::mc::session->log_state();
}
void MC_automaton_load(const char *file)
}
void MC_automaton_load(const char *file)
@@
-126,7
+106,7
@@
void MC_automaton_load(const char *file)
namespace simgrid {
namespace mc {
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];
{
int nframe = 0;
char buffer[100];
@@
-134,24
+114,20
@@
void dumpStack(FILE* file, unw_cursor_t cursor)
unw_word_t off;
do {
const char* name = not unw_get_proc_name(&cursor, buffer, 100, &off) ? buffer : "?";
unw_word_t off;
do {
const char* name = not unw_get_proc_name(&cursor, buffer, 100, &off) ? buffer : "?";
-
- int status;
-
// Unmangle C++ names:
// Unmangle C++ names:
-
char* realname = abi::__cxa_demangle(name, 0, 0, &status
);
+
auto realname = simgrid::xbt::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);
#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 ? realname : name, (std::uint64_t) rip, (std::uint64_t)
rsp);
+ fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
nframe, realname.get(), (std::uint64_t)rip,
+
(std::uint64_t)
rsp);
#else
#else
- fprintf(file, " %i: %s\n", nframe, realname
? realname : name
);
+ fprintf(file, " %i: %s\n", nframe, realname
.get()
);
#endif
#endif
- free(realname);
++nframe;
} while(unw_step(&cursor));
}
++nframe;
} while(unw_step(&cursor));
}
@@
-173,7
+149,7
@@
static void MC_dump_stacks(FILE* file)
context.initialize(&mc_model_checker->process(), &raw_context);
unw_cursor_t cursor = context.cursor();
context.initialize(&mc_model_checker->process(), &raw_context);
unw_cursor_t cursor = context.cursor();
- simgrid::mc::dumpStack(file,
cursor
);
+ simgrid::mc::dumpStack(file,
std::move(cursor)
);
}
}
#endif
}
}
#endif
@@
-183,11
+159,11
@@
double MC_process_clock_get(smx_actor_t process)
if (simgrid::mc::processes_time.empty())
return 0;
if (process != nullptr)
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)
{
return -1;
}
void MC_process_clock_add(smx_actor_t process, double amount)
{
- simgrid::mc::processes_time[process->
pid
] += amount;
+ simgrid::mc::processes_time[process->
get_pid()
] += amount;
}
}