From e717aac07363de43fcc74fa033767bb3c4acd25c Mon Sep 17 00:00:00 2001 From: Ehsan Azimi Date: Mon, 16 Nov 2020 18:40:34 +0100 Subject: [PATCH] get_maxpid() and take_snapshot() in mc_api --- src/mc/mc_api.cpp | 16 +++++++++++----- src/mc/mc_api.hpp | 3 ++- src/mc/mc_state.cpp | 10 ++++++---- 3 files changed, 19 insertions(+), 10 deletions(-) diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index e4b98cd39c..8e61bbe0e2 100644 --- a/src/mc/mc_api.cpp +++ b/src/mc/mc_api.cpp @@ -37,6 +37,11 @@ bool mc_api::actor_is_enabled(aid_t pid) const return session->actor_is_enabled(pid); } +unsigned long mc_api::get_maxpid() const +{ + return MC_smx_get_maxpid(); +} + void mc_api::s_initialize() const { session->initialize(); @@ -118,11 +123,6 @@ std::string const& mc_api::mc_get_host_name(std::string const& hostname) const return mc_model_checker->get_host_name(hostname); } -PageStore& mc_api::mc_page_store() const -{ - return mc_model_checker->page_store(); -} - void mc_api::mc_dump_record_path() const { simgrid::mc::dumpRecordPath(); @@ -158,6 +158,12 @@ bool mc_api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const return simgrid::mc::snapshot_equal(s1, s2); } +simgrid::mc::Snapshot* mc_api::take_snapshot(int num_state) const +{ + auto snapshot = new simgrid::mc::Snapshot(num_state); + return snapshot; +} + void mc_api::s_close() const { session->close(); diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp index be1f107286..4bfc92b6c0 100644 --- a/src/mc/mc_api.hpp +++ b/src/mc/mc_api.hpp @@ -41,6 +41,7 @@ public: // ACTOR FUNCTIONS std::vector& get_actors() const; bool actor_is_enabled(aid_t pid) const; + unsigned long get_maxpid() const; // MODEL_CHECKER FUNCTIONS ModelChecker* get_model_checker() const; @@ -58,7 +59,6 @@ public: void mc_wait_for_requests() const; void mc_exit(int status) const; std::string const& mc_get_host_name(std::string const& hostname) const; - PageStore& mc_page_store() const; void mc_dump_record_path() const; smx_simcall_t mc_state_choose_request(simgrid::mc::State* state) const; @@ -70,6 +70,7 @@ public: // SNAPSHOT FUNCTIONS bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const; + simgrid::mc::Snapshot* take_snapshot(int num_state) const; // SESSION FUNCTIONS void s_initialize() const; diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index d5e0c204c0..72627c263c 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -7,11 +7,12 @@ #include "src/mc/mc_comm_pattern.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_request.hpp" -#include "src/mc/mc_smx.hpp" +#include "src/mc/mc_api.hpp" #include using simgrid::mc::remote; +using mcapi = simgrid::mc::mc_api; namespace simgrid { namespace mc { @@ -19,11 +20,12 @@ namespace mc { State::State(unsigned long state_number) : num_(state_number) { this->internal_comm_.clear(); - - actor_states_.resize(MC_smx_get_maxpid()); + auto maxpid = mcapi::get().get_maxpid(); + actor_states_.resize(maxpid); /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (state_number % _sg_mc_checkpoint == 0)) || _sg_mc_termination) { - system_state_ = std::make_shared(num_); + auto snapshot_ptr = mcapi::get().take_snapshot(num_); + system_state_ = std::shared_ptr(snapshot_ptr); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { MC_state_copy_incomplete_communications_pattern(this); MC_state_copy_index_communications_pattern(this); -- 2.20.1