#include <simgrid/s4u.hpp>
XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
+namespace sg4 = simgrid::s4u;
static void server()
{
- const int* received1 = nullptr;
- const int* received2 = nullptr;
-
- received1 = simgrid::s4u::Mailbox::by_name("mymailbox")->get<int>();
+ auto received1 = sg4::Mailbox::by_name("mymailbox")->get_unique<int>();
long val1 = *received1;
- delete received1;
- received2 = simgrid::s4u::Mailbox::by_name("mymailbox")->get<int>();
+ auto received2 = sg4::Mailbox::by_name("mymailbox")->get_unique<int>();
long val2 = *received2;
- delete received2;
XBT_INFO("First pair received: %ld %ld", val1, val2);
MC_assert(std::min(val1, val2) == 1); // if the two messages of the second client arrive first, this is violated.
- received1 = simgrid::s4u::Mailbox::by_name("mymailbox")->get<int>();
+ received1 = sg4::Mailbox::by_name("mymailbox")->get_unique<int>();
val1 = *received1;
- delete received1;
- received2 = simgrid::s4u::Mailbox::by_name("mymailbox")->get<int>();
+ received2 = sg4::Mailbox::by_name("mymailbox")->get_unique<int>();
val2 = *received2;
- delete received2;
XBT_INFO("Second pair received: %ld %ld", val1, val2);
}
auto* payload1 = new int(id);
auto* payload2 = new int(id);
- simgrid::s4u::Mailbox::by_name("mymailbox")->put(payload1, 10000);
- simgrid::s4u::Mailbox::by_name("mymailbox")->put(payload2, 10000);
+ sg4::Mailbox::by_name("mymailbox")->put(payload1, 10000);
+ sg4::Mailbox::by_name("mymailbox")->put(payload2, 10000);
}
int main(int argc, char* argv[])
{
- simgrid::s4u::Engine e(&argc, argv);
+ sg4::Engine e(&argc, argv);
e.load_platform(argv[1]);
- simgrid::s4u::Actor::create("server", e.host_by_name("HostA"), server);
- simgrid::s4u::Actor::create("client", e.host_by_name("HostB"), client, 1);
- simgrid::s4u::Actor::create("client", e.host_by_name("HostC"), client, 2);
+ sg4::Actor::create("server", e.host_by_name("HostA"), server);
+ sg4::Actor::create("client", e.host_by_name("HostB"), client, 1);
+ sg4::Actor::create("client", e.host_by_name("HostC"), client, 2);
e.run();
return 0;
return simgrid::mc::snapshot_equal(s1, s2);
}
-simgrid::mc::Snapshot* Api::take_snapshot(int num_state) const
+simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
{
auto snapshot = new simgrid::mc::Snapshot(num_state);
return snapshot;
// SNAPSHOT APIs
bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const;
- simgrid::mc::Snapshot* take_snapshot(int num_state) const;
+ simgrid::mc::Snapshot* take_snapshot(long num_state) const;
// SESSION APIs
void s_close() const;
{
std::vector<ActorInformation>& actors = mc_model_checker->get_remote_process().actors();
- kernel::actor::ActorImpl* actor = actors[next].copy.get_buffer();
+ const kernel::actor::ActorImpl* actor = actors[next].copy.get_buffer();
aid_t aid = actor->get_pid();
int times_considered;
unsigned long Transition::executed_transitions_ = 0;
unsigned long Transition::replayed_transitions_ = 0;
-Transition::~Transition() {
-} // Make sure that we have a vtable for Transition by putting this virtual function out of the header
+// Do not move this to the header, to ensure that we have a vtable for Transition
+Transition::~Transition() = default;
-std::string Transition::to_string(bool verbose)
+std::string Transition::to_string(bool)
{
return textual_;
}
const char* Transition::to_cstring(bool verbose)
{
- to_string();
+ to_string(verbose);
return textual_.c_str();
}
void Transition::replay() const
const RemoteProcess& process = mc_model_checker->get_remote_process();
if (s1->hash_ != s2->hash_) {
- XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
+ XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
s2->hash_);
return false;
}
- XBT_VERB("(%d - %d) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_);
+ XBT_VERB("(%ld - %ld) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_);
/* Compare enabled processes */
if (s1->enabled_processes_ != s2->enabled_processes_) {
- XBT_VERB("(%d - %d) Different amount of enabled processes", s1->num_state_, s2->num_state_);
+ XBT_VERB("(%ld - %ld) Different amount of enabled processes", s1->num_state_, s2->num_state_);
return false;
}
size_t size_used1 = s1->stack_sizes_[i];
size_t size_used2 = s2->stack_sizes_[i];
if (size_used1 != size_used2) {
- XBT_VERB("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1,
+ XBT_VERB("(%ld - %ld) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1,
size_used2);
return false;
}
const s_xbt_mheap_t* heap2 = static_cast<xbt_mheap_t>(
s2->read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy()));
if (state_comparator.initHeapInformation(heap1, heap2, s1->to_ignore_, s2->to_ignore_) == -1) {
- XBT_VERB("(%d - %d) Different heap information", s1->num_state_, s2->num_state_);
+ XBT_VERB("(%ld - %ld) Different heap information", s1->num_state_, s2->num_state_);
return false;
}
const_mc_snapshot_stack_t stack2 = &s2->stacks_[cursor];
if (local_variables_differ(process, state_comparator, *s1, *s2, stack1, stack2)) {
- XBT_VERB("(%d - %d) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1);
+ XBT_VERB("(%ld - %ld) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1);
return false;
}
}
/* Compare global variables */
if (global_variables_differ(process, state_comparator, region1->object_info(), region1, region2, *s1, *s2)) {
std::string const& name = region1->object_info()->file_name;
- XBT_VERB("(%d - %d) Different global variables in %s", s1->num_state_, s2->num_state_, name.c_str());
+ XBT_VERB("(%ld - %ld) Different global variables in %s", s1->num_state_, s2->num_state_, name.c_str());
return false;
}
}
/* Compare heap */
if (mmalloc_heap_differ(process, state_comparator, *s1, *s2)) {
- XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_);
+ XBT_VERB("(%ld - %ld) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_);
return false;
}
- XBT_VERB("(%d - %d) No difference found", s1->num_state_, s2->num_state_);
+ XBT_VERB("(%ld - %ld) No difference found", s1->num_state_, s2->num_state_);
return true;
}
hash_type hash(Snapshot const& snapshot)
{
- XBT_DEBUG("START hash %i", snapshot.num_state_);
+ XBT_DEBUG("START hash %ld", snapshot.num_state_);
djb_hash hash;
// TODO:
// * nb_processes
// * root variables
// * basic stack frame information
// * stack frame local variables
- XBT_DEBUG("END hash %i", snapshot.num_state_);
+ XBT_DEBUG("END hash %ld", snapshot.num_state_);
return hash.value();
}
remote(ignored_data.start));
}
-Snapshot::Snapshot(int num_state, RemoteProcess* process) : AddressSpace(process), num_state_(num_state)
+Snapshot::Snapshot(long num_state, RemoteProcess* process) : AddressSpace(process), num_state_(num_state)
{
- XBT_DEBUG("Taking snapshot %i", num_state);
+ XBT_DEBUG("Taking snapshot %ld", num_state);
for (auto const& p : process->actors())
enabled_processes_.insert(p.copy.get_buffer()->get_pid());
void Snapshot::restore(RemoteProcess* process) const
{
- XBT_DEBUG("Restore snapshot %i", num_state_);
+ XBT_DEBUG("Restore snapshot %ld", num_state_);
// Restore regions
for (std::unique_ptr<Region> const& region : snapshot_regions_) {
class XBT_PRIVATE Snapshot final : public AddressSpace {
public:
/* Initialization */
- Snapshot(int num_state, RemoteProcess* process = &mc_model_checker->get_remote_process());
+ Snapshot(long num_state, RemoteProcess* process = &mc_model_checker->get_remote_process());
/* Regular use */
bool on_heap(const void* address) const
void restore(RemoteProcess* process) const;
// To be private
- int num_state_;
+ long num_state_;
std::size_t heap_bytes_used_ = 0;
std::vector<std::unique_ptr<Region>> snapshot_regions_;
std::set<pid_t> enabled_processes_;