From dc0b836b646303e8a540d20d9e86ecd4049bb372 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 7 Mar 2016 15:02:37 +0100 Subject: [PATCH] [mc] Move things in the MC namespace --- src/mc/mc_base.cpp | 37 ++++++++---- src/mc/mc_base.h | 29 +++++---- src/mc/mc_client.cpp | 2 +- src/mc/mc_comm_determinism.cpp | 10 +-- src/mc/mc_global.cpp | 44 ++++++++------ src/mc/mc_liveness.cpp | 12 ++-- src/mc/mc_record.cpp | 10 +-- src/mc/mc_request.cpp | 107 +++++++++++++-------------------- src/mc/mc_request.h | 44 +++++++------- src/mc/mc_safety.cpp | 16 ++--- src/mc/mc_state.cpp | 10 +-- 11 files changed, 162 insertions(+), 159 deletions(-) diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 9717dfc7ce..c3fbeedd58 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -21,6 +21,7 @@ #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" @@ -34,6 +35,8 @@ extern "C" { XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); +} + int MC_random(int min, int max) { xbt_assert(mc_mode != MC_MODE_SERVER); @@ -43,7 +46,10 @@ int MC_random(int min, int max) 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); @@ -55,14 +61,14 @@ void MC_wait_for_requests(void) 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; @@ -72,7 +78,7 @@ int MC_request_is_enabled(smx_simcall_t req) 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 */ @@ -90,7 +96,7 @@ int MC_request_is_enabled(smx_simcall_t req) /* 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 @@ -135,13 +141,13 @@ int MC_request_is_enabled(smx_simcall_t req) #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); @@ -153,7 +159,7 @@ int MC_request_is_enabled(smx_simcall_t req) } #endif if(mutex->owner == nullptr) - return TRUE; + return true; else #ifdef HAVE_MC // TODO, *(mutex->owner) :/ @@ -166,11 +172,11 @@ int MC_request_is_enabled(smx_simcall_t req) 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 @@ -188,6 +194,9 @@ int MC_request_is_visible(smx_simcall_t req) ; } +} +} + static int prng_random(int min, int max) { unsigned long output_size = ((unsigned long) max - (unsigned long) min) + 1; @@ -214,7 +223,10 @@ int simcall_HANDLER_mc_random(smx_simcall_t simcall, int min, int max) 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); @@ -236,3 +248,4 @@ void MC_simcall_handle(smx_simcall_t req, int value) } } +} diff --git a/src/mc/mc_base.h b/src/mc/mc_base.h index 0cd5848c52..c9a324b389 100644 --- a/src/mc/mc_base.h +++ b/src/mc/mc_base.h @@ -10,19 +10,19 @@ #include #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 * @@ -30,13 +30,16 @@ XBT_PRIVATE int MC_request_is_visible(smx_simcall_t req); * 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 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 diff --git a/src/mc/mc_client.cpp b/src/mc/mc_client.cpp index cf57b91816..cb822245a6 100644 --- a/src/mc/mc_client.cpp +++ b/src/mc/mc_client.cpp @@ -148,7 +148,7 @@ void MC_client_main_loop(void) 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(); } } diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index 623365919e..410510d9d4 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/mc_comm_determinism.cpp @@ -331,7 +331,7 @@ static void MC_pre_modelcheck_comm_determinism(void) /* 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); @@ -363,12 +363,12 @@ static int MC_modelcheck_comm_determinism_main(void) && (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++; @@ -379,7 +379,7 @@ static int MC_modelcheck_comm_determinism_main(void) 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); @@ -396,7 +396,7 @@ static int MC_modelcheck_comm_determinism_main(void) /* 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) diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index a77c61404c..0b430b53cf 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -9,6 +9,8 @@ #include #include +#include + #include "mc_base.h" #include "mc/mc.h" @@ -45,9 +47,17 @@ extern "C" { 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 processes_time; + +} +} #ifdef HAVE_MC int user_max_depth_reached = 0; @@ -103,13 +113,14 @@ void MC_init_dot_output() #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) @@ -131,8 +142,7 @@ void MC_run() void MC_exit(void) { - xbt_free(mc_time); - + simgrid::mc::processes_time.clear(); MC_memory_exit(); //xbt_abort(); } @@ -163,7 +173,7 @@ int MC_deadlock_check() 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; } @@ -236,7 +246,7 @@ void MC_replay(xbt_fifo_t stack) /* 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); } @@ -246,7 +256,7 @@ void MC_replay(xbt_fifo_t stack) 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); @@ -310,14 +320,14 @@ void MC_replay_liveness(xbt_fifo_t stack) /* 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(); } @@ -361,7 +371,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) { - 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); } @@ -375,7 +385,7 @@ void MC_show_deadlock(smx_simcall_t req) 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:"); @@ -406,7 +416,7 @@ void MC_show_stack_liveness(xbt_fifo_t stack) 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); } @@ -505,16 +515,16 @@ static void MC_dump_stacks(FILE* file) 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 @@ -549,5 +559,3 @@ void MC_report_crash(int status) } #endif - -} diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp index 3d9dd5372c..fbea394d25 100644 --- a/src/mc/mc_liveness.cpp +++ b/src/mc/mc_liveness.cpp @@ -194,7 +194,7 @@ static void MC_pre_modelcheck_liveness(void) /* 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); @@ -270,13 +270,13 @@ static int MC_modelcheck_liveness_main(void) 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); @@ -289,7 +289,7 @@ static int MC_modelcheck_liveness_main(void) 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(); @@ -313,7 +313,7 @@ static int MC_modelcheck_liveness_main(void) 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); @@ -388,7 +388,7 @@ int MC_modelcheck_liveness(void) int res = MC_modelcheck_liveness_main(); /* We're done */ - xbt_free(mc_time); + simgrid::mc::processes_time.clear(); return res; } diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index f0ff676b31..edd3d445f3 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -22,6 +22,7 @@ #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" @@ -37,7 +38,7 @@ char* MC_record_path = nullptr; 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: @@ -56,12 +57,13 @@ void MC_record_replay(mc_record_item_t start, std::size_t len) 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(); } } @@ -186,7 +188,7 @@ void MC_record_replay_from_string(const char* path_string) void MC_record_replay_init() { - mc_time = xbt_new0(double, simix_process_maxpid); + simgrid::mc::processes_time.resize(simix_process_maxpid); } } diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp index f85fad264f..0c2acf8651 100644 --- a/src/mc/mc_request.cpp +++ b/src/mc/mc_request.cpp @@ -24,6 +24,8 @@ extern "C" { 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); @@ -53,15 +55,18 @@ smx_mailbox_t MC_get_rdv(smx_simcall_t r) } } +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: @@ -75,25 +80,25 @@ int MC_request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) 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 @@ -106,18 +111,18 @@ int MC_request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) 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 @@ -127,19 +132,19 @@ int MC_request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) && 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) @@ -148,8 +153,8 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) 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: @@ -164,7 +169,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) 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 @@ -172,14 +177,17 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) && 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) { @@ -199,15 +207,15 @@ static char *buff_size_to_string(size_t buff_size) } -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; } @@ -427,44 +435,10 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req 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) { @@ -491,7 +465,7 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) break; default: - return TRUE; + return true; } s_smx_synchro_t synchro; @@ -500,12 +474,12 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) 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; @@ -669,3 +643,4 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) } } +} diff --git a/src/mc/mc_request.h b/src/mc/mc_request.h index 1ca589c922..1f9fc0dc0d 100644 --- a/src/mc/mc_request.h +++ b/src/mc/mc_request.h @@ -13,35 +13,37 @@ 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() diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp index 4047f13f41..bd63a0ab69 100644 --- a/src/mc/mc_safety.cpp +++ b/src/mc/mc_safety.cpp @@ -65,7 +65,7 @@ static void MC_pre_modelcheck_safety() /* 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; @@ -108,12 +108,12 @@ int MC_modelcheck_safety(void) 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++; @@ -122,7 +122,7 @@ int MC_modelcheck_safety(void) // 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 */ @@ -137,7 +137,7 @@ int MC_modelcheck_safety(void) /* 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; @@ -200,15 +200,15 @@ int MC_modelcheck_safety(void) "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); } diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 566d98db3c..510a7dee23 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -187,7 +187,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( 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) { @@ -197,8 +197,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( 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; } @@ -220,8 +220,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( 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; } -- 2.20.1