| Attribute name | Mandatory | Values | Description |
| --------------- | --------- | ------ | ----------- |
| id | yes | String | The identifier of the link that should be added to the route. |
-| direction | maybe | UP\|DOWN | If the link referenced by \c id has been declared as \ref pf_sharing_policy_fullduplex "FULLDUPLEX", this indicates which direction the route traverses through this link: UP or DOWN. If you don't use FULLDUPLEX, this attribute has no effect.
+| direction | maybe | UP\|DOWN | If the link referenced by \c id has been declared as \ref pf_sharing_policy_fullduplex "FULLDUPLEX", this indicates which direction the route traverses through this link: UP or DOWN. If you don't use FULLDUPLEX, do not use this attribute or SimGrid will not find the right link.
#### Example Files ####
* string (for printing). Have to strip off the decimal point put in there by the floating point print statement
* (internal file) */
fprintf(stdout," NAS Parallel Benchmarks 3.2 -- EP Benchmark");
- sprintf(size,"%zu",(unsigned long)pow(2,m+1));
+ sprintf(size,"%lu",(unsigned long)pow(2,m+1));
//size = size.replace('.', ' ');
fprintf(stdout," Number of random numbers generated: %s\n",size);
fprintf(stdout," Number of active processes: %d\n",no_nodes);
t2 = sqrt(-2. * log(t1) / t1);
t3 = (x1 * t2);
t4 = (x2 * t2);
- l = (int)(abs(t3) > abs(t4) ? abs(t3) : abs(t4));
+ l = (int)(fabs(t3) > fabs(t4) ? fabs(t3) : fabs(t4));
q[l] = q[l] + 1.;
sx = sx + t3;
sy = sy + t4;
fprintf(stdout,("sy_verify = " + sy_verify_value);
*/
if(verified) {
- sx_err = abs((sx - sx_verify_value)/sx_verify_value);
- sy_err = abs((sy - sy_verify_value)/sy_verify_value);
+ sx_err = fabs((sx - sx_verify_value)/sx_verify_value);
+ sy_err = fabs((sy - sy_verify_value)/sy_verify_value);
/*
fprintf(stdout,("sx_err = " + sx_err);
fprintf(stdout,("sy_err = " + sx_err);
double vranlc(int n, double x, double a, double *y)
{
int i;
- long i246m1=0x00003FFFFFFFFFFF;
- long LLx, Lx, La;
+ uint64_t i246m1=0x00003FFFFFFFFFFF;
+ uint64_t LLx, Lx, La;
double d2m46;
// This doesn't work, because the compiler does the calculation in 32 bits and overflows. No standard way (without
d2m46=pow(0.5,46);
- Lx = (long)x;
- La = (long)a;
+ Lx = (uint64_t)x;
+ La = (uint64_t)a;
//fprintf(stdout,("================== Vranlc ================");
//fprintf(stdout,("Before Loop: Lx = " + Lx + ", La = " + La);
LLx = Lx;
#include <stdlib.h>
#include <stdio.h>
+#include <stdint.h>
#include <math.h>
#include "mpi.h"
virtual int main(int argc, char **argv);
/** The Actor that is currently running */
- static Actor *current();
+ static Actor &self();
/** Retrieves the actor that have the given PID (or NULL if not existing) */
//static Actor *byPid(int pid); not implemented
--- /dev/null
+/* Copyright (c) 2015-2016. The SimGrid Team.
+ * All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <errno.h>
+#include <unistd.h>
+
+#include <sys/types.h>
+#include <sys/socket.h>
+
+#include <xbt/log.h>
+
+#include "src/mc/Channel.hpp"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Channel, mc, "MC interprocess communication");
+
+namespace simgrid {
+namespace mc {
+
+Channel::~Channel()
+{
+ if (this->socket_ >=0)
+ close(this->socket_);
+}
+
+int Channel::send(const void* message, size_t size) const
+{
+ XBT_DEBUG("Protocol [%s] send %s",
+ MC_mode_name(mc_mode),
+ MC_message_type_name(*(e_mc_message_type*) message));
+
+ while (::send(this->socket_, message, size, 0) == -1)
+ if (errno == EINTR)
+ continue;
+ else
+ return errno;
+ return 0;
+}
+
+ssize_t Channel::receive(void* message, size_t size, bool block) const
+{
+ int res = recv(this->socket_, message, size, block ? 0 : MSG_DONTWAIT);
+ if (res != -1)
+ XBT_DEBUG("Protocol [%s] received %s",
+ MC_mode_name(mc_mode),
+ MC_message_type_name(*(e_mc_message_type*) message));
+ return res;
+}
+
+}
+}
--- /dev/null
+/* Copyright (c) 2015-2016. The SimGrid Team.
+ * All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_CHANNEL_HPP
+#define SIMGRID_MC_CHANNEL_HPP
+
+#include <unistd.h>
+
+#include <type_traits>
+
+#include "src/mc/mc_protocol.h"
+
+namespace simgrid {
+namespace mc {
+
+class Channel {
+ int socket_ = -1;
+ template<class M>
+ static constexpr bool messageType()
+ {
+ return std::is_class<M>::value && std::is_trivial<M>::value;
+ }
+public:
+
+ Channel() {}
+ Channel(int sock) : socket_(sock) {}
+ ~Channel();
+
+ // No copy:
+ Channel(Channel const&) = delete;
+ Channel& operator=(Channel const&) = delete;
+
+ // Move:
+ Channel(Channel&& that) : socket_(that.socket_)
+ {
+ that.socket_ = -1;
+ }
+ Channel& operator=(Channel&& that)
+ {
+ this->socket_ = that.socket_;
+ that.socket_ = -1;
+ return *this;
+ }
+
+ // Send
+ int send(const void* message, size_t size) const;
+ int send(e_mc_message_type type) const
+ {
+ s_mc_message message = { type };
+ return this->send(&message, sizeof(message));
+ }
+ template<class M>
+ typename std::enable_if< messageType<M>(), int >::type
+ send(M const& m) const
+ {
+ return this->send(&m, sizeof(M));
+ }
+
+ // Receive
+ ssize_t receive(void* message, size_t size, bool block = true) const;
+ template<class M>
+ typename std::enable_if< messageType<M>(), ssize_t >::type
+ receive(M& m) const
+ {
+ return this->receive(&m, sizeof(M));
+ }
+
+ int getSocket() const
+ {
+ return socket_;
+ }
+
+};
+
+}
+}
+
+#endif
--- /dev/null
+/* Copyright (c) 2015. The SimGrid Team.
+ * All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <cstdlib>
+#include <cerrno>
+
+#include <sys/types.h>
+#include <sys/ptrace.h>
+#include <sys/socket.h>
+
+#include <xbt/log.h>
+#include <xbt/sysdep.h>
+#include <xbt/mmalloc.h>
+
+#include "src/internal_config.h"
+
+#include "src/mc/mc_protocol.h"
+#include "src/mc/Client.hpp"
+
+// We won't need those once the separation MCer/MCed is complete:
+#include "src/mc/mc_ignore.h"
+#include "src/mc/mc_private.h" // MC_deadlock_check()
+#include "src/mc/mc_smx.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
+
+namespace simgrid {
+namespace mc {
+
+std::unique_ptr<Client> Client::client_;
+
+Client* Client::initialize()
+{
+ // We are not in MC mode:
+ // TODO, handle this more gracefully.
+ if (!getenv(MC_ENV_SOCKET_FD))
+ return nullptr;
+
+ // Do not break if we are called multiple times:
+ if (client_)
+ return client_.get();
+
+ // Check and set the mode:
+ if (mc_mode != MC_MODE_NONE)
+ abort();
+ mc_mode = MC_MODE_CLIENT;
+
+ // Fetch socket from MC_ENV_SOCKET_FD:
+ char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
+ if (!fd_env)
+ xbt_die("No MC socket passed in the environment");
+ int fd = xbt_str_parse_int(fd_env, bprintf("Variable %s should contain a number but contains '%%s'", MC_ENV_SOCKET_FD));
+ XBT_DEBUG("Model-checked application found socket FD %i", fd);
+
+ // Check the socket type/validity:
+ int type;
+ socklen_t socklen = sizeof(type);
+ if (getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) != 0)
+ xbt_die("Could not check socket type");
+ if (type != SOCK_DGRAM)
+ xbt_die("Unexpected socket type %i", type);
+ XBT_DEBUG("Model-checked application found expected socket type");
+
+ client_ = std::unique_ptr<Client>(new simgrid::mc::Client(fd));
+
+ // Wait for the model-checker:
+ if (ptrace(PTRACE_TRACEME, 0, nullptr, NULL) == -1 || raise(SIGSTOP) != 0)
+ xbt_die("Could not wait for the model-checker");
+
+ client_->handleMessages();
+ return client_.get();
+}
+
+void Client::handleMessages()
+{
+ while (1) {
+ XBT_DEBUG("Waiting messages from model-checker");
+
+ char message_buffer[MC_MESSAGE_LENGTH];
+ ssize_t s;
+
+ if ((s = channel_.receive(&message_buffer, sizeof(message_buffer))) < 0)
+ xbt_die("Could not receive commands from the model-checker");
+
+ s_mc_message_t message;
+ if ((size_t) s < sizeof(message))
+ xbt_die("Received message is too small");
+ memcpy(&message, message_buffer, sizeof(message));
+ switch (message.type) {
+
+ case MC_MESSAGE_DEADLOCK_CHECK:
+ {
+ int result = MC_deadlock_check();
+ s_mc_int_message_t answer;
+ answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
+ answer.value = result;
+ if (channel_.send(answer))
+ xbt_die("Could not send response");
+ }
+ break;
+
+ case MC_MESSAGE_CONTINUE:
+ return;
+
+ case MC_MESSAGE_SIMCALL_HANDLE:
+ {
+ s_mc_simcall_handle_message_t message;
+ if (s != sizeof(message))
+ xbt_die("Unexpected size for SIMCALL_HANDLE");
+ memcpy(&message, message_buffer, sizeof(message));
+ smx_process_t process = SIMIX_process_from_PID(message.pid);
+ if (!process)
+ xbt_die("Invalid pid %lu", (unsigned long) message.pid);
+ SIMIX_simcall_handle(&process->simcall, message.value);
+ if (channel_.send(MC_MESSAGE_WAITING))
+ xbt_die("Could not send MESSAGE_WAITING to model-checker");
+ }
+ 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),
+ MC_message_type_name(message.type),
+ message.type
+ );
+ }
+ }
+}
+
+void Client::mainLoop(void)
+{
+ while (1) {
+ if (channel_.send(MC_MESSAGE_WAITING))
+ xbt_die("Could not send WAITING mesage to model-checker");
+ this->handleMessages();
+ simgrid::mc::wait_for_requests();
+ }
+}
+
+void Client::reportAssertionFailure(const char* description)
+{
+ if (channel_.send(MC_MESSAGE_ASSERTION_FAILED))
+ xbt_die("Could not send assertion to model-checker");
+ this->handleMessages();
+}
+
+void Client::ignoreMemory(void* addr, std::size_t size)
+{
+ s_mc_ignore_memory_message_t message;
+ message.type = MC_MESSAGE_IGNORE_MEMORY;
+ message.addr = (std::uintptr_t) addr;
+ message.size = size;
+ if (channel_.send(message))
+ xbt_die("Could not send IGNORE_MEMORY mesage to model-checker");
+}
+
+void Client::ignoreHeap(void* address, std::size_t size)
+{
+ xbt_mheap_t heap = mmalloc_get_current_heap();
+
+ s_mc_ignore_heap_message_t message;
+ message.type = MC_MESSAGE_IGNORE_HEAP;
+ message.address = address;
+ message.size = size;
+ message.block =
+ ((char *) address -
+ (char *) heap->heapbase) / BLOCKSIZE + 1;
+ if (heap->heapinfo[message.block].type == 0) {
+ message.fragment = -1;
+ heap->heapinfo[message.block].busy_block.ignore++;
+ } else {
+ message.fragment =
+ ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >>
+ heap->heapinfo[message.block].type;
+ heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++;
+ }
+
+ if (channel_.send(message))
+ xbt_die("Could not send ignored region to MCer");
+}
+
+void Client::unignoreHeap(void* address, std::size_t size)
+{
+ s_mc_ignore_memory_message_t message;
+ message.type = MC_MESSAGE_UNIGNORE_HEAP;
+ message.addr = (std::uintptr_t) address;
+ message.size = size;
+ if (channel_.send(message))
+ xbt_die("Could not send IGNORE_HEAP mesasge to model-checker");
+}
+
+void Client::declareSymbol(const char *name, int* value)
+{
+ s_mc_register_symbol_message_t message;
+ message.type = MC_MESSAGE_REGISTER_SYMBOL;
+ if (strlen(name) + 1 > sizeof(message.name))
+ xbt_die("Symbol is too long");
+ strncpy(message.name, name, sizeof(message.name));
+ message.callback = nullptr;
+ message.data = value;
+ if (channel_.send(message))
+ xbt_die("Could send REGISTER_SYMBOL message to model-checker");
+}
+
+void Client::declareStack(void *stack, size_t size, smx_process_t process, ucontext_t* context)
+{
+ xbt_mheap_t heap = mmalloc_get_current_heap();
+
+ s_stack_region_t region;
+ memset(®ion, 0, sizeof(region));
+ region.address = stack;
+ region.context = context;
+ region.size = size;
+ region.block =
+ ((char *) stack -
+ (char *) heap->heapbase) / BLOCKSIZE + 1;
+#if HAVE_SMPI
+ if (smpi_privatize_global_variables && process)
+ region.process_index = smpi_process_index_of_smx_process(process);
+ else
+#endif
+ region.process_index = -1;
+
+ s_mc_stack_region_message_t message;
+ message.type = MC_MESSAGE_STACK_REGION;
+ message.stack_region = region;
+ if (channel_.send(message))
+ xbt_die("Coule not send STACK_REGION to model-checker");
+}
+
+}
+}
--- /dev/null
+/* Copyright (c) 2015. The SimGrid Team.
+ * All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_CLIENT_H
+#define SIMGRID_MC_CLIENT_H
+
+#include <cstddef>
+
+#include <memory>
+
+#include <xbt/base.h>
+
+#include <simgrid/simix.h>
+
+#include "src/mc/mc_protocol.h"
+#include "src/mc/Channel.hpp"
+
+namespace simgrid {
+namespace mc {
+
+class XBT_PUBLIC() Client {
+private:
+ bool active_ = false;
+ Channel channel_;
+ static std::unique_ptr<Client> client_;
+public:
+ Client();
+ Client(int fd) : active_(true), channel_(fd) {}
+ void handleMessages();
+ Channel const& getChannel() const { return channel_; }
+ Channel& getChannel() { return channel_; }
+ void mainLoop(void);
+ void reportAssertionFailure(const char* description = nullptr);
+ void ignoreMemory(void* addr, std::size_t size);
+ void ignoreHeap(void* addr, std::size_t size);
+ void unignoreHeap(void* addr, std::size_t size);
+ void declareSymbol(const char *name, int* value);
+ void declareStack(void *stack, size_t size, smx_process_t process, ucontext_t* context);
+
+ // Singleton :/
+ // TODO, remove the singleton antipattern.
+ static Client* initialize();
+ static Client* get()
+ {
+ return client_.get();
+ }
+};
+
+}
+}
+
+SG_BEGIN_DECL()
+
+#if HAVE_MC
+void MC_ignore(void* addr, std::size_t size);
+#endif
+
+SG_END_DECL()
+
+#endif
#include "src/mc/mc_exit.h"
#include "src/mc/mc_liveness.h"
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
-}
-
::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
using simgrid::mc::remote;
// Prepare data for poll:
struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
- socket_pollfd->fd = process_->socket();;
+ socket_pollfd->fd = process_->getChannel().getSocket();
socket_pollfd->events = POLLIN;
socket_pollfd->revents = 0;
void ModelChecker::resume(simgrid::mc::Process& process)
{
- int res = process.send_message(MC_MESSAGE_CONTINUE);
+ int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
if (res)
throw simgrid::xbt::errno_error(res);
process.cache_flags = (mc_process_cache_flags_t) 0;
if (socket_pollfd->revents) {
if (socket_pollfd->revents & POLLIN) {
- ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
+ ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false);
if (size == -1 && errno != EAGAIN)
throw simgrid::xbt::errno_error(errno);
return handle_message(buffer, size);
m.type = MC_MESSAGE_SIMCALL_HANDLE;
m.pid = pid;
m.value = value;
- process.send_message(m);
+ process.getChannel().send(m);
process.cache_flags = (mc_process_cache_flags_t) 0;
while (process.running())
if (!this->handle_events())
#include "src/mc/mc_mmu.h"
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_page_snapshot, mc,
"Logging specific to mc_page_snapshot");
}
#endif /* SIMGRID_TEST */
-
-}
using simgrid::mc::remote;
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
"MC process information");
-}
-
// ***** Helper stuff
namespace simgrid {
// ***** Process
Process::Process(pid_t pid, int sockfd) :
- AddressSpace(this),pid_(pid), socket_(sockfd), running_(true)
+ AddressSpace(this), pid_(pid), channel_(sockfd), running_(true)
{}
void Process::init()
Process::~Process()
{
- if (this->socket_ >= 0 && close(this->socket_) < 0)
- xbt_die("Could not close communication socket");
-
- this->maestro_stack_start_ = nullptr;
- this->maestro_stack_end_ = nullptr;
-
if (this->memory_file >= 0)
close(this->memory_file);
unw_destroy_addr_space(this->unw_underlying_addr_space);
_UPT_destroy(this->unw_underlying_context);
}
- this->unw_underlying_context = nullptr;
- this->unw_underlying_addr_space = nullptr;
unw_destroy_addr_space(this->unw_addr_space);
- this->unw_addr_space = nullptr;
-
- this->cache_flags = MC_PROCESS_CACHE_FLAG_NONE;
if (this->clear_refs_fd_ >= 0)
close(this->clear_refs_fd_);
std::vector<simgrid::mc::SimixProcessInformation>& Process::simix_processes()
{
xbt_assert(mc_mode != MC_MODE_CLIENT);
- MC_process_smx_refresh(&mc_model_checker->process());
+ this->refresh_simix();
return smx_process_infos;
}
+std::vector<simgrid::mc::SimixProcessInformation>& Process::old_simix_processes()
+{
+ xbt_assert(mc_mode != MC_MODE_CLIENT);
+ this->refresh_simix();
+ return smx_old_process_infos;
+}
+
}
}
#include <xbt/dynar.h>
#include <xbt/mmalloc.h>
-#if HAVE_MC
#include "src/xbt/mmalloc/mmprivate.h"
-#endif
+#include "src/mc/Channel.hpp"
#include <simgrid/simix.h>
#include "src/simix/popping_private.h"
};
/** Representation of a process
+ *
+ * This class is mixing a lot of differents responsabilities and is tied
+ * to SIMIX. It should probably split into different classes.
+ *
+ * Responsabilities:
+ *
+ * - reading from the process memory (`AddressSpace`);
+ * - accessing the system state of the porcess (heap, …);
+ * - storing the SIMIX state of the process;
+ * - privatization;
+ * - communication with the model-checked process;
+ * - stack unwinding;
+ * - etc.
*/
class Process final : public AddressSpace {
public:
return this->heap_info.data();
}
+ Channel const& getChannel() const { return channel_; }
+ Channel& getChannel() { return channel_; }
+
std::vector<IgnoredRegion> const& ignored_regions() const
{
return ignored_regions_;
running_ = false;
}
- template<class M>
- typename std::enable_if< std::is_class<M>::value && std::is_trivial<M>::value, int >::type
- send_message(M const& m)
- {
- return MC_protocol_send(this->socket_, &m, sizeof(M));
- }
-
- int send_message(e_mc_message_type message_id)
- {
- return MC_protocol_send_simple_message(this->socket_, message_id);
- }
-
- template<class M>
- typename std::enable_if< std::is_class<M>::value && std::is_trivial<M>::value, ssize_t >::type
- receive_message(M& m)
- {
- return MC_receive_message(this->socket_, &m, sizeof(M), 0);
- }
-
void reset_soft_dirty();
void read_pagemap(uint64_t* pagemap, size_t start_page, size_t page_count);
void unignore_heap(void *address, size_t size);
void ignore_local_variable(const char *var_name, const char *frame_name);
- int socket() { return socket_; }
std::vector<simgrid::mc::SimixProcessInformation>& simix_processes();
+ std::vector<simgrid::mc::SimixProcessInformation>& old_simix_processes();
private:
void init_memory_map_info();
void refresh_heap();
void refresh_malloc_info();
+ void refresh_simix();
private:
pid_t pid_ = -1;
- int socket_ = -1;
+ Channel channel_;
bool running_ = false;
std::vector<simgrid::xbt::VmMap> memory_map_;
RemotePtr<void> maestro_stack_start_, maestro_stack_end_;
#include "src/mc/ChunkedData.hpp"
#include "src/mc/RegionSnapshot.hpp"
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_RegionSnaphot, mc,
"Logging specific to region snapshots");
-}
-
namespace simgrid {
namespace mc {
class Variable {
public:
Variable() {}
- unsigned dwarf_offset = 0; /* Global offset of the field. */
- int global = 0;
+ std::uint32_t id = 0;
+ bool global = false;
std::string name;
unsigned type_id = 0;
simgrid::mc::Type* type = nullptr;
- // Use either of:
- simgrid::dwarf::LocationList location_list;
+
+ /** Address of the variable -if it is fixed) */
void* address = nullptr;
+
+ /** Description of the location of the variable if it's not fixed */
+ simgrid::dwarf::LocationList location_list;
+
+ /** Offset of validity of the variable (DW_AT_start_scope)
+ *
+ * This variable is not valid since the beginning of its scope.
+ */
std::size_t start_scope = 0;
+
simgrid::mc::ObjectInformation* object_info = nullptr;
};
using simgrid::mc::remote;
#endif
-extern "C" {
-
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
-}
-
int MC_random(int min, int max)
{
xbt_assert(mc_mode != MC_MODE_SERVER);
using simgrid::mc::remote;
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
"Logging specific to mc_checkpoint");
-}
-
namespace simgrid {
namespace mc {
s_mc_restore_message message;
message.type = MC_MESSAGE_RESTORE;
message.index = snapshot->privatization_index;
- mc_model_checker->process().send_message(message);
+ mc_model_checker->process().getChannel().send(message);
}
#endif
}
+++ /dev/null
-/* Copyright (c) 2015. The SimGrid Team.
- * All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <cstdlib>
-#include <cerrno>
-
-#include <sys/types.h>
-#include <sys/ptrace.h>
-#include <sys/socket.h>
-
-#include <xbt/log.h>
-#include <xbt/sysdep.h>
-#include <xbt/mmalloc.h>
-
-#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_client.h"
-
-// We won't need those once the separation MCer/MCed is complete:
-#include "src/mc/mc_ignore.h"
-#include "src/mc/mc_private.h" // MC_deadlock_check()
-#include "src/mc/mc_smx.h"
-
-extern "C" {
-
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
-
-mc_client_t mc_client;
-
-void MC_client_init(void)
-{
- if (mc_mode != MC_MODE_NONE)
- return;
- if (!getenv(MC_ENV_SOCKET_FD))
- return;
- mc_mode = MC_MODE_CLIENT;
-
- if (mc_client) {
- XBT_WARN("MC_client_init called more than once.");
- return;
- }
-
- char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
- if (!fd_env)
- xbt_die("MC socket not found");
-
- int fd = xbt_str_parse_int(fd_env,bprintf("Variable %s should contain a number but contains '%%s'", MC_ENV_SOCKET_FD));
- XBT_DEBUG("Model-checked application found socket FD %i", fd);
-
- int type;
- socklen_t socklen = sizeof(type);
- if (getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) != 0)
- xbt_die("Could not check socket type");
- if (type != SOCK_DGRAM)
- xbt_die("Unexpected socket type %i", type);
- XBT_DEBUG("Model-checked application found expected socket type");
-
- mc_client = xbt_new0(s_mc_client_t, 1);
- mc_client->fd = fd;
- mc_client->active = 1;
-
- // Waiting for the model-checker:
- if (ptrace(PTRACE_TRACEME, 0, nullptr, NULL) == -1 || raise(SIGSTOP) != 0)
- xbt_die("Could not wait for the model-checker");
- MC_client_handle_messages();
-}
-
-void MC_client_send_message(void* message, size_t size)
-{
- if (MC_protocol_send(mc_client->fd, message, size))
- xbt_die("Could not send message %i", (int) ((mc_message_t)message)->type);
-}
-
-void MC_client_send_simple_message(e_mc_message_type type)
-{
- if (MC_protocol_send_simple_message(mc_client->fd, type))
- xbt_die("Could not send message %i", type);
-}
-
-void MC_client_handle_messages(void)
-{
- while (1) {
- XBT_DEBUG("Waiting messages from model-checker");
-
- char message_buffer[MC_MESSAGE_LENGTH];
- ssize_t s;
- if ((s = MC_receive_message(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) < 0)
- xbt_die("Could not receive commands from the model-checker");
-
- s_mc_message_t message;
- if ((size_t) s < sizeof(message))
- xbt_die("Received message is too small");
- memcpy(&message, message_buffer, sizeof(message));
- switch (message.type) {
-
- case MC_MESSAGE_DEADLOCK_CHECK:
- {
- int result = MC_deadlock_check();
- s_mc_int_message_t answer;
- answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
- answer.value = result;
- if (MC_protocol_send(mc_client->fd, &answer, sizeof(answer)))
- xbt_die("Could not send response");
- }
- break;
-
- case MC_MESSAGE_CONTINUE:
- return;
-
- case MC_MESSAGE_SIMCALL_HANDLE:
- {
- s_mc_simcall_handle_message_t message;
- if (s != sizeof(message))
- xbt_die("Unexpected size for SIMCALL_HANDLE");
- memcpy(&message, message_buffer, sizeof(message));
- smx_process_t process = SIMIX_process_from_PID(message.pid);
- if (!process)
- xbt_die("Invalid pid %lu", (unsigned long) message.pid);
- SIMIX_simcall_handle(&process->simcall, message.value);
- MC_protocol_send_simple_message(mc_client->fd, MC_MESSAGE_WAITING);
- }
- 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),
- MC_message_type_name(message.type),
- message.type
- );
- }
- }
-}
-
-void MC_client_main_loop(void)
-{
- while (1) {
- MC_protocol_send_simple_message(mc_client->fd, MC_MESSAGE_WAITING);
- MC_client_handle_messages();
- simgrid::mc::wait_for_requests();
- }
-}
-
-}
+++ /dev/null
-/* Copyright (c) 2015. The SimGrid Team.
- * All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#ifndef SIMGRID_MC_CLIENT_H
-#define SIMGRID_MC_CLIENT_H
-
-#include <cstddef>
-
-#include <xbt/base.h>
-#include "src/mc/mc_protocol.h"
-
-SG_BEGIN_DECL()
-
-typedef struct s_mc_client {
- int active;
- int fd;
-} s_mc_client_t, *mc_client_t;
-
-extern XBT_PRIVATE mc_client_t mc_client;
-
-XBT_PRIVATE void MC_client_init(void);
-XBT_PRIVATE void MC_client_handle_messages(void);
-XBT_PRIVATE void MC_client_send_message(void* message, std::size_t size);
-XBT_PRIVATE void MC_client_send_simple_message(e_mc_message_type type);
-
-#if HAVE_MC
-void MC_ignore(void* addr, std::size_t size);
-#endif
-
-void MC_client_main_loop(void);
-
-SG_END_DECL()
-
-#endif
#include "src/mc/mc_private.h"
#include "src/mc/mc_ignore.h"
#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_client.h"
+#include "src/mc/Client.hpp"
#include "src/mc/ModelChecker.hpp"
/** \file mc_client_api.cpp
* communicate with the MC (declared in modelchecker.h).
*/
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
"Public API for the model-checked application");
-}
-
// MC_random() is in mc_base.cpp
void MC_assert(int prop)
{
- if (MC_is_active() && !prop) {
- MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
- MC_client_handle_messages();
- }
+ if (MC_is_active() && !prop)
+ simgrid::mc::Client::get()->reportAssertionFailure();
}
void MC_cut(void)
{
- user_max_depth_reached = 1;
+ // FIXME, We want to do this in the model-checker:
+ // user_max_depth_reached = 1;
+ xbt_die("MC_cut() not implemented");
}
void MC_ignore(void* addr, size_t size)
xbt_assert(mc_mode != MC_MODE_SERVER);
if (mc_mode != MC_MODE_CLIENT)
return;
-
- s_mc_ignore_memory_message_t message;
- message.type = MC_MESSAGE_IGNORE_MEMORY;
- message.addr = (std::uintptr_t) addr;
- message.size = size;
- MC_client_send_message(&message, sizeof(message));
+ simgrid::mc::Client::get()->ignoreMemory(addr, size);
}
void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
xbt_assert(mc_mode != MC_MODE_SERVER);
if (mc_mode != MC_MODE_CLIENT)
return;
+ simgrid::mc::Client::get()->declareSymbol(name, value);
+}
+
+/** @brief Register a stack in the model checker
+ *
+ * The stacks are allocated in the heap. The MC handle them especially
+ * when we analyse/compare the content of the heap so it must be told where
+ * they are with this function.
+ *
+ * @param stack
+ * @param process Process owning the stack
+ * @param context
+ * @param size Size of the stack
+ */
+void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size)
+{
+ if (mc_mode != MC_MODE_CLIENT)
+ return;
+ simgrid::mc::Client::get()->declareStack(stack, size, process, context);
+}
+
+void MC_ignore_global_variable(const char *name)
+{
+ // TODO, send a message to the model_checker
+ xbt_die("Unimplemented");
+}
+
+void MC_ignore_heap(void *address, size_t size)
+{
+ if (mc_mode != MC_MODE_CLIENT)
+ return;
+ simgrid::mc::Client::get()->ignoreHeap(address, size);
+}
- s_mc_register_symbol_message_t message;
- message.type = MC_MESSAGE_REGISTER_SYMBOL;
- if (strlen(name) + 1 > sizeof(message.name))
- xbt_die("Symbol is too long");
- strncpy(message.name, name, sizeof(message.name));
- message.callback = nullptr;
- message.data = value;
- MC_client_send_message(&message, sizeof(message));
+void MC_remove_ignore_heap(void *address, size_t size)
+{
+ if (mc_mode != MC_MODE_CLIENT)
+ return;
+ simgrid::mc::Client::get()->unignoreHeap(address, size);
}
#include "src/mc/mc_private.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_smx.h"
-#include "src/mc/mc_client.h"
+#include "src/mc/Client.hpp"
#include "src/mc/mc_exit.h"
using simgrid::mc::remote;
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
"Logging specific to MC communication determinism detection");
+extern "C" {
+
/********** Global variables **********/
xbt_dynar_t initial_communications_pattern;
if (mc_mode == MC_MODE_CLIENT)
// This will move somehwere else:
- MC_client_handle_messages();
+ simgrid::mc::Client::get()->handleMessages();
/* Create exploration stack */
mc_stack = xbt_fifo_new();
using simgrid::mc::remote;
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_pattern, mc,
"Logging specific to MC communication patterns");
+extern "C" {
+
mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm)
{
mc_comm_pattern_t res = xbt_new0(s_mc_comm_pattern_t, 1);
using simgrid::mc::remote;
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt,
"Logging specific to mc_compare in mc");
-}
-
namespace simgrid {
namespace mc {
#include "src/mc/mc_record.h"
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc,
"Configuration of MC");
-}
-
#if HAVE_MC
namespace simgrid {
namespace mc {
using simgrid::mc::remote;
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
"Logging specific to mc_diff in mc");
+extern "C" {
+
/*********************************** Heap comparison ***********************************/
/***************************************************************************************/
std::unique_ptr<simgrid::mc::Variable> variable =
std::unique_ptr<simgrid::mc::Variable>(new simgrid::mc::Variable());
- variable->dwarf_offset = dwarf_dieoffset(die);
+ variable->id = dwarf_dieoffset(die);
variable->global = frame == nullptr; // Can be override base on DW_AT_location
variable->object_info = info;
xbt_die(
"Could not read location expression in DW_AT_location "
"of variable <%" PRIx64 ">%s",
- (uint64_t) variable->dwarf_offset,
+ (uint64_t) variable->id,
variable->name.c_str());
}
if (len == 1 && expr[0].atom == DW_OP_addr) {
- variable->global = 1;
+ variable->global = true;
uintptr_t offset = (uintptr_t) expr[0].number;
uintptr_t base = (uintptr_t) info->base_address();
variable->address = (void *) (base + offset);
xbt_die("Unexpected form 0x%x (%i), class 0x%x (%i) list for location "
"in <%" PRIx64 ">%s",
form, form, (int) form_class, (int) form_class,
- (uint64_t) variable->dwarf_offset,
+ (uint64_t) variable->id,
variable->name.c_str());
}
#include "src/mc/mc_record.h"
#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_client.h"
-
-extern "C" {
+#include "src/mc/Client.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
-}
-
e_mc_mode_t mc_mode;
namespace simgrid {
{
mc_mode = MC_MODE_CLIENT;
MC_init();
- MC_client_main_loop();
+ simgrid::mc::Client::get()->mainLoop();
}
void MC_exit(void)
{
if (mc_mode == MC_MODE_SERVER) {
int res;
- if ((res = mc_model_checker->process().send_message(MC_MESSAGE_DEADLOCK_CHECK)))
+ if ((res = mc_model_checker->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
xbt_die("Could not check deadlock state");
s_mc_int_message_t message;
- ssize_t s = mc_model_checker->process().receive_message(message);
+ ssize_t s = mc_model_checker->process().getChannel().receive(message);
if (s == -1)
xbt_die("Could not receive message");
if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
+++ /dev/null
-/* Copyright (c) 2008-2015. The SimGrid Team.
- * All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include "src/internal_config.h"
-#include "src/mc/mc_private.h"
-#include "src/smpi/private.h"
-#include "src/mc/mc_snapshot.h"
-#include "src/mc/mc_ignore.h"
-#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_client.h"
-
-extern "C" {
-
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
- "Logging specific to MC ignore mechanism");
-
-// ***** Model-checked
-
-void MC_ignore_heap(void *address, size_t size)
-{
- if (mc_mode != MC_MODE_CLIENT)
- return;
-
- xbt_mheap_t heap = mmalloc_get_current_heap();
-
- s_mc_ignore_heap_message_t message;
- message.type = MC_MESSAGE_IGNORE_HEAP;
- message.address = address;
- message.size = size;
- message.block =
- ((char *) address -
- (char *) heap->heapbase) / BLOCKSIZE + 1;
- if (heap->heapinfo[message.block].type == 0) {
- message.fragment = -1;
- heap->heapinfo[message.block].busy_block.ignore++;
- } else {
- message.fragment =
- ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >>
- heap->heapinfo[message.block].type;
- heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++;
- }
-
- if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
- xbt_die("Could not send ignored region to MCer");
-}
-
-void MC_remove_ignore_heap(void *address, size_t size)
-{
- if (mc_mode != MC_MODE_CLIENT)
- return;
-
- s_mc_ignore_memory_message_t message;
- message.type = MC_MESSAGE_UNIGNORE_HEAP;
- message.addr = (std::uintptr_t) address;
- message.size = size;
- MC_client_send_message(&message, sizeof(message));
-}
-
-void MC_ignore_global_variable(const char *name)
-{
- // TODO, send a message to the model_checker
- xbt_die("Unimplemented");
-}
-
-/** @brief Register a stack in the model checker
- *
- * The stacks are allocated in the heap. The MC handle them especially
- * when we analyse/compare the content of the heap so it must be told where
- * they are with this function.
- *
- * @param stack
- * @param process Process owning the stack
- * @param context
- * @param size Size of the stack
- */
-void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size)
-{
- if (mc_mode != MC_MODE_CLIENT)
- return;
-
- xbt_mheap_t heap = mmalloc_get_current_heap();
-
- s_stack_region_t region;
- memset(®ion, 0, sizeof(region));
- region.address = stack;
- region.context = context;
- region.size = size;
- region.block =
- ((char *) stack -
- (char *) heap->heapbase) / BLOCKSIZE + 1;
-#if HAVE_SMPI
- if (smpi_privatize_global_variables && process)
- region.process_index = smpi_process_index_of_smx_process(process);
- else
-#endif
- region.process_index = -1;
-
- s_mc_stack_region_message_t message;
- message.type = MC_MESSAGE_STACK_REGION;
- message.stack_region = region;
- MC_client_send_message(&message, sizeof(message));
-}
-
-}
#include "src/mc/mc_private.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_smx.h"
-#include "src/mc/mc_client.h"
+#include "src/mc/Client.hpp"
#include "src/mc/mc_replay.h"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_exit.h"
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
-}
-
/********* Global variables *********/
xbt_dynar_t acceptance_pairs;
#include "mc/mc.h"
#include "src/mc/mc_private.h"
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc,
"Logging specific to MC (memory)");
+extern "C" {
+
/* Initialize the model-checker memory subsystem */
/* It creates the two heap regions: std_heap and mc_heap */
void MC_memory_init()
#include <xbt/log.h>
#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_client.h"
-
-extern "C" {
+#include "src/mc/Client.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
-int MC_protocol_send(int socket, const void* message, std::size_t size)
-{
- XBT_DEBUG("Protocol [%s] send %s",
- MC_mode_name(mc_mode),
- MC_message_type_name(*(e_mc_message_type*) message));
-
- while (send(socket, message, size, 0) == -1)
- if (errno == EINTR)
- continue;
- else
- return errno;
- return 0;
-}
-
-int MC_protocol_send_simple_message(int socket, e_mc_message_type type)
-{
- s_mc_message_t message;
- message.type = type;
- return MC_protocol_send(socket, &message, sizeof(message));
-}
-
-ssize_t MC_receive_message(int socket, void* message, size_t size, int options)
-{
- int res = recv(socket, message, size, options);
- if (res != -1)
- XBT_DEBUG("Protocol [%s] received %s",
- MC_mode_name(mc_mode),
- MC_message_type_name(*(e_mc_message_type*) message));
- return res;
-}
-
const char* MC_message_type_name(e_mc_message_type type)
{
switch(type) {
return "?";
}
}
-
-}
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);
-
XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type);
XBT_PRIVATE const char* MC_mode_name(e_mc_mode_t mode);
#include "src/mc/mc_liveness.h"
#endif
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,
" Logging specific to MC record/replay facility");
+extern "C" {
+
char* MC_record_path = nullptr;
void MC_record_replay(mc_record_item_t start, std::size_t len)
using simgrid::mc::remote;
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
"Logging specific to MC (request)");
-}
-
static char *pointer_to_string(void *pointer);
static char *buff_size_to_string(size_t size);
#include "src/mc/mc_private.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_smx.h"
-#include "src/mc/mc_client.h"
+#include "src/mc/Client.hpp"
#include "src/mc/mc_exit.h"
#include "src/xbt/mmalloc/mmprivate.h"
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
-}
-
namespace simgrid {
namespace mc {
assert(i == swag.count);
}
-void MC_process_smx_refresh(simgrid::mc::Process* process)
+namespace simgrid {
+namespace mc {
+
+void Process::refresh_simix()
{
xbt_assert(mc_mode == MC_MODE_SERVER);
- if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
+ if (this->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
return;
// TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
// simix_global_p = REMOTE(simix_global);
smx_global_t simix_global_p;
- process->read_variable("simix_global", &simix_global_p, sizeof(simix_global_p));
+ this->read_variable("simix_global", &simix_global_p, sizeof(simix_global_p));
// simix_global = REMOTE(*simix_global)
s_smx_global_t simix_global;
- process->read_bytes(&simix_global, sizeof(simix_global),
+ this->read_bytes(&simix_global, sizeof(simix_global),
remote(simix_global_p));
MC_process_refresh_simix_process_list(
- process, process->smx_process_infos, simix_global.process_list);
+ this, this->smx_process_infos, simix_global.process_list);
MC_process_refresh_simix_process_list(
- process, process->smx_old_process_infos, simix_global.process_to_destroy);
+ this, this->smx_old_process_infos, simix_global.process_to_destroy);
- process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
+ this->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
+}
+
+}
}
/** Get the issuer of a simcall (`req->issuer`)
if (mc_mode == MC_MODE_CLIENT)
return req->issuer;
- MC_process_smx_refresh(&mc_model_checker->process());
-
// This is the address of the smx_process in the MCed process:
void* address = req->issuer;
// Lookup by address:
- for (auto& p : mc_model_checker->process().smx_process_infos)
+ for (auto& p : mc_model_checker->process().simix_processes())
if (p.address == address)
return &p.copy;
- for (auto& p : mc_model_checker->process().smx_old_process_infos)
+ for (auto& p : mc_model_checker->process().old_simix_processes())
if (p.address == address)
return &p.copy;
using simgrid::mc::remote;
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
"Logging specific to MC (state)");
+extern "C" {
+
/**
* \brief Creates a state data structure used by the exploration algorithm
*/
#include "src/mc/Process.hpp"
#include "src/mc/mc_smx.h"
-extern "C" {
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
"Logging specific to state equaity detection mechanisms");
-}
-
namespace simgrid {
namespace mc {
process->get_heap()->heaplimit,
process->get_malloc_info());
- MC_process_smx_refresh(&mc_model_checker->process());
this->nb_processes =
- mc_model_checker->process().smx_process_infos.size();
+ mc_model_checker->process().simix_processes().size();
this->num = mc_stats->expanded_states;
this->other_num = -1;
process->get_heap()->heaplimit,
process->get_malloc_info());
- MC_process_smx_refresh(&mc_model_checker->process());
this->nb_processes =
- mc_model_checker->process().smx_process_infos.size();
+ mc_model_checker->process().simix_processes().size();
this->automaton_state = automaton_state;
this->num = pair_num;
fprintf(stderr,"Error: You should override the method main(int, char**) in Actor class %s\n",getName());
return 0;
}
-s4u::Actor *s4u::Actor::current()
+s4u::Actor &s4u::Actor::self()
{
smx_process_t smx_proc = SIMIX_process_self();
simgrid::s4u::Actor* res = (simgrid::s4u::Actor*) SIMIX_process_self_get_data();
if (res == NULL) // The smx_process was not created by S4U (but by deployment?). Embed it in a S4U object
res = new Actor(smx_proc);
- return res;
+ return *res;
}
void s4u::Actor::setAutoRestart(bool autorestart) {
#if HAVE_MC
#include "src/mc/mc_private.h"
#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_client.h"
+#include "src/mc/Client.hpp"
#include <stdlib.h>
#include "src/mc/mc_protocol.h"
#if HAVE_MC
// The communication initialization is done ASAP.
// We need to communicate initialization of the different layers to the model-checker.
- MC_client_init();
+ simgrid::mc::Client::initialize();
#endif
if (_sg_cfg_exit_asap)
#include "xbt/dict.h"
#include "mc/mc.h"
#include "src/mc/mc_replay.h"
-#include "src/mc/mc_client.h"
+#include "src/mc/Client.hpp"
#include "src/simix/smx_private.hpp"
#include "src/msg/msg_private.h"
routing_model_create(NULL);
- simgrid::surf::on_link.connect([](sg_platf_link_cbarg_t link){
- xbt_die("There is no link in the Constant network model. "
- "Please remove any link from your platform (and switch to routing='None')");
- });
+ simgrid::surf::on_link.connect(netlink_parse_init);
}
namespace simgrid {
namespace surf {
+ Link* NetworkConstantModel::createLink(const char *name, double bw, double lat, e_surf_link_sharing_policy_t policy,
+ xbt_dict_t properties) {
+
+ xbt_die("Refusing to create the link %s: there is no link in the Constant network model. "
+ "Please remove any link from your platform (and switch to routing='None')", name);
+ }
+
double NetworkConstantModel::next_occuring_event(double /*now*/)
{
NetworkConstantAction *action = NULL;
bool next_occuring_event_isIdempotent() override {return true;}
void updateActionsState(double now, double delta) override;
- Link* createLink(const char *name, double bw, double lat, e_surf_link_sharing_policy_t policy, xbt_dict_t properties) override
- { DIE_IMPOSSIBLE; }
+ Link* createLink(const char *name, double bw, double lat, e_surf_link_sharing_policy_t policy, xbt_dict_t properties) override;
};
/**********
}
void netlink_parse_init(sg_platf_link_cbarg_t link){
- if (link->policy == SURF_LINK_FULLDUPLEX) {
- char *link_id;
- link_id = bprintf("%s_UP", link->id);
- Link *l = surf_network_model->createLink(link_id, link->bandwidth, link->latency,
- link->policy, link->properties);
- if (link->latency_trace)
- l->setLatencyTrace(link->latency_trace);
- if (link->bandwidth_trace)
- l->setBandwidthTrace(link->bandwidth_trace);
- if (link->state_trace)
- l->setStateTrace(link->state_trace);
+ std::vector<char*> names;
- xbt_free(link_id);
- link_id = bprintf("%s_DOWN", link->id);
- l = surf_network_model->createLink(link_id, link->bandwidth, link->latency,
- link->policy, link->properties);
- if (link->latency_trace)
- l->setLatencyTrace(link->latency_trace);
- if (link->bandwidth_trace)
- l->setBandwidthTrace(link->bandwidth_trace);
- if (link->state_trace)
- l->setStateTrace(link->state_trace);
- xbt_free(link_id);
+ if (link->policy == SURF_LINK_FULLDUPLEX) {
+ names.push_back(bprintf("%s_UP", link->id));
+ names.push_back(bprintf("%s_DOWN", link->id));
} else {
- Link *l=surf_network_model->createLink(link->id, link->bandwidth, link->latency,
- link->policy, link->properties);
+ names.push_back(xbt_strdup(link->id));
+ }
+ for (auto link_name : names) {
+ Link *l = surf_network_model->createLink(link_name, link->bandwidth, link->latency, link->policy, link->properties);
+
if (link->latency_trace)
l->setLatencyTrace(link->latency_trace);
if (link->bandwidth_trace)
l->setBandwidthTrace(link->bandwidth_trace);
if (link->state_trace)
l->setStateTrace(link->state_trace);
+
+ xbt_free(link_name);
}
}
int NS3_EXTENSION_ID;
-xbt_dynar_t IPV4addr;
+xbt_dynar_t IPV4addr = xbt_dynar_new(sizeof(char*),free);
static double time_to_next_flow_completion = -1;
extern xbt_dict_t dict_socket;
{
XBT_DEBUG("NS3_ADD_LINK '%s'",link->id);
- if(!IPV4addr)
- IPV4addr = xbt_dynar_new(sizeof(char*),free);
-
- Link *l = surf_network_model->createLink(link->id, link->bandwidth, link->latency,
- link->policy, link->properties);
+ Link *l = surf_network_model->createLink(link->id, link->bandwidth, link->latency, link->policy, link->properties);
if (link->bandwidth_trace)
l->setBandwidthTrace(link->latency_trace);
if (link->latency_trace)
{
simgrid::s4u::Host::onCreation.connect(simgrid_ns3_add_host);
simgrid::surf::netcardCreatedCallbacks.connect(simgrid_ns3_add_router);
- simgrid::surf::on_link.connect (&parse_ns3_add_link);
+ simgrid::surf::on_link.connect (parse_ns3_add_link);
simgrid::surf::on_cluster.connect (&parse_ns3_add_cluster);
simgrid::surf::asCreatedCallbacks.connect(parse_ns3_add_AS);
simgrid::surf::on_postparse.connect(&create_ns3_topology); //get_one_link_routes
/**************************************/
/*** Resource Creation & Destruction **/
/**************************************/
-
-static void ptask_netlink_parse_init(sg_platf_link_cbarg_t link)
-{
- netlink_parse_init(link);
- current_property_set = NULL;
-}
-
void surf_host_model_init_ptask_L07(void)
{
XBT_CINFO(xbt_cfg,"Switching to the L07 model to handle parallel tasks.");
xbt_assert(!surf_network_model, "network model type already defined");
// Define the callbacks to parse the XML
- simgrid::surf::on_link.connect(ptask_netlink_parse_init);
+ simgrid::surf::on_link.connect(netlink_parse_init);
surf_host_model = new simgrid::surf::HostL07Model();
xbt_dynar_push(all_existing_models, &surf_host_model);
XBT_DEBUG("Add a backbone to AS '%s'", current_routing->name());
}
+void sg_platf_new_cabinet(sg_platf_cabinet_cbarg_t cabinet)
+{
+ int start, end, i;
+ char *groups , *host_id , *link_id = NULL;
+ unsigned int iter;
+ xbt_dynar_t radical_elements;
+ xbt_dynar_t radical_ends;
+
+ //Make all hosts
+ radical_elements = xbt_str_split(cabinet->radical, ",");
+ xbt_dynar_foreach(radical_elements, iter, groups) {
+
+ radical_ends = xbt_str_split(groups, "-");
+ start = surf_parse_get_int(xbt_dynar_get_as(radical_ends, 0, char *));
+
+ switch (xbt_dynar_length(radical_ends)) {
+ case 1:
+ end = start;
+ break;
+ case 2:
+ end = surf_parse_get_int(xbt_dynar_get_as(radical_ends, 1, char *));
+ break;
+ default:
+ surf_parse_error("Malformed radical");
+ break;
+ }
+ s_sg_platf_host_cbarg_t host = SG_PLATF_HOST_INITIALIZER;
+ memset(&host, 0, sizeof(host));
+ host.pstate = 0;
+ host.core_amount = 1;
+
+ s_sg_platf_link_cbarg_t link = SG_PLATF_LINK_INITIALIZER;
+ memset(&link, 0, sizeof(link));
+ link.policy = SURF_LINK_FULLDUPLEX;
+ link.latency = cabinet->lat;
+ link.bandwidth = cabinet->bw;
+
+ s_sg_platf_host_link_cbarg_t host_link = SG_PLATF_HOST_LINK_INITIALIZER;
+ memset(&host_link, 0, sizeof(host_link));
+
+ for (i = start; i <= end; i++) {
+ host_id = bprintf("%s%d%s",cabinet->prefix,i,cabinet->suffix);
+ link_id = bprintf("link_%s%d%s",cabinet->prefix,i,cabinet->suffix);
+ host.id = host_id;
+ link.id = link_id;
+ host.speed_peak = xbt_dynar_new(sizeof(double), NULL);
+ xbt_dynar_push(host.speed_peak,&cabinet->speed);
+ sg_platf_new_host(&host);
+ xbt_dynar_free(&host.speed_peak);
+ sg_platf_new_link(&link);
+
+ char* link_up = bprintf("%s_UP",link_id);
+ char* link_down = bprintf("%s_DOWN",link_id);
+ host_link.id = host_id;
+ host_link.link_up = link_up;
+ host_link.link_down = link_down;
+ sg_platf_new_hostlink(&host_link);
+
+ free(host_id);
+ free(link_id);
+ free(link_up);
+ free(link_down);
+ }
+
+ xbt_dynar_free(&radical_ends);
+ }
+ xbt_dynar_free(&radical_elements);
+}
+
void sg_platf_new_storage(sg_platf_storage_cbarg_t storage)
{
xbt_assert(!xbt_lib_get_or_null(storage_lib, storage->id,ROUTING_STORAGE_LEVEL),
link.latency = peer->lat;
char* link_up = bprintf("%s_UP",link_id);
- XBT_DEBUG("<link\tid=\"%s\"\tbw=\"%f\"\tlat=\"%f\"/>", link_up,
- peer->bw_out, peer->lat);
+ XBT_DEBUG("<link\tid=\"%s\"\tbw=\"%f\"\tlat=\"%f\"/>", link_up, peer->bw_out, peer->lat);
link.id = link_up;
link.bandwidth = peer->bw_out;
sg_platf_new_link(&link);
char* link_down = bprintf("%s_DOWN",link_id);
- XBT_DEBUG("<link\tid=\"%s\"\tbw=\"%f\"\tlat=\"%f\"/>", link_down,
- peer->bw_in, peer->lat);
+ XBT_DEBUG("<link\tid=\"%s\"\tbw=\"%f\"\tlat=\"%f\"/>", link_down, peer->bw_in, peer->lat);
link.id = link_down;
link.bandwidth = peer->bw_in;
sg_platf_new_link(&link);
/* ************************************************************************** */
/* ************************* GENERIC PARSE FUNCTIONS ************************ */
-void sg_platf_new_cabinet(sg_platf_cabinet_cbarg_t cabinet)
-{
- int start, end, i;
- char *groups , *host_id , *link_id = NULL;
- unsigned int iter;
- xbt_dynar_t radical_elements;
- xbt_dynar_t radical_ends;
-
- //Make all hosts
- radical_elements = xbt_str_split(cabinet->radical, ",");
- xbt_dynar_foreach(radical_elements, iter, groups) {
-
- radical_ends = xbt_str_split(groups, "-");
- start = surf_parse_get_int(xbt_dynar_get_as(radical_ends, 0, char *));
-
- switch (xbt_dynar_length(radical_ends)) {
- case 1:
- end = start;
- break;
- case 2:
- end = surf_parse_get_int(xbt_dynar_get_as(radical_ends, 1, char *));
- break;
- default:
- surf_parse_error("Malformed radical");
- break;
- }
- s_sg_platf_host_cbarg_t host = SG_PLATF_HOST_INITIALIZER;
- memset(&host, 0, sizeof(host));
- host.pstate = 0;
- host.core_amount = 1;
-
- s_sg_platf_link_cbarg_t link = SG_PLATF_LINK_INITIALIZER;
- memset(&link, 0, sizeof(link));
- link.policy = SURF_LINK_FULLDUPLEX;
- link.latency = cabinet->lat;
- link.bandwidth = cabinet->bw;
-
- s_sg_platf_host_link_cbarg_t host_link = SG_PLATF_HOST_LINK_INITIALIZER;
- memset(&host_link, 0, sizeof(host_link));
-
- for (i = start; i <= end; i++) {
- host_id = bprintf("%s%d%s",cabinet->prefix,i,cabinet->suffix);
- link_id = bprintf("link_%s%d%s",cabinet->prefix,i,cabinet->suffix);
- host.id = host_id;
- link.id = link_id;
- host.speed_peak = xbt_dynar_new(sizeof(double), NULL);
- xbt_dynar_push(host.speed_peak,&cabinet->speed);
- sg_platf_new_host(&host);
- xbt_dynar_free(&host.speed_peak);
- sg_platf_new_link(&link);
-
- char* link_up = bprintf("%s_UP",link_id);
- char* link_down = bprintf("%s_DOWN",link_id);
- host_link.id = host_id;
- host_link.link_up = link_up;
- host_link.link_down = link_down;
- sg_platf_new_hostlink(&host_link);
-
- free(host_id);
- free(link_id);
- free(link_up);
- free(link_down);
- }
-
- xbt_dynar_free(&radical_ends);
- }
- xbt_dynar_free(&radical_elements);
-}
-
static void check_disk_attachment()
{
xbt_lib_cursor_t cursor;
#include "src/surf/xml/platf_private.hpp"
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_parse, surf,
- "Logging specific to the SURF parsing module");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_parse, surf, "Logging specific to the SURF parsing module");
#undef CLEANUP
int ETag_surfxml_include_state(void);
XBT_LOG_CONNECT(mc_diff);
XBT_LOG_CONNECT(mc_dwarf);
XBT_LOG_CONNECT(mc_hash);
- XBT_LOG_CONNECT(mc_ignore);
XBT_LOG_CONNECT(mc_liveness);
XBT_LOG_CONNECT(mc_memory);
XBT_LOG_CONNECT(mc_page_snapshot);
foreach (SCATTER ompi mpich ompi_basic_linear ompi_binomial mvapich2 mvapich2_two_level_binomial mvapich2_two_level_direct impi)
ADD_TESH(tesh-smpi-coll-scatter-${SCATTER} --cfg smpi/scatter:${SCATTER} --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-scatter --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/smpi/coll-scatter coll-scatter.tesh)
endforeach()
-endif()
# Extra allreduce test: large automatic
ADD_TESH(tesh-smpi-coll-allreduce-large --cfg smpi/allreduce:ompi_ring_segmented --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/smpi/coll-allreduce coll-allreduce-large.tesh)
ADD_TESH_FACTORIES(tesh-smpi-broken "thread" --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/smpi/pt2pt-pingpong --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/smpi/pt2pt-pingpong broken_hostfiles.tesh)
ADD_TESH(tesh-smpi-replay-ti-tracing --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/smpi/pt2pt-pingpong --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/smpi/pt2pt-pingpong TI_output.tesh)
+endif()
+
set(teshsuite_src ${teshsuite_src} PARENT_SCOPE)
set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/coll-allreduce/coll-allreduce-large.tesh
${CMAKE_CURRENT_SOURCE_DIR}/coll-allreduce/coll-allreduce-automatic.tesh
src/mc/RemotePtr.hpp
src/mc/AddressSpace.hpp
src/mc/AddressSpace.cpp
+ src/mc/Channel.cpp
+ src/mc/Channel.hpp
+ src/mc/Client.cpp
+ src/mc/Client.hpp
src/mc/Frame.hpp
src/mc/Frame.cpp
src/mc/ModelChecker.hpp
src/mc/mc_dwarf_tagnames.cpp
src/mc/mc_hash.hpp
src/mc/mc_hash.cpp
- src/mc/mc_ignore.cpp
src/mc/mc_ignore.h
src/mc/mc_mmalloc.h
src/mc/mc_liveness.h
src/mc/mc_state.h
src/mc/mc_state.cpp
src/mc/mc_visited.cpp
- src/mc/mc_client.cpp
src/mc/mc_client_api.cpp
- src/mc/mc_client.h
src/mc/mc_protocol.h
src/mc/mc_protocol.cpp
src/mc/mc_smx.h
string(REGEX MATCH "[0-9]+.[0-9]+.[0-9]+" NEW_VALGRIND_VERSION "${VALGRIND_VERSION}")
if(NEW_VALGRIND_VERSION)
message(STATUS "Valgrind version: ${NEW_VALGRIND_VERSION}")
- execute_process(COMMAND "${CMAKE_HOME_DIRECTORY}/tools/cmake/scripts/generate_memcheck_tests.pl ${CMAKE_HOME_DIRECTORY} ${CMAKE_HOME_DIRECTORY}/tools/cmake/Tests.cmake > ${CMAKE_HOME_DIRECTORY}/tools/cmake/memcheck_tests.cmake")
+ execute_process(COMMAND ${CMAKE_HOME_DIRECTORY}/tools/cmake/scripts/generate_memcheck_tests.pl ${CMAKE_HOME_DIRECTORY} ${CMAKE_HOME_DIRECTORY}/tools/cmake/Tests.cmake OUTPUT_FILE ${CMAKE_BINARY_DIR}/memcheck_tests.cmake)
set(MEMORYCHECK_COMMAND_OPTIONS "--trace-children=yes --trace-children-skip=/usr/bin/*,/bin/* --leak-check=full --show-reachable=yes --track-origins=no --read-var-info=no --num-callers=20 --suppressions=${CMAKE_HOME_DIRECTORY}/tools/simgrid.supp ${VALGRIND_EXTRA_COMMAND_OPTIONS} ")
message(STATUS "Valgrind options: ${MEMORYCHECK_COMMAND_OPTIONS}")
else()
IF(enable_memcheck)
INCLUDE(FindValgrind)
- INCLUDE(${CMAKE_HOME_DIRECTORY}/tools/cmake/memcheck_tests.cmake)
+ INCLUDE(${CMAKE_BINARY_DIR}/memcheck_tests.cmake)
ENDIF()
