initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
}
-void Session::execute(Transition const& transition)
+void Session::execute(Transition const& transition) const
{
model_checker_->handle_simcall(transition);
model_checker_->wait_for_requests();
}
-void Session::restore_initial_state()
+void Session::restore_initial_state() const
{
this->initial_snapshot_->restore(&model_checker_->get_remote_simulation());
}
-void Session::log_state()
+void Session::log_state() const
{
model_checker_->getChecker()->log_state();
}
}
-bool Session::actor_is_enabled(aid_t pid)
+bool Session::actor_is_enabled(aid_t pid) const
{
s_mc_message_actor_enabled_t msg{MC_MESSAGE_ACTOR_ENABLED, pid};
model_checker_->channel().send(msg);
void close();
void initialize();
- void execute(Transition const& transition);
- void log_state();
+ void execute(Transition const& transition) const;
+ void log_state() const;
- void restore_initial_state();
- bool actor_is_enabled(aid_t pid);
+ void restore_initial_state() const;
+ bool actor_is_enabled(aid_t pid) const;
};
// Temporary :)
Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
{}
-std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values()
+std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values() const
{
std::vector<int> values;
unsigned int cursor = 0;
void log_state() override;
private:
- std::shared_ptr<const std::vector<int>> get_proposition_values();
+ std::shared_ptr<const std::vector<int>> get_proposition_values() const;
std::shared_ptr<VisitedPair> insert_acceptance_pair(Pair* pair);
int insert_visited_pair(std::shared_ptr<VisitedPair> visited_pair, Pair* pair);
void show_acceptance_cycle(std::size_t depth);
{
state_ = (state_ << 5) + state_ + x;
}
- hash_type value()
- {
- return state_;
- }
+ hash_type value() const { return state_; }
};
}
namespace mc {
struct DerefAndCompareByActorsCountAndUsedHeap {
- template <class X, class Y> bool operator()(X const& a, Y const& b)
+ template <class X, class Y> bool operator()(X const& a, Y const& b) const
{
return std::make_pair(a->actors_count, a->heap_bytes_used) < std::make_pair(b->actors_count, b->heap_bytes_used);
}
return instance_.get();
}
-void AppSide::handle_deadlock_check(const s_mc_message_t*)
+void AppSide::handle_deadlock_check(const s_mc_message_t*) const
{
bool deadlock = false;
if (not simix_global->process_list.empty()) {
s_mc_message_int_t answer{MC_MESSAGE_DEADLOCK_CHECK_REPLY, deadlock};
xbt_assert(channel_.send(answer) == 0, "Could not send response");
}
-void AppSide::handle_continue(const s_mc_message_t*)
+void AppSide::handle_continue(const s_mc_message_t*) const
{
/* Nothing to do */
}
-void AppSide::handle_simcall(const s_mc_message_simcall_handle_t* message)
+void AppSide::handle_simcall(const s_mc_message_simcall_handle_t* message) const
{
smx_actor_t process = SIMIX_process_from_PID(message->pid);
xbt_assert(process != nullptr, "Invalid pid %lu", message->pid);
xbt_die("Could not send MESSAGE_WAITING to model-checker");
}
-void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg)
+void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const
{
bool res = simgrid::mc::actor_is_enabled(SIMIX_process_from_PID(msg->aid));
s_mc_message_int_t answer{MC_MESSAGE_ACTOR_ENABLED_REPLY, res};
this->handle_messages();
}
-void AppSide::ignore_memory(void* addr, std::size_t size)
+void AppSide::ignore_memory(void* addr, std::size_t size) const
{
s_mc_message_ignore_memory_t message;
message.type = MC_MESSAGE_IGNORE_MEMORY;
xbt_die("Could not send IGNORE_MEMORY message to model-checker");
}
-void AppSide::ignore_heap(void* address, std::size_t size)
+void AppSide::ignore_heap(void* address, std::size_t size) const
{
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
xbt_die("Could not send ignored region to MCer");
}
-void AppSide::unignore_heap(void* address, std::size_t size)
+void AppSide::unignore_heap(void* address, std::size_t size) const
{
s_mc_message_ignore_memory_t message;
message.type = MC_MESSAGE_UNIGNORE_HEAP;
xbt_die("Could not send IGNORE_HEAP message to model-checker");
}
-void AppSide::declare_symbol(const char* name, int* value)
+void AppSide::declare_symbol(const char* name, int* value) const
{
s_mc_message_register_symbol_t message;
message.type = MC_MESSAGE_REGISTER_SYMBOL;
xbt_die("Could send REGISTER_SYMBOL message to model-checker");
}
-void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context)
+void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
{
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
void handle_messages();
private:
- void handle_deadlock_check(const s_mc_message_t* msg);
- void handle_continue(const s_mc_message_t* msg);
- void handle_simcall(const s_mc_message_simcall_handle_t* message);
- void handle_actor_enabled(const s_mc_message_actor_enabled_t* msg);
+ void handle_deadlock_check(const s_mc_message_t* msg) const;
+ void handle_continue(const s_mc_message_t* msg) const;
+ void handle_simcall(const s_mc_message_simcall_handle_t* message) const;
+ void handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const;
public:
Channel const& get_channel() const { return channel_; }
Channel& get_channel() { return channel_; }
XBT_ATTRIB_NORETURN void main_loop();
void report_assertion_failure();
- void ignore_memory(void* addr, std::size_t size);
- void ignore_heap(void* addr, std::size_t size);
- void unignore_heap(void* addr, std::size_t size);
- void declare_symbol(const char* name, int* value);
+ void ignore_memory(void* addr, std::size_t size) const;
+ void ignore_heap(void* addr, std::size_t size) const;
+ void unignore_heap(void* addr, std::size_t size) const;
+ void declare_symbol(const char* name, int* value) const;
#if HAVE_UCONTEXT_H
- void declare_stack(void* stack, size_t size, ucontext_t* context);
+ void declare_stack(void* stack, size_t size, ucontext_t* context) const;
#endif
// Singleton :/
* @param len data size
* @param address target process memory address (target)
*/
-void RemoteSimulation::write_bytes(const void* buffer, size_t len, RemotePtr<void> address)
+void RemoteSimulation::write_bytes(const void* buffer, size_t len, RemotePtr<void> address) const
{
if (pwrite_whole(this->memory_file, buffer, len, (size_t)address.address()) < 0)
xbt_die("Write to process %lli failed", (long long)this->pid_);
}
-void RemoteSimulation::clear_bytes(RemotePtr<void> address, size_t len)
+void RemoteSimulation::clear_bytes(RemotePtr<void> address, size_t len) const
{
pthread_once(&zero_buffer_flag, zero_buffer_init);
while (len) {
}
}
-void RemoteSimulation::ignore_local_variable(const char* var_name, const char* frame_name)
+void RemoteSimulation::ignore_local_variable(const char* var_name, const char* frame_name) const
{
if (frame_name != nullptr && strcmp(frame_name, "*") == 0)
frame_name = nullptr;
return smx_dead_actors_infos;
}
-void RemoteSimulation::dump_stack()
+void RemoteSimulation::dump_stack() const
{
unw_addr_space_t as = unw_create_addr_space(&_UPT_accessors, BYTE_ORDER);
if (as == nullptr) {
using AddressSpace::read_string;
// Write memory:
- void write_bytes(const void* buffer, size_t len, RemotePtr<void> address);
- void clear_bytes(RemotePtr<void> address, size_t len);
+ void write_bytes(const void* buffer, size_t len, RemotePtr<void> address) const;
+ void clear_bytes(RemotePtr<void> address, size_t len) const;
// Debug information:
std::shared_ptr<ObjectInformation> find_object_info(RemotePtr<void> addr) const;
void terminate() { running_ = false; }
- void ignore_global_variable(const char* name)
+ void ignore_global_variable(const char* name) const
{
for (std::shared_ptr<ObjectInformation> const& info : this->object_infos)
info->remove_global_variable(name);
void ignore_heap(IgnoredHeapRegion const& region);
void unignore_heap(void* address, size_t size);
- void ignore_local_variable(const char* var_name, const char* frame_name);
+ void ignore_local_variable(const char* var_name, const char* frame_name) const;
std::vector<ActorInformation>& actors();
std::vector<ActorInformation>& dead_actors();
return nullptr;
}
- void dump_stack();
+ void dump_stack() const;
private:
void init_memory_map_info();
// Debug/test methods
/** @brief Get the number of references for a page */
- std::size_t get_ref(std::size_t pageno);
+ std::size_t get_ref(std::size_t pageno) const;
/** @brief Get the number of used pages */
- std::size_t size();
+ std::size_t size() const;
/** @brief Get the capacity of the page store
*
* The capacity is expanded by a system call (mremap).
* */
- std::size_t capacity();
+ std::size_t capacity() const;
};
XBT_ALWAYS_INLINE void PageStore::unref_page(std::size_t pageno)
return (void*)simgrid::mc::mmu::join(pageno, (std::uintptr_t)this->memory_);
}
-XBT_ALWAYS_INLINE std::size_t PageStore::get_ref(std::size_t pageno)
+XBT_ALWAYS_INLINE std::size_t PageStore::get_ref(std::size_t pageno) const
{
return this->page_counts_[pageno];
}
-XBT_ALWAYS_INLINE std::size_t PageStore::size()
+XBT_ALWAYS_INLINE std::size_t PageStore::size() const
{
return this->top_index_ - this->free_pages_.size();
}
-XBT_ALWAYS_INLINE std::size_t PageStore::capacity()
+XBT_ALWAYS_INLINE std::size_t PageStore::capacity() const
{
return this->capacity_;
}
*
* @param region Target region
*/
-void Region::restore()
+void Region::restore() const
{
xbt_assert(((start().address()) & (xbt_pagesize - 1)) == 0, "Not at the beginning of a page");
xbt_assert(simgrid::mc::mmu::chunk_count(size()) == get_chunks().page_count());
bool contain(RemotePtr<void> p) const { return p >= start() && p < end(); }
/** @brief Restore a region from a snapshot */
- void restore();
+ void restore() const;
/** @brief Read memory that was snapshotted in this region
*
return get_region(addr);
}
-void Snapshot::restore(RemoteSimulation* process)
+void Snapshot::restore(RemoteSimulation* process) const
{
XBT_DEBUG("Restore snapshot %i", num_state_);
ReadOptions options = ReadOptions::none()) const override;
Region* get_region(const void* addr) const;
Region* get_region(const void* addr, Region* hinted_region) const;
- void restore(RemoteSimulation* get_remote_simulation);
+ void restore(RemoteSimulation* get_remote_simulation) const;
// To be private
int num_state_;