/********** 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 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;
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*) 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);
}
}
}
}
- 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(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
+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 = xbt_new0(s_mc_comm_pattern_t, 1);
pattern->data_size = -1;
pattern->data = NULL;
(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);
+ // TODO, resolve comm
// 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;
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*) 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, 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) {
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, unsigned int issuer, int backtracking) {
+void MC_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;
mc_comm_pattern_t comm_pattern;
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);
+ initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
for (i=0; i < MC_smx_get_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);
}
/* 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) */
