From 639e88c95c355661b56405f608d54c27d24ac7c5 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 11 Apr 2016 10:55:31 +0200 Subject: [PATCH 1/1] [mc] Rename RecordTraceElement as Transition and use it to represent a transition --- src/mc/CommunicationDeterminismChecker.cpp | 8 +++-- src/mc/LivenessChecker.cpp | 11 +++--- src/mc/ModelChecker.cpp | 13 +++---- src/mc/ModelChecker.hpp | 3 +- src/mc/SafetyChecker.cpp | 11 +++--- src/mc/Transition.hpp | 38 ++++++++++++++++++++ src/mc/mc_global.cpp | 16 ++------- src/mc/mc_record.cpp | 17 ++++----- src/mc/mc_record.h | 21 +++-------- src/mc/mc_state.cpp | 42 ++++++++++++---------- src/mc/mc_state.h | 15 +++----- tools/cmake/DefinePackages.cmake | 1 + 12 files changed, 108 insertions(+), 88 deletions(-) create mode 100644 src/mc/Transition.hpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 7104f80a12..d2438e48b6 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -22,6 +22,7 @@ #include "src/mc/CommunicationDeterminismChecker.hpp" #include "src/mc/mc_exit.h" #include "src/mc/VisitedState.hpp" +#include "src/mc/Transition.hpp" using simgrid::mc::remote; @@ -320,7 +321,7 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o smx_simcall_t req = &state->executed_req; if (req) trace.push_back(simgrid::mc::request_to_string( - req, state->req_num, simgrid::mc::RequestType::executed)); + req, state->transition.argument, simgrid::mc::RequestType::executed)); } return trace; } @@ -397,7 +398,7 @@ int CommunicationDeterminismChecker::main(void) && (req = MC_state_get_request(state)) != nullptr && (visited_state == nullptr)) { - int req_num = state->req_num; + int req_num = state->transition.argument; XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string( @@ -415,7 +416,8 @@ int CommunicationDeterminismChecker::main(void) call = MC_get_call_type(req); /* Answer the request */ - simgrid::mc::handle_simcall(req, req_num); /* After this call req is no longer useful */ + mc_model_checker->handle_simcall(state->transition); + /* After this call req is no longer useful */ if(!initial_global_state->initial_communications_pattern_done) MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0); diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index f84e892e75..74751880bd 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -29,6 +29,7 @@ #include "src/mc/mc_replay.h" #include "src/mc/mc_safety.h" #include "src/mc/mc_exit.h" +#include "src/mc/Transition.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); @@ -199,7 +200,7 @@ void LivenessChecker::replay() if (pair->exploration_started) { - int req_num = state->req_num; + int req_num = state->transition.argument; smx_simcall_t saved_req = &state->executed_req; smx_simcall_t req = nullptr; @@ -218,7 +219,7 @@ void LivenessChecker::replay() state.get()); } - simgrid::mc::handle_simcall(req, req_num); + mc_model_checker->handle_simcall(state->transition); mc_model_checker->wait_for_requests(); } @@ -318,7 +319,7 @@ std::vector LivenessChecker::getTextualTrace() // override { std::vector trace; for (std::shared_ptr const& pair : explorationStack_) { - int req_num = pair->graph_state->req_num; + int req_num = pair->graph_state->transition.argument; smx_simcall_t req = &pair->graph_state->executed_req; if (req && req->call != SIMCALL_NONE) trace.push_back(simgrid::mc::request_to_string( @@ -371,7 +372,7 @@ int LivenessChecker::main(void) } smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get()); - int req_num = current_pair->graph_state->req_num; + int req_num = current_pair->graph_state->transition.argument; if (dot_output != nullptr) { if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) { @@ -397,7 +398,7 @@ int LivenessChecker::main(void) mc_stats->visited_pairs++; /* Answer the request */ - simgrid::mc::handle_simcall(req, req_num); + mc_model_checker->handle_simcall(current_pair->graph_state->transition); /* Wait for requests (schedules processes) */ mc_model_checker->wait_for_requests(); diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index af180ca3df..670f7193a3 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -30,6 +30,7 @@ #include "src/mc/mc_private.h" #include "src/mc/mc_ignore.h" #include "src/mc/mc_exit.h" +#include "src/mc/Transition.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker"); @@ -422,16 +423,16 @@ void ModelChecker::wait_client(simgrid::mc::Process& process) return; } -void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value) +void ModelChecker::handle_simcall(Transition const& transition) { s_mc_simcall_handle_message m; memset(&m, 0, sizeof(m)); m.type = MC_MESSAGE_SIMCALL_HANDLE; - m.pid = pid; - m.value = value; - process.getChannel().send(m); - process.clear_cache(); - while (process.running()) + m.pid = transition.pid; + m.value = transition.argument; + this->process_->getChannel().send(m); + this->process_->clear_cache(); + while (this->process_->running()) if (!this->handle_events()) return; } diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 2c1abd27df..394a8c1822 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -21,6 +21,7 @@ #include "src/mc/Process.hpp" #include "src/mc/PageStore.hpp" #include "src/mc/mc_protocol.h" +#include "src/mc/Transition.hpp" namespace simgrid { namespace mc { @@ -61,7 +62,7 @@ public: void loop(); bool handle_events(); void wait_client(simgrid::mc::Process& process); - void simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value); + void handle_simcall(Transition const& transition); void wait_for_requests() { mc_model_checker->wait_client(mc_model_checker->process()); diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 8055c65b60..0ff20dfcb3 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -25,6 +25,7 @@ #include "src/mc/Checker.hpp" #include "src/mc/SafetyChecker.hpp" #include "src/mc/VisitedState.hpp" +#include "src/mc/Transition.hpp" #include "src/xbt/mmalloc/mmprivate.h" @@ -76,7 +77,7 @@ std::vector SafetyChecker::getTextualTrace() // override { std::vector trace; for (auto const& state : stack_) { - int value = state->req_num; + int value = state->transition.argument; smx_simcall_t req = &state->executed_req; if (req) trace.push_back(simgrid::mc::request_to_string( @@ -115,7 +116,7 @@ int SafetyChecker::run() continue; } - int req_num = state->req_num; + int req_num = state->transition.argument; // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. @@ -133,7 +134,7 @@ int SafetyChecker::run() // MC_execute_transition(req, req_num) /* Answer the request */ - simgrid::mc::handle_simcall(req, req_num); + mc_model_checker->handle_simcall(state->transition); mc_model_checker->wait_for_requests(); /* Create the new expanded state */ @@ -220,13 +221,13 @@ int SafetyChecker::backtrack() && simgrid::mc::request_depend(req, &prev_state->internal_req)) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); - int value = prev_state->req_num; + int value = prev_state->transition.argument; smx_simcall_t prev_req = &prev_state->executed_req; XBT_DEBUG("%s (state=%d)", simgrid::mc::request_to_string( prev_req, value, simgrid::mc::RequestType::internal).c_str(), prev_state->num); - value = state->req_num; + value = state->transition.argument; prev_req = &state->executed_req; XBT_DEBUG("%s (state=%d)", simgrid::mc::request_to_string( diff --git a/src/mc/Transition.hpp b/src/mc/Transition.hpp new file mode 100644 index 0000000000..c0a6d0af6e --- /dev/null +++ b/src/mc/Transition.hpp @@ -0,0 +1,38 @@ +/* Copyright (c) 2015-2016. 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. */ + +#ifndef SIMGRID_MC_TRANSITION_HPP +#define SIMGRID_MC_TRANSITION_HPP + +namespace simgrid { +namespace mc { + +/** An element in the recorded path + * + * At each decision point, we need to record which process transition + * is trigerred and potentially which value is associated with this + * transition. The value is used to find which communication is triggerred + * in things like waitany and for associating a given value of MC_random() + * calls. + */ +struct Transition { + int pid = 0; + + /* Which transition was executed for this simcall + * + * Some simcalls can lead to different transitions: + * + * * waitany/testany can trigger on different messages; + * + * * random can produce different values. + */ + int argument = 0; +}; + +} +} + +#endif diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 766665b9cf..56169daff7 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -44,6 +44,7 @@ #include "src/mc/mc_record.h" #include "src/mc/mc_protocol.h" #include "src/mc/Client.hpp" +#include "src/mc/Transition.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); @@ -115,17 +116,6 @@ void MC_run() namespace simgrid { namespace mc { -void handle_simcall(smx_simcall_t req, int req_num) -{ - for (auto& pi : mc_model_checker->process().smx_process_infos) - if (req == &pi.copy.simcall) { - mc_model_checker->simcall_handle( - mc_model_checker->process(), pi.copy.pid, req_num); - return; - } - xbt_die("Could not find the request"); -} - /** * \brief Re-executes from the state at position start all the transitions indicated by * a given model-checker stack. @@ -171,7 +161,7 @@ void replay(std::list> const& stack) if (state == stack.back()) break; - int req_num = state->req_num; + int req_num = state->transition.argument; smx_simcall_t saved_req = &state->executed_req; if (saved_req) { @@ -192,7 +182,7 @@ void replay(std::list> const& stack) if (_sg_mc_comms_determinism || _sg_mc_send_determinism) call = MC_get_call_type(req); - simgrid::mc::handle_simcall(req, req_num); + mc_model_checker->handle_simcall(state->transition); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) MC_handle_comm_pattern(call, req, req_num, nullptr, 1); mc_model_checker->wait_for_requests(); diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index a5043726b9..2bc655b633 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -23,6 +23,7 @@ #include "src/mc/mc_replay.h" #include "src/mc/mc_record.h" #include "src/mc/mc_base.h" +#include "src/mc/Transition.hpp" #if HAVE_MC #include "src/mc/mc_request.h" @@ -46,11 +47,11 @@ void replay(RecordTrace const& trace) { simgrid::mc::wait_for_requests(); - for (auto& item : trace) { - XBT_DEBUG("Executing %i$%i", item.pid, item.value); + for (simgrid::mc::Transition const& transition : trace) { + XBT_DEBUG("Executing %i$%i", transition.pid, transition.argument); // Choose a request: - smx_process_t process = SIMIX_process_from_PID(item.pid); + smx_process_t process = SIMIX_process_from_PID(transition.pid); if (!process) xbt_die("Unexpected process."); smx_simcall_t simcall = &(process->simcall); @@ -61,7 +62,7 @@ void replay(RecordTrace const& trace) xbt_die("Unexpected simcall."); // Execute the request: - SIMIX_simcall_handle(simcall, item.value); + SIMIX_simcall_handle(simcall, transition.argument); simgrid::mc::wait_for_requests(); } } @@ -84,8 +85,8 @@ RecordTrace parseRecordTrace(const char* data) const char* current = data; while (*current) { - simgrid::mc::RecordTraceElement item; - int count = sscanf(current, "%u/%u", &item.pid, &item.value); + simgrid::mc::Transition item; + int count = sscanf(current, "%u/%u", &item.pid, &item.argument); if(count != 2 && count != 1) throw std::runtime_error("Could not parse record path"); res.push_back(item); @@ -110,8 +111,8 @@ std::string traceToString(simgrid::mc::RecordTrace const& trace) if (i != trace.begin()) stream << ';'; stream << i->pid; - if (i->value) - stream << '/' << i->value; + if (i->argument) + stream << '/' << i->argument; } return stream.str(); } diff --git a/src/mc/mc_record.h b/src/mc/mc_record.h index db7636ffac..7901b67e07 100644 --- a/src/mc/mc_record.h +++ b/src/mc/mc_record.h @@ -22,27 +22,14 @@ #include +#include "src/mc/Transition.hpp" + namespace simgrid { namespace mc { -/** An element in the recorded path - * - * At each decision point, we need to record which process transition - * is trigerred and potentially which value is associated with this - * transition. The value is used to find which communication is triggerred - * in things like waitany and for associating a given value of MC_random() - * calls. - */ -struct RecordTraceElement { - int pid = 0; - int value = 0; - RecordTraceElement() {} - RecordTraceElement(int pid, int value) : pid(pid), value(value) {} -}; - -typedef std::vector RecordTrace; +typedef std::vector RecordTrace; -/** Convert a string representation of the path into a array of `simgrid::mc::RecordTraceElement` +/** Convert a string representation of the path into a array of `simgrid::mc::Transition` */ XBT_PRIVATE RecordTrace parseRecordTrace(const char* data); XBT_PRIVATE std::string traceToString(simgrid::mc::RecordTrace const& trace); diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index a6f51d354b..a40b2cadb8 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -18,6 +18,7 @@ #include "src/mc/mc_comm_pattern.h" #include "src/mc/mc_smx.h" #include "src/mc/mc_xbt.hpp" +#include "src/mc/Transition.hpp" using simgrid::mc::remote; @@ -59,10 +60,9 @@ std::size_t State::interleaveSize() const [](simgrid::mc::ProcessState const& state) { return state.isToInterleave(); }); } -RecordTraceElement State::getRecordElement() const +Transition State::getRecordElement() const { - smx_process_t issuer = MC_smx_simcall_get_issuer(&this->executed_req); - return RecordTraceElement(issuer->pid, this->req_num); + return this->transition; } } @@ -72,6 +72,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( simgrid::mc::State* state, smx_process_t process) { simgrid::mc::ProcessState* procstate = &state->processStates[process->pid]; + state->transition.pid = -1; + state->transition.argument = -1; if (!procstate->isToInterleave()) return nullptr; @@ -81,13 +83,13 @@ static inline smx_simcall_t MC_state_get_request_for_process( smx_simcall_t req = nullptr; switch (process->simcall.call) { case SIMCALL_COMM_WAITANY: - state->req_num = -1; + state->transition.argument = -1; while (procstate->interleave_count < read_length(mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(&process->simcall)))) { if (simgrid::mc::request_is_enabled_by_idx(&process->simcall, procstate->interleave_count++)) { - state->req_num = procstate->interleave_count - 1; + state->transition.argument = procstate->interleave_count - 1; break; } } @@ -96,19 +98,19 @@ static inline smx_simcall_t MC_state_get_request_for_process( simgrid::mc::read_length(mc_model_checker->process(), simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall)))) procstate->setDone(); - if (state->req_num != -1) + if (state->transition.argument != -1) req = &process->simcall; break; case SIMCALL_COMM_TESTANY: { unsigned start_count = procstate->interleave_count; - state->req_num = -1; + state->transition.argument = -1; while (procstate->interleave_count < read_length(mc_model_checker->process(), remote(simcall_comm_testany__get__comms(&process->simcall)))) if (simgrid::mc::request_is_enabled_by_idx(&process->simcall, procstate->interleave_count++)) { - state->req_num = procstate->interleave_count - 1; + state->transition.argument = procstate->interleave_count - 1; break; } @@ -117,7 +119,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( remote(simcall_comm_testany__get__comms(&process->simcall)))) procstate->setDone(); - if (state->req_num != -1 || start_count == 0) + if (state->transition.argument != -1 || start_count == 0) req = &process->simcall; break; @@ -129,12 +131,12 @@ static inline smx_simcall_t MC_state_get_request_for_process( mc_model_checker->process().read_bytes( &act, sizeof(act), remote(remote_act)); if (act.comm.src_proc && act.comm.dst_proc) - state->req_num = 0; + state->transition.argument = 0; else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY && act.comm.detached == 1) - state->req_num = 0; + state->transition.argument = 0; else - state->req_num = -1; + state->transition.argument = -1; procstate->setDone(); req = &process->simcall; break; @@ -142,9 +144,9 @@ static inline smx_simcall_t MC_state_get_request_for_process( case SIMCALL_MC_RANDOM: { int min_value = simcall_mc_random__get__min(&process->simcall); - state->req_num = procstate->interleave_count + min_value; + state->transition.argument = procstate->interleave_count + min_value; procstate->interleave_count++; - if (state->req_num == simcall_mc_random__get__max(&process->simcall)) + if (state->transition.argument == simcall_mc_random__get__max(&process->simcall)) procstate->setDone(); req = &process->simcall; break; @@ -152,7 +154,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( default: procstate->setDone(); - state->req_num = 0; + state->transition.argument = 0; req = &process->simcall; break; } @@ -161,6 +163,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( // Fetch the data of the request and translate it: + state->transition.pid = process->pid; + state->executed_req = *req; /* The waitany and testany request are transformed into a wait or test request @@ -173,7 +177,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( smx_synchro_t remote_comm; read_element(mc_model_checker->process(), &remote_comm, remote(simcall_comm_waitany__get__comms(req)), - state->req_num, sizeof(remote_comm)); + state->transition.argument, sizeof(remote_comm)); mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm); simcall_comm_wait__set__timeout(&state->internal_req, 0); @@ -184,16 +188,16 @@ static inline smx_simcall_t MC_state_get_request_for_process( state->internal_req.call = SIMCALL_COMM_TEST; state->internal_req.issuer = req->issuer; - if (state->req_num > 0) { + if (state->transition.argument > 0) { smx_synchro_t remote_comm; read_element(mc_model_checker->process(), &remote_comm, remote(simcall_comm_testany__get__comms(req)), - state->req_num, sizeof(remote_comm)); + state->transition.argument, sizeof(remote_comm)); mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); } simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); - simcall_comm_test__set__result(&state->internal_req, state->req_num); + simcall_comm_test__set__result(&state->internal_req, state->transition.argument); break; case SIMCALL_COMM_WAIT: diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index fbff700820..851d7c07b5 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -17,6 +17,7 @@ #include "src/simix/smx_private.h" #include "src/mc/mc_snapshot.h" #include "src/mc/mc_record.h" +#include "src/mc/Transition.hpp" namespace simgrid { namespace mc { @@ -110,19 +111,11 @@ struct XBT_PRIVATE State { /** Sequential state number (used for debugging) */ int num = 0; - /* Which transition was executed for this simcall - * - * Some simcalls can lead to different transitions: - * - * * waitany/testany can trigger on different messages; - * - * * random can produce different values. - */ - int req_num = 0; - /** State's exploration status by process */ std::vector processStates; + Transition transition; + /** The simcall which was executed */ s_smx_simcall_t executed_req; @@ -150,7 +143,7 @@ struct XBT_PRIVATE State { { this->processStates[process->pid].interleave(); } - RecordTraceElement getRecordElement() const; + Transition getRecordElement() const; }; XBT_PRIVATE void replay(std::list> const& stack); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 1208987eb8..74ff5d9996 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -619,6 +619,7 @@ set(MC_SRC src/mc/mc_xbt.hpp src/mc/mc_xbt.cpp src/mc/mc_exit.h + src/mc/Transition.hpp ) set(MC_SIMGRID_MC_SRC -- 2.20.1