From b08e93079ce626559903d763ea5c79d3de220a24 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 21 May 2015 16:15:17 +0200 Subject: [PATCH 1/1] [mc] Move cross process reading support for SBT structure in a separate file --- buildtools/Cmake/DefinePackages.cmake | 2 ++ src/mc/mc_base.cpp | 2 ++ src/mc/mc_comm_pattern.cpp | 7 ++++-- src/mc/mc_process.cpp | 27 -------------------- src/mc/mc_process.h | 5 ---- src/mc/mc_request.cpp | 23 +++++++++-------- src/mc/mc_state.cpp | 25 ++++++++++--------- src/mc/mc_xbt.cpp | 36 +++++++++++++++++++++++++++ src/mc/mc_xbt.hpp | 22 ++++++++++++++++ 9 files changed, 93 insertions(+), 56 deletions(-) create mode 100644 src/mc/mc_xbt.cpp create mode 100644 src/mc/mc_xbt.hpp diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 836b430f7b..9efb8bf973 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -649,6 +649,8 @@ set(MC_SRC 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 diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 008f129bd8..bc0e31470c 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -22,7 +22,9 @@ #include "mc_server.h" #endif +#ifdef HAVE_MC using simgrid::mc::remote; +#endif extern "C" { diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp index a5b6e49f5e..f63a529634 100644 --- a/src/mc/mc_comm_pattern.cpp +++ b/src/mc/mc_comm_pattern.cpp @@ -11,6 +11,9 @@ #include "mc_comm_pattern.h" #include "mc_smx.h" +#include "mc_xbt.hpp" + +using simgrid::mc::remote; extern "C" { @@ -125,8 +128,8 @@ void MC_handle_comm_pattern( 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); } diff --git a/src/mc/mc_process.cpp b/src/mc/mc_process.cpp index 476a1a9d45..66bb067f5d 100644 --- a/src/mc/mc_process.cpp +++ b/src/mc/mc_process.cpp @@ -593,30 +593,3 @@ void Process::clear_bytes(remote_ptr address, size_t len) } } - -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; -} - -} diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h index c21e951b7b..703dd555e7 100644 --- a/src/mc/mc_process.h +++ b/src/mc/mc_process.h @@ -176,11 +176,6 @@ int open_vm(pid_t pid, int flags); 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() diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp index e28f11983f..27d74e31a2 100644 --- a/src/mc/mc_request.cpp +++ b/src/mc/mc_request.cpp @@ -10,6 +10,7 @@ #include "mc_safety.h" #include "mc_private.h" #include "mc_smx.h" +#include "mc_xbt.hpp" using simgrid::mc::remote; @@ -374,8 +375,8 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req &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)", @@ -395,8 +396,8 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req 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; @@ -502,15 +503,17 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) 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; @@ -610,8 +613,8 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) } 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, diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index f3b35cdf6e..208187ed24 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -13,6 +13,7 @@ #include "mc_private.h" #include "mc_comm_pattern.h" #include "mc_smx.h" +#include "mc_xbt.hpp" using simgrid::mc::remote; @@ -107,8 +108,8 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, 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); @@ -119,8 +120,8 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, 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); @@ -192,8 +193,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( 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; @@ -202,8 +203,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( } 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) @@ -215,8 +216,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( 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; @@ -225,8 +226,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( } 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) diff --git a/src/mc/mc_xbt.cpp b/src/mc/mc_xbt.cpp new file mode 100644 index 0000000000..7742139b8a --- /dev/null +++ b/src/mc/mc_xbt.cpp @@ -0,0 +1,36 @@ +/* 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 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 addr) +{ + if (!addr) + return 0; + unsigned long res; + as.read_bytes(&res, sizeof(res), + remote(&((xbt_dynar_t)addr.address())->used)); + return res; +} + +} +} diff --git a/src/mc/mc_xbt.hpp b/src/mc/mc_xbt.hpp new file mode 100644 index 0000000000..530319516e --- /dev/null +++ b/src/mc/mc_xbt.hpp @@ -0,0 +1,22 @@ +/* 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 addr, size_t i, size_t len); +std::size_t read_length(AddressSpace const& as, remote_ptr addr); + +} +} + +#endif -- 2.30.2