#include "src/mc/mc_protocol.h"
#ifdef HAVE_MC
+#include "src/mc/mc_request.h"
#include "src/mc/Process.hpp"
#include "src/mc/ModelChecker.hpp"
#include "src/mc/mc_smx.h"
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
+}
+
int MC_random(int min, int max)
{
xbt_assert(mc_mode != MC_MODE_SERVER);
return simcall_mc_random(min, max);
}
-void MC_wait_for_requests(void)
+namespace simgrid {
+namespace mc {
+
+void wait_for_requests(void)
{
assert(mc_mode != MC_MODE_SERVER);
SIMIX_process_runall();
xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
req = &process->simcall;
- if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
+ if (req->call != SIMCALL_NONE && !simgrid::mc::request_is_visible(req))
SIMIX_simcall_handle(req, 0);
}
}
}
// Called from both MCer and MCed:
-int MC_request_is_enabled(smx_simcall_t req)
+bool request_is_enabled(smx_simcall_t req)
{
unsigned int index = 0;
smx_synchro_t act = 0;
switch (req->call) {
case SIMCALL_NONE:
- return FALSE;
+ return false;
case SIMCALL_COMM_WAIT:
/* FIXME: check also that src and dst processes are not suspended */
/* If it has a timeout it will be always be enabled, because even if the
* communication is not ready, it can timeout and won't block. */
if (_sg_mc_timeout == 1)
- return TRUE;
+ return true;
}
/* On the other hand if it hasn't a timeout, check if the comm is ready.*/
else if (act->comm.detached && act->comm.src_proc == nullptr
#endif
act = xbt_dynar_get_as(comms, index, smx_synchro_t);
if (act->comm.src_proc && act->comm.dst_proc)
- return TRUE;
+ return true;
}
- return FALSE;
+ return false;
}
case SIMCALL_MUTEX_TRYLOCK:
- return TRUE;
+ return true;
case SIMCALL_MUTEX_LOCK: {
smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
}
#endif
if(mutex->owner == nullptr)
- return TRUE;
+ return true;
else
#ifdef HAVE_MC
// TODO, *(mutex->owner) :/
default:
/* The rest of the requests are always enabled */
- return TRUE;
+ return true;
}
}
-int MC_request_is_visible(smx_simcall_t req)
+bool request_is_visible(smx_simcall_t req)
{
return req->call == SIMCALL_COMM_ISEND
|| req->call == SIMCALL_COMM_IRECV
;
}
+}
+}
+
static int prng_random(int min, int max)
{
unsigned long output_size = ((unsigned long) max - (unsigned long) min) + 1;
return simcall->mc_value;
}
-void MC_simcall_handle(smx_simcall_t req, int value)
+namespace simgrid {
+namespace mc {
+
+void handle_simcall(smx_simcall_t req, int value)
{
#ifndef HAVE_MC
SIMIX_simcall_handle(req, value);
}
}
+}
#include <xbt/base.h>
#include "src/simix/popping_private.h" // smx_simcall_t
-SG_BEGIN_DECL()
+#ifdef __cplusplus
-/** Check if the given simcall can be resolved
- *
- * \return `TRUE` or `FALSE`
- */
-XBT_PRIVATE int MC_request_is_enabled(smx_simcall_t req);
+namespace simgrid {
+namespace mc {
-/** Check if the given simcall is visible
+/** Can this requests can be executed.
*
- * \return `TRUE` or `FALSE`
+ * Most requests are always enabled but WAIT and WAITANY
+ * are not always enabled: a WAIT where the communication does not
+ * have both a source and a destination yet is not enabled
+ * (unless timeout is enabled in the wait and enabeld in SimGridMC).
*/
-XBT_PRIVATE int MC_request_is_visible(smx_simcall_t req);
+XBT_PRIVATE bool request_is_enabled(smx_simcall_t req);
/** Execute everything which is invisible
*
* iteratively until there doesn't remain any. At this point, the function
* returns to the caller which can handle the visible (and ready) simcalls.
*/
-XBT_PRIVATE void MC_wait_for_requests(void);
+XBT_PRIVATE void wait_for_requests(void);
-XBT_PRIVATE extern double *mc_time;
+XBT_PRIVATE extern std::vector<double> processes_time;
/** Execute a given simcall */
-XBT_PRIVATE void MC_simcall_handle(smx_simcall_t req, int value);
+XBT_PRIVATE void handle_simcall(smx_simcall_t req, int value);
-SG_END_DECL()
+}
+}
+
+#endif
#endif
while (1) {
MC_protocol_send_simple_message(mc_client->fd, MC_MESSAGE_WAITING);
MC_client_handle_messages();
- MC_wait_for_requests();
+ simgrid::mc::wait_for_requests();
}
}
/* Get an enabled process and insert it in the interleave set of the initial state */
for (auto& p : mc_model_checker->process().simix_processes())
- if (MC_process_is_enabled(&p.copy))
+ if (simgrid::mc::process_is_enabled(&p.copy))
MC_state_interleave_process(initial_state, &p.copy);
xbt_fifo_unshift(mc_stack, initial_state);
&& (req = MC_state_get_request(state, &value))
&& (visited_state == nullptr)) {
- 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("Execute: %s", req_str);
xbt_free(req_str);
if (dot_output != nullptr)
- req_str = MC_request_get_dot_output(req, value);
+ req_str = simgrid::mc::request_get_dot_output(req, value);
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
call = MC_get_call_type(req);
/* Answer the request */
- MC_simcall_handle(req, value); /* After this call req is no longer useful */
+ simgrid::mc::handle_simcall(req, value); /* After this call req is no longer useful */
if(!initial_global_state->initial_communications_pattern_done)
MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
/* Get enabled processes and insert them in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
- if (MC_process_is_enabled(&p.copy))
+ if (simgrid::mc::process_is_enabled(&p.copy))
MC_state_interleave_process(next_state, &p.copy);
if (dot_output != nullptr)
#include <cstddef>
#include <cstdint>
+#include <vector>
+
#include "mc_base.h"
#include "mc/mc.h"
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
int user_max_depth_reached = 0;
#ifdef HAVE_MC
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: */
- 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)
void MC_exit(void)
{
- xbt_free(mc_time);
-
+ simgrid::mc::processes_time.clear();
MC_memory_exit();
//xbt_abort();
}
if (xbt_swag_size(simix_global->process_list)) {
deadlock = TRUE;
xbt_swag_foreach(process, simix_global->process_list)
- if (MC_process_is_enabled(process)) {
+ if (simgrid::mc::process_is_enabled(process)) {
deadlock = FALSE;
break;
}
/* 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);
}
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);
/* 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);
}
}
- MC_simcall_handle(req, value);
+ simgrid::mc::handle_simcall(req, value);
mc_model_checker->wait_for_requests();
}
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("*** 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:");
pair = (mc_pair_t) xbt_fifo_get_item_content(item);
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);
}
double MC_process_clock_get(smx_process_t process)
{
- if (!mc_time)
+ if (simgrid::mc::processes_time.empty())
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)
{
- mc_time[process->pid] += amount;
+ simgrid::mc::processes_time[process->pid] += amount;
}
#ifdef HAVE_MC
}
#endif
-
-}
/* Get enabled processes and insert them in the interleave set of the graph_state */
for (auto& p : mc_model_checker->process().simix_processes())
- if (MC_process_is_enabled(&p.copy))
+ if (simgrid::mc::process_is_enabled(&p.copy))
MC_state_interleave_process(initial_pair->graph_state, &p.copy);
initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
xbt_free(initial_global_state->prev_req);
}
initial_global_state->prev_pair = current_pair->num;
- initial_global_state->prev_req = MC_request_get_dot_output(req, value);
+ initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value);
if (current_pair->search_cycle)
fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
fflush(dot_output);
}
- char* req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+ char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
mc_stats->visited_pairs++;
/* Answer the request */
- MC_simcall_handle(req, value);
+ simgrid::mc::handle_simcall(req, value);
/* Wait for requests (schedules processes) */
mc_model_checker->wait_for_requests();
next_pair->depth = current_pair->depth + 1;
/* Get enabled processes and insert them in the interleave set of the next graph_state */
for (auto& p : mc_model_checker->process().simix_processes())
- if (MC_process_is_enabled(&p.copy))
+ if (simgrid::mc::process_is_enabled(&p.copy))
MC_state_interleave_process(next_pair->graph_state, &p.copy);
next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
int res = MC_modelcheck_liveness_main();
/* We're done */
- xbt_free(mc_time);
+ simgrid::mc::processes_time.clear();
return res;
}
#include "src/mc/mc_base.h"
#ifdef HAVE_MC
+#include "src/mc/mc_request.h"
#include "src/mc/mc_private.h"
#include "src/mc/mc_state.h"
#include "src/mc/mc_smx.h"
void MC_record_replay(mc_record_item_t start, std::size_t len)
{
- MC_wait_for_requests();
+ simgrid::mc::wait_for_requests();
mc_record_item_t end = start + len;
// Choose the recorded simcall and execute it:
smx_simcall_t simcall = &(process->simcall);
if(!simcall || simcall->call == SIMCALL_NONE)
xbt_die("No simcall for this process.");
- if (!MC_request_is_visible(simcall) || !MC_request_is_enabled(simcall))
+ if (!simgrid::mc::request_is_visible(simcall)
+ || !simgrid::mc::request_is_enabled(simcall))
xbt_die("Unexpected simcall.");
// Execute the request:
SIMIX_simcall_handle(simcall, item->value);
- MC_wait_for_requests();
+ simgrid::mc::wait_for_requests();
}
}
void MC_record_replay_init()
{
- mc_time = xbt_new0(double, simix_process_maxpid);
+ simgrid::mc::processes_time.resize(simix_process_maxpid);
}
}
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
"Logging specific to MC (request)");
+}
+
static char *pointer_to_string(void *pointer);
static char *buff_size_to_string(size_t size);
}
}
+namespace simgrid {
+namespace mc {
+
// Does half the job
static inline
-int MC_request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
+bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
{
if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
- return FALSE;
+ return false;
if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
- return FALSE;
+ return false;
// Those are internal requests, we do not need indirection
// because those objects are copies:
if (rdv != synchro2->comm.rdv_cpy
&& simcall_comm_wait__get__timeout(r2) <= 0)
- return FALSE;
+ return false;
if ((r1->issuer != synchro2->comm.src_proc)
&& (r1->issuer != synchro2->comm.dst_proc)
&& simcall_comm_wait__get__timeout(r2) <= 0)
- return FALSE;
+ return false;
if ((r1->call == SIMCALL_COMM_ISEND)
&& (synchro2->comm.type == SIMIX_COMM_SEND)
&& (synchro2->comm.src_buff !=
simcall_comm_isend__get__src_buff(r1))
&& simcall_comm_wait__get__timeout(r2) <= 0)
- return FALSE;
+ return false;
if ((r1->call == SIMCALL_COMM_IRECV)
&& (synchro2->comm.type == SIMIX_COMM_RECEIVE)
&& (synchro2->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
&& simcall_comm_wait__get__timeout(r2) <= 0)
- return FALSE;
+ return false;
}
/* FIXME: the following rule assumes that the result of the
if (r1->call == SIMCALL_COMM_WAIT
&& (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
&& (synchro1->comm.src_proc == nullptr || synchro1->comm.dst_proc == NULL))
- return FALSE;
+ return false;
if (r1->call == SIMCALL_COMM_TEST &&
(simcall_comm_test__get__comm(r1) == nullptr
|| synchro1->comm.src_buff == nullptr
|| synchro1->comm.dst_buff == nullptr))
- return FALSE;
+ return false;
if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
&& synchro1->comm.src_buff == synchro2->comm.src_buff
&& synchro1->comm.dst_buff == synchro2->comm.dst_buff)
- return FALSE;
+ return false;
if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
&& synchro1->comm.src_buff != nullptr
&& synchro1->comm.dst_buff != synchro2->comm.src_buff
&& synchro1->comm.dst_buff != synchro2->comm.dst_buff
&& synchro2->comm.dst_buff != synchro1->comm.src_buff)
- return FALSE;
+ return false;
- return TRUE;
+ return true;
}
// Those are MC_state_get_internal_request(state)
-int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
+bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
{
if (mc_reduce_kind == e_mc_reduce_none)
- return TRUE;
+ return true;
if (r1->issuer == r2->issuer)
- return FALSE;
+ return false;
/* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
return TRUE;
if (r1->call != r2->call)
- return MC_request_depend_asymmetric(r1, r2)
- && MC_request_depend_asymmetric(r2, r1);
+ return request_depend_asymmetric(r1, r2)
+ && request_depend_asymmetric(r2, r1);
// Those are internal requests, we do not need indirection
// because those objects are copies:
case SIMCALL_COMM_WAIT:
if (synchro1->comm.src_buff == synchro2->comm.src_buff
&& synchro1->comm.dst_buff == synchro2->comm.dst_buff)
- return FALSE;
+ return false;
else if (synchro1->comm.src_buff != nullptr
&& synchro1->comm.dst_buff != nullptr
&& synchro2->comm.src_buff != nullptr
&& synchro1->comm.dst_buff != synchro2->comm.src_buff
&& synchro1->comm.dst_buff != synchro2->comm.dst_buff
&& synchro2->comm.dst_buff != synchro1->comm.src_buff)
- return FALSE;
+ return false;
else
- return TRUE;
+ return true;
default:
- return TRUE;
+ return true;
}
}
+}
+}
+
static char *pointer_to_string(void *pointer)
{
}
-char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t request_type)
+char *simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType request_type)
{
bool use_remote_comm = true;
switch(request_type) {
- case MC_REQUEST_SIMIX:
+ case simgrid::mc::RequestType::simix:
use_remote_comm = true;
break;
- case MC_REQUEST_EXECUTED:
- case MC_REQUEST_INTERNAL:
+ case simgrid::mc::RequestType::executed:
+ case simgrid::mc::RequestType::internal:
use_remote_comm = false;
break;
}
return str;
}
-unsigned int MC_request_testany_fail(smx_simcall_t req)
-{
- // Remote xbt_dynar_foreach on simcall_comm_testany__get__comms(req).
-
- // Read the dynar:
- s_xbt_dynar_t comms;
- mc_model_checker->process().read_bytes(
- &comms, sizeof(comms), remote(simcall_comm_testany__get__comms(req)));
+namespace simgrid {
+namespace mc {
- // Read ther dynar buffer:
- size_t buffer_size = comms.elmsize * comms.used;
- char buffer[buffer_size];
- mc_model_checker->process().read_bytes(
- buffer, buffer_size, remote(comms.data));
-
- // Iterate over the elements:
- assert(comms.elmsize == sizeof(smx_synchro_t));
- unsigned cursor;
- for (cursor=0; cursor != comms.used; ++cursor) {
-
- // Get the element:
- smx_synchro_t remote_action = nullptr;
- memcpy(&remote_action, buffer + comms.elmsize * cursor, sizeof(remote_action));
-
- // Dereference the pointer:
- s_smx_synchro_t action;
- mc_model_checker->process().read_bytes(
- &action, sizeof(action), remote(remote_action));
-
- // Finally so something useful about it:
- if (action.comm.src_proc && action.comm.dst_proc)
- return FALSE;
- }
-
- return TRUE;
-}
-
-int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
+bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
{
smx_synchro_t remote_act = nullptr;
switch (req->call) {
break;
default:
- return TRUE;
+ return true;
}
s_smx_synchro_t synchro;
return synchro.comm.src_proc && synchro.comm.dst_proc;
}
-int MC_process_is_enabled(smx_process_t process)
+bool process_is_enabled(smx_process_t process)
{
- return MC_request_is_enabled(&process->simcall);
+ return simgrid::mc::request_is_enabled(&process->simcall);
}
-char *MC_request_get_dot_output(smx_simcall_t req, int value)
+char *request_get_dot_output(smx_simcall_t req, int value)
{
char *label = nullptr;
}
}
+}
SG_BEGIN_DECL()
-typedef enum e_mc_request_type {
- MC_REQUEST_SIMIX,
- MC_REQUEST_EXECUTED,
- MC_REQUEST_INTERNAL,
-} e_mc_request_type_t;
-
-XBT_PRIVATE int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
-XBT_PRIVATE char* MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t type);
-XBT_PRIVATE unsigned int MC_request_testany_fail(smx_simcall_t req);
-/* XBT_PRIVATE int MC_waitany_is_enabled_by_comm(smx_req_t req, unsigned int comm);*/
-XBT_PRIVATE int MC_request_is_visible(smx_simcall_t req);
-
-/** Can this requests can be executed.
+namespace simgrid {
+namespace mc {
+
+enum class RequestType {
+ simix,
+ executed,
+ internal,
+};
+
+XBT_PRIVATE bool request_depend(smx_simcall_t req1, smx_simcall_t req2);
+
+XBT_PRIVATE char* request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType type);
+
+/** Check if the given simcall is visible
*
- * Most requests are always enabled but WAIT and WAITANY
- * are not always enabled: a WAIT where the communication does not
- * have both a source and a destination yet is not enabled
- * (unless timeout is enabled in the wait and enabeld in SimGridMC).
+ * \return `TRUE` or `FALSE`
*/
-XBT_PRIVATE int MC_request_is_enabled(smx_simcall_t req);
-XBT_PRIVATE int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx);
+XBT_PRIVATE bool request_is_visible(smx_simcall_t req);
+
+XBT_PRIVATE bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx);
/** Is the process ready to execute its simcall?
*
* This is true if the request associated with the process is ready.
*/
-XBT_PRIVATE int MC_process_is_enabled(smx_process_t process);
+XBT_PRIVATE bool process_is_enabled(smx_process_t process);
+
+XBT_PRIVATE char *request_get_dot_output(smx_simcall_t req, int value);
-XBT_PRIVATE char *MC_request_get_dot_output(smx_simcall_t req, int value);
+}
+}
SG_END_DECL()
/* Get an enabled process and insert it in the interleave set of the initial state */
for (auto& p : mc_model_checker->process().simix_processes())
- if (MC_process_is_enabled(&p.copy)) {
+ if (simgrid::mc::process_is_enabled(&p.copy)) {
MC_state_interleave_process(initial_state, &p.copy);
if (mc_reduce_kind != e_mc_reduce_none)
break;
if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
&& (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
- 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("Execute: %s", req_str);
xbt_free(req_str);
if (dot_output != nullptr)
- req_str = MC_request_get_dot_output(req, value);
+ req_str = simgrid::mc::request_get_dot_output(req, value);
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
// MC_execute_transition(req, value)
/* Answer the request */
- MC_simcall_handle(req, value);
+ simgrid::mc::handle_simcall(req, value);
mc_model_checker->wait_for_requests();
/* Create the new expanded state */
/* Get an enabled process and insert it in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
- if (MC_process_is_enabled(&p.copy)) {
+ if (simgrid::mc::process_is_enabled(&p.copy)) {
MC_state_interleave_process(next_state, &p.copy);
if (mc_reduce_kind != e_mc_reduce_none)
break;
"use --cfg=model-check/reduction:none");
const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
- if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
+ if (simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
- req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
+ req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
xbt_free(req_str);
prev_req = MC_state_get_executed_request(state, &value);
- req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
+ req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
XBT_DEBUG("%s (state=%d)", req_str, state->num);
xbt_free(req_str);
}
if (procstate->state != MC_INTERLEAVE
&& procstate->state != MC_MORE_INTERLEAVE)
return nullptr;
- if (!MC_process_is_enabled(process))
+ if (!simgrid::mc::process_is_enabled(process))
return nullptr;
switch (process->simcall.call) {
while (procstate->interleave_count <
read_length(mc_model_checker->process(),
remote(simcall_comm_waitany__get__comms(&process->simcall)))) {
- if (MC_request_is_enabled_by_idx
- (&process->simcall, procstate->interleave_count++)) {
+ if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
+ procstate->interleave_count++)) {
*value = procstate->interleave_count - 1;
break;
}
while (procstate->interleave_count <
read_length(mc_model_checker->process(),
remote(simcall_comm_testany__get__comms(&process->simcall))))
- if (MC_request_is_enabled_by_idx
- (&process->simcall, procstate->interleave_count++)) {
+ if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
+ procstate->interleave_count++)) {
*value = procstate->interleave_count - 1;
break;
}
