From 96d281781f5a45598b4c1fa42fa2059d15d53c73 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 24 Mar 2016 10:42:29 +0100 Subject: [PATCH 1/1] [mc] Move main communication determinism code in a CommunicationDeterminismChecker class --- ...pp => CommunicationDeterminismChecker.cpp} | 42 ++++++++++++------- src/mc/CommunicationDeterminismChecker.hpp | 29 +++++++++++++ src/mc/mc_comm_pattern.h | 1 - src/mc/simgrid_mc.cpp | 5 ++- tools/cmake/DefinePackages.cmake | 3 +- 5 files changed, 61 insertions(+), 19 deletions(-) rename src/mc/{mc_comm_determinism.cpp => CommunicationDeterminismChecker.cpp} (97%) create mode 100644 src/mc/CommunicationDeterminismChecker.hpp diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/CommunicationDeterminismChecker.cpp similarity index 97% rename from src/mc/mc_comm_determinism.cpp rename to src/mc/CommunicationDeterminismChecker.cpp index 3870c388c6..5262982bce 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -20,6 +20,7 @@ #include "src/mc/mc_record.h" #include "src/mc/mc_smx.h" #include "src/mc/Client.hpp" +#include "src/mc/CommunicationDeterminismChecker.hpp" #include "src/mc/mc_exit.h" using simgrid::mc::remote; @@ -27,8 +28,6 @@ using simgrid::mc::remote; XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection"); -extern "C" { - /********** Global variables **********/ xbt_dynar_t initial_communications_pattern; @@ -165,10 +164,10 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int initial_global_state->recv_diff = nullptr; MC_print_statistics(mc_stats); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); - } + } } } - + MC_comm_pattern_free(comm); } @@ -231,7 +230,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type } return; } - } else if (call_type == MC_CALL_TYPE_RECV) { + } else if (call_type == MC_CALL_TYPE_RECV) { pattern->type = SIMIX_COMM_RECEIVE; pattern->comm_addr = simcall_comm_irecv__get__result(request); @@ -296,16 +295,28 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne /************************ Main algorithm ************************/ -static int MC_modelcheck_comm_determinism_main(void); +namespace simgrid { +namespace mc { + +CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session) + : Checker(session) +{ + +} + +CommunicationDeterminismChecker::~CommunicationDeterminismChecker() +{ + +} -static void MC_pre_modelcheck_comm_determinism(void) +void CommunicationDeterminismChecker::prepare() { mc_state_t initial_state = nullptr; int i; const int maxpid = MC_smx_get_maxpid(); simgrid::mc::visited_states.clear(); - + // Create initial_communications_pattern elements: initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp); for (i=0; i < maxpid; i++){ @@ -323,7 +334,7 @@ static void MC_pre_modelcheck_comm_determinism(void) } initial_state = MC_state_new(); - + XBT_DEBUG("********* Start communication determinism verification *********"); /* Wait for requests (schedules processes) */ @@ -351,7 +362,7 @@ bool all_communications_are_finished() return true; } -static int MC_modelcheck_comm_determinism_main(void) +int CommunicationDeterminismChecker::main(void) { char *req_str = nullptr; @@ -380,7 +391,7 @@ static int MC_modelcheck_comm_determinism_main(void) 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 = simgrid::mc::request_get_dot_output(req, value); @@ -441,7 +452,7 @@ static int MC_modelcheck_comm_determinism_main(void) else XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack)); - if (!initial_global_state->initial_communications_pattern_done) + if (!initial_global_state->initial_communications_pattern_done) initial_global_state->initial_communications_pattern_done = 1; /* Trash the current state, no longer needed */ @@ -480,7 +491,7 @@ static int MC_modelcheck_comm_determinism_main(void) return SIMGRID_MC_EXIT_SUCCESS; } -int MC_modelcheck_comm_determinism(void) +int CommunicationDeterminismChecker::run() { XBT_INFO("Check communication determinism"); mc_model_checker->wait_for_requests(); @@ -492,7 +503,7 @@ int MC_modelcheck_comm_determinism(void) /* Create exploration stack */ mc_stack = xbt_fifo_new(); - MC_pre_modelcheck_comm_determinism(); + this->prepare(); initial_global_state = xbt_new0(s_mc_global_t, 1); initial_global_state->snapshot = simgrid::mc::take_snapshot(0); @@ -502,7 +513,8 @@ int MC_modelcheck_comm_determinism(void) initial_global_state->recv_diff = nullptr; initial_global_state->send_diff = nullptr; - return MC_modelcheck_comm_determinism_main(); + return this->main(); } } +} \ No newline at end of file diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp new file mode 100644 index 0000000000..d23c95c42f --- /dev/null +++ b/src/mc/CommunicationDeterminismChecker.hpp @@ -0,0 +1,29 @@ +/* Copyright (c) 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. */ + +#include "src/mc/mc_forward.hpp" +#include "src/mc/Checker.hpp" + +#ifndef SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP +#define SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP + +namespace simgrid { +namespace mc { + +class CommunicationDeterminismChecker : public Checker { +public: + CommunicationDeterminismChecker(Session& session); + ~CommunicationDeterminismChecker(); + int run() override; +private: + void prepare(); + int main(); +}; + +#endif + +} +} diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h index 83c386a4c8..926e9337b9 100644 --- a/src/mc/mc_comm_pattern.h +++ b/src/mc/mc_comm_pattern.h @@ -90,7 +90,6 @@ XBT_PRIVATE void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_ XBT_PRIVATE void MC_comm_pattern_free_voidp(void *p); XBT_PRIVATE void MC_list_comm_pattern_free_voidp(void *p); XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking); -int MC_modelcheck_comm_determinism(void); XBT_PRIVATE void MC_restore_communications_pattern(mc_state_t state); diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index ac45108e7d..949ed65cd0 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -28,6 +28,7 @@ #include "src/mc/mc_exit.h" #include "src/mc/Session.hpp" #include "src/mc/Checker.hpp" +#include "src/mc/CommunicationDeterminismChecker.hpp" #include "src/mc/SafetyChecker.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); @@ -49,8 +50,8 @@ std::unique_ptr createChecker(simgrid::mc::Session& sessio std::function code; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - code = [](Session& session) { - return MC_modelcheck_comm_determinism(); }; + return std::unique_ptr( + new simgrid::mc::CommunicationDeterminismChecker(session)); else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') return std::unique_ptr( new simgrid::mc::SafetyChecker(session)); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index ca3b2bedc4..9b9dc68f93 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -554,6 +554,8 @@ set(MC_SRC src/mc/Checker.hpp src/mc/Client.cpp src/mc/Client.hpp + src/mc/CommunicationDeterminismChecker.cpp + src/mc/CommunicationDeterminismChecker.hpp src/mc/Frame.hpp src/mc/Frame.cpp src/mc/ModelChecker.hpp @@ -585,7 +587,6 @@ set(MC_SRC src/mc/mc_page_snapshot.cpp src/mc/mc_comm_pattern.h src/mc/mc_comm_pattern.cpp - src/mc/mc_comm_determinism.cpp src/mc/mc_compare.cpp src/mc/mc_diff.cpp src/mc/mc_dwarf.hpp -- 2.20.1