#include "mc_private.h"
#include "mc_record.h"
#include "mc_smx.h"
+#include "mc_client.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
"Logging specific to MC communication determinism detection");
/********** Static functions ***********/
-static void comm_pattern_free(mc_comm_pattern_t p)
-{
- xbt_free(p->rdv);
- xbt_free(p->data);
- xbt_free(p);
- p = NULL;
-}
-
-static void list_comm_pattern_free(mc_list_comm_pattern_t l)
-{
- xbt_dynar_free(&(l->list));
- xbt_free(l);
- l = NULL;
-}
-
static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
if(comm1->type != comm2->type)
return TYPE_DIFF;
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();
}
+ return 0;
}
-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 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_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)
+static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
{
- mc_process_t process = &mc_model_checker->process;
- void *addr_pointed;
- 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);
+ s_smx_synchro_t comm;
+ MC_process_read_simple(&mc_model_checker->process,
+ &comm, comm_addr, sizeof(comm));
+
+ 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);
+ if (comm_pattern->data_size == -1 && comm.comm.src_buff != NULL) {
+ size_t buff_size;
+ MC_process_read_simple(&mc_model_checker->process,
+ &buff_size, comm.comm.dst_buff_size, sizeof(buff_size));
+ comm_pattern->data_size = buff_size;
comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
- addr_pointed = *(void **) comm->comm.src_buff;
- 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_process_read_simple(&mc_model_checker->process,
+ comm_pattern->data, comm.comm.src_buff, comm_pattern->data_size);
}
}
static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
- 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);
+ mc_list_comm_pattern_t list =
+ 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);
- e_mc_comm_pattern_difference_t diff;
-
- if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){
- if (comm->type == SIMIX_COMM_SEND)
+ mc_comm_pattern_t initial_comm =
+ xbt_dynar_get_as(list->list, list->index_comm, mc_comm_pattern_t);
+ e_mc_comm_pattern_difference_t diff =
+ compare_comm_pattern(initial_comm, comm);
+
+ if (diff != NONE_DIFF) {
+ 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->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->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);
+ MC_comm_pattern_free(comm);
}
/********** Non Static functions ***********/
-void comm_pattern_free_voidp(void *p) {
- comm_pattern_free((mc_comm_pattern_t) * (void **) p);
-}
-
-void list_comm_pattern_free_voidp(void *p) {
- 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 MC_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);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
+ mc_list_comm_pattern_t initial_pattern = xbt_dynar_get_as(
+ initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
+ xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
+ incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+
+ mc_comm_pattern_t 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;
-
+
if (call_type == MC_CALL_TYPE_SEND) {
/* 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 = MC_smx_resolve_process(pattern->comm->comm.src_proc)->pid;
+ pattern->comm_addr = simcall_comm_isend__get__result(request);
+
+ s_smx_synchro_t synchro;
+ MC_process_read_simple(&mc_model_checker->process,
+ &synchro, pattern->comm_addr, sizeof(synchro));
+
+ char* remote_name;
+ MC_process_read_simple(&mc_model_checker->process, &remote_name,
+ synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name,
+ sizeof(remote_name));
+ pattern->rdv =
+ MC_process_read_string(&mc_model_checker->process, remote_name);
+ pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
pattern->src_host = MC_smx_process_get_host_name(issuer);
- if(pattern->comm->comm.src_buff != NULL){
- pattern->data_size = pattern->comm->comm.src_buff_size;
+
+ struct s_smpi_mpi_request mpi_request;
+ MC_process_read_simple(&mc_model_checker->process,
+ &mpi_request, (MPI_Request) simcall_comm_isend__get__data(request),
+ sizeof(mpi_request));
+ pattern->tag = mpi_request.tag;
+
+ if(synchro.comm.src_buff != NULL){
+ pattern->data_size = synchro.comm.src_buff_size;
pattern->data = xbt_malloc0(pattern->data_size);
- addr_pointed = *(void **) pattern->comm->comm.src_buff;
- 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);
+ MC_process_read_simple(&mc_model_checker->process,
+ pattern->data, synchro.comm.src_buff, pattern->data_size);
+ }
+ if(mpi_request.detached){
+ if (!initial_global_state->initial_communications_pattern_done) {
+ /* Store comm pattern */
+ xbt_dynar_push(
+ 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);
+ 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->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
- pattern->dst_proc = MC_smx_resolve_process(pattern->comm->comm.dst_proc)->pid;
- // FIXME, remote process access
+ pattern->comm_addr = simcall_comm_irecv__get__result(request);
+
+ struct s_smpi_mpi_request mpi_request;
+ MC_process_read_simple(&mc_model_checker->process,
+ &mpi_request, (MPI_Request) simcall_comm_irecv__get__data(request),
+ sizeof(mpi_request));
+ pattern->tag = mpi_request.tag;
+
+ s_smx_synchro_t synchro;
+ MC_process_read_simple(&mc_model_checker->process,
+ &synchro, pattern->comm_addr, sizeof(synchro));
+
+ char* remote_name;
+ MC_process_read_simple(&mc_model_checker->process, &remote_name,
+ synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name,
+ sizeof(remote_name));
+ pattern->rdv =
+ MC_process_read_string(&mc_model_checker->process, remote_name);
+ pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
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, issuer->pid, xbt_dynar_t), &pattern);
+ xbt_dynar_push(
+ xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
+ &pattern);
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 MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, 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) {
- 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);
+ xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) {
+ if (current_comm_pattern->comm_addr == comm_addr) {
+ update_comm_pattern(current_comm_pattern, comm_addr);
+ completed = 1;
+ xbt_dynar_remove_at(
+ 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;
+ mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
+ initial_communications_pattern, issuer, mc_list_comm_pattern_t);
- 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(pattern->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);
+ pattern->index_comm++;
}
}
+
/************************ Main algorithm ************************/
-void MC_pre_modelcheck_comm_determinism(void)
+static void MC_modelcheck_comm_determinism_main(void);
+
+static void MC_pre_modelcheck_comm_determinism(void)
{
MC_SET_MC_HEAP;
mc_state_t initial_state = NULL;
smx_process_t process;
int i;
+ const int maxpid = MC_smx_get_maxpid();
if (_sg_mc_visited > 0)
visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
- initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), list_comm_pattern_free_voidp);
- for (i=0; i<simix_process_maxpid; i++){
+ // Create initial_communications_pattern elements:
+ initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
+ for (i=0; i < maxpid; i++){
mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
- process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+ process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp);
process_list_pattern->index_comm = 0;
xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
}
+
+ // Create incomplete_communications_pattern elements:
incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
- for (i=0; i<simix_process_maxpid; i++){
+ for (i=0; i < maxpid; i++){
xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), NULL);
xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
}
}
-void MC_modelcheck_comm_determinism(void)
+static void MC_modelcheck_comm_determinism_main(void)
{
char *req_str = NULL;
&& (req = MC_state_get_request(state, &value))
&& (visited_state == NULL)) {
- req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Execute: %s", req_str);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+ XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
if (dot_output != NULL) {
/* TODO : handle test and testany simcalls */
e_mc_call_type_t call = MC_CALL_TYPE_NONE;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- call = mc_get_call_type(req);
+ call = MC_get_call_type(req);
}
/* Answer the request */
MC_SET_MC_HEAP;
if(!initial_global_state->initial_communications_pattern_done)
- handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
+ MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
else
- handle_comm_pattern(call, req, value, NULL, 0);
+ MC_handle_comm_pattern(call, req, value, NULL, 0);
MC_SET_STD_HEAP;
/* Wait for requests (schedules processes) */
MC_print_statistics(mc_stats);
MC_SET_STD_HEAP;
- return;
+ exit(0);
+}
+
+void MC_modelcheck_comm_determinism(void)
+{
+ if (mc_mode == MC_MODE_CLIENT) {
+ // This will move somehwere else:
+ MC_client_handle_messages();
+ }
+
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+
+ /* Create exploration stack */
+ mc_stack = xbt_fifo_new();
+
+ MC_SET_STD_HEAP;
+
+ MC_pre_modelcheck_comm_determinism();
+
+ MC_SET_MC_HEAP;
+ initial_global_state = xbt_new0(s_mc_global_t, 1);
+ initial_global_state->snapshot = MC_take_snapshot(0);
+ initial_global_state->initial_communications_pattern_done = 0;
+ initial_global_state->recv_deterministic = 1;
+ initial_global_state->send_deterministic = 1;
+ initial_global_state->recv_diff = NULL;
+ initial_global_state->send_diff = NULL;
+
+ MC_SET_STD_HEAP;
+
+ MC_modelcheck_comm_determinism_main();
+
+ mmalloc_set_current_heap(heap);
}
