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);
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;
/* 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);
} 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;
}
}
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);
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)
