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(
string(REPLACE "\n" "" GIT_DATE "${GIT_DATE}")
message(STATUS "Git date: ${GIT_DATE}")
string(REGEX REPLACE " .*" "" GIT_VERSION "${GIT_VERSION}")
+
+ execute_process(COMMAND git --git-dir=${CMAKE_HOME_DIRECTORY}/.git log --pretty=format:%H -1
+ WORKING_DIRECTORY ${CMAKE_HOME_DIRECTORY}/.git/
+ OUTPUT_VARIABLE SIMGRID_GITHASH
+ RESULT_VARIABLE ret
+ )
+ string(REPLACE "\n" "" SIMGRID_GITHASH "${SIMGRID_GITHASH}")
+
endif()
elseif(EXISTS ${CMAKE_HOME_DIRECTORY}/.gitversion)
FILE(STRINGS ${CMAKE_HOME_DIRECTORY}/.gitversion GIT_VERSION)
tools/tesh/run_context.h
tools/tesh/tesh.h
tools/tesh/generate_tesh
- examples/smpi/mc/non_deterministic.tesh
- examples/smpi/mc/send_deterministic.tesh
+ examples/smpi/mc/only_send_deterministic.tesh
)
set(SMPI_SRC
)
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_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
examples/msg/chainsend/CMakeLists.txt
examples/msg/chord/CMakeLists.txt
examples/msg/cloud/CMakeLists.txt
- examples/msg/energy/e1/CMakeLists.txt
+ examples/msg/energy/pstate/CMakeLists.txt
examples/msg/energy/e2/CMakeLists.txt
examples/msg/energy/e3/CMakeLists.txt
examples/msg/exception/CMakeLists.txt
--- /dev/null
-$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'surf/precision' to '1e-9'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/TCP_gamma' to '4194304'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check' to '1'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/communications_determinism' to '1'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/send_is_detached_thres' to '0'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/running_power' to '1e9'
+ #! ./tesh
+
+ ! timeout 60
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
++$ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic
+ > [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
+ > [0.000000] [mc_global/INFO] Check communication determinism
-
-
+ > [0.000000] [mc_global/INFO] ******************************************************
+ > [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern ****
+ > [0.000000] [mc_global/INFO] ******************************************************
+ > [0.000000] [mc_global/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2
+ > [0.000000] [mc_global/INFO] Expanded states = 1025
+ > [0.000000] [mc_global/INFO] Visited states = 3640
+ > [0.000000] [mc_global/INFO] Executed transitions = 3360
+ > [0.000000] [mc_global/INFO] Send-deterministic : Yes
+ > [0.000000] [mc_global/INFO] Recv-deterministic : No
extern int _sg_mc_send_determinism;
extern int _sg_mc_safety;
extern int _sg_mc_liveness;
+extern int _sg_mc_snapshot_fds;
+ extern int _sg_mc_termination;
extern xbt_dynar_t mc_heap_comparison_ignore;
extern xbt_dynar_t stacks_areas;
-extern void *maestro_stack_start;
-extern void *maestro_stack_end;
/********************************* Global *************************************/
void _mc_cfg_cb_reduce(const char *name, int pos);
void _mc_cfg_cb_property(const char *name, int pos);
void _mc_cfg_cb_timeout(const char *name, int pos);
void _mc_cfg_cb_hash(const char *name, int pos);
+void _mc_cfg_cb_snapshot_fds(const char *name, int pos);
void _mc_cfg_cb_max_depth(const char *name, int pos);
void _mc_cfg_cb_visited(const char *name, int pos);
void _mc_cfg_cb_dot_output(const char *name, int pos);
void _mc_cfg_cb_comms_determinism(const char *name, int pos);
void _mc_cfg_cb_send_determinism(const char *name, int pos);
+ void _mc_cfg_cb_termination(const char *name, int pos);
XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
XBT_PUBLIC(void) MC_init(void);
/********************************* Memory *************************************/
XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */
XBT_PUBLIC(void) MC_memory_exit(void);
+XBT_PUBLIC(void) MC_memory_init_server(void);
SG_END_DECL()
#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"
+#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)
{
smx_process_t process;
{
unsigned int index = 0;
smx_synchro_t act = 0;
+#ifdef HAVE_MC
+ s_smx_synchro_t temp_synchro;
+#endif
+ smx_mutex_t mutex = NULL;
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. */
case SIMCALL_COMM_WAITANY:
/* Check if it has at least one communication ready */
- xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act)
+ xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) {
+
+#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);
+ if(mutex->owner == NULL)
+ return TRUE;
+ else
+ return (mutex->owner->pid == req->issuer->pid);
+
default:
/* The rest of the requests are always enabled */
return TRUE;
|| req->call == SIMCALL_COMM_TEST
|| req->call == SIMCALL_COMM_TESTANY
|| req->call == SIMCALL_MC_RANDOM
+ || req->call == SIMCALL_MUTEX_LOCK
#ifdef HAVE_MC
|| req->call == SIMCALL_MC_SNAPSHOT
|| req->call == SIMCALL_MC_COMPARE_SNAPSHOTS
#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");
return SRC_PROC_DIFF;
if (comm1->dst_proc != comm2->dst_proc)
return DST_PROC_DIFF;
+ if (comm1->tag != comm2->tag)
+ return TAG_DIFF;
if (comm1->data_size != comm2->data_size)
return DATA_SIZE_DIFF;
if(comm1->data == NULL && comm2->data == NULL)
return 0;
- /*if(comm1->data != NULL && comm2->data !=NULL) {
+ if(comm1->data != NULL && comm2->data !=NULL) {
if (!memcmp(comm1->data, comm2->data, comm1->data_size))
return 0;
return DATA_DIFF;
}else{
return DATA_DIFF;
- }*/
+ }
return 0;
}
- static void print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
- if (_sg_mc_comms_determinism && !initial_global_state->comm_deterministic) {
- XBT_INFO("****************************************************");
- XBT_INFO("***** Non-deterministic communications pattern *****");
- XBT_INFO("****************************************************");
- XBT_INFO("The communications pattern of the process %d is different!", process);
- switch(diff) {
- case TYPE_DIFF:
- XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case RDV_DIFF:
- XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case SRC_PROC_DIFF:
- XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case DST_PROC_DIFF:
- XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case DATA_SIZE_DIFF:
- XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case DATA_DIFF:
- XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- default:
- break;
- }
- MC_print_statistics(mc_stats);
- xbt_abort();
- } else if (_sg_mc_send_determinism && !initial_global_state->send_deterministic) {
- XBT_INFO("*********************************************************");
- XBT_INFO("***** Non-send-deterministic communications pattern *****");
- XBT_INFO("*********************************************************");
- XBT_INFO("The communications pattern of the process %d is different!", process);
- switch(diff) {
- case TYPE_DIFF:
- XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case RDV_DIFF:
- XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case SRC_PROC_DIFF:
- XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case DST_PROC_DIFF:
- XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case DATA_SIZE_DIFF:
- XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- case DATA_DIFF:
- XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
- break;
- default:
- break;
- }
- MC_print_statistics(mc_stats);
- xbt_abort();
+ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
+ char *type, *res;
+
+ if(comm->type == SIMIX_COMM_SEND)
+ type = bprintf("The send communications pattern of the process %d is different!", process - 1);
+ else
+ type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
+
+ switch(diff) {
+ case TYPE_DIFF:
+ res = bprintf("%s Different type for communication #%d", type, cursor);
+ break;
+ case RDV_DIFF:
+ res = bprintf("%s Different rdv for communication #%d", type, cursor);
+ break;
+ case TAG_DIFF:
+ res = bprintf("%s Different tag for communication #%d", type, cursor);
+ break;
+ case SRC_PROC_DIFF:
+ res = bprintf("%s Different source for communication #%d", type, cursor);
+ break;
+ case DST_PROC_DIFF:
+ res = bprintf("%s Different destination for communication #%d", type, cursor);
+ break;
+ case DATA_SIZE_DIFF:
+ res = bprintf("%s\n Different data size for communication #%d", type, cursor);
+ break;
+ case DATA_DIFF:
+ res = bprintf("%s\n Different data for communication #%d", type, cursor);
+ break;
+ default:
+ res = NULL;
+ break;
}
- }
- static void print_communications_pattern()
- {
- unsigned int cursor = 0, cursor2 = 0;
- mc_comm_pattern_t current_comm;
- mc_list_comm_pattern_t current_list;
- unsigned int current_process = 1;
- while (current_process < simix_process_maxpid) {
- current_list = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, current_process, mc_list_comm_pattern_t);
- XBT_INFO("Communications from the process %u:", current_process);
- while(cursor2 < current_list->index_comm){
- current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(current_list->list, cursor2, mc_comm_pattern_t);
- if (current_comm->type == SIMIX_COMM_SEND) {
- XBT_INFO("(%u) [(%lu) %s -> (%lu) %s] %s ", cursor,current_comm->src_proc,
- current_comm->src_host, current_comm->dst_proc,
- current_comm->dst_host, "iSend");
- } else {
- XBT_INFO("(%u) [(%lu) %s <- (%lu) %s] %s ", cursor, current_comm->dst_proc,
- current_comm->dst_host, current_comm->src_proc,
- current_comm->src_host, "iRecv");
- }
- cursor2++;
- }
- current_process++;
- cursor = 0;
- cursor2 = 0;
- }
- }
-
- static void print_incomplete_communications_pattern(){
- unsigned int cursor = 0;
- unsigned int current_process = 1;
- xbt_dynar_t current_pattern;
- mc_comm_pattern_t comm;
- while (current_process < simix_process_maxpid) {
- current_pattern = (xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t);
- XBT_INFO("Incomplete communications from the process %u:", current_process);
- xbt_dynar_foreach(current_pattern, cursor, comm) {
- XBT_DEBUG("(%u) Communication %p", cursor, comm);
- }
- current_process++;
- cursor = 0;
- }
+ return res;
}
+// FIXME, remote comm
static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm)
{
+ mc_process_t process = &mc_model_checker->process;
void *addr_pointed;
- comm_pattern->src_proc = comm->comm.src_proc->pid;
- comm_pattern->dst_proc = comm->comm.dst_proc->pid;
- 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);
+ smx_process_t src_proc = MC_smx_resolve_process(comm->comm.src_proc);
+ smx_process_t dst_proc = MC_smx_resolve_process(comm->comm.dst_proc);
+ comm_pattern->src_proc = src_proc->pid;
+ comm_pattern->dst_proc = dst_proc->pid;
+ // TODO, resolve host name
+ comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
+ comm_pattern->dst_host = MC_smx_process_get_host_name(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);
addr_pointed = *(void **) comm->comm.src_buff;
- if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval)
+ if (addr_pointed > (void*) process->heap_address
+ && addr_pointed < MC_process_get_heap(process)->breakval)
memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size);
else
memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size);
mc_list_comm_pattern_t list_comm_pattern = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
if(!backtracking){
- mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, comm->index, mc_comm_pattern_t);
+ mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, list_comm_pattern->index_comm, mc_comm_pattern_t);
e_mc_comm_pattern_difference_t diff;
if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){
- if (comm->type == SIMIX_COMM_SEND)
+ if (comm->type == SIMIX_COMM_SEND){
initial_global_state->send_deterministic = 0;
- initial_global_state->comm_deterministic = 0;
- print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+ if(initial_global_state->send_diff != NULL)
+ xbt_free(initial_global_state->send_diff);
+ initial_global_state->send_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+ }else{
+ initial_global_state->recv_deterministic = 0;
+ if(initial_global_state->recv_diff != NULL)
+ xbt_free(initial_global_state->recv_diff);
+ initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+ }
+ if(_sg_mc_send_determinism && !initial_global_state->send_deterministic){
+ XBT_INFO("*********************************************************");
+ XBT_INFO("***** Non-send-deterministic communications pattern *****");
+ XBT_INFO("*********************************************************");
+ XBT_INFO("%s", initial_global_state->send_diff);
+ xbt_free(initial_global_state->send_diff);
+ initial_global_state->send_diff = NULL;
+ MC_print_statistics(mc_stats);
+ xbt_abort();
+ }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
+ XBT_INFO("****************************************************");
+ XBT_INFO("***** Non-deterministic communications pattern *****");
+ XBT_INFO("****************************************************");
+ XBT_INFO("%s", initial_global_state->send_diff);
+ XBT_INFO("%s", initial_global_state->recv_diff);
+ xbt_free(initial_global_state->send_diff);
+ initial_global_state->send_diff = NULL;
+ xbt_free(initial_global_state->recv_diff);
+ initial_global_state->recv_diff = NULL;
+ MC_print_statistics(mc_stats);
+ xbt_abort();
+ }
}
}
- list_comm_pattern->index_comm++;
comm_pattern_free(comm);
}
list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
}
- void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const e_mc_call_type_t call_type)
+ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
{
-
+ mc_process_t process = &mc_model_checker->process;
mc_comm_pattern_t pattern = NULL;
pattern = xbt_new0(s_mc_comm_pattern_t, 1);
pattern->data_size = -1;
pattern->data = NULL;
+
+ 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 =
+ (xbt_dynar_t) xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+ pattern->index =
+ initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
void *addr_pointed;
/* Create comm pattern */
pattern->type = SIMIX_COMM_SEND;
pattern->comm = simcall_comm_isend__get__result(request);
+ // FIXME, remote access to rdv->name
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;
- pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
+ pattern->src_proc = MC_smx_resolve_process(pattern->comm->comm.src_proc)->pid;
+ pattern->src_host = MC_smx_process_get_host_name(issuer);
+ pattern->tag = ((MPI_Request)simcall_comm_isend__get__data(request))->tag;
if(pattern->comm->comm.src_buff != NULL){
pattern->data_size = pattern->comm->comm.src_buff_size;
pattern->data = xbt_malloc0(pattern->data_size);
addr_pointed = *(void **) pattern->comm->comm.src_buff;
- if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval)
+ if (addr_pointed > (void*) process->heap_address
+ && addr_pointed < MC_process_get_heap(process)->breakval)
memcpy(pattern->data, addr_pointed, pattern->data_size);
else
memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
}
+ if(((MPI_Request)simcall_comm_isend__get__data(request))->detached){
+ if (!initial_global_state->initial_communications_pattern_done) {
+ /* Store comm pattern */
+ xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->list, &pattern);
+ } else {
+ /* Evaluate comm determinism */
+ deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
+ ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->index_comm++;
+ }
+ return;
+ }
} else if (call_type == MC_CALL_TYPE_RECV) {
pattern->type = SIMIX_COMM_RECEIVE;
pattern->comm = simcall_comm_irecv__get__result(request);
+ // TODO, remote access
+ pattern->tag = ((MPI_Request)simcall_comm_irecv__get__data(request))->tag;
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;
- pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
+ pattern->dst_proc = MC_smx_resolve_process(pattern->comm->comm.dst_proc)->pid;
+ // FIXME, remote process access
+ pattern->dst_host = MC_smx_process_get_host_name(issuer);
} else {
xbt_die("Unexpected call_type %i", (int) call_type);
}
- xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), &pattern);
+ xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), &pattern);
- XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, request->issuer->pid);
+ XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
}
- void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) {
+ void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int issuer, int backtracking) {
-
mc_comm_pattern_t current_comm_pattern;
unsigned int cursor = 0;
-
- smx_process_t src_proc = MC_smx_resolve_process(comm->comm.src_proc);
- smx_process_t dst_proc = MC_smx_resolve_process(comm->comm.dst_proc);
- unsigned int src = src_proc->pid;
- unsigned int dst = dst_proc->pid;
-
- mc_comm_pattern_t src_comm_pattern;
- mc_comm_pattern_t dst_comm_pattern;
- int src_completed = 0, dst_completed = 0;
+ mc_comm_pattern_t comm_pattern;
+ int completed = 0;
/* Complete comm pattern */
- xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, current_comm_pattern) {
+ xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) {
if (current_comm_pattern-> comm == comm) {
update_comm_pattern(current_comm_pattern, comm);
- src_completed = 1;
- xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, &src_comm_pattern);
- XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", src, cursor);
+ completed = 1;
+ xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &comm_pattern);
+ XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
break;
}
}
- if(!src_completed)
- xbt_die("Corresponding communication for the source process not found!");
+ if(!completed)
+ xbt_die("Corresponding communication not found!");
- cursor = 0;
-
- xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, current_comm_pattern) {
- if (current_comm_pattern-> comm == comm) {
- update_comm_pattern(current_comm_pattern, comm);
- dst_completed = 1;
- xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, &dst_comm_pattern);
- XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", dst, cursor);
- break;
- }
- }
- if(!dst_completed)
- xbt_die("Corresponding communication for the destination process not found!");
-
if (!initial_global_state->initial_communications_pattern_done) {
/* Store comm pattern */
- if(src_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list)){
- xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern);
- ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list->used++;
- } else {
- xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern);
- }
-
- if(dst_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list)) {
- xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern);
- ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list->used++;
- } else {
- xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern);
- }
- ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->index_comm++;
- ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->index_comm++;
+ xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->list, &comm_pattern);
} else {
/* Evaluate comm determinism */
- deterministic_comm_pattern(src, src_comm_pattern, backtracking);
- deterministic_comm_pattern(dst, dst_comm_pattern, backtracking);
+ deterministic_comm_pattern(issuer, comm_pattern, backtracking);
+ ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->index_comm++;
}
}
+
/************************ Main algorithm ************************/
void MC_pre_modelcheck_comm_determinism(void)
{
-
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
+ MC_SET_MC_HEAP;
mc_state_t initial_state = NULL;
smx_process_t process;
int i;
- if (!mc_mem_set)
- MC_SET_MC_HEAP;
-
if (_sg_mc_visited > 0)
visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
MC_SET_MC_HEAP;
/* Get an enabled process and insert it in the interleave set of the initial state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(initial_state, process);
}
- }
+ );
xbt_fifo_unshift(mc_stack, initial_state);
}
/* Answer the request */
- SIMIX_simcall_handle(req, value); /* After this call req is no longer useful */
+ MC_simcall_handle(req, value); /* After this call req is no longer useful */
MC_SET_MC_HEAP;
if(!initial_global_state->initial_communications_pattern_done)
if ((visited_state = is_visited_state(next_state)) == NULL) {
/* Get enabled processes and insert them in the interleave set of the next state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(next_state, process);
}
- }
+ );
if (dot_output != NULL)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
static void stack_region_free(stack_region_t s)
{
if (s) {
- xbt_free(s->process_name);
xbt_free(s);
}
}
void* real_area2, mc_snapshot_t snapshot2, mc_mem_region_t region2,
dw_type_t type, int pointer_level)
{
+ mc_process_t process = &mc_model_checker->process;
+
unsigned int cursor = 0;
dw_type_t member, subtype, subsubtype;
int elm_size, i, res;
case DW_TAG_enumeration_type:
case DW_TAG_union_type:
{
- return mc_snapshot_region_memcmp(
+ return MC_snapshot_region_memcmp(
real_area1, region1, real_area2, region2,
type->byte_size) != 0;
}
case DW_TAG_reference_type:
case DW_TAG_rvalue_reference_type:
{
- void* addr_pointed1 = mc_snapshot_read_pointer_region(real_area1, region1);
- void* addr_pointed2 = mc_snapshot_read_pointer_region(real_area2, region2);
+ void* addr_pointed1 = MC_region_read_pointer(region1, real_area1);
+ void* addr_pointed2 = MC_region_read_pointer(region2, real_area2);
if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) {
return (addr_pointed1 != addr_pointed2);
// * a pointer leads to the read-only segment of the current object;
// * a pointer lead to a different ELF object.
- if (addr_pointed1 > std_heap
+ if (addr_pointed1 > process->heap_address
&& addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)) {
if (!
- (addr_pointed2 > std_heap
+ (addr_pointed2 > process->heap_address
&& addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)))
return 1;
// The pointers are both in the heap:
case DW_TAG_class_type:
xbt_dynar_foreach(type->members, cursor, member) {
void *member1 =
- mc_member_resolve(real_area1, type, member, snapshot1, process_index);
+ mc_member_resolve(real_area1, type, member, (mc_address_space_t) snapshot1, process_index);
void *member2 =
- mc_member_resolve(real_area2, type, member, snapshot2, process_index);
+ mc_member_resolve(real_area2, type, member, (mc_address_space_t) snapshot2, process_index);
mc_mem_region_t subregion1 = mc_get_region_hinted(member1, snapshot1, process_index, region1);
mc_mem_region_t subregion2 = mc_get_region_hinted(member2, snapshot2, process_index, region2);
res =
mc_snapshot_t snapshot2)
{
xbt_assert(r1 && r2, "Missing region.");
+
+#ifdef HAVE_SMPI
+ if (r1->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED) {
+ xbt_assert(process_index >= 0);
+ if (r2->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED) {
+ return 1;
+ }
+
+ size_t process_count = smpi_process_count();
+ xbt_assert(process_count == r1->privatized.regions_count
+ && process_count == r2->privatized.regions_count);
+
+ // Compare the global variables separately for each simulates process:
+ for (size_t process_index = 0; process_index < process_count; process_index++) {
+ int is_diff = compare_global_variables(object_info, process_index,
+ r1->privatized.regions[process_index], r2->privatized.regions[process_index],
+ snapshot1, snapshot2);
+ if (is_diff) return 1;
+ }
+ return 0;
+ }
+#else
+ xbt_assert(r1->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED);
+#endif
+ xbt_assert(r2->storage_type != MC_REGION_STORAGE_TYPE_PRIVATIZED);
+
struct mc_compare_state state;
xbt_dynar_t variables;
int snapshot_compare(void *state1, void *state2)
{
+ mc_process_t process = &mc_model_checker->process;
mc_snapshot_t s1, s2;
int num1, num2;
s2 = ((mc_visited_pair_t) state2)->graph_state->system_state;
num1 = ((mc_visited_pair_t) state1)->num;
num2 = ((mc_visited_pair_t) state2)->num;
+ }else if (_sg_mc_termination) { /* Non-progressive cycle MC */
+ s1 = ((mc_state_t) state1)->system_state;
+ s2 = ((mc_state_t) state2)->system_state;
+ num1 = ((mc_state_t) state1)->num;
+ num2 = ((mc_state_t) state2)->num;
} else { /* Safety or comm determinism MC */
s1 = ((mc_visited_state_t) state1)->system_state;
s2 = ((mc_visited_state_t) state2)->system_state;
#endif
/* Init heap information used in heap comparison algorithm */
- xbt_mheap_t heap1 = (xbt_mheap_t) mc_snapshot_read(std_heap, s1, MC_NO_PROCESS_INDEX,
- alloca(sizeof(struct mdesc)), sizeof(struct mdesc));
- xbt_mheap_t heap2 = (xbt_mheap_t) mc_snapshot_read(std_heap, s2, MC_NO_PROCESS_INDEX,
- alloca(sizeof(struct mdesc)), sizeof(struct mdesc));
+ xbt_mheap_t heap1 = (xbt_mheap_t) MC_snapshot_read(
+ s1, MC_ADDRESS_SPACE_READ_FLAGS_LAZY,
+ alloca(sizeof(struct mdesc)), process->heap_address, sizeof(struct mdesc),
+ MC_PROCESS_INDEX_MISSING);
+ xbt_mheap_t heap2 = (xbt_mheap_t) MC_snapshot_read(
+ s2, MC_ADDRESS_SPACE_READ_FLAGS_LAZY,
+ alloca(sizeof(struct mdesc)), process->heap_address, sizeof(struct mdesc),
+ MC_PROCESS_INDEX_MISSING);
res_init = init_heap_information(heap1, heap2, s1->to_ignore, s2->to_ignore);
if (res_init == -1) {
#ifdef MC_DEBUG
cursor++;
}
+ size_t regions_count = s1->snapshot_regions_count;
+ // TODO, raise a difference instead?
+ xbt_assert(regions_count == s2->snapshot_regions_count);
+ mc_comp_times->global_variables_comparison_time = 0;
- const char *names[3] = { "?", "libsimgrid", "binary" };
-#ifdef MC_DEBUG
- double *times[3] = {
- NULL,
- &mc_comp_times->libsimgrid_global_variables_comparison_time,
- &mc_comp_times->binary_global_variables_comparison_time
- };
-#endif
+ for (size_t k = 0; k != regions_count; ++k) {
+ mc_mem_region_t region1 = s1->snapshot_regions[k];
+ mc_mem_region_t region2 = s2->snapshot_regions[k];
- mc_object_info_t object_infos[] = { NULL, mc_libsimgrid_info, mc_binary_info };
+ // Preconditions:
+ if (region1->region_type != MC_REGION_TYPE_DATA)
+ continue;
+
+ xbt_assert(region1->region_type == region2->region_type);
+ xbt_assert(region1->object_info == region2->object_info);
+
+ xbt_assert(region1->object_info);
+
+ const char* name = region1->object_info->file_name;
- int k = 0;
- for (k = 2; k != 0; --k) {
#ifdef MC_DEBUG
if (is_diff == 0)
xbt_os_walltimer_stop(timer);
#endif
/* Compare global variables */
-#ifdef HAVE_SMPI
- if (object_infos[k] == mc_binary_info && smpi_privatize_global_variables) {
- // Compare the global variables separately for each simulates process:
- for (int process_index = 0; process_index < smpi_process_count(); process_index++) {
- is_diff =
- compare_global_variables(object_infos[k], process_index,
- s1->privatization_regions[process_index], s2->privatization_regions[process_index], s1, s2);
- if (is_diff) break;
- }
- }
- else
-#endif
- is_diff =
- compare_global_variables(object_infos[k], MC_NO_PROCESS_INDEX, s1->regions[k], s2->regions[k], s1, s2);
+ is_diff =
+ compare_global_variables(region1->object_info, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+ region1, region2,
+ s1, s2);
if (is_diff != 0) {
XBT_TRACE3(mc, state_diff, num1, num2, "Different global variables");
#ifdef MC_DEBUG
xbt_os_walltimer_stop(timer);
- *times[k] = xbt_os_timer_elapsed(timer);
+ mc_comp_times->global_variables_comparison_time
+ += xbt_os_timer_elapsed(timer);
XBT_DEBUG("(%d - %d) Different global variables in %s", num1, num2,
- names[k]);
+ name);
errors++;
#else
#ifdef MC_VERBOSE
XBT_VERB("(%d - %d) Different global variables in %s", num1, num2,
- names[k]);
+ name);
#endif
reset_heap_information();
XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time);
XBT_DEBUG("- Nb bytes used : %f", mc_comp_times->bytes_used_comparison_time);
XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time);
- XBT_DEBUG("- Binary global variables : %f",
- mc_comp_times->binary_global_variables_comparison_time);
- XBT_DEBUG("- Libsimgrid global variables : %f",
- mc_comp_times->libsimgrid_global_variables_comparison_time);
+ XBT_DEBUG("- GLobal variables : %f", mc_comp_times->global_variables_comparison_time);
XBT_DEBUG("- Heap : %f", mc_comp_times->heap_comparison_time);
XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time);
}
-/**************************** MC snapshot compare simcall **************************/
-/***********************************************************************************/
-
-int simcall_HANDLER_mc_compare_snapshots(smx_simcall_t simcall,
- mc_snapshot_t s1, mc_snapshot_t s2)
-{
- return snapshot_compare(s1, s2);
-}
-
-int MC_compare_snapshots(void *s1, void *s2)
-{
-
- return simcall_mc_compare_snapshots(s1, s2);
-
-}
-
}
int _sg_mc_send_determinism = 0;
int _sg_mc_safety = 0;
int _sg_mc_liveness = 0;
+int _sg_mc_snapshot_fds = 0;
+ int _sg_mc_termination = 0;
-
void _mc_cfg_cb_reduce(const char *name, int pos)
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
_sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
+void _mc_cfg_cb_snapshot_fds(const char *name, int pos)
+{
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die
+ ("You are specifying a value to enable/disable the use of FD snapshoting, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _sg_mc_snapshot_fds = xbt_cfg_get_boolean(_sg_cfg_set, name);
+}
+
void _mc_cfg_cb_max_depth(const char *name, int pos)
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
- mc_reduce_kind = e_mc_reduce_none;
}
void _mc_cfg_cb_send_determinism(const char *name, int pos)
("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
- mc_reduce_kind = e_mc_reduce_none;
+ }
+
+ void _mc_cfg_cb_termination(const char *name, int pos)
+ {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die
+ ("You are specifying a value to enable/disable the detection of non progressive cycles after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _sg_mc_termination = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
#endif
/* 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 <string.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/dict.h"
#ifdef HAVE_MC
-#define UNW_LOCAL_ONLY
#include <libunwind.h>
+#include <xbt/mmalloc.h>
#include "../xbt/mmalloc/mmprivate.h"
#include "mc_object_info.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)
-{
- 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_model_checker_t mc_model_checker = NULL;
-
-mc_model_checker_t MC_model_checker_new()
+void MC_init()
{
- 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);
+ MC_init_pid(getpid(), -1);
}
-void MC_init()
+void MC_init_pid(pid_t pid, int socket)
{
- int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
+ if (mc_mode == MC_MODE_NONE) {
+ if (getenv(MC_ENV_SOCKET_FD)) {
+ mc_mode = MC_MODE_CLIENT;
+ } else {
+ mc_mode = MC_MODE_STANDALONE;
+ }
+ }
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();
+ mc_model_checker = MC_model_checker_new(pid, socket);
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) {
+ if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination) {
/* 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: */
+
+ MC_ignore_heap(mc_time, simix_process_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));
+ 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);
+
+ if (mc_mode == MC_MODE_CLIENT) {
+ // This will move somehwere else:
+ MC_client_handle_messages();
+ }
}
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;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
/* Create exploration stack */
mc_stack = xbt_fifo_new();
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->comm_deterministic = 1;
+ 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;
-
+ mmalloc_set_current_heap(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;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
/* Create exploration stack */
mc_stack = xbt_fifo_new();
MC_modelcheck_safety();
- if (mc_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(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;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
/* Create exploration stack */
mc_stack = xbt_fifo_new();
MC_print_statistics(mc_stats);
xbt_free(mc_time);
- if (mc_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(heap);
}
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 (mc_reduce_kind == e_mc_reduce_unset)
- mc_reduce_kind = e_mc_reduce_dpor;
- XBT_INFO("Check a safety property");
+ if(_sg_mc_termination){
+ XBT_INFO("Check non progressive cycles");
+ mc_reduce_kind = e_mc_reduce_none;
+ }else{
+ XBT_INFO("Check a safety property");
+ }
MC_modelcheck_safety_init();
} else {
if (mc_reduce_kind == e_mc_reduce_unset)
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));
+ if (s == -1)
+ xbt_die("Could not receive message");
+ else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
+ xbt_die("Unexpected message, expected MC_MESSAGE_DEADLOCK_CHECK_REPLY %i %i vs %i %i",
+ (int) s, (int) message.type, (int) sizeof(message), (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY
+ );
+ }
+ 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;
}
break;
case MC_CALL_TYPE_SEND:
case MC_CALL_TYPE_RECV:
- get_comm_pattern(pattern, req, call_type);
+ get_comm_pattern(pattern, req, call_type, backtracking);
break;
case MC_CALL_TYPE_WAIT:
case MC_CALL_TYPE_WAITANY:
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);
- // First wait only must be considered:
- if (current_comm->comm.refcount == 1)
- complete_comm_pattern(pattern, current_comm, backtracking);
- break;
+ complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking);
}
+ break;
default:
xbt_die("Unexpected call type %i", (int)call_type);
}
*/
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;
XBT_DEBUG("**** Begin Replay ****");
/* Intermediate backtracking */
- if(_sg_mc_checkpoint > 0) {
+ if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
start_item = xbt_fifo_get_first_item(stack);
state = (mc_state_t)xbt_fifo_get_item_content(start_item);
if(state->system_state){
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)) {
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
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)
}
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)) {
}
- 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;
}
}
- if (!raw_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
}
void MC_show_deadlock(smx_simcall_t req)
MC_print_statistics(mc_stats);
}
+ void MC_show_non_termination(void){
+ XBT_INFO("******************************************");
+ XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+ XBT_INFO("******************************************");
+ XBT_INFO("Counter-example execution trace:");
+ MC_dump_stack_safety(mc_stack);
+ MC_print_statistics(mc_stats);
+ }
+
void MC_show_stack_liveness(xbt_fifo_t stack)
{
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("**** Only-send-deterministic communication pattern ****");
+ XBT_INFO("******************************************************");
+ XBT_INFO("%s", initial_global_state->recv_diff);
+ }else if(!initial_global_state->send_deterministic && initial_global_state->recv_deterministic) {
+ XBT_INFO("******************************************************");
+ XBT_INFO("**** Only-recv-deterministic communication pattern ****");
+ 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 (initial_global_state != NULL) {
+ if (initial_global_state != NULL && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
+ XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes");
if (_sg_mc_comms_determinism)
- XBT_INFO("Communication-deterministic : %s", !initial_global_state->comm_deterministic ? "No" : "Yes");
- if (_sg_mc_send_determinism)
- XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes");
+ 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);
}
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;
++nstack;
}
-
- if (raw_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(heap);
}
#endif
+ /* MC interface: definitions that non-MC modules must see, but not the user */
+
+ /* 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 <unistd.h> // pread, pwrite
+
#include "mc_page_store.h"
#include "mc_mmu.h"
#include "mc_private.h"
* @param reference_pages Snapshot page numbers of the previous soft_dirty_reset (or NULL)
* @return Snapshot page numbers of this new snapshot
*/
-size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages)
+size_t* mc_take_page_snapshot_region(mc_process_t process,
+ void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages)
{
size_t* pagenos = (size_t*) malloc(page_count * sizeof(size_t));
+ const bool is_self = MC_process_is_self(process);
+
+ void* temp = NULL;
+ if (!is_self)
+ temp = malloc(xbt_pagesize);
+
for (size_t i=0; i!=page_count; ++i) {
bool softclean = pagemap && !(pagemap[i] & SOFT_DIRTY);
if (softclean && reference_pages) {
// Otherwise, we need to store the page the hard way
// (by reading its content):
void* page = (char*) data + (i << xbt_pagebits);
- pagenos[i] = mc_model_checker->pages->store_page(page);
+ xbt_assert(mc_page_offset(page)==0, "Not at the beginning of a page");
+ void* page_data;
+ if (is_self) {
+ page_data = page;
+ } else {
+ /* Adding another copy (and a syscall) will probably slow things a lot.
+ TODO, optimize this somehow (at least by grouping the syscalls)
+ if needed. Either:
+ - reduce the number of syscalls;
+ - let the application snapshot itself;
+ - move the segments in shared memory (this will break `fork` however).
+ */
+ page_data = temp;
+ MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+ temp, page, xbt_pagesize, MC_PROCESS_INDEX_DISABLED);
+ }
+ pagenos[i] = mc_model_checker->pages->store_page(page_data);
}
}
+ free(temp);
return pagenos;
}
* @param pagemap Linux kernel pagemap values fot this region (or NULL)
* @param reference_pages Snapshot page numbers of the previous soft_dirty_reset (or NULL)
*/
-void mc_restore_page_snapshot_region(void* start_addr, size_t page_count, size_t* pagenos, uint64_t* pagemap, size_t* reference_pagenos)
+void mc_restore_page_snapshot_region(mc_process_t process,
+ void* start_addr, size_t page_count, size_t* pagenos, uint64_t* pagemap, size_t* reference_pagenos)
{
for (size_t i=0; i!=page_count; ++i) {
// Otherwise, copy the page:
void* target_page = mc_page_from_number(start_addr, i);
const void* source_page = mc_model_checker->pages->get_page(pagenos[i]);
- memcpy(target_page, source_page, xbt_pagesize);
+ MC_process_write(process, source_page, target_page, xbt_pagesize);
}
}
// ***** High level API
-mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg)
+mc_mem_region_t mc_region_new_sparse(mc_region_type_t region_type,
+ void *start_addr, void* permanent_addr, size_t size,
+ mc_mem_region_t ref_reg)
{
- mc_mem_region_t new_reg = xbt_new(s_mc_mem_region_t, 1);
+ mc_process_t process = &mc_model_checker->process;
- new_reg->start_addr = start_addr;
- new_reg->permanent_addr = permanent_addr;
- new_reg->data = NULL;
- new_reg->size = size;
- new_reg->page_numbers = NULL;
+ mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
+ region->region_type = region_type;
+ region->storage_type = MC_REGION_STORAGE_TYPE_CHUNKED;
+ region->start_addr = start_addr;
+ region->permanent_addr = permanent_addr;
+ region->size = size;
xbt_assert((((uintptr_t)start_addr) & (xbt_pagesize-1)) == 0,
"Not at the beginning of a page");
size_t page_count = mc_page_count(size);
uint64_t* pagemap = NULL;
- if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot) {
- pagemap = (uint64_t*) mmalloc_no_memset(mc_heap, sizeof(uint64_t) * page_count);
+ if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot &&
+ MC_process_is_self(process)) {
+ pagemap = (uint64_t*) malloc_no_memset(sizeof(uint64_t) * page_count);
mc_read_pagemap(pagemap, mc_page_number(NULL, permanent_addr), page_count);
}
+ size_t* reg_page_numbers = NULL;
+ if (ref_reg!=NULL && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_CHUNKED)
+ reg_page_numbers = ref_reg->chunked.page_numbers;
+
// Take incremental snapshot:
- new_reg->page_numbers = mc_take_page_snapshot_region(permanent_addr, page_count, pagemap,
- ref_reg==NULL ? NULL : ref_reg->page_numbers);
+ region->chunked.page_numbers = mc_take_page_snapshot_region(process,
+ permanent_addr, page_count, pagemap, reg_page_numbers);
if(pagemap) {
mfree(mc_heap, pagemap);
}
- return new_reg;
+ return region;
}
-void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg)
+void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg, mc_mem_region_t ref_reg)
{
xbt_assert((((uintptr_t)reg->permanent_addr) & (xbt_pagesize-1)) == 0,
"Not at the beginning of a page");
uint64_t* pagemap = NULL;
// Read soft-dirty bits if necessary in order to know which pages have changed:
- if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot) {
- pagemap = (uint64_t*) mmalloc_no_memset(mc_heap, sizeof(uint64_t) * page_count);
+ if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot
+ && MC_process_is_self(process)) {
+ pagemap = (uint64_t*) malloc_no_memset(sizeof(uint64_t) * page_count);
mc_read_pagemap(pagemap, mc_page_number(NULL, reg->permanent_addr), page_count);
}
- // Incremental per-page snapshot restoration:
- mc_restore_page_snapshot_region(reg->permanent_addr, page_count, reg->page_numbers,
- pagemap, ref_reg ? ref_reg->page_numbers : NULL);
+ // Incremental per-page snapshot restoration:s
+ size_t* reg_page_numbers = NULL;
+ if (ref_reg && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_CHUNKED)
+ reg_page_numbers = ref_reg->chunked.page_numbers;
+
+ mc_restore_page_snapshot_region(process,
+ reg->permanent_addr, page_count, reg->chunked.page_numbers,
+ pagemap, reg_page_numbers);
if(pagemap) {
free(pagemap);
#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"
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_show_deadlock(smx_simcall_t req);
void MC_show_stack_safety(xbt_fifo_t stack);
void MC_dump_stack_safety(xbt_fifo_t stack);
+ void MC_show_non_termination(void);
/** Stack (of `mc_state_t`) representing the current position of the
* the MC in the exploration graph
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 **********************************/
#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)");
SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) :
simcall_comm_irecv__get__rdv(r1);
+ // FIXME, remote access to comm object
+
if (rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy
&& simcall_comm_wait__get__timeout(r2) <= 0)
return FALSE;
{
char *type = NULL, *args = NULL, *str = NULL, *p = NULL, *bs = NULL;
smx_synchro_t act = NULL;
+ smx_mutex_t mutex = NULL;
size_t size = 0;
+ smx_process_t issuer = MC_smx_simcall_get_issuer(req);
+
switch (req->call) {
case SIMCALL_COMM_ISEND:
type = xbt_strdup("iSend");
p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
args =
- bprintf("src=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+ bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
+ MC_smx_process_get_host_name(issuer),
+ MC_smx_process_get_name(issuer),
p, bs);
else
args =
- bprintf("src=(%lu)%s, buff=%s, size=%s", req->issuer->pid,
- req->issuer->name, p, bs);
+ bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
+ MC_smx_process_get_name(issuer), p, bs);
break;
case SIMCALL_COMM_IRECV:
size =
type = xbt_strdup("iRecv");
p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
bs = buff_size_to_string(size);
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
args =
- bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+ bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
+ MC_smx_process_get_host_name(issuer),
+ MC_smx_process_get_name(issuer),
p, bs);
else
args =
- bprintf("dst=(%lu)%s, buff=%s, size=%s", req->issuer->pid,
- req->issuer->name, p, bs);
+ bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
+ MC_smx_process_get_name(issuer),
+ p, bs);
break;
case SIMCALL_COMM_WAIT:
act = simcall_comm_wait__get__comm(req);
} else {
type = xbt_strdup("Wait");
p = pointer_to_string(act);
+ // TODO, fix remote access to comm
+ smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
+ smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
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) : "",
- 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) : "",
- act->comm.dst_proc ? act->comm.dst_proc->name : "");
+ src_proc ? src_proc->pid : 0,
+ src_proc ? MC_smx_process_get_host_name(src_proc) : "",
+ src_proc ? MC_smx_process_get_name(src_proc) : "",
+ dst_proc ? dst_proc->pid : 0,
+ dst_proc ? MC_smx_process_get_host_name(dst_proc) : "",
+ dst_proc ? MC_smx_process_get_name(dst_proc) : "");
}
break;
case SIMCALL_COMM_TEST:
} else {
type = xbt_strdup("Test TRUE");
p = pointer_to_string(act);
+ // TODO, get process, get process name
+ smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
+ smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
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),
- act->comm.dst_proc->pid, act->comm.dst_proc->name,
- MSG_host_get_name(act->comm.dst_proc->smx_host));
+ src_proc->pid,
+ MC_smx_process_get_name(src_proc),
+ MC_smx_process_get_host_name(src_proc),
+ dst_proc->pid,
+ MC_smx_process_get_name(dst_proc),
+ MC_smx_process_get_host_name(dst_proc));
}
break;
}
break;
+ case SIMCALL_MUTEX_LOCK:
+ mutex = simcall_mutex_lock__get__mutex(req);
+ type = xbt_strdup("Mutex LOCK");
+ args = bprintf("locked = %d, owner = %d, sleeping = %d", mutex->locked, mutex->owner != NULL ? (int)mutex->owner->pid : -1, xbt_swag_size(mutex->sleeping));
+ break;
+
case SIMCALL_MC_SNAPSHOT:
type = xbt_strdup("MC_SNAPSHOT");
args = NULL;
}
if (args != NULL) {
+ // FIXME, get process name
str =
- bprintf("[(%lu)%s (%s)] %s(%s)", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+ bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
+ MC_smx_process_get_host_name(issuer),
+ MC_smx_process_get_name(issuer),
type, args);
} else {
+ // FIXME, get process name
str =
- bprintf("[(%lu)%s (%s)] %s ", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+ bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
+ MC_smx_process_get_host_name(issuer),
+ MC_smx_process_get_name(issuer),
type);
}
smx_synchro_t action;
xbt_dynar_foreach(simcall_comm_testany__get__comms(req), cursor, action) {
+ // FIXME, remote access to comm object
if (action->comm.src_proc && action->comm.dst_proc)
return FALSE;
}
{
smx_synchro_t act;
+ // FIXME, remote access to comm object
+
switch (req->call) {
case SIMCALL_COMM_WAIT:
char *MC_request_get_dot_output(smx_simcall_t req, int value)
{
-
char *str = NULL, *label = NULL;
smx_synchro_t act = NULL;
-
+
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
+
switch (req->call) {
case SIMCALL_COMM_ISEND:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] iSend", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] iSend", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
else
- label = bprintf("[(%lu)] iSend", req->issuer->pid);
+ label = bprintf("[(%lu)] iSend", issuer->pid);
break;
case SIMCALL_COMM_IRECV:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] iRecv", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] iRecv", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
else
- label = bprintf("[(%lu)] iRecv", req->issuer->pid);
+ label = bprintf("[(%lu)] iRecv", issuer->pid);
break;
case SIMCALL_COMM_WAIT:
act = simcall_comm_wait__get__comm(req);
if (value == -1) {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] WaitTimeout", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
else
- label = bprintf("[(%lu)] WaitTimeout", req->issuer->pid);
+ label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
} else {
- if (req->issuer->smx_host)
+ // FIXME, remote access to act->comm
+ smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
+ smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host),
- act->comm.src_proc ? act->comm.src_proc->pid : 0,
- act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
+ bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
+ MC_smx_process_get_host_name(issuer),
+ src_proc ? src_proc->pid : 0,
+ dst_proc ? dst_proc->pid : 0);
else
label =
- bprintf("[(%lu)] Wait [(%lu)->(%lu)]", req->issuer->pid,
- act->comm.src_proc ? act->comm.src_proc->pid : 0,
- act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
+ bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
+ src_proc ? src_proc->pid : 0,
+ dst_proc ? dst_proc->pid : 0);
}
break;
case SIMCALL_COMM_TEST:
act = simcall_comm_test__get__comm(req);
if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] Test FALSE", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] Test FALSE", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
else
- label = bprintf("[(%lu)] Test FALSE", req->issuer->pid);
+ label = bprintf("[(%lu)] Test FALSE", issuer->pid);
} else {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] Test TRUE", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] Test TRUE", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
else
- label = bprintf("[(%lu)] Test TRUE", req->issuer->pid);
+ label = bprintf("[(%lu)] Test TRUE", issuer->pid);
}
break;
case SIMCALL_COMM_WAITANY:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] WaitAny [%d of %lu]", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), value + 1,
+ bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
+ MC_smx_process_get_host_name(issuer), value + 1,
xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
else
label =
- bprintf("[(%lu)] WaitAny [%d of %lu]", req->issuer->pid, value + 1,
+ bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
break;
case SIMCALL_COMM_TESTANY:
if (value == -1) {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] TestAny FALSE", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
else
- label = bprintf("[(%lu)] TestAny FALSE", req->issuer->pid);
+ label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
} else {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), value + 1,
+ bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
+ MC_smx_process_get_host_name(issuer), value + 1,
xbt_dynar_length(simcall_comm_testany__get__comms(req)));
else
label =
- bprintf("[(%lu)] TestAny TRUE [%d of %lu]", req->issuer->pid,
+ bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
value + 1,
xbt_dynar_length(simcall_comm_testany__get__comms(req)));
}
break;
+ case SIMCALL_MUTEX_LOCK:
+ label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid);
+ break;
+
case SIMCALL_MC_RANDOM:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] MC_RANDOM (%d)", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), value);
+ bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
+ MC_smx_process_get_host_name(issuer), value);
else
- label = bprintf("[(%lu)] MC_RANDOM (%d)", req->issuer->pid, value);
+ label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
break;
case SIMCALL_MC_SNAPSHOT:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] MC_SNAPSHOT", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
else
- label = bprintf("[(%lu)] MC_SNAPSHOT", req->issuer->pid);
+ label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
break;
case SIMCALL_MC_COMPARE_SNAPSHOTS:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
else
- label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", req->issuer->pid);
+ label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
break;
default:
str =
bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
- colors[req->issuer->pid - 1], colors[req->issuer->pid - 1]);
+ colors[issuer->pid - 1], colors[issuer->pid - 1]);
xbt_free(label);
return str;
/* 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 "mc_state.h"
#include "mc_request.h"
#include "mc_safety.h"
#include "mc_private.h"
#include "mc_record.h"
+#include "mc_smx.h"
#include "xbt/mmalloc/mmprivate.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
+ static int is_exploration_stack_state(mc_state_t current_state){
+
+ xbt_fifo_item_t item;
+ mc_state_t stack_state;
+ for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
+ stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
+ if(snapshot_compare(stack_state, current_state) == 0){
+ XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
+ return 1;
+ }
+ }
+ return 0;
+ }
+
/**
* \brief Initialize the DPOR exploration algorithm
*/
void MC_pre_modelcheck_safety()
{
-
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
mc_state_t initial_state = NULL;
smx_process_t process;
- /* Create the initial state and push it into the exploration stack */
- if (!mc_mem_set)
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if (_sg_mc_visited > 0)
visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
initial_state = MC_state_new();
-
MC_SET_STD_HEAP;
XBT_DEBUG("**************************************************");
MC_SET_MC_HEAP;
/* Get an enabled process and insert it in the interleave set of the initial state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(initial_state, process);
if (mc_reduce_kind != e_mc_reduce_none)
break;
}
- }
+ );
xbt_fifo_unshift(mc_stack, initial_state);
-
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
}
mc_stats->executed_transitions++;
/* Answer the request */
- SIMIX_simcall_handle(req, value);
+ MC_simcall_handle(req, value);
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
next_state = MC_state_new();
+ if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+ MC_show_non_termination();
+ return;
+ }
+
if ((visited_state = is_visited_state(next_state)) == NULL) {
/* Get an enabled process and insert it in the interleave set of the next state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(next_state, process);
if (mc_reduce_kind != e_mc_reduce_none)
break;
}
- }
+ );
if (dot_output != NULL)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
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_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)) {
xbt_free(req_str);
}
- if (!MC_state_process_is_done(prev_state, req->issuer))
- MC_state_interleave_process(prev_state, req->issuer);
+ if (!MC_state_process_is_done(prev_state, issuer))
+ MC_state_interleave_process(prev_state, issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
} else {
+ 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, req->issuer->pid, state->num,
+ req->call, issuer->pid, state->num,
MC_state_get_internal_request(prev_state)->call,
- MC_state_get_internal_request(prev_state)->issuer->pid,
+ previous_issuer->pid,
prev_state->num);
}
#include "mc_model_checker.h"
#include "mc_page_store.h"
#include "mc_mmalloc.h"
+#include "mc_address_space.h"
+#include "mc_unw.h"
SG_BEGIN_DECL()
// ***** Snapshot region
-#define NB_REGIONS 3 /* binary data (data + BSS) (type = 2), libsimgrid data (data + BSS) (type = 1), std_heap (type = 0)*/
+typedef enum e_mc_region_type_t {
+ MC_REGION_TYPE_UNKNOWN = 0,
+ MC_REGION_TYPE_HEAP = 1,
+ MC_REGION_TYPE_DATA = 2
+} mc_region_type_t;
+
+// TODO, use OO instead of this
+typedef enum e_mc_region_storeage_type_t {
+ MC_REGION_STORAGE_TYPE_NONE = 0,
+ MC_REGION_STORAGE_TYPE_FLAT = 1,
+ MC_REGION_STORAGE_TYPE_CHUNKED = 2,
+ MC_REGION_STORAGE_TYPE_PRIVATIZED = 3
+} mc_region_storage_type_t;
/** @brief Copy/snapshot of a given memory region
*
- * Two types of region snapshots exist:
+ * Different types of region snapshot storage types exist:
* <ul>
* <li>flat/dense snapshots are a simple copy of the region;</li>
* <li>sparse/per-page snapshots are snaapshots which shared
* identical pages.</li>
+ * <li>privatized (SMPI global variable privatisation).
* </ul>
+ *
+ * This is handled with a variant based approch:
+ *
+ * * `storage_type` identified the type of storage;
+ * * an anonymous enum is used to distinguish the relevant types for
+ * each type.
*/
-typedef struct s_mc_mem_region{
+typedef struct s_mc_mem_region s_mc_mem_region_t, *mc_mem_region_t;
+
+struct s_mc_mem_region {
+ mc_region_type_t region_type;
+ mc_region_storage_type_t storage_type;
+ mc_object_info_t object_info;
+
/** @brief Virtual address of the region in the simulated process */
void *start_addr;
+ /** @brief Size of the data region in bytes */
+ size_t size;
+
/** @brief Permanent virtual address of the region
*
* This is usually the same address as the simuilated process address.
* */
void *permanent_addr;
- /** @brief Copy of the snapshot for flat snapshots regions (NULL otherwise) */
- void *data;
+ union {
+ struct {
+ /** @brief Copy of the snapshot for flat snapshots regions (NULL otherwise) */
+ void *data;
+ } flat;
+ struct {
+ /** @brief Pages indices in the page store for per-page snapshots (NULL otherwise) */
+ size_t* page_numbers;
+ } chunked;
+ struct {
+ size_t regions_count;
+ mc_mem_region_t* regions;
+ } privatized;
+ };
- /** @brief Size of the data region in bytes */
- size_t size;
-
- /** @brief Pages indices in the page store for per-page snapshots (NULL otherwise) */
- size_t* page_numbers;
-
-} s_mc_mem_region_t, *mc_mem_region_t;
+};
-mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, void* data_addr, size_t size, mc_mem_region_t ref_reg);
+mc_mem_region_t mc_region_new_sparse(mc_region_type_t type, void *start_addr, void* data_addr, size_t size, mc_mem_region_t ref_reg);
void MC_region_destroy(mc_mem_region_t reg);
-void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg);
+void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg, mc_mem_region_t ref_reg);
static inline __attribute__ ((always_inline))
-bool mc_region_contain(mc_mem_region_t region, void* p)
+bool mc_region_contain(mc_mem_region_t region, const void* p)
{
return p >= region->start_addr &&
p < (void*)((char*) region->start_addr + region->size);
void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region)
{
size_t pageno = mc_page_number(region->start_addr, (void*) addr);
- size_t snapshot_pageno = region->page_numbers[pageno];
+ size_t snapshot_pageno = region->chunked.page_numbers[pageno];
const void* snapshot_page = mc_page_store_get_page(mc_model_checker->pages, snapshot_pageno);
return (char*) snapshot_page + mc_page_offset((void*) addr);
}
-mc_mem_region_t mc_get_snapshot_region(void* addr, mc_snapshot_t snapshot, int process_index);
+mc_mem_region_t mc_get_snapshot_region(const void* addr, mc_snapshot_t snapshot, int process_index);
/** \brief Translate a pointer from process address space to snapshot address space
*
return (void *) addr;
}
- // Flat snapshot:
- else if (region->data) {
- uintptr_t offset = addr - (uintptr_t) region->start_addr;
- return (void *) ((uintptr_t) region->data + offset);
- }
+ switch (region->storage_type) {
+ case MC_REGION_STORAGE_TYPE_NONE:
+ default:
+ xbt_die("Storage type not supported");
+
+ case MC_REGION_STORAGE_TYPE_FLAT:
+ {
+ uintptr_t offset = addr - (uintptr_t) region->start_addr;
+ return (void *) ((uintptr_t) region->flat.data + offset);
+ }
- // Per-page snapshot:
- else if (region->page_numbers) {
+ case MC_REGION_STORAGE_TYPE_CHUNKED:
return mc_translate_address_region(addr, region);
- }
- else {
- xbt_die("No data for this memory region");
+ case MC_REGION_STORAGE_TYPE_PRIVATIZED:
+ {
+ xbt_assert(process_index >=0,
+ "Missing process index for privatized region");
+ xbt_assert((size_t) process_index < region->privatized.regions_count,
+ "Out of range process index");
+ mc_mem_region_t subregion = region->privatized.regions[process_index];
+ xbt_assert(subregion, "Missing memory region for process %i", process_index);
+ return mc_translate_address(addr, snapshot, process_index);
+ }
}
}
int flags;
}s_fd_infos_t, *fd_infos_t;
-struct s_mc_snapshot{
+struct s_mc_snapshot {
+ mc_process_t process;
+ s_mc_address_space_t address_space;
size_t heap_bytes_used;
- mc_mem_region_t regions[NB_REGIONS];
+ mc_mem_region_t* snapshot_regions;
+ size_t snapshot_regions_count;
xbt_dynar_t enabled_processes;
- mc_mem_region_t* privatization_regions;
int privatization_index;
size_t *stack_sizes;
xbt_dynar_t stacks;
fd_infos_t *current_fd;
};
-/** @brief Process index used when no process is available
- *
- * The expected behaviour is that if a process index is needed it will fail.
- * */
-#define MC_NO_PROCESS_INDEX -1
-
-/** @brief Process index when any process is suitable
- *
- * We could use a special negative value in the future.
- */
-#define MC_ANY_PROCESS_INDEX 0
-
static inline __attribute__ ((always_inline))
mc_mem_region_t mc_get_region_hinted(void* addr, mc_snapshot_t snapshot, int process_index, mc_mem_region_t region)
{
typedef struct s_mc_snapshot_stack{
xbt_dynar_t local_variables;
+ mc_unw_context_t context;
xbt_dynar_t stack_frames; // mc_stack_frame_t
int process_index;
}s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
-typedef struct s_mc_global_t{
+typedef struct s_mc_global_t {
mc_snapshot_t snapshot;
int raw_mem_set;
int prev_pair;
char *prev_req;
int initial_communications_pattern_done;
- int comm_deterministic;
+ int recv_deterministic;
int send_deterministic;
+ char *send_diff;
+ char *recv_diff;
}s_mc_global_t, *mc_global_t;
typedef struct s_mc_checkpoint_ignore_region{
size_t size;
}s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
-static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
+static const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
mc_snapshot_t MC_take_snapshot(int num_state);
void MC_restore_snapshot(mc_snapshot_t);
int mc_important_snapshot(mc_snapshot_t snapshot);
-size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages);
+size_t* mc_take_page_snapshot_region(mc_process_t process,
+ void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages);
void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
-void mc_restore_page_snapshot_region(void* start_addr, size_t page_count, size_t* pagenos, uint64_t* pagemap, size_t* reference_pagenos);
-
-static inline __attribute__((always_inline))
-bool mc_snapshot_region_linear(mc_mem_region_t region) {
- return !region || !region->data;
-}
-
-void* mc_snapshot_read_fragmented(void* addr, mc_mem_region_t region, void* target, size_t size);
-
-void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, int process_index, void* target, size_t size);
-int mc_snapshot_region_memcmp(
- void* addr1, mc_mem_region_t region1,
- void* addr2, mc_mem_region_t region2, size_t size);
-int mc_snapshot_memcmp(
- void* addr1, mc_snapshot_t snapshot1,
- void* addr2, mc_snapshot_t snapshot2, int process_index, size_t size);
-
-static void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot, int process_index);
+void mc_restore_page_snapshot_region(
+ mc_process_t process,
+ void* start_addr, size_t page_count, size_t* pagenos,
+ uint64_t* pagemap, size_t* reference_pagenos);
+
+const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, const void* addr, size_t size);
+
+const void* MC_snapshot_read(mc_snapshot_t snapshot, e_adress_space_read_flags_t flags,
+ void* target, const void* addr, size_t size, int process_index);
+int MC_snapshot_region_memcmp(
+ const void* addr1, mc_mem_region_t region1,
+ const void* addr2, mc_mem_region_t region2, size_t size);
+int MC_snapshot_memcmp(
+ const void* addr1, mc_snapshot_t snapshot1,
+ const void* addr2, mc_snapshot_t snapshot2, int process_index, size_t size);
static inline __attribute__ ((always_inline))
-void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot, int process_index)
+const void* MC_snapshot_read_pointer(mc_snapshot_t snapshot, const void* addr, int process_index)
{
void* res;
- return *(void**) mc_snapshot_read(addr, snapshot, process_index, &res, sizeof(void*));
+ return *(const void**) MC_snapshot_read(snapshot, MC_ADDRESS_SPACE_READ_FLAGS_LAZY,
+ &res, addr, sizeof(void*), process_index);
}
static inline __attribute__ ((always_inline))
- void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) {
+const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot)
+{
if(snapshot==NULL)
xbt_die("snapshot is NULL");
- void** addr = &(std_heap->breakval);
- return mc_snapshot_read_pointer(addr, snapshot, MC_ANY_PROCESS_INDEX);
+ // This is &std_heap->breakval in the target process:
+ void** addr = &MC_process_get_heap(&mc_model_checker->process)->breakval;
+ // Read (std_heap->breakval) in the target process (*addr i.e. std_heap->breakval):
+ return MC_snapshot_read_pointer(snapshot, addr, MC_PROCESS_INDEX_ANY);
}
/** @brief Read memory from a snapshot region
* @return Pointer where the data is located (target buffer of original location)
*/
static inline __attribute__((always_inline))
-void* mc_snapshot_read_region(void* addr, mc_mem_region_t region, void* target, size_t size)
+const void* MC_region_read(mc_mem_region_t region, void* target, const void* addr, size_t size)
{
if (region==NULL)
+ // Should be deprecated:
return addr;
uintptr_t offset = (char*) addr - (char*) region->start_addr;
xbt_assert(mc_region_contain(region, addr),
"Trying to read out of the region boundary.");
- // Linear memory region:
- if (region->data) {
- return (char*) region->data + offset;
- }
-
- // Fragmented memory region:
- else if (region->page_numbers) {
- // Last byte of the region:
- void* end = (char*) addr + size - 1;
- if( mc_same_page(addr, end) ) {
- // The memory is contained in a single page:
- return mc_translate_address_region((uintptr_t) addr, region);
- } else {
- // The memory spans several pages:
- return mc_snapshot_read_fragmented(addr, region, target, size);
+ switch (region->storage_type) {
+ case MC_REGION_STORAGE_TYPE_NONE:
+ default:
+ xbt_die("Storage type not supported");
+
+ case MC_REGION_STORAGE_TYPE_FLAT:
+ return (char*) region->flat.data + offset;
+
+ case MC_REGION_STORAGE_TYPE_CHUNKED:
+ {
+ // Last byte of the region:
+ void* end = (char*) addr + size - 1;
+ if (mc_same_page(addr, end) ) {
+ // The memory is contained in a single page:
+ return mc_translate_address_region((uintptr_t) addr, region);
+ } else {
+ // The memory spans several pages:
+ return MC_region_read_fragmented(region, target, addr, size);
+ }
}
- }
- else {
- xbt_die("No data available for this region");
+ // We currently do not pass the process_index to this function so we assume
+ // that the privatized region has been resolved in the callers:
+ case MC_REGION_STORAGE_TYPE_PRIVATIZED:
+ xbt_die("Storage type not supported");
}
}
static inline __attribute__ ((always_inline))
-void* mc_snapshot_read_pointer_region(void* addr, mc_mem_region_t region)
+void* MC_region_read_pointer(mc_mem_region_t region, const void* addr)
{
void* res;
- return *(void**) mc_snapshot_read_region(addr, region, &res, sizeof(void*));
+ return *(void**) MC_region_read(region, &res, addr, sizeof(void*));
}
SG_END_DECL()
/* 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 "../simix/smx_private.h"
#include "xbt/fifo.h"
#include "mc_state.h"
#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;
state->in_visited_states = 0;
state->incomplete_comm_pattern = NULL;
/* Stateful model checking */
- if(_sg_mc_checkpoint > 0 && mc_stats->expanded_states % _sg_mc_checkpoint == 0){
+ if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){
state->system_state = MC_take_snapshot(state->num);
if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
copy_incomplete_communications_pattern(state);
void MC_state_interleave_process(mc_state_t state, smx_process_t process)
{
+ assert(state);
state->proc_status[process->pid].state = MC_INTERLEAVE;
state->proc_status[process->pid].interleave_count = 0;
}
case SIMCALL_COMM_WAITANY:
state->internal_req.call = SIMCALL_COMM_WAIT;
state->internal_req.issuer = req->issuer;
+ // FIXME, read from remote process
state->internal_comm =
*xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
smx_synchro_t);
state->internal_req.issuer = req->issuer;
if (value > 0)
+ // FIXME, read from remote process
state->internal_comm =
*xbt_dynar_get_as(simcall_comm_testany__get__comms(req), value,
smx_synchro_t);
case SIMCALL_COMM_WAIT:
state->internal_req = *req;
+ // FIXME, read from remote process
state->internal_comm = *(simcall_comm_wait__get__comm(req));
simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm);
simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
case SIMCALL_COMM_TEST:
state->internal_req = *req;
+ // FIXME, read from remote process
state->internal_comm = *simcall_comm_test__get__comm(req);
simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm);
simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
case SIMCALL_MC_RANDOM:
state->internal_req = *req;
- if (value != simcall_mc_random__get__max(req)) {
- xbt_swag_foreach(process, simix_global->process_list) {
+ int random_max = simcall_mc_random__get__max(req);
+ if (value != random_max) {
+ MC_EACH_SIMIX_PROCESS(process,
procstate = &state->proc_status[process->pid];
- if (process->pid == req->issuer->pid) {
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
+ if (process->pid == issuer->pid) {
procstate->state = MC_MORE_INTERLEAVE;
break;
}
- }
+ );
}
break;
unsigned int start_count;
smx_synchro_t act = NULL;
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
procstate = &state->proc_status[process->pid];
if (procstate->state == MC_INTERLEAVE
}
}
}
- }
+ );
return NULL;
}
}
/* New Module missing */
- find_coll_description(table, val);
+ find_coll_description(table, val, category);
}
static void _sg_cfg_cb__coll_gather(const char *name, int pos){
_sg_cfg_cb__coll("gather", mpi_coll_gather_description, name, pos);
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)",
"Specify the name of dot file corresponding to graph state",
xbt_cfgelm_string, 1, 1, _mc_cfg_cb_dot_output, NULL);
xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/dot_output", "");
+
+ /* Enable/disable non progressive cycles detection with model-checking */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/termination",
+ "Enable/Disable non progressive cycle detection",
+ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_termination, NULL);
+ xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/termination", "no");
#endif
/* do verbose-exit */
surf_callback(void, void) surfExitCallbacks;
s_surf_model_description_t surf_plugin_description[] = {
- {"Energy",
- "Cpu energy consumption.",
- sg_energy_plugin_init},
+ {"Energy", "Cpu energy consumption.", sg_energy_plugin_init},
{NULL, NULL, NULL} /* this array must be NULL terminated */
};
m_lastUpdate = now;
m_lastValue = lmm_variable_getvalue(getVariable());
}
-
