CHECK_FUNCTION_EXISTS(vasprintf HAVE_VASPRINTF)
CHECK_FUNCTION_EXISTS(makecontext HAVE_MAKECONTEXT)
CHECK_FUNCTION_EXISTS(mmap HAVE_MMAP)
+CHECK_FUNCTION_EXISTS(process_vm_readv HAVE_PROCESS_VM_READV)
#Check if __thread is defined
execute_process(
set(CONTEXT_UCONTEXT 0)
SET(CONTEXT_THREADS 0)
- SET(HAVE_TRACING 1)
-
- if(enable_tracing)
- SET(HAVE_TRACING 1)
- else()
- SET(HAVE_TRACING 0)
- endif()
if(enable_jedule)
SET(HAVE_JEDULE 1)
src/bindings/java/org/simgrid/trace/Trace.java
)
- if(HAVE_TRACING)
- list(APPEND JMSG_C_SRC ${JTRACE_C_SRC})
- list(APPEND JMSG_JAVA_SRC ${JTRACE_JAVA_SRC})
- else()
- list(APPEND EXTRA_DIST ${JTRACE_C_SRC})
- list(APPEND EXTRA_DIST ${JTRACE_JAVA_SRC})
- endif()
+ list(APPEND JMSG_C_SRC ${JTRACE_C_SRC})
+ list(APPEND JMSG_JAVA_SRC ${JTRACE_JAVA_SRC})
set(LUA_SRC
src/bindings/lua/lua_comm.c
)
set(JEDULE_SRC
- include/instr/jedule/jedule_events.h
- include/instr/jedule/jedule_output.h
- include/instr/jedule/jedule_platform.h
- include/instr/jedule/jedule_sd_binding.h
+ include/simgrid/jedule/jedule_events.h
+ include/simgrid/jedule/jedule_output.h
+ include/simgrid/jedule/jedule_platform.h
+ include/simgrid/jedule/jedule_sd_binding.h
src/instr/jedule/jedule_events.c
src/instr/jedule/jedule_output.c
src/instr/jedule/jedule_platform.c
)
set(MC_SRC
+ src/mc/mc_address_space.h
+ src/mc/mc_address_space.c
src/mc/mc_forward.h
+ src/mc/mc_process.h
+ src/mc/mc_process.c
+ src/mc/mc_unw.h
+ src/mc/mc_unw.c
+ src/mc/mc_unw_vmread.c
src/mc/mc_mmalloc.h
src/mc/mc_model_checker.h
+ src/mc/mc_model_checker.c
src/mc/mc_object_info.h
+ src/mc/mc_object_info.c
src/mc/mc_checkpoint.c
src/mc/mc_snapshot.h
src/mc/mc_snapshot.c
src/mc/mc_page_store.cpp
src/mc/mc_page_snapshot.cpp
src/mc/mc_comm_pattern.h
+ src/mc/mc_comm_pattern.c
src/mc/mc_comm_determinism.c
src/mc/mc_compare.cpp
src/mc/mc_diff.c
src/mc/mc_visited.c
src/mc/mc_memory_map.h
src/mc/memory_map.c
+ src/mc/mc_client.c
+ src/mc/mc_client_api.c
+ src/mc/mc_client.h
+ src/mc/mc_protocol.h
+ 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
+ src/mc/simgrid_mc.cpp)
+
set(headers_to_install
- include/instr/instr.h
- include/msg/datatypes.h
include/msg/msg.h
- include/simdag/datatypes.h
+ include/msg/datatypes.h
include/simdag/simdag.h
+ include/simdag/datatypes.h
+
+ include/simgrid/instr.h
+ include/simgrid/msg.h
+ include/simgrid/simdag.h
include/simgrid.h
include/simgrid/datatypes.h
include/simgrid/modelchecker.h
)
endif()
- if(${HAVE_TRACING})
- set(simgrid_sources
+ set(simgrid_sources
${simgrid_sources}
${TRACING_SRC}
)
- else()
- set(EXTRA_DIST
- ${EXTRA_DIST}
- ${TRACING_SRC}
- )
- endif()
set(simgrid_sources
${simgrid_sources}
/* Define to 1 if mmap is available */
#cmakedefine HAVE_MMAP @HAVE_MMAP@
+/* Define to 1 if process_vm_readv is available */
+#cmakedefine HAVE_PROCESS_VM_READV @HAVE_PROCESS_VM_READV@
+
/* Define to 1 if you have the `getdtablesize' function. */
#cmakedefine HAVE_GETDTABLESIZE @HAVE_GETDTABLESIZE@
/* Define to 1 if you can safely include both <sys/time.h> and <time.h>. */
#cmakedefine TIME_WITH_SYS_TIME @TIME_WITH_SYS_TIME@
- /* Tracing SimGrid */
- #cmakedefine HAVE_TRACING @HAVE_TRACING@
-
/* Tracking of latency bound */
#cmakedefine HAVE_LATENCY_BOUND_TRACKING @HAVE_LATENCY_BOUND_TRACKING@
/* which is incorrect because the message ordering is non-deterministic */
/******************************************************************************/
--#include <msg/msg.h>
++#include <simgrid/msg.h>
#include <simgrid/modelchecker.h>
#define N 3
#include <unistd.h>
#endif
- #include "msg/msg.h"
+ #include "simgrid/msg.h"
#include "mc/mc.h"
#include "xbt/automaton.h"
#include "bugged1_liveness.h"
int r=0;
int cs=0;
-int predR(){
- return r;
-}
-
-int predCS(){
- return cs;
-}
-
#ifdef GARBAGE_STACK
/** Do not use a clean stack */
static void garbage_stack(void) {
int coordinator(int argc, char *argv[])
{
-
int CS_used = 0;
msg_task_t task = NULL, answer = NULL;
xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
int main(int argc, char *argv[])
{
-
MSG_init(&argc, argv);
-
char **options = &argv[1];
- MSG_config("model-check/property","promela_bugged1_liveness");
- MC_automaton_new_propositional_symbol("r", &predR);
- MC_automaton_new_propositional_symbol("cs", &predCS);
+ MC_automaton_new_propositional_symbol_pointer("r", &r);
+ MC_automaton_new_propositional_symbol_pointer("cs", &cs);
const char* platform_file = options[0];
const char* application_file = options[1];
-
+
MSG_create_environment(platform_file);
+
MSG_function_register("coordinator", coordinator);
MSG_function_register("client", raw_client);
MSG_launch_application(application_file);
+
MSG_main();
return 0;
/* which is incorrect because the message ordering is non-deterministic */
/******************************************************************************/
--#include <msg/msg.h>
++#include <simgrid/msg.h>
#include <simgrid/modelchecker.h>
#define N 3
/* LTL property checked : !(GFcs) */
/******************************************************************************/
- #include "msg/msg.h"
+ #include "simgrid/msg.h"
#include "mc/mc.h"
#include "xbt/automaton.h"
#include "bugged2_liveness.h"
int cs = 0;
-int predCS(){
- return cs;
-}
-
-
int coordinator(int argc, char **argv);
int client(int argc, char **argv);
MSG_init(&argc, argv);
- MSG_config("model-check/property","promela_bugged2_liveness");
- MC_automaton_new_propositional_symbol("cs", &predCS);
+ MC_automaton_new_propositional_symbol_pointer("cs", &cs);
MSG_create_environment("../msg_platform.xml");
MSG_function_register("coordinator", coordinator);
/* same buffer for reception (task1). */
/******************************************************************************/
--#include <msg/msg.h>
++#include <simgrid/msg.h>
#include <simgrid/modelchecker.h>
XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "this example");
/* --cfg=model-check/max_depth:) is reached. */
/******************************************************************************/
--#include <msg/msg.h>
++#include <simgrid/msg.h>
#include <simgrid/modelchecker.h>
#define N 2
/* 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 <simgrid/simix.h>
#include "mc_base.h"
#include "../simix/smx_private.h"
#include "mc_record.h"
+#ifdef HAVE_MC
+#include "mc_process.h"
+#include "mc_model_checker.h"
+#include "mc_protocol.h"
+#include "mc_smx.h"
+#include "mc_server.h"
+#endif
+
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
-/**
- * \brief Schedules all the process that are ready to run
- */
void MC_wait_for_requests(void)
{
++#ifdef HAVE_MC
+ if (mc_mode == MC_MODE_SERVER) {
+ MC_server_wait_client(&mc_model_checker->process);
+ return;
+ }
++#endif
+
smx_process_t process;
smx_simcall_t req;
unsigned int iter;
{
unsigned int index = 0;
smx_synchro_t act = 0;
- smx_mutex_t mutex = NULL;
+#ifdef HAVE_MC
+ s_smx_synchro_t temp_synchro;
+#endif
switch (req->call) {
case SIMCALL_NONE:
case SIMCALL_COMM_WAIT:
/* FIXME: check also that src and dst processes are not suspended */
act = simcall_comm_wait__get__comm(req);
+
+#ifdef HAVE_MC
+ // Fetch from MCed memory:
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_synchro, act, sizeof(temp_synchro),
+ MC_PROCESS_INDEX_ANY);
+ act = &temp_synchro;
+ }
+#endif
+
if (simcall_comm_wait__get__timeout(req) >= 0) {
/* If it has a timeout it will be always be enabled, because even if the
* communication is not ready, it can timeout and won't block. */
}
return (act->comm.src_proc && act->comm.dst_proc);
- case SIMCALL_COMM_WAITANY:
- /* Check if it has at least one communication ready */
- xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act)
+ case SIMCALL_COMM_WAITANY: {
+#ifdef HAVE_MC
+ // Read dynar:
+ s_xbt_dynar_t comms;
+ MC_process_read_simple(&mc_model_checker->process,
+ &comms, simcall_comm_waitany__get__comms(req), sizeof(comms));
+ // Read dynar buffer:
+ assert(comms.elmsize == sizeof(act));
+ size_t buffer_size = comms.elmsize * comms.used;
+ char buffer[buffer_size];
+ MC_process_read_simple(&mc_model_checker->process,
+ buffer, comms.data, sizeof(buffer));
+#endif
+
+#ifdef HAVE_MC
+ for (index = 0; index < comms.used; ++index) {
+ memcpy(&act, buffer + comms.elmsize * index, sizeof(act));
+#else
+ xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) {
+#endif
+
+#ifdef HAVE_MC
+ // Fetch from MCed memory:
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_synchro, act, sizeof(temp_synchro),
+ MC_PROCESS_INDEX_ANY);
+ act = &temp_synchro;
+ }
+#endif
+
if (act->comm.src_proc && act->comm.dst_proc)
return TRUE;
+ }
return FALSE;
+ }
- case SIMCALL_MUTEX_LOCK:
- mutex = simcall_mutex_lock__get__mutex(req);
+ case SIMCALL_MUTEX_LOCK: {
+ smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
+#ifdef HAVE_MC
+ s_smx_mutex_t temp_mutex;
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_mutex, mutex, sizeof(temp_mutex),
+ MC_PROCESS_INDEX_ANY);
+ mutex = &temp_mutex;
+ }
+#endif
if(mutex->owner == NULL)
return TRUE;
else
- return (mutex->owner->pid == req->issuer->pid);
+#ifdef HAVE_MC
+ // TODO, *(mutex->owner) :/
+ return MC_smx_resolve_process(mutex->owner)->pid ==
+ MC_smx_resolve_process(req->issuer)->pid;
+#else
+ return mutex->owner->pid == req->issuer->pid;
+#endif
+ }
default:
/* The rest of the requests are always enabled */
/* 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 <string.h>
+#include <stdint.h>
+
#include "mc_base.h"
#ifndef _XBT_WIN32
#include <unistd.h>
-#include <sys/types.h>
#include <sys/wait.h>
#include <sys/time.h>
-#include <sys/mman.h>
-#include <libgen.h>
#endif
#include "simgrid/sg_config.h"
#include "xbt/fifo.h"
#include "xbt/automaton.h"
#include "xbt/dict.h"
- #include "mc_server.h"
++#include "mc_record.h"
#ifdef HAVE_MC
-#define UNW_LOCAL_ONLY
++#include "mc_server.h"
#include <libunwind.h>
-
+#include <xbt/mmalloc.h>
-
#include "../xbt/mmalloc/mmprivate.h"
#include "mc_object_info.h"
#include "mc_comm_pattern.h"
#include "mc_snapshot.h"
#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"
+#include "mc_client.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
+e_mc_mode_t mc_mode;
+
double *mc_time = NULL;
#ifdef HAVE_MC
/* Liveness */
xbt_automaton_t _mc_property_automaton = NULL;
-/* Variables */
-mc_object_info_t mc_libsimgrid_info = NULL;
-mc_object_info_t mc_binary_info = NULL;
-
-mc_object_info_t mc_object_infos[2] = { NULL, NULL };
-
-size_t mc_object_infos_size = 2;
-
/* Dot output */
FILE *dot_output = NULL;
const char *colors[13];
}
-static void MC_init_debug_info(void)
+void MC_init()
{
- XBT_INFO("Get debug information ...");
-
- memory_map_t maps = MC_get_memory_map();
-
- /* Get local variables for state equality detection */
- mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
- mc_object_infos[0] = mc_binary_info;
-
- mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0);
- mc_object_infos[1] = mc_libsimgrid_info;
-
- // Use information of the other objects:
- MC_post_process_object_info(mc_binary_info);
- MC_post_process_object_info(mc_libsimgrid_info);
-
- MC_free_memory_map(maps);
- XBT_INFO("Get debug information done !");
+ MC_init_pid(getpid(), -1);
}
-
-mc_model_checker_t mc_model_checker = NULL;
-
-mc_model_checker_t MC_model_checker_new()
+static void MC_init_mode(void)
{
- mc_model_checker_t mc = xbt_new0(s_mc_model_checker_t, 1);
- mc->pages = mc_pages_store_new();
- mc->fd_clear_refs = -1;
- mc->fd_pagemap = -1;
- return mc;
-}
-
-void MC_model_checker_delete(mc_model_checker_t mc) {
- mc_pages_store_delete(mc->pages);
- if(mc->record)
- xbt_dynar_free(&mc->record);
+ if (mc_mode == MC_MODE_NONE) {
+ if (getenv(MC_ENV_SOCKET_FD)) {
+ mc_mode = MC_MODE_CLIENT;
+ } else {
+ mc_mode = MC_MODE_STANDALONE;
+ }
+ }
}
-void MC_init()
+void MC_init_pid(pid_t pid, int socket)
{
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- mc_time = xbt_new0(double, simix_process_maxpid);
-
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+ mc_model_checker = MC_model_checker_new(pid, socket);
- mc_model_checker = MC_model_checker_new();
+ // It's not useful anymore:
+ if (0 && mc_mode == MC_MODE_SERVER) {
+ unsigned long maxpid;
+ MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
+ &maxpid, sizeof(maxpid));
+ simix_process_maxpid = maxpid;
+ }
+
+ mmalloc_set_current_heap(std_heap);
+ mc_time = xbt_new0(double, MC_smx_get_maxpid());
+ mmalloc_set_current_heap(mc_heap);
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
mc_stats = xbt_new0(s_mc_stats_t, 1);
mc_stats->state_size = 1;
- MC_init_memory_map_info();
- MC_init_debug_info(); /* FIXME : get debug information only if liveness verification or visited state reduction */
-
if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0'))
MC_init_dot_output();
MC_SET_STD_HEAP;
- if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination) {
+ if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
/* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
MC_ignore_local_variable("e", "*");
MC_ignore_local_variable("__ex_cleanup", "*");
/* SIMIX */
MC_ignore_global_variable("smx_total_comms");
- MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+ if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
+ /* Those requests are handled on the client side and propagated by message
+ * to the server: */
- smx_process_t process;
- xbt_swag_foreach(process, simix_global->process_list) {
- MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
+ MC_ignore_heap(mc_time, MC_smx_get_maxpid() * sizeof(double));
+
+ smx_process_t process;
+ xbt_swag_foreach(process, simix_global->process_list) {
+ MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
+ }
}
- }
- if (raw_mem_set)
- MC_SET_MC_HEAP;
+ }
+ mmalloc_set_current_heap(heap);
}
/******************************* Core of MC *******************************/
/**************************************************************************/
-static void MC_modelcheck_comm_determinism_init(void)
-{
-
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_init();
-
- if (!mc_mem_set)
- MC_SET_MC_HEAP;
-
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- MC_SET_STD_HEAP;
-
- MC_pre_modelcheck_comm_determinism();
-
- MC_SET_MC_HEAP;
- initial_global_state = xbt_new0(s_mc_global_t, 1);
- initial_global_state->snapshot = MC_take_snapshot(0);
- initial_global_state->initial_communications_pattern_done = 0;
- initial_global_state->recv_deterministic = 1;
- initial_global_state->send_deterministic = 1;
- initial_global_state->recv_diff = NULL;
- initial_global_state->send_diff = NULL;
-
- MC_SET_STD_HEAP;
-
- MC_modelcheck_comm_determinism();
-
- if(mc_mem_set)
- MC_SET_MC_HEAP;
-
-}
-
-static void MC_modelcheck_safety_init(void)
-{
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- _sg_mc_safety = 1;
-
- MC_init();
-
- if (!mc_mem_set)
- MC_SET_MC_HEAP;
-
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- MC_SET_STD_HEAP;
-
- MC_pre_modelcheck_safety();
-
- MC_SET_MC_HEAP;
- /* Save the initial state */
- initial_global_state = xbt_new0(s_mc_global_t, 1);
- initial_global_state->snapshot = MC_take_snapshot(0);
- MC_SET_STD_HEAP;
-
- MC_modelcheck_safety();
-
- if (mc_mem_set)
- MC_SET_MC_HEAP;
-
- xbt_abort();
- //MC_exit();
-}
-
-static void MC_modelcheck_liveness_init()
-{
-
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- _sg_mc_liveness = 1;
-
- MC_init();
-
- if (!mc_mem_set)
- MC_SET_MC_HEAP;
-
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- /* Create the initial state */
- initial_global_state = xbt_new0(s_mc_global_t, 1);
-
- MC_SET_STD_HEAP;
-
- MC_pre_modelcheck_liveness();
-
- /* We're done */
- MC_print_statistics(mc_stats);
- xbt_free(mc_time);
-
- if (mc_mem_set)
- MC_SET_MC_HEAP;
-
-}
-
void MC_do_the_modelcheck_for_real()
{
+ MC_init_mode();
+
+ switch(mc_mode) {
+ default:
+ xbt_die("Unexpected mc mode");
+ break;
+ case MC_MODE_CLIENT:
+ MC_init();
+ MC_client_main_loop();
+ return;
+ case MC_MODE_SERVER:
+ break;
+ case MC_MODE_STANDALONE:
+ MC_init();
+ break;
+ }
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
XBT_INFO("Check communication determinism");
mc_reduce_kind = e_mc_reduce_none;
- MC_modelcheck_comm_determinism_init();
- } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
- if(_sg_mc_termination){
- XBT_INFO("Check non progressive cycles");
+ MC_wait_for_requests();
+ MC_modelcheck_comm_determinism();
+ }
+
+ else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
+ if(_sg_mc_termination)
mc_reduce_kind = e_mc_reduce_none;
- }else{
+ else if (mc_reduce_kind == e_mc_reduce_unset)
+ mc_reduce_kind = e_mc_reduce_dpor;
+ _sg_mc_safety = 1;
+ if (_sg_mc_termination)
+ XBT_INFO("Check non progressive cycles");
+ else
XBT_INFO("Check a safety property");
- }
- MC_modelcheck_safety_init();
- } else {
+ MC_wait_for_requests();
+ MC_modelcheck_safety();
+ }
+
+ else {
if (mc_reduce_kind == e_mc_reduce_unset)
mc_reduce_kind = e_mc_reduce_none;
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_automaton_load(_sg_mc_property_file);
- MC_modelcheck_liveness_init();
+ MC_wait_for_requests();
+ MC_modelcheck_liveness();
}
+
}
int MC_deadlock_check()
{
+ if (mc_mode == MC_MODE_SERVER) {
+ int res;
+ if ((res = MC_protocol_send_simple_message(mc_model_checker->process.socket,
+ MC_MESSAGE_DEADLOCK_CHECK)))
+ xbt_die("Could not check deadlock state");
+ s_mc_int_message_t message;
+ ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message), 0);
+ if (s == -1)
+ xbt_die("Could not receive message");
+ else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
+ xbt_die("%s received unexpected message %s (%i, size=%i) "
+ "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
+ MC_mode_name(mc_mode),
+ MC_message_type_name(message.type), (int) message.type, (int) s,
+ (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
+ );
+ }
+ else
+ return message.value;
+ }
+
int deadlock = FALSE;
smx_process_t process;
if (xbt_swag_size(simix_global->process_list)) {
deadlock = TRUE;
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_request_is_enabled(&process->simcall)) {
+ MC_EACH_SIMIX_PROCESS(process,
+ if (MC_process_is_enabled(process)) {
deadlock = FALSE;
break;
}
- }
+ );
}
return deadlock;
}
-void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) {
-
- switch(call_type) {
- case MC_CALL_TYPE_NONE:
- break;
- case MC_CALL_TYPE_SEND:
- case MC_CALL_TYPE_RECV:
- get_comm_pattern(pattern, req, call_type, backtracking);
- break;
- case MC_CALL_TYPE_WAIT:
- case MC_CALL_TYPE_WAITANY:
- {
- smx_synchro_t current_comm = NULL;
- if (call_type == MC_CALL_TYPE_WAIT)
- current_comm = simcall_comm_wait__get__comm(req);
- else
- current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t);
- complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking);
- }
- break;
- default:
- xbt_die("Unexpected call type %i", (int)call_type);
- }
-
-}
-
-static void MC_restore_communications_pattern(mc_state_t state) {
- mc_list_comm_pattern_t list_process_comm;
- unsigned int cursor, cursor2;
- xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
- list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int);
- }
- mc_comm_pattern_t comm;
- cursor = 0;
- xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms;
- for(int i=0; i<simix_process_maxpid; i++){
- initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
- xbt_dynar_reset(initial_incomplete_process_comms);
- incomplete_process_comms = xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t);
- xbt_dynar_foreach(incomplete_process_comms, cursor2, comm) {
- mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1);
- copy_comm->index = comm->index;
- copy_comm->type = comm->type;
- copy_comm->comm = comm->comm;
- copy_comm->rdv = strdup(comm->rdv);
- copy_comm->data_size = -1;
- copy_comm->data = NULL;
- if(comm->type == SIMIX_COMM_SEND){
- copy_comm->src_proc = comm->src_proc;
- copy_comm->src_host = comm->src_host;
- if(comm->data != NULL){
- copy_comm->data_size = comm->data_size;
- copy_comm->data = xbt_malloc0(comm->data_size);
- memcpy(copy_comm->data, comm->data, comm->data_size);
- }
- }else{
- copy_comm->dst_proc = comm->dst_proc;
- copy_comm->dst_host = comm->dst_host;
- }
- xbt_dynar_push(initial_incomplete_process_comms, ©_comm);
- }
- }
-}
-
/**
* \brief Re-executes from the state at position start all the transitions indicated by
* a given model-checker stack.
*/
void MC_replay(xbt_fifo_t stack)
{
- int raw_mem = (mmalloc_get_current_heap() == mc_heap);
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
int value, count = 1, j;
char *req_str;
MC_SET_MC_HEAP;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- for (j=0; j<simix_process_maxpid; j++) {
+ // int n = xbt_dynar_length(incomplete_communications_pattern);
+ int n = MC_smx_get_maxpid();
+ assert(n == xbt_dynar_length(incomplete_communications_pattern));
+ assert(n == xbt_dynar_length(initial_communications_pattern));
+ for (j=0; j < n ; j++) {
xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
- ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t))->index_comm = 0;
+ xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t)->index_comm = 0;
}
}
if (saved_req) {
/* 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 */
- req = &saved_req->issuer->simcall;
+
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ req = &issuer->simcall;
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = MC_request_to_string(req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
XBT_DEBUG("Replay: %s (%p)", req_str, state);
xbt_free(req_str);
}
/* TODO : handle test and testany simcalls */
e_mc_call_type_t call = MC_CALL_TYPE_NONE;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- call = mc_get_call_type(req);
+ call = MC_get_call_type(req);
- SIMIX_simcall_handle(req, value);
+ MC_simcall_handle(req, value);
MC_SET_MC_HEAP;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- handle_comm_pattern(call, req, value, NULL, 1);
+ MC_handle_comm_pattern(call, req, value, NULL, 1);
MC_SET_STD_HEAP;
-
+
MC_wait_for_requests();
count++;
}
XBT_DEBUG("**** End Replay ****");
-
- if (raw_mem)
- MC_SET_MC_HEAP;
- else
- MC_SET_STD_HEAP;
-
-
+ mmalloc_set_current_heap(heap);
}
void MC_replay_liveness(xbt_fifo_t stack)
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 */
- req = &saved_req->issuer->simcall;
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ req = &issuer->simcall;
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = MC_request_to_string(req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
xbt_free(req_str);
}
}
- SIMIX_simcall_handle(req, value);
+ MC_simcall_handle(req, value);
MC_wait_for_requests();
}
*/
void MC_dump_stack_safety(xbt_fifo_t stack)
{
-
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
MC_show_stack_safety(stack);
MC_SET_MC_HEAP;
while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
- MC_SET_STD_HEAP;
-
- if (raw_mem_set)
- MC_SET_MC_HEAP;
- else
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
}
void MC_show_stack_safety(xbt_fifo_t stack)
{
-
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
int value;
mc_state_t state;
: (NULL)); item = xbt_fifo_get_prev_item(item)) {
req = MC_state_get_executed_request(state, &value);
if (req) {
- req_str = MC_request_to_string(req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
XBT_INFO("%s", req_str);
xbt_free(req_str);
}
}
- if (!raw_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
}
void MC_show_deadlock(smx_simcall_t req)
item = xbt_fifo_get_prev_item(item)) {
req = MC_state_get_executed_request(pair->graph_state, &value);
if (req && req->call != SIMCALL_NONE) {
- req_str = MC_request_to_string(req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
XBT_INFO("%s", req_str);
xbt_free(req_str);
}
void MC_dump_stack_liveness(xbt_fifo_t stack)
{
-
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
mc_pair_t pair;
-
- MC_SET_MC_HEAP;
while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
MC_pair_delete(pair);
- MC_SET_STD_HEAP;
-
- if (raw_mem_set)
- MC_SET_MC_HEAP;
-
+ mmalloc_set_current_heap(heap);
}
void MC_print_statistics(mc_stats_t stats)
{
- xbt_mheap_t previous_heap = mmalloc_get_current_heap();
-
if(_sg_mc_comms_determinism) {
if (!initial_global_state->recv_deterministic && initial_global_state->send_deterministic){
XBT_INFO("******************************************************");
XBT_INFO("%s", initial_global_state->send_diff);
}
}
+
if (stats->expanded_pairs == 0) {
XBT_INFO("Expanded states = %lu", stats->expanded_states);
XBT_INFO("Visited states = %lu", stats->visited_states);
XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
}
XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) {
fprintf(dot_output, "}\n");
fclose(dot_output);
if (_sg_mc_comms_determinism)
XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes");
}
- mmalloc_set_current_heap(previous_heap);
-}
-
-void MC_assert(int prop)
-{
- if (MC_is_active() && !prop) {
- XBT_INFO("**************************");
- XBT_INFO("*** PROPERTY NOT VALID ***");
- XBT_INFO("**************************");
- XBT_INFO("Counter-example execution trace:");
- MC_record_dump_path(mc_stack);
- MC_dump_stack_safety(mc_stack);
- MC_print_statistics(mc_stats);
- xbt_abort();
- }
-}
-
-void MC_cut(void)
-{
- user_max_depth_reached = 1;
+ mmalloc_set_current_heap(heap);
}
void MC_automaton_load(const char *file)
{
-
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if (_mc_property_automaton == NULL)
_mc_property_automaton = xbt_automaton_new();
xbt_automaton_load(_mc_property_automaton, file);
-
- MC_SET_STD_HEAP;
-
- if (raw_mem_set)
- MC_SET_MC_HEAP;
-
+ mmalloc_set_current_heap(heap);
}
-void MC_automaton_new_propositional_symbol(const char *id, void *fct)
+static void register_symbol(xbt_automaton_propositional_symbol_t symbol)
{
+ if (mc_mode != MC_MODE_CLIENT)
+ return;
+ s_mc_register_symbol_message_t message;
+ message.type = MC_MESSAGE_REGISTER_SYMBOL;
+ const char* name = xbt_automaton_propositional_symbol_get_name(symbol);
+ if (strlen(name) + 1 > sizeof(message.name))
+ xbt_die("Symbol is too long");
+ strncpy(message.name, name, sizeof(message.name));
+ message.callback = xbt_automaton_propositional_symbol_get_callback(symbol);
+ message.data = xbt_automaton_propositional_symbol_get_data(symbol);
+ MC_client_send_message(&message, sizeof(message));
+}
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
+{
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if (_mc_property_automaton == NULL)
_mc_property_automaton = xbt_automaton_new();
- xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct);
-
- MC_SET_STD_HEAP;
+ xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct);
+ register_symbol(symbol);
+ mmalloc_set_current_heap(heap);
+}
- if (raw_mem_set)
- MC_SET_MC_HEAP;
+void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value)
+{
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+ xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value);
+ register_symbol(symbol);
+ mmalloc_set_current_heap(heap);
+}
+void MC_automaton_new_propositional_symbol_callback(const char* id,
+ xbt_automaton_propositional_symbol_callback_type callback,
+ void* data, xbt_automaton_propositional_symbol_free_function_type free_function)
+{
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+ xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_callback(
+ _mc_property_automaton, id, callback, data, free_function);
+ register_symbol(symbol);
+ mmalloc_set_current_heap(heap);
}
+// TODO, fix cross-process access (this function is not used)
void MC_dump_stacks(FILE* file)
{
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
int nstack = 0;
stack_region_t current_stack;
unw_word_t off;
do {
const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?";
+#if defined(__x86_64__)
+ unw_word_t rip = 0;
+ unw_word_t rsp = 0;
+ unw_get_reg(&c, UNW_X86_64_RIP, &rip);
+ unw_get_reg(&c, UNW_X86_64_RSP, &rsp);
+ fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
+ nframe, name, rip, rsp);
+#else
fprintf(file, " %i: %s\n", nframe, name);
+#endif
++nframe;
} while(unw_step(&c));
++nstack;
}
-
- if (raw_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(heap);
}
#endif
{
mc_time[process->pid] += amount;
}
+
++#ifdef HAVE_MC
+void MC_report_assertion_error(void)
+{
+ XBT_INFO("**************************");
+ XBT_INFO("*** PROPERTY NOT VALID ***");
+ XBT_INFO("**************************");
+ XBT_INFO("Counter-example execution trace:");
+ MC_record_dump_path(mc_stack);
+ MC_dump_stack_safety(mc_stack);
+ MC_print_statistics(mc_stats);
+}
++#endif
#ifndef MC_PRIVATE_H
#define MC_PRIVATE_H
+#include <sys/types.h>
+
#include "simgrid_config.h"
#include <stdio.h>
#include <stdint.h>
#include "mc/datatypes.h"
#include "xbt/fifo.h"
#include "xbt/config.h"
+
#include "xbt/function_types.h"
#include "xbt/mmalloc.h"
#include "../simix/smx_private.h"
#include "../xbt/mmalloc/mmprivate.h"
#include "xbt/automaton.h"
#include "xbt/hash.h"
- #include "msg/msg.h"
-#include "simgrid/msg.h"
--#include "msg/datatypes.h"
++#include <simgrid/msg.h>
#include "xbt/strbuff.h"
#include "xbt/parmap.h"
#include "mc_forward.h"
+#include "mc_protocol.h"
SG_BEGIN_DECL()
typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function_index_item_t;
-/****************************** Snapshots ***********************************/
-
-extern xbt_dynar_t mc_checkpoint_ignore;
-
/********************************* MC Global **********************************/
+/** Initialisation of the model-checker
+ *
+ * @param pid PID of the target process
+ * @param socket FD for the communication socket **in server mode** (or -1 otherwise)
+ */
+void MC_init_pid(pid_t pid, int socket);
+
extern FILE *dot_output;
extern const char* colors[13];
extern xbt_parmap_t parmap;
void MC_print_statistics(mc_stats_t stats);
-extern char *libsimgrid_path;
-
/********************************** Snapshot comparison **********************************/
typedef struct s_mc_comparison_times{
double nb_processes_comparison_time;
double bytes_used_comparison_time;
double stacks_sizes_comparison_time;
- double binary_global_variables_comparison_time;
- double libsimgrid_global_variables_comparison_time;
+ double global_variables_comparison_time;
double heap_comparison_time;
double stacks_comparison_time;
}s_mc_comparison_times_t, *mc_comparison_times_t;
/********************************** Variables with DWARF **********************************/
-dw_frame_t MC_find_function_by_ip(void* ip);
-mc_object_info_t MC_ip_find_object_info(void* ip);
-
void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
/********************************** Miscellaneous **********************************/
*/
void MC_dump_stacks(FILE* file);
+void MC_report_assertion_error(void);
+
SG_END_DECL()
#endif
--- /dev/null
+/* Copyright (c) 2008-2014. 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_PROCESS_H
+#define MC_PROCESS_H
+
+#include <stdbool.h>
+#include <sys/types.h>
+
+#include "simgrid_config.h"
+
+#include <sys/types.h>
+
+#include <xbt/mmalloc.h>
++
++#ifdef HAVE_MC
+#include "xbt/mmalloc/mmprivate.h"
++#endif
+
+#include "simix/popping_private.h"
+#include "simix/smx_private.h"
+
+#include "mc_forward.h"
+#include "mc_mmalloc.h" // std_heap
+#include "mc_memory_map.h"
+#include "mc_address_space.h"
+#include "mc_protocol.h"
+
+SG_BEGIN_DECL()
+
+int MC_process_vm_open(pid_t pid, int flags);
+
+typedef enum {
+ MC_PROCESS_NO_FLAG = 0,
+ MC_PROCESS_SELF_FLAG = 1,
+} e_mc_process_flags_t;
+
+// Those flags are used to track down which cached information
+// is still up to date and which information needs to be updated.
+typedef enum {
+ MC_PROCESS_CACHE_FLAG_HEAP = 1,
+ MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2,
+ MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4,
+} e_mc_process_cache_flags_t ;
+
+typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t;
+
+/** Representation of a process
+ */
+struct s_mc_process {
+ s_mc_address_space_t address_space;
+ e_mc_process_flags_t process_flags;
+ pid_t pid;
+ int socket;
+ int status;
+ bool running;
+ memory_map_t memory_map;
+ void *maestro_stack_start, *maestro_stack_end;
+ mc_object_info_t libsimgrid_info;
+ mc_object_info_t binary_info;
+ mc_object_info_t* object_infos;
+ 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) */
+ e_mc_process_cache_flags_t cache_flags;
+
+ /** Address of the heap structure in the MCed process. */
+ void* heap_address;
+
+ /** Copy of the heap structure of the process
+ *
+ * This is refreshed with the `MC_process_refresh` call.
+ * This is not used if the process is the current one:
+ * use `MC_process_get_heap_info` in order to use it.
+ */
+ xbt_mheap_t heap;
+
+ /** Copy of the allocation info structure
+ *
+ * This is refreshed with the `MC_process_refresh` call.
+ * This is not used if the process is the current one:
+ * use `MC_process_get_malloc_info` in order to use it.
+ */
+ malloc_info* heap_info;
+
+ // ***** Libunwind-data
+
+ /** Full-featured MC-aware libunwind address space for the process
+ *
+ * This address space is using a mc_unw_context_t
+ * (with mc_process_t/mc_address_space_t and unw_context_t).
+ */
+ unw_addr_space_t unw_addr_space;
+
+ /** Underlying libunwind addres-space
+ *
+ * The `find_proc_info`, `put_unwind_info`, `get_dyn_info_list_addr`
+ * operations of the native MC address space is currently delegated
+ * to this address space (either the local or a ptrace unwinder).
+ */
+ unw_addr_space_t unw_underlying_addr_space;
+
+ /** The corresponding context
+ */
+ void* unw_underlying_context;
+
+ xbt_dynar_t checkpoint_ignore;
+};
+
+bool MC_is_process(mc_address_space_t p);
+
+void MC_process_init(mc_process_t process, pid_t pid, int sockfd);
+void MC_process_clear(mc_process_t process);
+
+/** Refresh the information about the process
+ *
+ * Do not use direclty, this is used by the getters when appropriate
+ * in order to have fresh data.
+ */
+void MC_process_refresh_heap(mc_process_t process);
+
+/** Refresh the information about the process
+ *
+ * Do not use direclty, this is used by the getters when appropriate
+ * in order to have fresh data.
+ * */
+void MC_process_refresh_malloc_info(mc_process_t process);
+
+static inline
+bool MC_process_is_self(mc_process_t process)
+{
+ return process->process_flags & MC_PROCESS_SELF_FLAG;
+}
+
+/* Process memory access: */
+
+/** Read data from a process memory
+ *
+ * @param process the process
+ * @param local local memory address (destination)
+ * @param remote target process memory address (source)
+ * @param len data size
+ */
+const void* MC_process_read(mc_process_t process,
+ e_adress_space_read_flags_t flags,
+ void* local, const void* remote, size_t len,
+ int process_index);
+
+// Simplified versions/wrappers (whould be moved in mc_address_space):
+const void* MC_process_read_simple(mc_process_t process,
+ void* local, const void* remote, size_t len);
+const void* MC_process_read_dynar_element(mc_process_t process,
+ void* local, const void* remote_dynar, size_t i, size_t len);
+unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar);
+
+/** Write data to a process memory
+ *
+ * @param process the process
+ * @param local local memory address (source)
+ * @param remote target process memory address (target)
+ * @param len data size
+ */
+void MC_process_write(mc_process_t process, const void* local, void* remote, size_t len);
+
+void MC_process_clear_memory(mc_process_t process, void* remote, size_t len);
+
+/* Functions, variables of the process: */
+
+mc_object_info_t MC_process_find_object_info(mc_process_t process, const void* addr);
+mc_object_info_t MC_process_find_object_info_exec(mc_process_t process, const void* addr);
+mc_object_info_t MC_process_find_object_info_rw(mc_process_t process, const void* addr);
+
+dw_frame_t MC_process_find_function(mc_process_t process, const void* ip);
+
+void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size);
+char* MC_process_read_string(mc_process_t, void* address);
+
+static inline xbt_mheap_t MC_process_get_heap(mc_process_t process)
+{
+ if (MC_process_is_self(process))
+ return std_heap;
+ if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP))
+ MC_process_refresh_heap(process);
+ return process->heap;
+}
+
+static inline malloc_info* MC_process_get_malloc_info(mc_process_t process)
+{
+ if (MC_process_is_self(process))
+ return std_heap->heapinfo;
+ if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_MALLOC_INFO))
+ MC_process_refresh_malloc_info(process);
+ return process->heap_info;
+}
+
+/** Find (one occurence of) the named variable definition
+ */
+dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
+
+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);
- int pid = saved_req->issuer->pid;
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ const int pid = issuer->pid;
// Serialization the (pid, value) pair:
const char* sep = (item!=start) ? ";" : "";
void MC_record_replay_init()
{
- mc_time = xbt_new0(double, MC_smx_get_maxpid());
+ mc_time = xbt_new0(double, simix_process_maxpid);
}
if (host)
THROW_UNIMPLEMENTED;
- #ifdef HAVE_TRACING
TRACE_msg_task_get_start();
double start_time = MSG_get_clock();
- #endif
/* Sanity check */
xbt_assert(task, "Null pointer for the task storage");
xbt_ex_free(e);
}
- #ifdef HAVE_TRACING
if (ret != MSG_HOST_FAILURE &&
ret != MSG_TRANSFER_FAILURE &&
ret != MSG_TIMEOUT) {
TRACE_msg_task_get_end(start_time, *task);
}
- #endif
MSG_RETURN(ret);
}
MSG_mailbox_put_with_timeout(msg_mailbox_t mailbox, msg_task_t task,
double timeout)
{
- xbt_ex_t e;
msg_error_t ret = MSG_OK;
simdata_task_t t_simdata = NULL;
msg_process_t process = MSG_process_self();
simdata_process_t p_simdata = SIMIX_process_self_get_data(process);
- #ifdef HAVE_TRACING
int call_end = TRACE_msg_task_put_start(task); //must be after CHECK_HOST()
- #endif
/* Prepare the task to send */
t_simdata = task->simdata;
p_simdata->waiting_task = task;
+ xbt_ex_t e;
/* Try to send it by calling SIMIX network layer */
TRY {
smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simix call */
- comm = simcall_comm_isend(SIMIX_process_self(), mailbox,t_simdata->message_size,
+ comm = simcall_comm_isend(SIMIX_process_self(), mailbox,t_simdata->bytes_amount,
t_simdata->rate, task, sizeof(void *),
NULL, NULL, NULL, task, 0);
- #ifdef HAVE_TRACING
- if (TRACE_is_enabled()) {
+ if (TRACE_is_enabled())
simcall_set_category(comm, task->category);
- }
- #endif
t_simdata->comm = comm;
simcall_comm_wait(comm, timeout);
}
p_simdata->waiting_task = NULL;
- #ifdef HAVE_TRACING
if (call_end)
TRACE_msg_task_put_end();
- #endif
MSG_RETURN(ret);
}
#include "smpi/smpi_interface.h"
#include "mc/mc.h"
#include "mc/mc_record.h"
- #include "instr/instr.h"
+ #include "simgrid/instr.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_config, surf,
"About the configuration of simgrid");
"to the command line.\n"
"\n"
"You can also use --help-models to see the details of all models known by this simulator.\n"
- #ifdef HAVE_TRACING
"\n"
"You can also use --help-tracing to see the details of all tracing options known by this simulator.\n"
- #endif
"\n"
"You can also use --help-logs and --help-log-categories to see the details of logging output.\n"
"\n"
surf_optimization_mode_description[k].description);
printf("Both network and CPU models have 'Lazy' as default optimization level\n\n");
shall_exit = 1;
- #ifdef HAVE_TRACING
} else if (!strcmp(argv[i], "--help-tracing")) {
TRACE_help (1);
shall_exit = 1;
- #endif
} else {
argv[j++] = argv[i];
}
xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_hash, NULL);
xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no");
+ /* Set max depth exploration */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/snapshot_fds",
+ "Whether file descriptors must be snapshoted",
+ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_snapshot_fds, NULL);
+ xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/snapshot_fds", "no");
+
/* Set max depth exploration */
xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth",
"Specify the max depth of exploration (default : 1000)",
#include "smx_private.h"
#ifdef HAVE_MC
+#include "mc/mc_process.h"
+#include "mc/mc_model_checker.h"
#endif
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);
[SIMCALL_STORAGE_GET_CONTENT] = "SIMCALL_STORAGE_GET_CONTENT",
[SIMCALL_ASR_GET_PROPERTIES] = "SIMCALL_ASR_GET_PROPERTIES",
[SIMCALL_MC_RANDOM] = "SIMCALL_MC_RANDOM",
+ [SIMCALL_SET_CATEGORY] = "SIMCALL_SET_CATEGORY",
#ifdef HAVE_LATENCY_BOUND_TRACKING
[SIMCALL_COMM_IS_LATENCY_BOUNDED] = "SIMCALL_COMM_IS_LATENCY_BOUNDED",
#endif
- #ifdef HAVE_TRACING
- [SIMCALL_SET_CATEGORY] = "SIMCALL_SET_CATEGORY",
- #endif
-
#ifdef HAVE_MC
[SIMCALL_MC_SNAPSHOT] = "SIMCALL_MC_SNAPSHOT",
[SIMCALL_MC_COMPARE_SNAPSHOTS] = "SIMCALL_MC_COMPARE_SNAPSHOTS",
*/
void SIMIX_simcall_handle(smx_simcall_t simcall, int value) {
XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call));
+ #ifdef HAVE_MC
+ if (mc_model_checker) {
+ mc_model_checker->process.cache_flags = 0;
+ }
+ #endif
SIMCALL_SET_MC_VALUE(simcall, value);
if (simcall->issuer->context->iwannadie && simcall->call != SIMCALL_PROCESS_CLEANUP)
return;
SIMIX_simcall_answer(simcall);
break;
- #ifdef HAVE_LATENCY_BOUND_TRACKING
- case SIMCALL_COMM_IS_LATENCY_BOUNDED:
- simcall->result.i = SIMIX_comm_is_latency_bounded((smx_synchro_t) simcall->args[0].dp);
+ case SIMCALL_SET_CATEGORY:
+ SIMIX_set_category((smx_synchro_t) simcall->args[0].dp, simcall->args[1].cc);
SIMIX_simcall_answer(simcall);
break;
- #endif
-
- #ifdef HAVE_TRACING
- case SIMCALL_SET_CATEGORY:
- SIMIX_set_category((smx_synchro_t) simcall->args[0].dp, simcall->args[1].cc);
+ #ifdef HAVE_LATENCY_BOUND_TRACKING
+ case SIMCALL_COMM_IS_LATENCY_BOUNDED:
+ simcall->result.i = SIMIX_comm_is_latency_bounded((smx_synchro_t) simcall->args[0].dp);
SIMIX_simcall_answer(simcall);
break;
/* 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 <stdlib.h>
+
#include "smx_private.h"
#include "xbt/heap.h"
#include "xbt/sysdep.h"
#ifdef HAVE_MC
#include "mc/mc_private.h"
+#include "mc/mc_model_checker.h"
+#include "mc/mc_protocol.h"
+#include "mc/mc_client.h"
#endif
#include "mc/mc_record.h"
if (sg_cfg_get_boolean("clean_atexit"))
atexit(SIMIX_clean);
+#ifdef HAVE_MC
+ // The communication initialisation is done ASAP.
+ // We need to commuicate initialisation of the different layers to the model-checker.
+ if (mc_mode == MC_MODE_NONE) {
+ if (getenv(MC_ENV_SOCKET_FD)) {
+ mc_mode = MC_MODE_CLIENT;
+ MC_client_init();
+ MC_client_hello();
+ MC_client_handle_messages();
+ } else {
+ mc_mode = MC_MODE_STANDALONE;
+ }
+ }
+#endif
+
if (_sg_cfg_exit_asap)
exit(0);
}
SIMIX_simcall_handle(&process->simcall, 0);
}
}
+ /* Wake up all processes waiting for a Surf action to finish */
+ xbt_dynar_foreach(model_list, iter, model) {
+ XBT_DEBUG("Handling process whose action failed");
+ while ((action = surf_model_extract_failed_action_set(model))) {
+ XBT_DEBUG(" Handling Action %p",action);
+ SIMIX_simcall_exit((smx_synchro_t) surf_action_get_data(action));
+ }
+ XBT_DEBUG("Handling process whose action terminated normally");
+ while ((action = surf_model_extract_done_action_set(model))) {
+ XBT_DEBUG(" Handling Action %p",action);
+ if (surf_action_get_data(action) == NULL)
+ XBT_DEBUG("probably vcpu's action %p, skip", action);
+ else
+ SIMIX_simcall_exit((smx_synchro_t) surf_action_get_data(action));
+ }
+ }
}
time = SIMIX_timer_next();
- if (time != -1.0 || xbt_swag_size(simix_global->process_list) != 0)
+ if (time != -1.0 || xbt_swag_size(simix_global->process_list) != 0) {
+ XBT_DEBUG("Calling surf_solve");
time = surf_solve(time);
-
+ XBT_DEBUG("Moving time ahead : %g", time);
+ }
/* Notify all the hosts that have failed */
/* FIXME: iterate through the list of failed host and mark each of them */
/* as failed. On each host, signal all the running processes with host_fail */
/* Wake up all processes waiting for a Surf action to finish */
xbt_dynar_foreach(model_list, iter, model) {
- while ((action = surf_model_extract_failed_action_set(model)))
+ XBT_DEBUG("Handling process whose action failed");
+ while ((action = surf_model_extract_failed_action_set(model))) {
+ XBT_DEBUG(" Handling Action %p",action);
SIMIX_simcall_exit((smx_synchro_t) surf_action_get_data(action));
-
- while ((action = surf_model_extract_done_action_set(model)))
+ }
+ XBT_DEBUG("Handling process whose action terminated normally");
+ while ((action = surf_model_extract_done_action_set(model))) {
+ XBT_DEBUG(" Handling Action %p",action);
if (surf_action_get_data(action) == NULL)
XBT_DEBUG("probably vcpu's action %p, skip", action);
else
SIMIX_simcall_exit((smx_synchro_t) surf_action_get_data(action));
+ }
}
/* Autorestart all process */
if (xbt_swag_size(simix_global->process_list) != 0) {
- #ifdef HAVE_TRACING
- TRACE_end();
- #endif
+ TRACE_end();
XBT_CRITICAL("Oops ! Deadlock or code not perfectly clean.");
SIMIX_display_process_status();
#include "xbt/log.h"
#include "xbt/dict.h"
#include "mc/mc.h"
+#include "mc/mc_client.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix,
"Logging specific to SIMIX (process)");
}
}
+ XBT_DEBUG("%p should not be run anymore",process);
xbt_swag_remove(process, simix_global->process_list);
xbt_swag_remove(process, SIMIX_host_priv(process->smx_host)->process_list);
xbt_swag_insert(process, simix_global->process_to_destroy);
smx_process_t process = NULL;
while ((process = xbt_swag_extract(simix_global->process_to_destroy))) {
+ XBT_DEBUG("Getting rid of %p",process);
+
SIMIX_context_free(process->context);
/* Free the exception allocated at creation time */
}
}
if(!xbt_dynar_member(simix_global->process_to_run, &(process)) && process != issuer) {
+ XBT_DEBUG("Inserting %s in the to_run list", process->name);
xbt_dynar_push_as(simix_global->process_to_run, smx_process_t, process);
}
break;
case SIMIX_SYNC_SLEEP:
- SIMIX_process_sleep_destroy(process->waiting_synchro);
- break;
-
case SIMIX_SYNC_JOIN:
SIMIX_process_sleep_destroy(process->waiting_synchro);
+ if (!xbt_dynar_member(simix_global->process_to_run, &(process)) && process != SIMIX_process_self()) {
+ XBT_DEBUG("Inserting %s in the to_run list", process->name);
+ xbt_dynar_push_as(simix_global->process_to_run, smx_process_t, process);
+ }
break;
case SIMIX_SYNC_SYNCHRO:
}
process->waiting_synchro = NULL;
- if (!xbt_dynar_member(simix_global->process_to_run, &(process)) && process != SIMIX_process_self())
- xbt_dynar_push_as(simix_global->process_to_run, smx_process_t, process);
}
void simcall_HANDLER_process_killall(smx_simcall_t simcall, int reset_pid) {
synchro = xbt_mallocator_get(simix_global->synchro_mallocator);
synchro->type = SIMIX_SYNC_SLEEP;
synchro->name = NULL;
- #ifdef HAVE_TRACING
synchro->category = NULL;
- #endif
synchro->sleep.host = host;
synchro->sleep.surf_sleep =
MPI_Request detached_sender;
int refcount;
MPI_Op op;
- #ifdef HAVE_TRACING
int send;
int recv;
- #endif
} s_smpi_mpi_request_t;
typedef struct s_smpi_mpi_comm_key_elem {
extern double smpi_cpu_threshold;
extern double smpi_running_power;
extern int smpi_privatize_global_variables;
-extern char* start_data_exe; //start of the data+bss segment of the executable
-extern int size_data_exe; //size of the data+bss segment of the executable
+extern char* smpi_start_data_exe; //start of the data+bss segment of the executable
+extern int smpi_size_data_exe; //size of the data+bss segment of the executable
void smpi_switch_data_segment(int dest);
void mpi_comm_get_parent_ ( int*parent, int* ierr);
- #ifdef HAVE_TRACING
/********** Tracing **********/
/* from smpi_instr.c */
void TRACE_internal_smpi_set_category (const char *category);
void TRACE_smpi_recv(int rank, int src, int dst);
void TRACE_smpi_init(int rank);
void TRACE_smpi_finalize(int rank);
- #endif
const char* encode_datatype(MPI_Datatype datatype, int* known);
typedef struct s_smpi_privatisation_region {
void* address;
int file_descriptor;
-} *smpi_privatisation_region_t;
+} s_smpi_privatisation_region_t, *smpi_privatisation_region_t;
extern smpi_privatisation_region_t smpi_privatisation_regions;
-
extern int smpi_loaded_page;
int SIMIX_process_get_PID(smx_process_t self);
else
request->refcount = 0;
request->op = MPI_REPLACE;
- #ifdef HAVE_TRACING
request->send = 0;
request->recv = 0;
- #endif
if (flags & SEND) smpi_datatype_unuse(datatype);
return request;
int receiver = request->dst;
- #ifdef HAVE_TRACING
- int rank = request->src;
- if (TRACE_smpi_view_internals()) {
- TRACE_smpi_send(rank, rank, receiver,request->size);
- }
- #endif
+ int rank = request->src;
+ if (TRACE_smpi_view_internals()) {
+ TRACE_smpi_send(rank, rank, receiver,request->size);
+ }
print_request("New send", request);
//if we are giving back the control to the user without waiting for completion, we have to inject timings
oldbuf = request->buf;
if (!smpi_process_get_replaying() && oldbuf && request->size!=0){
if((smpi_privatize_global_variables)
- && ((char*)request->buf >= start_data_exe)
- && ((char*)request->buf < start_data_exe + size_data_exe )){
+ && ((char*) request->buf >= smpi_start_data_exe)
+ && ((char*)request->buf < smpi_start_data_exe + smpi_size_data_exe )){
XBT_DEBUG("Privatization : We are sending from a zone inside global memory. Switch data segment ");
- smpi_switch_data_segment(request->src);
- }
+ smpi_switch_data_segment(request->src);
+ }
buf = xbt_malloc(request->size);
memcpy(buf,oldbuf,request->size);
XBT_DEBUG("buf %p copied into %p",oldbuf,buf);
- #ifdef HAVE_TRACING
/* FIXME: detached sends are not traceable (request->action == NULL) */
if (request->action)
- simcall_set_category(request->action, TRACE_internal_smpi_get_category());
+ simcall_set_category(request->action, TRACE_internal_smpi_get_category());
- #endif
xbt_mutex_release(mut);
}
if((req->flags & ACCUMULATE) || (datatype->has_subtype == 1)){
if (!smpi_process_get_replaying()){
if( smpi_privatize_global_variables
- && ((char*)req->old_buf >= start_data_exe)
- && ((char*)req->old_buf < start_data_exe + size_data_exe )
+ && ((char*)req->old_buf >= smpi_start_data_exe)
+ && ((char*)req->old_buf < smpi_start_data_exe + smpi_size_data_exe )
){
XBT_VERB("Privatization : We are unserializing to a zone in global memory - Switch data segment ");
smpi_switch_data_segment(smpi_process_index());
}
- #ifdef HAVE_TRACING
if (TRACE_smpi_view_internals()) {
if(req->flags & RECV){
int rank = smpi_process_index();
TRACE_smpi_recv(rank, src_traced, rank);
}
}
- #endif
if(req->detached_sender!=NULL){
smpi_mpi_request_free(&(req->detached_sender));
double smpi_running_power;
int smpi_loaded_page = -1;
-char* start_data_exe = NULL;
-int size_data_exe = 0;
+char* smpi_start_data_exe = NULL;
+int smpi_size_data_exe = 0;
int smpi_privatize_global_variables;
double smpi_total_benched_time = 0;
-
-
smpi_privatisation_region_t smpi_privatisation_regions;
typedef struct {
host = SIMIX_host_self();
XBT_DEBUG("Handle real computation time: %f flops", flops);
action = simcall_host_execute("computation", host, flops, 1, 0, 0);
- #ifdef HAVE_TRACING
simcall_set_category (action, TRACE_internal_smpi_get_category());
- #endif
simcall_host_execution_wait(action);
smpi_switch_data_segment(smpi_process_index());
}
if (duration >= smpi_cpu_threshold) {
XBT_DEBUG("Sleep for %g to handle real computation time", duration);
double flops = duration * smpi_running_power;
- #ifdef HAVE_TRACING
int rank = smpi_process_index();
instr_extra_data extra = xbt_new0(s_instr_extra_data_t,1);
extra->type=TRACING_COMPUTING;
extra->comp_size=flops;
TRACE_smpi_computing_in(rank, extra);
- #endif
smpi_execute_flops(flops);
- #ifdef HAVE_TRACING
TRACE_smpi_computing_out(rank);
- #endif
} else {
XBT_DEBUG("Real computation took %g while option smpi/cpu_threshold is set to %g => ignore it",
smpi_bench_end();
XBT_DEBUG("Sleep for: %lf secs", secs);
- #ifdef HAVE_TRACING
int rank = smpi_comm_rank(MPI_COMM_WORLD);
instr_extra_data extra = xbt_new0(s_instr_extra_data_t,1);
extra->type=TRACING_SLEEPING;
extra->sleep_duration=secs;
TRACE_smpi_sleeping_in(rank, extra);
- #endif
+
simcall_process_sleep(secs);
- #ifdef HAVE_TRACING
+
TRACE_smpi_sleeping_out(rank);
- #endif
smpi_bench_begin();
return 0;
*/
void smpi_really_switch_data_segment(int dest) {
- if(size_data_exe == 0)//no need to switch
+ if(smpi_size_data_exe == 0)//no need to switch
return;
#ifdef HAVE_MMAP
int i;
if(smpi_loaded_page==-1){//initial switch, do the copy from the real page here
for (i=0; i< SIMIX_process_count(); i++){
- memcpy(smpi_privatisation_regions[i].address,TOPAGE(start_data_exe),size_data_exe);
+ memcpy(smpi_privatisation_regions[i].address,
+ TOPAGE(smpi_start_data_exe), smpi_size_data_exe);
}
}
+ // FIXME, cross-process support (mmap across process when necessary)
int current = smpi_privatisation_regions[dest].file_descriptor;
XBT_DEBUG("Switching data frame to the one of process %d", dest);
- void* tmp = mmap (TOPAGE(start_data_exe), size_data_exe, PROT_READ | PROT_WRITE, MAP_FIXED | MAP_SHARED, current, 0);
- if (tmp != TOPAGE(start_data_exe))
+ void* tmp = mmap (TOPAGE(smpi_start_data_exe), smpi_size_data_exe,
+ PROT_READ | PROT_WRITE, MAP_FIXED | MAP_SHARED, current, 0);
+ if (tmp != TOPAGE(smpi_start_data_exe))
xbt_die("Couldn't map the new region");
- smpi_loaded_page=dest;
+ smpi_loaded_page = dest;
#endif
}
if(i>=6){
if(strcmp(lfields[1], ".data") == 0){
size_data_binary = strtoul(lfields[2], NULL, 16);
- start_data_exe = (char*) strtoul(lfields[4], NULL, 16);
+ smpi_start_data_exe = (char*) strtoul(lfields[4], NULL, 16);
found++;
}else if(strcmp(lfields[1], ".bss") == 0){
//the beginning of bss is not exactly the end of data if not aligned, grow bss reported size accordingly
//TODO : check if this is OK, as some segments may be inserted between them..
- size_bss_binary = ((char*) strtoul(lfields[4], NULL, 16) - (start_data_exe + size_data_binary))
+ size_bss_binary = ((char*) strtoul(lfields[4], NULL, 16) - (smpi_start_data_exe + size_data_binary))
+ strtoul(lfields[2], NULL, 16);
found++;
}
}
- size_data_exe =(unsigned long)start_data_exe - (unsigned long)TOPAGE(start_data_exe)+ size_data_binary+size_bss_binary;
+ smpi_size_data_exe = (unsigned long) smpi_start_data_exe
+ - (unsigned long) TOPAGE(smpi_start_data_exe)
+ + size_data_binary+size_bss_binary;
xbt_free(command);
xbt_free(line);
pclose(fp);
unsigned int i = 0;
smpi_get_executable_global_size();
- XBT_DEBUG ("bss+data segment found : size %d starting at %p",size_data_exe, start_data_exe );
+ XBT_DEBUG ("bss+data segment found : size %d starting at %p",
+ smpi_size_data_exe, smpi_start_data_exe );
- if(size_data_exe == 0){//no need to switch
+ if (smpi_size_data_exe == 0){//no need to switch
smpi_privatize_global_variables=0;
return;
}
if (status)
xbt_die("Impossible to unlink temporary file for memory mapping");
- status = ftruncate(file_descriptor, size_data_exe);
+ status = ftruncate(file_descriptor, smpi_size_data_exe);
if(status)
xbt_die("Impossible to set the size of the temporary file for memory mapping");
/* Ask for a free region */
- address = mmap (NULL, size_data_exe, PROT_READ | PROT_WRITE, MAP_SHARED, file_descriptor, 0);
+ address = mmap (NULL, smpi_size_data_exe, PROT_READ | PROT_WRITE, MAP_SHARED, file_descriptor, 0);
if (address == MAP_FAILED)
xbt_die("Couldn't find a free region for memory mapping");
//initialize the values
- memcpy(address,TOPAGE(start_data_exe),size_data_exe);
+ memcpy(address, TOPAGE(smpi_start_data_exe), smpi_size_data_exe);
//store the address of the mapping for further switches
smpi_privatisation_regions[i].file_descriptor = file_descriptor;
}
void smpi_destroy_global_memory_segments(){
- if(size_data_exe == 0)//no need to switch
+ if (smpi_size_data_exe == 0)//no need to switch
return;
#ifdef HAVE_MMAP
int i;
for (i=0; i< smpi_process_count(); i++){
- if(munmap(smpi_privatisation_regions[i].address,size_data_exe) < 0) {
+ if(munmap(smpi_privatisation_regions[i].address, smpi_size_data_exe) < 0) {
XBT_WARN("Unmapping of fd %d failed: %s",
smpi_privatisation_regions[i].file_descriptor, strerror(errno));
}
void* tmpbuff=buff;
if((smpi_privatize_global_variables)
- && ((char*)buff >= start_data_exe)
- && ((char*)buff < start_data_exe + size_data_exe )
+ && ((char*)buff >= smpi_start_data_exe)
+ && ((char*)buff < smpi_start_data_exe + smpi_size_data_exe )
){
XBT_DEBUG("Privatization : We are copying from a zone inside global memory... Saving data to temp buffer !");
smpi_switch_data_segment(((smpi_process_data_t)SIMIX_process_get_data(comm->comm.src_proc))->index);
if((smpi_privatize_global_variables)
- && ((char*)comm->comm.dst_buff >= start_data_exe)
- && ((char*)comm->comm.dst_buff < start_data_exe + size_data_exe )
+ && ((char*)comm->comm.dst_buff >= smpi_start_data_exe)
+ && ((char*)comm->comm.dst_buff < smpi_start_data_exe + smpi_size_data_exe )
){
XBT_DEBUG("Privatization : We are copying to a zone inside global memory - Switch data segment");
smpi_switch_data_segment(((smpi_process_data_t)SIMIX_process_get_data(comm->comm.dst_proc))->index);
function: xbt_log_appender_file.c depends on it
DO NOT connect this in XBT or so, or it will be
useless to xbt_log_appender_file.c */
- #ifdef HAVE_TRACING
XBT_LOG_CONNECT(instr_smpi);
- #endif
XBT_LOG_CONNECT(smpi_base);
XBT_LOG_CONNECT(smpi_bench);
XBT_LOG_CONNECT(smpi_coll);
smpi_init_logs();
- #ifdef HAVE_TRACING
TRACE_global_init(&argc, argv);
TRACE_add_start_function(TRACE_smpi_alloc);
TRACE_add_end_function(TRACE_smpi_release);
- #endif
SIMIX_global_init(&argc, argv);
smpi_global_destroy();
- #ifdef HAVE_TRACING
TRACE_end();
- #endif
return 0;
}
smpi_init_options();
smpi_global_init();
smpi_check_options();
- #ifdef HAVE_TRACING
- if (TRACE_is_enabled() && TRACE_is_configured()) {
+ if (TRACE_is_enabled() && TRACE_is_configured())
TRACE_smpi_alloc();
- }
- #endif
if(smpi_privatize_global_variables)
smpi_initialize_global_memory_segments();
}
if (!history)
history = tmgr_history_new();
- #ifdef HAVE_TRACING
TRACE_add_start_function(TRACE_surf_alloc);
TRACE_add_end_function(TRACE_surf_release);
- #endif
sg_config_init(argc, argv);
unsigned int iter;
ModelPtr model = NULL;
- #ifdef HAVE_TRACING
TRACE_end(); /* Just in case it was not called by the upper
* layer (or there is no upper layer) */
- #endif
sg_config_finalize();
Action::Action(ModelPtr model, double cost, bool failed)
{
initialize(model, cost, failed);
- #ifdef HAVE_TRACING
- p_category = NULL;
- #endif
+ p_category = NULL;
p_stateHookup.prev = 0;
p_stateHookup.next = 0;
if (failed)
Action::Action(ModelPtr model, double cost, bool failed, lmm_variable_t var)
{
initialize(model, cost, failed, var);
- #ifdef HAVE_TRACING
- p_category = NULL;
- #endif
+ p_category = NULL;
p_stateHookup.prev = 0;
p_stateHookup.next = 0;
if (failed)
}
Action::~Action() {
- #ifdef HAVE_TRACING
xbt_free(p_category);
- #endif
}
void Action::finish() {
p_data = data;
}
- #ifdef HAVE_TRACING
void Action::setCategory(const char *category)
{
XBT_IN("(%p,%s)", this, category);
p_category = xbt_strdup(category);
XBT_OUT();
}
- #endif
void Action::ref(){
m_refcount++;
XBT_DEBUG("Updating action(%p): remains was %f, last_update was: %f", this, m_remains, m_lastUpdate);
double_update(&m_remains, m_lastValue * delta, sg_surf_precision*sg_maxmin_precision);
- #ifdef HAVE_TRACING
if (getModel() == surf_cpu_model_pm && TRACE_is_enabled()) {
ResourcePtr cpu = static_cast<ResourcePtr>(lmm_constraint_id(lmm_get_cnst_from_var(getModel()->getMaxminSystem(), getVariable(), 0)));
TRACE_surf_host_set_utilization(cpu->getName(), getCategory(), m_lastValue, m_lastUpdate, now - m_lastUpdate);
}
- #endif
XBT_DEBUG("Updating action(%p): remains is now %f", this, m_remains);
}
m_lastUpdate = now;
m_lastValue = lmm_variable_getvalue(getVariable());
}
-
#include <stdio.h>
-
- #include <msg/msg.h>
+#include <xbt/log.h>
+ #include <simgrid/msg.h>
#include <simgrid/modelchecker.h>
+XBT_LOG_NEW_DEFAULT_CATEGORY(random_bug, "Application");
+
/** An (fake) application with a bug occuring for some random values
*/
static int app(int argc, char *argv[])
MSG_function_register("app", &app);
MSG_create_environment(argv[1]);
MSG_launch_application(argv[2]);
- return (int) MSG_main();
+ return MSG_main();
}
