Session::Session(pid_t pid, int socket)
{
std::unique_ptr<simgrid::mc::RemoteClient> process(new simgrid::mc::RemoteClient(pid, socket));
+
#if HAVE_SMPI
- // TODO, automatic detection of the config from the process
- process->privatized(smpi_privatize_global_variables != SmpiPrivStrategies::NONE);
-#else
- process->privatized(false);
+ xbt_assert(smpi_privatize_global_variables != SmpiPrivStrategies::MMAP,
+ "Please use the dlopen privatization schema when model-checking SMPI code");
#endif
+
model_checker_.reset(new simgrid::mc::ModelChecker(std::move(process)));
xbt_assert(mc_model_checker == nullptr);
mc_model_checker = model_checker_.get();
{
xbt_assert(r1 && r2, "Missing region.");
-#if HAVE_SMPI
- if (r1->storage_type() == simgrid::mc::StorageType::Privatized) {
- xbt_assert(process_index >= 0);
- if (r2->storage_type() != simgrid::mc::StorageType::Privatized)
- return 1;
-
- size_t process_count = MC_smpi_process_count();
- xbt_assert(process_count == r1->privatized_data().size()
- && process_count == r2->privatized_data().size());
-
- // Compare the global variables separately for each simulates process:
- for (size_t i = 0; i < process_count; i++) {
- if (compare_global_variables(state, object_info, i, r1->privatized_data()[i].get(),
- r2->privatized_data()[i].get(), snapshot1, snapshot2))
- return 1;
- }
- return 0;
- }
-#else
- xbt_assert(r1->storage_type() != simgrid::mc::StorageType::Privatized);
-#endif
- xbt_assert(r2->storage_type() != simgrid::mc::StorageType::Privatized);
-
std::vector<simgrid::mc::Variable>& variables = object_info->global_variables;
for (simgrid::mc::Variable const& current_var : variables) {
if (channel_.send(MC_MESSAGE_WAITING))
xbt_die("Could not send MESSAGE_WAITING to model-checker");
}
-void Client::handleRestore(s_mc_message_restore_t* message)
-{
-#if HAVE_SMPI
- smpi_really_switch_data_segment(simgrid::s4u::Actor::by_pid(message->index));
-#endif
-}
+
void Client::handleActorEnabled(s_mc_message_actor_enabled_t* msg)
{
bool res = simgrid::mc::actor_is_enabled(SIMIX_process_from_PID(msg->aid));
handleSimcall((s_mc_message_simcall_handle_t*)message_buffer);
break;
- case MC_MESSAGE_RESTORE:
- xbt_assert(received_size == sizeof(s_mc_message_t), "Unexpected size for MESSAGE_RESTORE (%zd != %zu)",
- received_size, sizeof(s_mc_message_t));
- handleRestore((s_mc_message_restore_t*)message_buffer);
- break;
-
case MC_MESSAGE_ACTOR_ENABLED:
xbt_assert(received_size == sizeof(s_mc_message_actor_enabled_t),
"Unexpected size for ACTOR_ENABLED (%zd != %zu)", received_size,
void handleDeadlockCheck(s_mc_message_t* msg);
void handleContinue(s_mc_message_t* msg);
void handleSimcall(s_mc_message_simcall_handle_t* message);
- void handleRestore(s_mc_message_restore_t* msg);
void handleActorEnabled(s_mc_message_actor_enabled_t* msg);
public:
const void* RemoteClient::read_bytes(void* buffer, std::size_t size, RemotePtr<void> address, int process_index,
ReadOptions /*options*/) const
{
-#if HAVE_SMPI
- if (process_index != simgrid::mc::ProcessIndexDisabled) {
- std::shared_ptr<simgrid::mc::ObjectInformation> const& info = this->find_object_info_rw(address);
- // Segment overlap is not handled.
- if (info.get() && this->privatized(*info)) {
- if (process_index < 0)
- xbt_die("Missing process index");
- if (process_index >= (int)MC_smpi_process_count())
- xbt_die("Invalid process index");
-
- // Read smpi_privatization_regions from MCed:
- smpi_privatization_region_t remote_smpi_privatization_regions =
- mc_model_checker->process().read_variable<smpi_privatization_region_t>("smpi_privatization_regions");
-
- s_smpi_privatization_region_t privatization_region =
- mc_model_checker->process().read<s_smpi_privatization_region_t>(
- remote(remote_smpi_privatization_regions + process_index));
-
- // Address translation in the privatization segment:
- size_t offset = address.address() - (std::uint64_t)info->start_rw;
- address = remote((char*)privatization_region.address + offset);
- }
- }
-#endif
if (pread_whole(this->memory_file, buffer, size, (size_t)address.address()) < 0)
xbt_die("Read at %p from process %lli failed", (void*)address.address(), (long long)this->pid_);
return buffer;
void terminate() { running_ = false; }
- bool privatized(ObjectInformation const& info) const { return privatized_ && info.executable(); }
- bool privatized() const { return privatized_; }
- void privatized(bool privatized) { privatized_ = privatized; }
-
void ignore_global_variable(const char* name)
{
for (std::shared_ptr<simgrid::mc::ObjectInformation> const& info : this->object_infos)
RemotePtr<void> maestro_stack_end_;
int memory_file = -1;
std::vector<IgnoredRegion> ignored_regions_;
- bool privatized_ = false;
std::vector<s_stack_region_t> stack_areas_;
std::vector<IgnoredHeapRegion> ignored_heap_;
MC_MESSAGE_WAITING,
MC_MESSAGE_SIMCALL_HANDLE,
MC_MESSAGE_ASSERTION_FAILED,
- // MCer request to finish the restoration:
- MC_MESSAGE_RESTORE,
MC_MESSAGE_ACTOR_ENABLED,
MC_MESSAGE_ACTOR_ENABLED_REPLY
};
storage_type_ = StorageType::Flat;
page_numbers_.clear();
- privatized_regions_.clear();
XBT_DEBUG("New region : type : %s, data : %p (real addr %p), size : %zu",
(region_type == RegionType::Heap ? "Heap" : (region_type == RegionType::Data ? "Data" : "?")),
storage_type_ = StorageType::Chunked;
flat_data_.clear();
- privatized_regions_.clear();
page_numbers_ =
ChunkedData(mc_model_checker->page_store(), *process, RemotePtr<void>(permanent_addr), mmu::chunk_count(size));
}
-#if HAVE_SMPI
-RegionPrivatized::RegionPrivatized(RegionType region_type, void* start_addr, void* permanent_addr, std::size_t size)
- : RegionSnapshot(region_type, start_addr, permanent_addr, size)
-{
- storage_type_ = StorageType::Privatized;
-
- size_t process_count = MC_smpi_process_count();
-
- // Read smpi_privatization_regions from MCed:
- smpi_privatization_region_t remote_smpi_privatization_regions;
- mc_model_checker->process().read_variable("smpi_privatization_regions", &remote_smpi_privatization_regions,
- sizeof(remote_smpi_privatization_regions));
- s_smpi_privatization_region_t privatization_regions[process_count];
- mc_model_checker->process().read_bytes(&privatization_regions, sizeof(privatization_regions),
- remote(remote_smpi_privatization_regions));
-
- privatized_regions_.reserve(process_count);
- for (size_t i = 0; i < process_count; i++)
- privatized_regions_.push_back(std::unique_ptr<simgrid::mc::RegionSnapshot>(
- region(region_type, start_addr, privatization_regions[i].address, size)));
-
- flat_data_.clear();
- page_numbers_.clear();
-}
-#endif
-
/** @brief Restore a region from a snapshot
*
* @param region Target region
break;
- case simgrid::mc::StorageType::Privatized:
- for (auto& p : privatized_data())
- p.get()->restore();
- break;
-
default: // includes StorageType::NoData
xbt_die("Storage type not supported");
break;
enum class RegionType { Unknown = 0, Heap = 1, Data = 2 };
-enum class StorageType { NoData = 0, Flat = 1, Chunked = 2, Privatized = 3 };
+enum class StorageType { NoData = 0, Flat = 1, Chunked = 2 };
class Buffer {
private:
Buffer flat_data_;
ChunkedData page_numbers_;
- std::vector<std::unique_ptr<RegionSnapshot>> privatized_regions_;
public:
RegionSnapshot() {}
, permanent_addr_(that.permanent_addr_)
, flat_data_(std::move(that.flat_data_))
, page_numbers_(std::move(that.page_numbers_))
- , privatized_regions_(std::move(that.privatized_regions_))
{
that.clear();
}
permanent_addr_ = that.permanent_addr_;
flat_data_ = std::move(that.flat_data_);
page_numbers_ = std::move(that.page_numbers_);
- privatized_regions_ = std::move(that.privatized_regions_);
that.clear();
return *this;
}
{
region_type_ = UnknownRegion;
storage_type_ = StorageType::NoData;
- privatized_regions_.clear();
page_numbers_.clear();
flat_data_.clear();
object_info_ = nullptr;
storage_type_ = StorageType::NoData;
flat_data_.clear();
page_numbers_.clear();
- privatized_regions_.clear();
}
const Buffer& flat_data() const { return flat_data_; }
ChunkedData const& page_data() const { return page_numbers_; }
- std::vector<std::unique_ptr<RegionSnapshot>> const& privatized_data() const { return privatized_regions_; }
- std::vector<std::unique_ptr<RegionSnapshot>>& privatized_data() { return privatized_regions_; }
-
simgrid::mc::ObjectInformation* object_info() const { return object_info_; }
void object_info(simgrid::mc::ObjectInformation* info) { object_info_ = info; }
public:
RegionSparse(RegionType type, void* start_addr, void* data_addr, std::size_t size);
};
-class RegionPrivatized : public RegionSnapshot {
-public:
- RegionPrivatized(RegionType type, void* start_addr, void* data_addr, std::size_t size);
-};
RegionSnapshot* region(RegionType type, void* start_addr, void* data_addr, std::size_t size);
add_region(simgrid::mc::RegionType::Heap, nullptr, start_heap, start_heap, (char*)end_heap - (char*)start_heap);
heap_bytes_used_ = mmalloc_get_bytes_used_remote(heap->heaplimit, process->get_malloc_info());
privatization_index_ = simgrid::mc::ProcessIndexMissing;
-
-#if HAVE_SMPI
- 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", &privatization_index_, sizeof(privatization_index_));
-#endif
}
/** @brief Checks whether the variable is in scope for a given IP.
else if (type == simgrid::mc::RegionType::Heap)
xbt_assert(not object_info, "Unexpected object info for heap region.");
- simgrid::mc::RegionSnapshot* region;
-#if HAVE_SMPI
- const bool privatization_aware = object_info && mc_model_checker->process().privatized(*object_info);
- if (privatization_aware && MC_smpi_process_count())
- region = new RegionPrivatized(type, start_addr, permanent_addr, size);
- else
-#endif
- region = simgrid::mc::region(type, start_addr, permanent_addr, size);
-
+ simgrid::mc::RegionSnapshot* region = simgrid::mc::region(type, start_addr, permanent_addr, size);
region->object_info(object_info);
snapshot_regions_.push_back(std::unique_ptr<simgrid::mc::RegionSnapshot>(std::move(region)));
}
if (not(region && region->contain(simgrid::mc::remote(addr))))
continue;
- if (region->storage_type() == simgrid::mc::StorageType::Privatized) {
-#if HAVE_SMPI
- // Use the current process index of the snapshot:
- if (process_index == simgrid::mc::ProcessIndexDisabled)
- process_index = privatization_index_;
- xbt_assert(process_index >= 0, "Missing process index");
- xbt_assert(process_index < (int)region->privatized_data().size(), "Invalid process index");
-
- RegionSnapshot* priv_region = region->privatized_data()[process_index].get();
- xbt_assert(priv_region->contain(simgrid::mc::remote(addr)));
- return priv_region;
-#else
- xbt_die("Privatized region in a non SMPI build (this should not happen)");
-#endif
- }
-
return region;
}
region.get()->restore();
}
- // Fix the privatization mmap if needed
- if (privatization_index_ >= 0) {
- s_mc_message_restore_t message{MC_MESSAGE_RESTORE, privatization_index_};
- process->getChannel().send(message);
- }
-
snapshot_ignore_restore(this);
process->clear_cache();
}
}
case simgrid::mc::StorageType::Chunked:
return mc_translate_address_region_chunked(addr, region);
- case simgrid::mc::StorageType::Privatized: {
- xbt_assert(process_index >= 0, "Missing process index for privatized region");
- xbt_assert((size_t)process_index < region->privatized_data().size(), "Out of range process index");
- simgrid::mc::RegionSnapshot* subregion = region->privatized_data()[process_index].get();
- return mc_translate_address_region(addr, subregion, process_index);
- }
default: // includes StorageType::NoData
xbt_die("Storage type not supported");
}
