It was broken (TODO) since the switch to split-process MC.
#include <cassert>
+#include "simgrid/sg_config.h" // sg_cfg_get_boolean
+
#include "ModelChecker.hpp"
#include "PageStore.hpp"
process_(pid, socket),
parent_snapshot_(nullptr)
{
+ // TODO, avoid direct dependency on sg_cfg
+ process_.privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
}
ModelChecker::~ModelChecker()
return this->flags & simgrid::mc::ObjectInformation::Executable;
}
- bool privatized() const
- {
-#ifdef HAVE_SMPI
- return this->executable() && smpi_privatize_global_variables;
-#else
- return false;
-#endif
- }
-
void* base_address() const;
simgrid::mc::Frame* find_function(const void *ip) const;
process->init_memory_map_info();
process->clear_refs_fd_ = -1;
process->pagemap_fd_ = -1;
+ process->privatized_ = false;
int fd = open_vm(process->pid_, O_RDWR);
if (fd<0)
this->find_object_info_rw((void*)address.address());
// Segment overlap is not handled.
#ifdef HAVE_SMPI
- if (info.get() && info.get()->privatized()) {
+ if (info.get() && this->privatized(*info)) {
if (process_index < 0)
xbt_die("Missing process index");
if (process_index >= (int) MC_smpi_process_count())
#include "AddressSpace.hpp"
#include "mc_protocol.h"
+#include "ObjectInformation.hpp"
+
// Those flags are used to track down which cached information
// is still up to date and which information needs to be updated.
typedef int mc_process_cache_flags_t;
void reset_soft_dirty();
void read_pagemap(uint64_t* pagemap, size_t start_page, size_t page_count);
+ bool privatized(ObjectInformation const& info) const
+ {
+ return privatized_ && info.executable();
+ }
+ bool privatized() const
+ {
+ return privatized_;
+ }
+ void privatized(bool privatized) { privatized_ = privatized; }
+
private:
void init_memory_map_info();
void refresh_heap();
std::vector<IgnoredRegion> ignored_regions_;
int clear_refs_fd_;
int pagemap_fd_;
+ bool privatized_;
public: // object info
// TODO, make private (first, objectify simgrid::mc::ObjectInformation*)
std::vector<std::shared_ptr<simgrid::mc::ObjectInformation>> object_infos;
simgrid::mc::RegionSnapshot region;
#ifdef HAVE_SMPI
- const bool privatization_aware = object_info && object_info->privatized();
+ const bool privatization_aware = object_info
+ && mc_model_checker->process().privatized(*object_info);
if (privatization_aware && MC_smpi_process_count())
region = simgrid::mc::privatized_region(
type, start_addr, permanent_addr, size, ref_region);
process->get_malloc_info());
#ifdef HAVE_SMPI
- if (smpi_privatize_global_variables && MC_smpi_process_count()) {
+ if (mc_model_checker->process().privatized() && MC_smpi_process_count()) {
// snapshot->privatization_index = smpi_loaded_page
mc_model_checker->process().read_variable(
"smpi_loaded_page", &snapshot->privatization_index,
#ifdef HAVE_SMPI
// TODO, send a message to implement this in the MCed process
if(snapshot->privatization_index >= 0) {
- // We just rewrote the global variables.
- // The privatisation segment SMPI thinks
- // is mapped might be inconsistent with the segment which
- // is really mapped in memory (kernel state).
- // We ask politely SMPI to map the segment anyway,
- // even if it thinks it is the current one:
- smpi_really_switch_data_segment(snapshot->privatization_index);
+ // Fix the privatization mmap:
+ s_mc_restore_message message;
+ message.type = MC_MESSAGE_RESTORE;
+ message.index = snapshot->privatization_index;
+ mc_model_checker->process().send_message(message);
}
#endif
}
}
break;
+ case MC_MESSAGE_RESTORE:
+ {
+ s_mc_restore_message_t message;
+ if (s != sizeof(message))
+ xbt_die("Unexpected size for SIMCALL_HANDLE");
+ memcpy(&message, message_buffer, sizeof(message));
+ smpi_really_switch_data_segment(message.index);
+ }
+ break;
+
default:
xbt_die("%s received unexpected message %s (%i)",
MC_mode_name(mc_mode),
#include <errno.h>
#include <string.h>
+#include <stdio.h> // perror
#include <sys/types.h>
#include <sys/socket.h>
MC_MESSAGE_WAITING,
MC_MESSAGE_SIMCALL_HANDLE,
MC_MESSAGE_ASSERTION_FAILED,
+ // MCer request to finish the restoration:
+ MC_MESSAGE_RESTORE,
} e_mc_message_type;
#define MC_MESSAGE_LENGTH 512
void* data;
} s_mc_register_symbol_message_t, * mc_register_symbol_message_t;
+typedef struct s_mc_restore_message {
+ e_mc_message_type type;
+ int index;
+} s_mc_restore_message_t, *mc_restore_message_t;
+
XBT_PRIVATE int MC_protocol_send(int socket, const void* message, size_t size);
XBT_PRIVATE int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
XBT_PRIVATE ssize_t MC_receive_message(int socket, void* message, size_t size, int options);