return res;
}
-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)
{
- 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;
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);
MC_process_read_simple(&mc_model_checker->process,
- comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size);
+ 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, 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){
+ 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;
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);
+ 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_comm_pattern->index_comm + 1);
+ 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("*********************************************************");
void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
{
+ 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;
-
- // Fill initial_pattern->index_comm:
- 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);
-
if (call_type == MC_CALL_TYPE_SEND) {
/* Create comm pattern */
pattern->type = SIMIX_COMM_SEND;
- pattern->comm = simcall_comm_isend__get__result(request);
+ 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, sizeof(synchro));
+ &synchro, pattern->comm_addr, sizeof(synchro));
char* remote_name;
MC_process_read_simple(&mc_model_checker->process, &remote_name,
if(mpi_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);
+ 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);
- ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->index_comm++;
+ 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);
+ pattern->comm_addr = simcall_comm_irecv__get__result(request);
struct s_smpi_mpi_request mpi_request;
MC_process_read_simple(&mc_model_checker->process,
s_smx_synchro_t synchro;
MC_process_read_simple(&mc_model_checker->process,
- &synchro, pattern->comm, sizeof(synchro));
+ &synchro, pattern->comm_addr, sizeof(synchro));
char* remote_name;
MC_process_read_simple(&mc_model_checker->process, &remote_name,
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 MC_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_addr, unsigned int issuer, int backtracking) {
mc_comm_pattern_t current_comm_pattern;
unsigned int cursor = 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, issuer, xbt_dynar_t), cursor, current_comm_pattern) {
- if (current_comm_pattern-> comm == comm) {
- update_comm_pattern(current_comm_pattern, comm);
+ 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_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &comm_pattern);
+ 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(!completed)
xbt_die("Corresponding communication not found!");
+ mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
+ initial_communications_pattern, issuer, mc_list_comm_pattern_t);
+
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, issuer, mc_list_comm_pattern_t))->list, &comm_pattern);
+ xbt_dynar_push(pattern->list, &comm_pattern);
} else {
/* Evaluate comm determinism */
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++;
+ pattern->index_comm++;
}
}
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);
+ // 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 < MC_smx_get_maxpid(); i++){
+ 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), 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 < MC_smx_get_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);
}
MC_print_statistics(mc_stats);
MC_SET_STD_HEAP;
- return;
+ exit(0);
}
void MC_modelcheck_comm_determinism(void)
#include <xbt/dynar.h>
#include "mc_comm_pattern.h"
+#include "mc_smx.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_pattern, mc,
+ "Logging specific to MC communication patterns");
mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm)
{
mc_comm_pattern_t res = xbt_new0(s_mc_comm_pattern_t, 1);
res->index = comm->index;
res->type = comm->type;
- res->comm = comm->comm;
+ res->comm_addr = comm->comm_addr;
res->rdv = strdup(comm->rdv);
res->data_size = -1;
res->data = NULL;
return res;
}
+static void MC_patterns_copy(xbt_dynar_t dest, xbt_dynar_t source)
+{
+ xbt_dynar_reset(dest);
+
+ unsigned int cursor;
+ mc_comm_pattern_t comm;
+ xbt_dynar_foreach(source, cursor, comm) {
+ mc_comm_pattern_t copy_comm = MC_comm_pattern_dup(comm);
+ xbt_dynar_push(dest, ©_comm);
+ }
+}
+
void MC_restore_communications_pattern(mc_state_t state)
{
mc_list_comm_pattern_t list_process_comm;
}
for (int i = 0; i < MC_smx_get_maxpid(); i++) {
- xbt_dynar_t initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
- xbt_dynar_reset(initial_incomplete_process_comms);
- xbt_dynar_t incomplete_process_comms = xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t);
-
- mc_comm_pattern_t comm;
- xbt_dynar_foreach(incomplete_process_comms, cursor, comm) {
- mc_comm_pattern_t copy_comm = MC_comm_pattern_dup(comm);
- xbt_dynar_push(initial_incomplete_process_comms, ©_comm);
- }
-
+ MC_patterns_copy(
+ xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t),
+ xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t)
+ );
}
}
}
}
+void MC_handle_comm_pattern(
+ e_mc_call_type_t call_type, smx_simcall_t req,
+ int value, xbt_dynar_t pattern, int backtracking)
+{
+
+ switch(call_type) {
+ case MC_CALL_TYPE_NONE:
+ break;
+ case MC_CALL_TYPE_SEND:
+ case MC_CALL_TYPE_RECV:
+ MC_get_comm_pattern(pattern, req, call_type, backtracking);
+ break;
+ case MC_CALL_TYPE_WAIT:
+ case MC_CALL_TYPE_WAITANY:
+ {
+ smx_synchro_t comm_addr = NULL;
+ if (call_type == MC_CALL_TYPE_WAIT)
+ comm_addr = simcall_comm_wait__get__comm(req);
+ else
+ // comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):
+ MC_process_read_dynar_element(&mc_model_checker->process, &comm_addr,
+ simcall_comm_waitany__get__comms(req), value, sizeof(comm_addr));
+ MC_complete_comm_pattern(pattern, comm_addr,
+ MC_smx_simcall_get_issuer(req)->pid, backtracking);
+ }
+ break;
+ default:
+ xbt_die("Unexpected call type %i", (int)call_type);
+ }
+
+}
+
void MC_comm_pattern_free(mc_comm_pattern_t p)
{
xbt_free(p->rdv);
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
+#include <assert.h>
#include <string.h>
#include <stdint.h>
iteration of the model-checker (in RAW memory) */
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
mc_model_checker = MC_model_checker_new(pid, socket);
- if (mc_mode == MC_MODE_SERVER) {
+
+ // It's not useful anymore:
+ if (0 && mc_mode == MC_MODE_SERVER) {
unsigned long maxpid;
MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
&maxpid, sizeof(maxpid));
MC_client_main_loop();
return;
case MC_MODE_SERVER:
+ break;
case MC_MODE_STANDALONE:
+ MC_init();
break;
}
return deadlock;
}
-void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) {
-
- switch(call_type) {
- case MC_CALL_TYPE_NONE:
- break;
- case MC_CALL_TYPE_SEND:
- case MC_CALL_TYPE_RECV:
- MC_get_comm_pattern(pattern, req, call_type, backtracking);
- break;
- case MC_CALL_TYPE_WAIT:
- case MC_CALL_TYPE_WAITANY:
- {
- smx_synchro_t current_comm = NULL;
- if (call_type == MC_CALL_TYPE_WAIT)
- current_comm = simcall_comm_wait__get__comm(req);
- else
- current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t);
- MC_complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking);
- }
- break;
- default:
- xbt_die("Unexpected call type %i", (int)call_type);
- }
-
-}
-
/**
* \brief Re-executes from the state at position start all the transitions indicated by
* a given model-checker stack.
MC_SET_MC_HEAP;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- for (j=0; j < simix_process_maxpid; j++) {
+ // int n = xbt_dynar_length(incomplete_communications_pattern);
+ int n = MC_smx_get_maxpid();
+ assert(n == xbt_dynar_length(incomplete_communications_pattern));
+ assert(n == xbt_dynar_length(initial_communications_pattern));
+ for (j=0; j < n ; j++) {
xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
- ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t))->index_comm = 0;
+ xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t)->index_comm = 0;
}
}
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_handle_comm_pattern(call, req, value, NULL, 1);
MC_SET_STD_HEAP;
-
+
MC_wait_for_requests();
count++;