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
obsolete script: RuleBased routing was removed in v3.10
[simgrid.git]
/
src
/
mc
/
mc_global.cpp
diff --git
a/src/mc/mc_global.cpp
b/src/mc/mc_global.cpp
index
a77c614
..
d47939e
100644
(file)
--- a/
src/mc/mc_global.cpp
+++ b/
src/mc/mc_global.cpp
@@
-9,6
+9,8
@@
#include <cstddef>
#include <cstdint>
#include <cstddef>
#include <cstdint>
+#include <vector>
+
#include "mc_base.h"
#include "mc/mc.h"
#include "mc_base.h"
#include "mc/mc.h"
@@
-24,7
+26,7
@@
#include "src/simix/smx_process_private.h"
#include "src/simix/smx_process_private.h"
-#if
def
HAVE_MC
+#if HAVE_MC
#include <libunwind.h>
#include "src/mc/mc_comm_pattern.h"
#include "src/mc/mc_request.h"
#include <libunwind.h>
#include "src/mc/mc_comm_pattern.h"
#include "src/mc/mc_request.h"
@@
-38,30
+40,41
@@
#include "src/mc/mc_record.h"
#include "src/mc/mc_protocol.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_client.h"
-
-extern "C" {
+#include "src/mc/Client.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
e_mc_mode_t mc_mode;
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
e_mc_mode_t mc_mode;
-double *mc_time = nullptr;
+namespace simgrid {
+namespace mc {
+
+std::vector<double> processes_time;
-#ifdef HAVE_MC
+}
+}
+
+#if HAVE_MC
int user_max_depth_reached = 0;
/* MC global data structures */
mc_state_t mc_current_state = nullptr;
int user_max_depth_reached = 0;
/* MC global data structures */
mc_state_t mc_current_state = nullptr;
-char mc_replay_mode =
FALSE
;
+char mc_replay_mode =
false
;
mc_stats_t mc_stats = nullptr;
mc_global_t initial_global_state = nullptr;
xbt_fifo_t mc_stack = nullptr;
/* Liveness */
mc_stats_t mc_stats = nullptr;
mc_global_t initial_global_state = nullptr;
xbt_fifo_t mc_stack = nullptr;
/* Liveness */
-xbt_automaton_t _mc_property_automaton = nullptr;
+
+namespace simgrid {
+namespace mc {
+
+xbt_automaton_t property_automaton = nullptr;
+
+}
+}
/* Dot output */
FILE *dot_output = nullptr;
/* Dot output */
FILE *dot_output = nullptr;
@@
-100,16
+113,17
@@
void MC_init_dot_output()
}
}
-#if
def
HAVE_MC
+#if HAVE_MC
void MC_init()
{
void MC_init()
{
-
mc_time = xbt_new0(double,
simix_process_maxpid);
+
simgrid::mc::processes_time.resize(
simix_process_maxpid);
if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
/* Those requests are handled on the client side and propagated by message
* to the server: */
if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
/* Those requests are handled on the client side and propagated by message
* to the server: */
- MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+ MC_ignore_heap(simgrid::mc::processes_time.data(),
+ simix_process_maxpid * sizeof(double));
smx_process_t process;
xbt_swag_foreach(process, simix_global->process_list)
smx_process_t process;
xbt_swag_foreach(process, simix_global->process_list)
@@
-126,26
+140,25
@@
void MC_run()
{
mc_mode = MC_MODE_CLIENT;
MC_init();
{
mc_mode = MC_MODE_CLIENT;
MC_init();
-
MC_client_main_l
oop();
+
simgrid::mc::Client::get()->mainL
oop();
}
void MC_exit(void)
{
}
void MC_exit(void)
{
- xbt_free(mc_time);
-
+ simgrid::mc::processes_time.clear();
MC_memory_exit();
//xbt_abort();
}
MC_memory_exit();
//xbt_abort();
}
-#if
def
HAVE_MC
+#if HAVE_MC
int MC_deadlock_check()
{
if (mc_mode == MC_MODE_SERVER) {
int res;
int MC_deadlock_check()
{
if (mc_mode == MC_MODE_SERVER) {
int res;
- if ((res = mc_model_checker->process().
send_message
(MC_MESSAGE_DEADLOCK_CHECK)))
+ if ((res = mc_model_checker->process().
getChannel().send
(MC_MESSAGE_DEADLOCK_CHECK)))
xbt_die("Could not check deadlock state");
s_mc_int_message_t message;
xbt_die("Could not check deadlock state");
s_mc_int_message_t message;
- ssize_t s = mc_model_checker->process().
receive_messag
e(message);
+ ssize_t s = mc_model_checker->process().
getChannel().receiv
e(message);
if (s == -1)
xbt_die("Could not receive message");
if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
if (s == -1)
xbt_die("Could not receive message");
if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
@@
-158,13
+171,13
@@
int MC_deadlock_check()
return message.value;
}
return message.value;
}
-
int deadlock = FALSE
;
+
bool deadlock = false
;
smx_process_t process;
if (xbt_swag_size(simix_global->process_list)) {
smx_process_t process;
if (xbt_swag_size(simix_global->process_list)) {
- deadlock =
TRUE
;
+ deadlock =
true
;
xbt_swag_foreach(process, simix_global->process_list)
xbt_swag_foreach(process, simix_global->process_list)
- if (
MC_
process_is_enabled(process)) {
- deadlock =
FALSE
;
+ if (
simgrid::mc::
process_is_enabled(process)) {
+ deadlock =
false
;
break;
}
}
break;
}
}
@@
-236,7
+249,7
@@
void MC_replay(xbt_fifo_t stack)
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str =
MC_request_to_string(req, value, MC_REQUEST_SIMIX
);
+ req_str =
simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix
);
XBT_DEBUG("Replay: %s (%p)", req_str, state);
xbt_free(req_str);
}
XBT_DEBUG("Replay: %s (%p)", req_str, state);
xbt_free(req_str);
}
@@
-246,7
+259,7
@@
void MC_replay(xbt_fifo_t stack)
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
call = MC_get_call_type(req);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
call = MC_get_call_type(req);
-
MC_simcall_handle
(req, value);
+
simgrid::mc::handle_simcall
(req, value);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_handle_comm_pattern(call, req, value, nullptr, 1);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_handle_comm_pattern(call, req, value, nullptr, 1);
@@
-268,7
+281,7
@@
void MC_replay(xbt_fifo_t stack)
void MC_replay_liveness(xbt_fifo_t stack)
{
xbt_fifo_item_t item;
void MC_replay_liveness(xbt_fifo_t stack)
{
xbt_fifo_item_t item;
-
mc_pair_t
pair = nullptr;
+
simgrid::mc::Pair*
pair = nullptr;
mc_state_t state = nullptr;
smx_simcall_t req = nullptr, saved_req = NULL;
int value, depth = 1;
mc_state_t state = nullptr;
smx_simcall_t req = nullptr, saved_req = NULL;
int value, depth = 1;
@@
-279,7
+292,7
@@
void MC_replay_liveness(xbt_fifo_t stack)
/* Intermediate backtracking */
if(_sg_mc_checkpoint > 0) {
item = xbt_fifo_get_first_item(stack);
/* Intermediate backtracking */
if(_sg_mc_checkpoint > 0) {
item = xbt_fifo_get_first_item(stack);
- pair = (
mc_pair_t
) xbt_fifo_get_item_content(item);
+ pair = (
simgrid::mc::Pair*
) xbt_fifo_get_item_content(item);
if(pair->graph_state->system_state){
simgrid::mc::restore_snapshot(pair->graph_state->system_state);
return;
if(pair->graph_state->system_state){
simgrid::mc::restore_snapshot(pair->graph_state->system_state);
return;
@@
-294,7
+307,7
@@
void MC_replay_liveness(xbt_fifo_t stack)
item != xbt_fifo_get_first_item(stack);
item = xbt_fifo_get_prev_item(item)) {
item != xbt_fifo_get_first_item(stack);
item = xbt_fifo_get_prev_item(item)) {
- pair = (
mc_pair_t
) xbt_fifo_get_item_content(item);
+ pair = (
simgrid::mc::Pair*
) xbt_fifo_get_item_content(item);
state = (mc_state_t) pair->graph_state;
state = (mc_state_t) pair->graph_state;
@@
-310,14
+323,14
@@
void MC_replay_liveness(xbt_fifo_t stack)
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str =
MC_request_to_string(req, value, MC_REQUEST_SIMIX
);
+ req_str =
simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix
);
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
xbt_free(req_str);
}
}
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
xbt_free(req_str);
}
}
-
MC_simcall_handle
(req, value);
+
simgrid::mc::handle_simcall
(req, value);
mc_model_checker->wait_for_requests();
}
mc_model_checker->wait_for_requests();
}
@@
-361,7
+374,7
@@
void MC_show_stack_safety(xbt_fifo_t stack)
state = (mc_state_t)xbt_fifo_get_item_content(item);
req = MC_state_get_executed_request(state, &value);
if (req) {
state = (mc_state_t)xbt_fifo_get_item_content(item);
req = MC_state_get_executed_request(state, &value);
if (req) {
- req_str =
MC_request_to_string(req, value, MC_REQUEST_EXECUTED
);
+ req_str =
simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed
);
XBT_INFO("%s", req_str);
xbt_free(req_str);
}
XBT_INFO("%s", req_str);
xbt_free(req_str);
}
@@
-375,7
+388,7
@@
void MC_show_deadlock(smx_simcall_t req)
XBT_INFO("*** DEAD-LOCK DETECTED ***");
XBT_INFO("**************************");
XBT_INFO("Locked request:");
XBT_INFO("*** DEAD-LOCK DETECTED ***");
XBT_INFO("**************************");
XBT_INFO("Locked request:");
- /*req_str =
MC_
request_to_string(req);
+ /*req_str =
simgrid::mc::
request_to_string(req);
XBT_INFO("%s", req_str);
xbt_free(req_str); */
XBT_INFO("Counter-example execution trace:");
XBT_INFO("%s", req_str);
xbt_free(req_str); */
XBT_INFO("Counter-example execution trace:");
@@
-392,33
+405,37
@@
void MC_show_non_termination(void){
MC_print_statistics(mc_stats);
}
MC_print_statistics(mc_stats);
}
+namespace simgrid {
+namespace mc {
-void
MC_
show_stack_liveness(xbt_fifo_t stack)
+void show_stack_liveness(xbt_fifo_t stack)
{
int value;
{
int value;
-
mc_pair_t
pair;
+
simgrid::mc::Pair*
pair;
xbt_fifo_item_t item;
smx_simcall_t req;
char *req_str = nullptr;
for (item = xbt_fifo_get_last_item(stack);
item; item = xbt_fifo_get_prev_item(item)) {
xbt_fifo_item_t item;
smx_simcall_t req;
char *req_str = nullptr;
for (item = xbt_fifo_get_last_item(stack);
item; item = xbt_fifo_get_prev_item(item)) {
- pair = (
mc_pair_t
) xbt_fifo_get_item_content(item);
+ pair = (
simgrid::mc::Pair*
) xbt_fifo_get_item_content(item);
req = MC_state_get_executed_request(pair->graph_state, &value);
if (req && req->call != SIMCALL_NONE) {
req = MC_state_get_executed_request(pair->graph_state, &value);
if (req && req->call != SIMCALL_NONE) {
- req_str =
MC_request_to_string(req, value, MC_REQUEST_EXECUTED
);
+ req_str =
simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed
);
XBT_INFO("%s", req_str);
xbt_free(req_str);
}
}
}
XBT_INFO("%s", req_str);
xbt_free(req_str);
}
}
}
-
-void MC_dump_stack_liveness(xbt_fifo_t stack)
+void dump_stack_liveness(xbt_fifo_t stack)
{
{
- mc_pair_t pair;
- while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != nullptr)
- MC_pair_delete(pair);
+ simgrid::mc::Pair* pair;
+ while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
+ delete pair;
+}
+
+}
}
void MC_print_statistics(mc_stats_t stats)
}
void MC_print_statistics(mc_stats_t stats)
@@
-462,10
+479,10
@@
void MC_print_statistics(mc_stats_t stats)
void MC_automaton_load(const char *file)
{
void MC_automaton_load(const char *file)
{
- if (
_mc_
property_automaton == nullptr)
-
_mc_
property_automaton = xbt_automaton_new();
+ if (
simgrid::mc::
property_automaton == nullptr)
+
simgrid::mc::
property_automaton = xbt_automaton_new();
- xbt_automaton_load(
_mc_
property_automaton, file);
+ xbt_automaton_load(
simgrid::mc::
property_automaton, file);
}
// TODO, fix cross-process access (this function is not used)
}
// TODO, fix cross-process access (this function is not used)
@@
-505,19
+522,19
@@
static void MC_dump_stacks(FILE* file)
double MC_process_clock_get(smx_process_t process)
{
double MC_process_clock_get(smx_process_t process)
{
- if (
!mc_time
)
+ if (
simgrid::mc::processes_time.empty()
)
return 0;
if (process != nullptr)
return 0;
if (process != nullptr)
- return
mc
_time[process->pid];
+ return
simgrid::mc::processes
_time[process->pid];
return -1;
}
void MC_process_clock_add(smx_process_t process, double amount)
{
return -1;
}
void MC_process_clock_add(smx_process_t process, double amount)
{
-
mc
_time[process->pid] += amount;
+
simgrid::mc::processes
_time[process->pid] += amount;
}
}
-#if
def
HAVE_MC
+#if HAVE_MC
void MC_report_assertion_error(void)
{
XBT_INFO("**************************");
void MC_report_assertion_error(void)
{
XBT_INFO("**************************");
@@
-549,5
+566,3
@@
void MC_report_crash(int status)
}
#endif
}
#endif
-
-}