src/mc/mc_protocol.c
src/mc/mc_server.cpp
src/mc/mc_server.h
+ src/mc/mc_smx.h
+ src/mc/mc_smx.c
)
set(MC_SIMGRID_MC_SRC
#include "mc_mmu.h"
#include "mc_unw.h"
#include "mc_protocol.h"
+#include "mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
"Logging specific to mc_checkpoint");
#include "mc_safety.h"
#include "mc_private.h"
#include "mc_record.h"
+#include "mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
"Logging specific to MC communication determinism detection");
void *addr_pointed;
comm_pattern->src_proc = comm->comm.src_proc->pid;
comm_pattern->dst_proc = comm->comm.dst_proc->pid;
- // FIXME, get remote host name
- comm_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
- comm_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
+ // TODO, resolve host name
+ comm_pattern->src_host = MC_smx_process_get_host_name(MC_smx_resolve_process(comm->comm.src_proc));
+ comm_pattern->dst_host = MC_smx_process_get_host_name(MC_smx_resolve_process(comm->comm.dst_proc));
if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) {
comm_pattern->data_size = *(comm->comm.dst_buff_size);
comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
pattern->data_size = -1;
pattern->data = NULL;
- const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, request);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
mc_list_comm_pattern_t initial_pattern =
(mc_list_comm_pattern_t) xbt_dynar_get_as(initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
xbt_dynar_t incomplete_pattern =
pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
pattern->src_proc = pattern->comm->comm.src_proc->pid;
// FIXME, get remote host name
- pattern->src_host = simcall_host_get_name(issuer->smx_host);
+ pattern->src_host = MC_smx_process_get_host_name(issuer);
if(pattern->comm->comm.src_buff != NULL){
pattern->data_size = pattern->comm->comm.src_buff_size;
pattern->data = xbt_malloc0(pattern->data_size);
pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
// FIXME, remote process access
- pattern->dst_host = simcall_host_get_name(issuer->smx_host);
+ pattern->dst_host = MC_smx_process_get_host_name(issuer);
} else {
xbt_die("Unexpected call_type %i", (int) call_type);
}
#include "mc_liveness.h"
#include "mc_private.h"
#include "mc_unw.h"
+#include "mc_smx.h"
#endif
#include "mc_record.h"
#include "mc_protocol.h"
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
- const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
req = &issuer->simcall;
/* Debug information */
if (saved_req != NULL) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
- const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
req = &issuer->simcall;
/* Debug information */
#include "mc_liveness.h"
#include "mc_private.h"
#include "mc_record.h"
+#include "mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
mc->fd_clear_refs = -1;
mc->fd_pagemap = -1;
MC_process_init(&mc->process, pid, socket);
+ mc->hosts = xbt_dict_new();
return mc;
}
if(mc->record)
xbt_dynar_free(&mc->record);
MC_process_clear(&mc->process);
+ xbt_dict_free(&mc->hosts);
}
int fd_pagemap;
xbt_dynar_t record;
s_mc_process_t process;
+ /** String pool for host names */
+ xbt_dict_t /* <hostname, NULL> */ hosts;
};
mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
void MC_model_checker_delete(mc_model_checker_t mc);
-#define MC_EACH_SIMIX_PROCESS(process, code) \
- if (MC_process_is_self(&mc_model_checker->process)) { \
- xbt_swag_foreach(process, simix_global->process_list) { \
- code; \
- } \
- } else { \
- MC_process_refresh_simix_processes(&mc_model_checker->process); \
- unsigned int _smx_process_index; \
- mc_smx_process_info_t _smx_process_info; \
- xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, _smx_process_index, _smx_process_info) { \
- smx_process_t process = &_smx_process_info->copy; \
- code; \
- } \
- }
-
SG_END_DECL()
#endif
#include "mc_unw.h"
#include "mc_snapshot.h"
#include "mc_ignore.h"
-
-#include "simix/smx_private.h"
+#include "mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
"MC process information");
&process->heap_address, std_heap_var->address, sizeof(struct mdesc*),
MC_PROCESS_INDEX_DISABLED);
- process->smx_process_infos = mc_smx_process_info_list_new();
- process->smx_old_process_infos = mc_smx_process_info_list_new();
+ process->smx_process_infos = MC_smx_process_info_list_new();
+ process->smx_old_process_infos = MC_smx_process_info_list_new();
process->checkpoint_ignore = MC_checkpoint_ignore_new();
MC_PROCESS_INDEX_DISABLED);
}
-/** Load the remote swag of processes into a dynar
- *
- * @param process MCed process
- * @param target Local dynar (to be filled with copies of `s_smx_process_t`)
- * @param remote_swag Address of the process SWAG in the remote list
- */
-static void MC_process_refresh_simix_process_list(
- mc_process_t process,
- xbt_dynar_t target, xbt_swag_t remote_swag)
-{
- // swag = REMOTE(*simix_global->process_list)
- s_xbt_swag_t swag;
- MC_process_read(process, MC_PROCESS_NO_FLAG, &swag, remote_swag, sizeof(swag),
- MC_PROCESS_INDEX_ANY);
-
- smx_process_t p;
- xbt_dynar_reset(target);
-
- int i = 0;
- for (p = swag.head; p; ++i) {
-
- s_mc_smx_process_info_t info;
- info.address = p;
- MC_process_read(process, MC_PROCESS_NO_FLAG,
- &info.copy, p, sizeof(info.copy), MC_PROCESS_INDEX_ANY);
- xbt_dynar_push(target, &info);
-
- // Lookup next process address:
- p = xbt_swag_getNext(&info.copy, swag.offset);
- }
- assert(i == swag.count);
-}
-
-void MC_process_refresh_simix_processes(mc_process_t process)
-{
- if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
- return;
-
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
- // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
-
- // simix_global_p = REMOTE(simix_global);
- smx_global_t simix_global_p;
- MC_process_read_variable(process, "simix_global", &simix_global_p, sizeof(simix_global_p));
-
- // simix_global = REMOTE(*simix_global)
- s_smx_global_t simix_global;
- MC_process_read(process, MC_PROCESS_NO_FLAG, &simix_global, simix_global_p, sizeof(simix_global),
- MC_PROCESS_INDEX_ANY);
-
- MC_process_refresh_simix_process_list(
- process, process->smx_process_infos, simix_global.process_list);
- MC_process_refresh_simix_process_list(
- process, process->smx_old_process_infos, simix_global.process_to_destroy);
-
- process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
- mmalloc_set_current_heap(heap);
-}
-
#define SO_RE "\\.so[\\.0-9]*$"
#define VERSION_RE "-[\\.0-9]*$"
}
}
+const void* MC_process_read_simple(mc_process_t process,
+ void* local, const void* remote, size_t len)
+{
+ e_adress_space_read_flags_t flags = MC_PROCESS_NO_FLAG;
+ int index = MC_PROCESS_INDEX_ANY;
+ return MC_process_read(process, flags, local, remote, len, index);
+}
+
void MC_process_write(mc_process_t process, const void* local, void* remote, size_t len)
{
if (MC_process_is_self(process)) {
}
}
-/** Get the issuer of a simcall (`req->issuer`)
- *
- * In split-process mode, it does the black magic necessary to get an address
- * of a (shallow) copy of the data structure the issuer SIMIX process in the local
- * address space.
- *
- * @param process the MCed process
- * @param req the simcall (copied in the local process)
- */
-smx_process_t MC_process_get_issuer(mc_process_t process, smx_simcall_t req)
-{
- if (MC_process_is_self(&mc_model_checker->process))
- return req->issuer;
-
- MC_process_refresh_simix_processes(process);
-
- // This is the address of the smx_process in the MCed process:
- void* address = req->issuer;
-
- unsigned i;
- mc_smx_process_info_t p;
-
- xbt_dynar_foreach_ptr(process->smx_process_infos, i, p)
- if (p->address == address)
- return &p->copy;
- xbt_dynar_foreach_ptr(process->smx_old_process_infos, i, p)
- if (p->address == address)
- return &p->copy;
-
- xbt_die("Issuer not found");
-}
-
void MC_simcall_handle(smx_simcall_t req, int value)
{
if (MC_process_is_self(&mc_model_checker->process)) {
return;
}
- MC_process_refresh_simix_processes(&mc_model_checker->process);
+ MC_process_smx_refresh(&mc_model_checker->process);
unsigned i;
mc_smx_process_info_t pi = NULL;
xbt_die("Could not find the request");
}
-
-void mc_smx_process_info_clear(mc_smx_process_info_t p)
-{
- // Nothing yet
-}
MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4,
} e_mc_process_cache_flags_t ;
-struct s_mc_smx_process_info {
- void* address;
- struct s_smx_process copy;
-};
-
typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t;
/** Representation of a process
size_t object_infos_size;
int memory_file;
+ /** Copy of `simix_global->process_list`
+ *
+ * See mc_smx.c.
+ */
xbt_dynar_t smx_process_infos;
+
+ /** Copy of `simix_global->process_to_destroy`
+ *
+ * See mc_smx.c.
+ */
xbt_dynar_t smx_old_process_infos;
/** State of the cache (which variables are up to date) */
* */
void MC_process_refresh_malloc_info(mc_process_t process);
-void MC_process_refresh_simix_processes(mc_process_t process);
-
static inline
bool MC_process_is_self(mc_process_t process)
{
void* local, const void* remote, size_t len,
int process_index);
+const void* MC_process_read_simple(mc_process_t process,
+ void* local, const void* remote, size_t len);
+
/** Write data to a process memory
*
* @param process the process
*/
dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
-// ***** Things to move somewhere else:
-
-smx_process_t MC_process_get_issuer(mc_process_t process, smx_simcall_t req);
-
-void MC_simcall_handle(smx_simcall_t req, int value);
-
-void mc_smx_process_info_clear(mc_smx_process_info_t p);
-
-static inline
-xbt_dynar_t mc_smx_process_info_list_new()
-{
- return xbt_dynar_new(
- sizeof(s_mc_smx_process_info_t), (void_f_pvoid_t) &mc_smx_process_info_clear);
-}
-
SG_END_DECL()
#endif
#include "mc_private.h"
#include "mc_model_checker.h"
#include "mc_state.h"
+#include "mc_smx.h"
#endif
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,
mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
int value = 0;
smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
- const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
const int pid = issuer->pid;
// Serialization the (pid, value) pair:
#include "mc_request.h"
#include "mc_safety.h"
#include "mc_private.h"
+#include "mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
"Logging specific to MC (request)");
// FIXME, host_get_name
// FIXME, buffer access (issuer->name, issuer->smx_host)
- smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+ smx_process_t issuer = MC_smx_simcall_get_issuer(req);
switch (req->call) {
case SIMCALL_COMM_ISEND:
if (issuer->smx_host)
args =
bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
- MSG_host_get_name(issuer->smx_host), issuer->name,
+ MC_smx_process_get_host_name(issuer), issuer->name,
p, bs);
else
args =
if (issuer->smx_host)
args =
bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
- MSG_host_get_name(issuer->smx_host), issuer->name,
+ MC_smx_process_get_host_name(issuer), issuer->name,
p, bs);
else
args =
p = pointer_to_string(act);
args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
act->comm.src_proc ? act->comm.src_proc->pid : 0,
- act->comm.src_proc ? MSG_host_get_name(act->comm.src_proc->
- smx_host) : "",
+ // TODO, get process
+ act->comm.src_proc ? MC_smx_process_get_host_name(MC_smx_resolve_process(act->comm.src_proc)) : "",
act->comm.src_proc ? act->comm.src_proc->name : "",
act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
- act->comm.dst_proc ? MSG_host_get_name(act->comm.dst_proc->
- smx_host) : "",
+ // TOTO get process
+ act->comm.dst_proc ? MC_smx_process_get_host_name(MC_smx_resolve_process(act->comm.dst_proc)) : "",
act->comm.dst_proc ? act->comm.dst_proc->name : "");
}
break;
} else {
type = xbt_strdup("Test TRUE");
p = pointer_to_string(act);
+ // TODO, get process, get process name
args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
act->comm.src_proc->pid, act->comm.src_proc->name,
- MSG_host_get_name(act->comm.src_proc->smx_host),
+ MC_smx_process_get_host_name(MC_smx_resolve_process(act->comm.src_proc)),
act->comm.dst_proc->pid, act->comm.dst_proc->name,
- MSG_host_get_name(act->comm.dst_proc->smx_host));
+ MC_smx_process_get_host_name(MC_smx_resolve_process(act->comm.dst_proc)));
}
break;
}
if (args != NULL) {
+ // FIXME, get process name
str =
bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
- MSG_host_get_name(issuer->smx_host), issuer->name,
+ MC_smx_process_get_host_name(issuer), issuer->name,
type, args);
} else {
+ // FIXME, get process name
str =
bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
- MSG_host_get_name(issuer->smx_host), issuer->name,
+ MC_smx_process_get_host_name(issuer), issuer->name,
type);
}
char *MC_request_get_dot_output(smx_simcall_t req, int value)
{
- // TODO, remote access to MSG_host_get_name(issuer->smx_host)
-
char *str = NULL, *label = NULL;
smx_synchro_t act = NULL;
- const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
switch (req->call) {
case SIMCALL_COMM_ISEND:
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] iSend", issuer->pid,
- MSG_host_get_name(issuer->smx_host));
+ MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] iSend", issuer->pid);
break;
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] iRecv", issuer->pid,
- MSG_host_get_name(issuer->smx_host));
+ MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] iRecv", issuer->pid);
break;
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
- MSG_host_get_name(issuer->smx_host));
+ MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
} else {
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
- MSG_host_get_name(issuer->smx_host),
+ MC_smx_process_get_host_name(issuer),
act->comm.src_proc ? act->comm.src_proc->pid : 0,
act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
else
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] Test FALSE", issuer->pid,
- MSG_host_get_name(issuer->smx_host));
+ MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] Test FALSE", issuer->pid);
} else {
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] Test TRUE", issuer->pid,
- MSG_host_get_name(issuer->smx_host));
+ MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] Test TRUE", issuer->pid);
}
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
- MSG_host_get_name(issuer->smx_host), value + 1,
+ MC_smx_process_get_host_name(issuer), value + 1,
xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
else
label =
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
- MSG_host_get_name(issuer->smx_host));
+ MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
} else {
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
- MSG_host_get_name(issuer->smx_host), value + 1,
+ MC_smx_process_get_host_name(issuer), value + 1,
xbt_dynar_length(simcall_comm_testany__get__comms(req)));
else
label =
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
- MSG_host_get_name(issuer->smx_host), value);
+ MC_smx_process_get_host_name(issuer), value);
else
label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
break;
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
- MSG_host_get_name(issuer->smx_host));
+ MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
break;
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
- MSG_host_get_name(issuer->smx_host));
+ MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
break;
#include "mc_safety.h"
#include "mc_private.h"
#include "mc_record.h"
+#include "mc_smx.h"
#include "xbt/mmalloc/mmprivate.h"
while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
if (mc_reduce_kind == e_mc_reduce_dpor) {
req = MC_state_get_internal_request(state);
- const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
} else {
- const smx_process_t previous_issuer = MC_process_get_issuer(&mc_model_checker->process, MC_state_get_internal_request(prev_state));
+ const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
req->call, issuer->pid, state->num,
MC_state_get_internal_request(prev_state)->call,
--- /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 <assert.h>
+
+#include <xbt/log.h>
+
+#include "simix/smx_private.h"
+
+#include "mc_smx.h"
+#include "mc_model_checker.h"
+
+xbt_dynar_t MC_smx_process_info_list_new(void)
+{
+ return xbt_dynar_new(
+ sizeof(s_mc_smx_process_info_t), NULL);
+}
+
+static inline
+bool is_in_dynar(smx_process_t p, xbt_dynar_t dynar)
+{
+ return (uintptr_t) p >= (uintptr_t) dynar->data
+ && (uintptr_t) p < ((uintptr_t) dynar->data + dynar->used * dynar->elmsize);
+}
+
+static inline
+mc_smx_process_info_t MC_smx_process_get_info(smx_process_t p)
+{
+ assert(is_in_dynar(p, mc_model_checker->process.smx_process_infos)
+ || is_in_dynar(p, mc_model_checker->process.smx_old_process_infos));
+ mc_smx_process_info_t process_info =
+ (mc_smx_process_info_t)
+ ((char*) p - offsetof(s_mc_smx_process_info_t, copy));
+ return process_info;
+}
+
+/** Load the remote swag of processes into a dynar
+ *
+ * @param process MCed process
+ * @param target Local dynar (to be filled with copies of `s_smx_process_t`)
+ * @param remote_swag Address of the process SWAG in the remote list
+ */
+static void MC_process_refresh_simix_process_list(
+ mc_process_t process,
+ xbt_dynar_t target, xbt_swag_t remote_swag)
+{
+ // swag = REMOTE(*simix_global->process_list)
+ s_xbt_swag_t swag;
+ MC_process_read(process, MC_PROCESS_NO_FLAG, &swag, remote_swag, sizeof(swag),
+ MC_PROCESS_INDEX_ANY);
+
+ smx_process_t p;
+ xbt_dynar_reset(target);
+
+ // Load each element of the dynar from the MCed process:
+ int i = 0;
+ for (p = swag.head; p; ++i) {
+
+ s_mc_smx_process_info_t info;
+ info.address = p;
+ info.hostname = NULL;
+ MC_process_read(process, MC_PROCESS_NO_FLAG,
+ &info.copy, p, sizeof(info.copy), MC_PROCESS_INDEX_ANY);
+ xbt_dynar_push(target, &info);
+
+ // Lookup next process address:
+ p = xbt_swag_getNext(&info.copy, swag.offset);
+ }
+ assert(i == swag.count);
+}
+
+void MC_process_smx_refresh(mc_process_t process)
+{
+ if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
+ return;
+
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+
+ // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
+
+ // simix_global_p = REMOTE(simix_global);
+ smx_global_t simix_global_p;
+ MC_process_read_variable(process, "simix_global", &simix_global_p, sizeof(simix_global_p));
+
+ // simix_global = REMOTE(*simix_global)
+ s_smx_global_t simix_global;
+ MC_process_read(process, MC_PROCESS_NO_FLAG, &simix_global, simix_global_p, sizeof(simix_global),
+ MC_PROCESS_INDEX_ANY);
+
+ MC_process_refresh_simix_process_list(
+ process, process->smx_process_infos, simix_global.process_list);
+ MC_process_refresh_simix_process_list(
+ process, process->smx_old_process_infos, simix_global.process_to_destroy);
+
+ process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
+ mmalloc_set_current_heap(heap);
+}
+
+/** Get the issuer of a simcall (`req->issuer`)
+ *
+ * In split-process mode, it does the black magic necessary to get an address
+ * of a (shallow) copy of the data structure the issuer SIMIX process in the local
+ * address space.
+ *
+ * @param process the MCed process
+ * @param req the simcall (copied in the local process)
+ */
+smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req)
+{
+ if (MC_process_is_self(&mc_model_checker->process))
+ 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;
+
+ unsigned i;
+ mc_smx_process_info_t p;
+
+ // Lookup by address:
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, p)
+ if (p->address == address)
+ return &p->copy;
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_old_process_infos, i, p)
+ if (p->address == address)
+ return &p->copy;
+
+ xbt_die("Issuer not found");
+}
+
+smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address)
+{
+ if (MC_process_is_self(&mc_model_checker->process))
+ return process_remote_address;
+
+ mc_smx_process_info_t process_info = MC_smx_resolve_process_info(process_remote_address);
+ if (process_info)
+ return &process_info->copy;
+ else
+ return NULL;
+}
+
+mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address)
+{
+ if (MC_process_is_self(&mc_model_checker->process))
+ xbt_die("No process_info for local process is not enabled.");
+
+ unsigned index;
+ mc_smx_process_info_t process_info;
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, index, process_info)
+ if (process_info->address == process_remote_address)
+ return process_info;
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_old_process_infos, index, process_info)
+ if (process_info->address == process_remote_address)
+ return process_info;
+ xbt_die("Process info not found");
+}
+
+const char* MC_smx_process_get_host_name(smx_process_t p)
+{
+ if (MC_process_is_self(&mc_model_checker->process))
+ return SIMIX_host_get_name(p->smx_host);
+
+ mc_process_t process = &mc_model_checker->process;
+
+ // Currently, smx_host_t = xbt_dictelm_t.
+ // TODO, add an static_assert on this if switching to C++
+ // The host name is host->key and the host->key_len==strlen(host->key).
+ s_xbt_dictelm_t host_copy;
+ mc_smx_process_info_t info = MC_smx_process_get_info(p);
+ if (!info->hostname) {
+
+ // Read the hostname from the MCed process:
+ MC_process_read_simple(process, &host_copy, p->smx_host, sizeof(host_copy));
+ int len = host_copy.key_len + 1;
+ char hostname[len];
+ MC_process_read_simple(process, hostname, host_copy.key, len);
+
+ // Lookup the host name in the dictionary (or create it):
+ xbt_dictelm_t elt = xbt_dict_get_elm_or_null(mc_model_checker->hosts, hostname);
+ if (!elt) {
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+ xbt_dict_set(mc_model_checker->hosts, hostname, NULL, NULL);
+ elt = xbt_dict_get_elm_or_null(mc_model_checker->hosts, hostname);
+ assert(elt);
+ mmalloc_set_current_heap(heap);
+ }
+
+ info->hostname = elt->key;
+ }
+ return info->hostname;
+}
--- /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 MC_SMX_H
+#define MC_SMX_H
+
+#include <stddef.h>
+
+#include <xbt/log.h>
+#include <simgrid/simix.h>
+
+#include "mc_process.h"
+#include "mc_protocol.h"
+
+/** @file
+ * @brief (Cross-process, MCer/MCed) Access to SMX structures
+ *
+ * We copy some C data structure from the MCed process in the MCer process.
+ * This is implemented by:
+ *
+ * - `model_checker->process.smx_process_infos`
+ * (copy of `simix_global->process_list`);
+ *
+ * - `model_checker->process.smx_old_process_infos`
+ * (copy of `simix_global->process_to_destroy`);
+ *
+ * - `model_checker->hostnames`.
+ *
+ * The process lists are currently refreshed each time MCed code is executed.
+ * We don't try to give a persistent MCer address for a given MCed process.
+ * For this reason, a MCer mc_process_t is currently not reusable after
+ * MCed code.
+ */
+
+SG_BEGIN_DECL()
+
+struct s_mc_smx_process_info {
+ /** MCed address of the process */
+ void* address;
+ /** (Flat) Copy of the process data structure */
+ struct s_smx_process copy;
+ /** Hostname (owned by `mc_modelchecker->hostnames`) */
+ char* hostname;
+};
+
+xbt_dynar_t MC_smx_process_info_list_new(void);
+
+void MC_process_smx_refresh(mc_process_t process);
+
+/** Get the issuer of a simcall (`req->issuer`)
+ *
+ * In split-process mode, it does the black magic necessary to get an address
+ * of a (shallow) copy of the data structure the issuer SIMIX process in the local
+ * address space.
+ *
+ * @param process the MCed process
+ * @param req the simcall (copied in the local process)
+ */
+smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req);
+
+const char* MC_smx_process_get_host_name(smx_process_t p);
+
+#define MC_EACH_SIMIX_PROCESS(process, code) \
+ if (MC_process_is_self(&mc_model_checker->process)) { \
+ xbt_swag_foreach(process, simix_global->process_list) { \
+ code; \
+ } \
+ } else { \
+ MC_process_smx_refresh(&mc_model_checker->process); \
+ unsigned int _smx_process_index; \
+ mc_smx_process_info_t _smx_process_info; \
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, _smx_process_index, _smx_process_info) { \
+ smx_process_t process = &_smx_process_info->copy; \
+ code; \
+ } \
+ }
+
+/** Execute a given simcall */
+void MC_simcall_handle(smx_simcall_t req, int value);
+
+
+
+/* ***** Resolve (local/MCer structure from remote/MCed addresses) ***** */
+
+/** Get a local copy of the process from the process remote address */
+smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address);
+
+/** Get the process info structure from the process remote address */
+mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address);
+
+
+
+SG_END_DECL()
+
+#endif
#include "mc_request.h"
#include "mc_private.h"
#include "mc_comm_pattern.h"
+#include "mc_smx.h"
static void copy_incomplete_communications_pattern(mc_state_t state) {
int i;
if (value != random_max) {
MC_EACH_SIMIX_PROCESS(process,
procstate = &state->proc_status[process->pid];
- const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
if (process->pid == issuer->pid) {
procstate->state = MC_MORE_INTERLEAVE;
break;
