src/mc/mc_server.h
src/mc/mc_smx.h
src/mc/mc_smx.cpp
+ src/mc/mc_xbt.hpp
+ src/mc/mc_xbt.cpp
)
set(MC_SIMGRID_MC_SRC
#include "mc_server.h"
#endif
+#ifdef HAVE_MC
using simgrid::mc::remote;
+#endif
extern "C" {
#include "mc_comm_pattern.h"
#include "mc_smx.h"
+#include "mc_xbt.hpp"
+
+using simgrid::mc::remote;
extern "C" {
comm_addr = simcall_comm_wait__get__comm(req);
else
// comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):
- MC_process_read_dynar_element(&mc_model_checker->process(), &comm_addr,
- simcall_comm_waitany__get__comms(req), value, sizeof(comm_addr));
+ simgrid::mc::read_element(mc_model_checker->process(), &comm_addr,
+ remote(simcall_comm_waitany__get__comms(req)), value, sizeof(comm_addr));
MC_complete_comm_pattern(pattern, comm_addr,
MC_smx_simcall_get_issuer(req)->pid, backtracking);
}
}
}
-
-extern "C" {
-
-const void* MC_process_read_dynar_element(mc_process_t process,
- void* local, const void* remote_dynar, size_t i, size_t len)
-{
- s_xbt_dynar_t d;
- process->read_bytes(&d, sizeof(d), remote(remote_dynar));
- if (i >= d.used)
- xbt_die("Out of bound index %zi/%lu", i, d.used);
- if (len != d.elmsize)
- xbt_die("Bad size in MC_process_read_dynar_element");
- process->read_bytes(local, len, remote(xbt_dynar_get_ptr(&d, i)));
- return local;
-}
-
-unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar)
-{
- if (!remote_dynar)
- return 0;
- unsigned long res;
- process->read_bytes(&res, sizeof(res),
- remote(&((xbt_dynar_t)remote_dynar)->used));
- return res;
-}
-
-}
SG_BEGIN_DECL()
-XBT_INTERNAL const void* MC_process_read_dynar_element(mc_process_t process,
- void* local, const void* remote_dynar, size_t i, size_t len);
-XBT_INTERNAL unsigned long MC_process_read_dynar_length(mc_process_t process,
- const void* remote_dynar);
-
XBT_INTERNAL void MC_invalidate_cache(void);
SG_END_DECL()
#include "mc_safety.h"
#include "mc_private.h"
#include "mc_smx.h"
+#include "mc_xbt.hpp"
using simgrid::mc::remote;
&comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req)));
if (!xbt_dynar_is_empty(&comms)) {
smx_synchro_t remote_sync;
- MC_process_read_dynar_element(&mc_model_checker->process(),
- &remote_sync, simcall_comm_waitany__get__comms(req), value,
+ read_element(mc_model_checker->process(),
+ &remote_sync, remote(simcall_comm_waitany__get__comms(req)), value,
sizeof(remote_sync));
char* p = pointer_to_string(remote_sync);
args = bprintf("comm=%s (%d of %lu)",
type = "TestAny";
args =
bprintf("(%d of %lu)", value + 1,
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_testany__get__comms(req)));
+ read_length(mc_model_checker->process(),
+ remote(simcall_comm_testany__get__comms(req))));
}
break;
break;
case SIMCALL_COMM_WAITANY: {
- MC_process_read_dynar_element(
- &mc_model_checker->process(), &remote_act, simcall_comm_waitany__get__comms(req),
+ read_element(
+ mc_model_checker->process(), &remote_act,
+ remote(simcall_comm_waitany__get__comms(req)),
idx, sizeof(remote_act));
}
break;
case SIMCALL_COMM_TESTANY: {
- MC_process_read_dynar_element(
- &mc_model_checker->process(), &remote_act, simcall_comm_testany__get__comms(req),
+ read_element(
+ mc_model_checker->process(), &remote_act,
+ remote(simcall_comm_testany__get__comms(req)),
idx, sizeof(remote_act));
}
break;
}
case SIMCALL_COMM_WAITANY: {
- unsigned long comms_size = MC_process_read_dynar_length(
- &mc_model_checker->process(), simcall_comm_waitany__get__comms(req));
+ unsigned long comms_size = read_length(
+ mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));
if (issuer->smx_host)
label =
bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
#include "mc_private.h"
#include "mc_comm_pattern.h"
#include "mc_smx.h"
+#include "mc_xbt.hpp"
using simgrid::mc::remote;
case SIMCALL_COMM_WAITANY:
state->internal_req.call = SIMCALL_COMM_WAIT;
state->internal_req.issuer = req->issuer;
- MC_process_read_dynar_element(&mc_model_checker->process(),
- &state->internal_comm, simcall_comm_waitany__get__comms(req),
+ read_element(mc_model_checker->process(),
+ &state->internal_comm, remote(simcall_comm_waitany__get__comms(req)),
value, sizeof(state->internal_comm));
simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
simcall_comm_wait__set__timeout(&state->internal_req, 0);
state->internal_req.issuer = req->issuer;
if (value > 0)
- MC_process_read_dynar_element(&mc_model_checker->process(),
- &state->internal_comm, simcall_comm_testany__get__comms(req),
+ read_element(mc_model_checker->process(),
+ &state->internal_comm, remote(simcall_comm_testany__get__comms(req)),
value, sizeof(state->internal_comm));
simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
case SIMCALL_COMM_WAITANY:
*value = -1;
while (procstate->interleave_count <
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_waitany__get__comms(&process->simcall))) {
+ read_length(mc_model_checker->process(),
+ remote(simcall_comm_waitany__get__comms(&process->simcall)))) {
if (MC_request_is_enabled_by_idx
(&process->simcall, procstate->interleave_count++)) {
*value = procstate->interleave_count - 1;
}
if (procstate->interleave_count >=
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_waitany__get__comms(&process->simcall)))
+ simgrid::mc::read_length(mc_model_checker->process(),
+ simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall))))
procstate->state = MC_DONE;
if (*value != -1)
unsigned start_count = procstate->interleave_count;
*value = -1;
while (procstate->interleave_count <
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_testany__get__comms(&process->simcall))) {
+ read_length(mc_model_checker->process(),
+ remote(simcall_comm_testany__get__comms(&process->simcall)))) {
if (MC_request_is_enabled_by_idx
(&process->simcall, procstate->interleave_count++)) {
*value = procstate->interleave_count - 1;
}
if (procstate->interleave_count >=
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_testany__get__comms(&process->simcall)))
+ read_length(mc_model_checker->process(),
+ remote(simcall_comm_testany__get__comms(&process->simcall))))
procstate->state = MC_DONE;
if (*value != -1 || start_count == 0)
--- /dev/null
+/* Copyright (c) 2014-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 "mc/AddressSpace.hpp"
+#include "mc_xbt.hpp"
+
+namespace simgrid {
+namespace mc {
+
+void read_element(AddressSpace const& as,
+ void* local, remote_ptr<s_xbt_dynar_t> addr, size_t i, size_t len)
+{
+ s_xbt_dynar_t d;
+ as.read_bytes(&d, sizeof(d), addr);
+ if (i >= d.used)
+ xbt_die("Out of bound index %zi/%lu", i, d.used);
+ if (len != d.elmsize)
+ xbt_die("Bad size in simgrid::mc::read_element");
+ as.read_bytes(local, len, remote(xbt_dynar_get_ptr(&d, i)));
+}
+
+std::size_t read_length(AddressSpace const& as, remote_ptr<s_xbt_dynar_t> addr)
+{
+ if (!addr)
+ return 0;
+ unsigned long res;
+ as.read_bytes(&res, sizeof(res),
+ remote(&((xbt_dynar_t)addr.address())->used));
+ return res;
+}
+
+}
+}
--- /dev/null
+/* Copyright (c) 2014-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_XBT_HPP
+#define SIMGRID_MC_XBT_HPP
+
+#include "mc/AddressSpace.hpp"
+
+namespace simgrid {
+namespace mc {
+
+void read_element(AddressSpace const& as,
+ void* local, remote_ptr<s_xbt_dynar_t> addr, size_t i, size_t len);
+std::size_t read_length(AddressSpace const& as, remote_ptr<s_xbt_dynar_t> addr);
+
+}
+}
+
+#endif