are fullfiled. If it cannot be started right away, it will start as soon as it becomes
possible.
- Allow to set a concurrency limit on disks and hosts, as it was already the case for links.
+ - Rename Link::get_usage() to Link::get_load() for consistency with Host::
New plugin: Operation
- Operations are designed to represent workflows, i.e, graphs of repeatable Activities.
add_dependencies(tests-mc s4u-mc-bugged1-liveness-cleaner-off)
endif()
+ ADD_TESH(s4u-mc-synchro-mutex-stateful
+ --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/synchro-mutex
+ --setenv libdir=${CMAKE_BINARY_DIR}/lib
+ --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
+ --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/synchro-mutex
+ --cd ${CMAKE_CURRENT_SOURCE_DIR}/synchro-mutex
+ ${CMAKE_HOME_DIRECTORY}/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh)
+
# Model-checking liveness
if(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64)
# liveness model-checking works only on 64bits (for now ...)
--- /dev/null
+#!/usr/bin/env tesh
+
+p This file tests the cfg=model-check/checkpoint option for DFS explorer
+
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/checkpoint:5 --cfg=model-check/sleep-set:true -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/checkpoint' to '5'
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '2'
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 130 unique states visited; 27 backtracks (209 transition replays, 52 states visited overall)
+
+p The stats without checkpoints is: 130 unique states visited; 27 backtracks (308 transition replays, 151 states visited overall)
+p But it runs much faster (0.6 sec vs. 1.6 sec), damn slow checkpointing code.
void set_host_wifi_rate(const s4u::Host* host, int level) const;
/** @brief Returns the current load (in bytes per second) */
- double get_usage() const;
+ double get_load() const;
+
+#ifndef DOXYGEN
+ XBT_ATTRIB_DEPRECATED_v337("Please use get_load() instead") double get_usage() const
+ {
+ return get_load();
+ }
+#endif
/** @brief Check if the Link is used (at least one flow uses the link) */
bool is_used() const;
* If the resource is not shared (ie in FATPIPE mode), then the load is the max (not the sum)
* of all resource usages located on this resource.
*/
-double Constraint::get_usage() const
+double Constraint::get_load() const
{
double result = 0.0;
if (sharing_policy_ != SharingPolicy::FATPIPE) {
/** @brief Check how a constraint is shared */
SharingPolicy get_sharing_policy() const { return sharing_policy_; }
- /** @brief Get the usage of the constraint after the last lmm solve */
- double get_usage() const;
+ /** @brief Get the load of the constraint after the last lmm solve */
+ double get_load() const;
/** @brief Sets the concurrency limit for this constraint */
void set_concurrency_limit(int limit)
/** @brief returns the current load due to activities (in flops per second, byte per second or similar)
*
* The load due to external usages modeled by profile files is ignored.*/
- virtual double get_load() const { return constraint_->get_usage(); }
+ virtual double get_load() const { return constraint_->get_load(); }
bool is_used() const override { return model_->get_maxmin_system()->constraint_used(constraint_); }
};
RecordTrace DFSExplorer::get_record_trace() // override
{
RecordTrace res;
- for (auto const& transition : stack_.back()->get_recipe())
- res.push_back(transition);
- res.push_back(stack_.back()->get_transition_out().get());
- return res;
-}
-std::vector<std::string> DFSExplorer::get_textual_trace() // override
-{
- std::vector<std::string> trace;
- for (auto const& transition : stack_.back()->get_recipe()) {
- trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str()));
- }
if (const auto trans = stack_.back()->get_transition_out(); trans != nullptr)
- trace.push_back(xbt::string_printf("%ld: %s", trans->aid_, trans->to_string().c_str()));
- return trace;
+ res.push_back(trans.get());
+ for (const auto* state = stack_.back().get(); state != nullptr; state = state->get_parent_state().get())
+ if (state->get_transition_in() != nullptr)
+ res.push_front(state->get_transition_in().get());
+
+ return res;
}
void DFSExplorer::restore_stack(std::shared_ptr<State> state)
}
#endif
+ // Search how to restore the backtracking point
+ State* init_state = nullptr;
+ std::deque<Transition*> replay_recipe;
+ for (auto* s = backtracking_point.get(); s != nullptr; s = s->get_parent_state().get()) {
+#if SIMGRID_HAVE_STATEFUL_MC
+ if (s->get_system_state() != nullptr) { // Found a state that I can restore
+ init_state = s;
+ break;
+ }
+#endif
+ if (s->get_transition_in() != nullptr) // The root has no transition_in
+ replay_recipe.push_front(s->get_transition_in().get());
+ }
+
+ // Restore the init_state, if any
+ if (init_state != nullptr) {
+#if SIMGRID_HAVE_STATEFUL_MC
+ const auto* system_state = init_state->get_system_state();
+ system_state->restore(*get_remote_app().get_remote_process_memory());
+ on_restore_system_state_signal(init_state, get_remote_app());
+#endif
+ } else { // Restore the initial state if no intermediate state was found
+ get_remote_app().restore_initial_state();
+ on_restore_initial_state_signal(get_remote_app());
+ }
+
/* if no snapshot, we need to restore the initial state and replay the transitions */
- get_remote_app().restore_initial_state();
- on_restore_initial_state_signal(get_remote_app());
/* Traverse the stack from the state at position start and re-execute the transitions */
- for (auto& state : backtracking_point->get_recipe()) {
- state->replay(get_remote_app());
- on_transition_replay_signal(state, get_remote_app());
+ for (auto& transition : replay_recipe) {
+ transition->replay(get_remote_app());
+ on_transition_replay_signal(transition, get_remote_app());
visited_states_count_++;
}
this->restore_stack(backtracking_point);
}
DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info)
- : Exploration(args, need_memory_info || _sg_mc_termination)
+ : Exploration(args, need_memory_info || _sg_mc_termination
+#if SIMGRID_HAVE_STATEFUL_MC
+ || _sg_mc_checkpoint > 0
+#endif
+ )
{
if (with_dpor)
reduction_mode_ = ReductionMode::dpor;
explicit DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info = false);
void run() override;
RecordTrace get_record_trace() override;
- std::vector<std::string> get_textual_trace() override;
void log_state() override;
/** Called once when the exploration starts */
#include "src/mc/mc_environ.h"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
+#include "xbt/string.hpp"
#if SIMGRID_HAVE_STATEFUL_MC
#include "src/mc/sosp/RemoteProcessMemory.hpp"
return strsignal(WTERMSIG(status));
}
}
+
+std::vector<std::string> Exploration::get_textual_trace()
+{
+ std::vector<std::string> trace;
+ for (auto const& transition : get_record_trace())
+ trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str()));
+ return trace;
+}
+
XBT_ATTRIB_NORETURN void Exploration::report_crash(int status)
{
XBT_INFO("**************************");
* to get and display information about the current state of the
* model-checking algorithm: */
- /** Show the current trace/stack
- *
- * Could this be handled in the Session/ModelChecker instead? */
+ /** Retrieve the current stack to build an execution trace */
virtual RecordTrace get_record_trace() = 0;
/** Generate a textual execution trace of the simulated application */
- virtual std::vector<std::string> get_textual_trace() = 0;
+ std::vector<std::string> get_textual_trace();
/** Log additional information about the state of the model-checker */
virtual void log_state();
{
RecordTrace res;
for (std::shared_ptr<Pair> const& pair : exploration_stack_)
- res.push_back(pair->app_state_->get_transition_out().get());
+ if (pair->app_state_->get_transition_out() != nullptr)
+ res.push_back(pair->app_state_->get_transition_out().get());
return res;
}
XBT_INFO("Counter-example depth: %zu", depth);
}
-std::vector<std::string> LivenessChecker::get_textual_trace() // override
-{
- std::vector<std::string> trace;
- for (std::shared_ptr<Pair> const& pair : exploration_stack_)
- if (pair->app_state_->get_transition_out() != nullptr)
- trace.push_back(pair->app_state_->get_transition_out()->to_string());
-
- return trace;
-}
-
std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state,
std::shared_ptr<const std::vector<int>> propositions)
{
void run() override;
RecordTrace get_record_trace() override;
- std::vector<std::string> get_textual_trace() override;
void log_state() override;
private:
return res;
}
-std::vector<std::string> UdporChecker::get_textual_trace()
-{
- std::vector<std::string> trace;
- for (auto const& state : state_stack) {
- const auto t = state->get_transition_out();
- trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
- }
- return trace;
-}
-
} // namespace simgrid::mc::udpor
namespace simgrid::mc {
void run() override;
RecordTrace get_record_trace() override;
- std::vector<std::string> get_textual_trace() override;
std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
private:
const auto& actor_list = engine->get_actor_list();
if (actor_list.empty()) {
XBT_INFO("The replay of the trace is complete. The application is terminating.");
- } else if (std::none_of(begin(actor_list), end(actor_list),
+ } else if (std::none_of(std::begin(actor_list), std::end(actor_list),
[](const auto& kv) { return mc::actor_is_enabled(kv.second); })) {
XBT_INFO("The replay of the trace is complete. DEADLOCK detected.");
engine->display_all_actor_status();
#include "src/mc/mc_forward.hpp"
#include "xbt/base.h"
+#include <deque>
#include <string>
-#include <vector>
namespace simgrid::mc {
class RecordTrace {
- std::vector<Transition*> transitions_;
+ std::deque<Transition*> transitions_;
public:
RecordTrace() = default;
/** Make a string representation that can later be used to create a new trace */
std::string to_string() const;
+ void push_front(Transition* t) { transitions_.push_front(t); }
void push_back(Transition* t) { transitions_.push_back(t); }
+ std::deque<Transition*>::const_iterator begin() const { return transitions_.begin(); }
+ std::deque<Transition*>::const_iterator end() const { return transitions_.end(); }
/** Replay all transitions of a trace */
void replay() const;
double power_slope = busy_ - idle_;
- double normalized_link_usage = link_->get_usage() / link_->get_bandwidth();
+ double normalized_link_usage = link_->get_load() / link_->get_bandwidth();
double dynamic_power = power_slope * normalized_link_usage;
return idle_ + dynamic_power;
* - if idle i.e. get_usage = 0, update P_{stat}
* P_{tot} = P_{dyn}+P_{stat}
*/
- if (link_->get_usage() != 0.0) {
+ if (link_->get_load() != 0.0) {
eDyn_ += /*duration * */ durUsage * ((host_count * pRx_) + pTx_);
eStat_ += (duration - durUsage) * pIdle_ * (host_count + 1);
XBT_DEBUG("eDyn += %f * ((%f * %f) + %f) | eDyn = %f (durusage =%f)", durUsage, host_count, pRx_, pTx_, eDyn_,
" Please track your link with sg_link_load_track before trying to access any of its load metrics.",
link_->get_cname());
- double current_instantaneous_bytes_per_second = link_->get_usage();
+ double current_instantaneous_bytes_per_second = link_->get_load();
double now = simgrid::s4u::Engine::get_clock();
// Update minimum/maximum observed values if needed
return this;
}
-double Link::get_usage() const
+double Link::get_load() const
{
- return this->pimpl_->get_constraint()->get_usage();
+ return this->pimpl_->get_constraint()->get_load();
}
void Link::turn_on()
