X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e5149b6787696e0041d192b0573dd0882a296c73..abf7c33aff8279f498000149d39448946c3297b3:/src/mc/mc_request.c diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index af7f1ef766..47609e83eb 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -4,9 +4,12 @@ /* 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 + #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)"); @@ -34,6 +37,25 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND) return FALSE; + // Read object from MCed memory: + s_smx_synchro_t synchro1, synchro2; + if (r1->call == SIMCALL_COMM_WAIT) { + MC_process_read_simple(&mc_model_checker->process, &synchro1, + simcall_comm_wait__get__comm(r1), sizeof(synchro1)); + } + if (r2->call == SIMCALL_COMM_WAIT) { + MC_process_read_simple(&mc_model_checker->process, &synchro2, + simcall_comm_wait__get__comm(r2), sizeof(synchro2)); + } + if (r1->call == SIMCALL_COMM_TEST) { + MC_process_read_simple(&mc_model_checker->process, &synchro1, + simcall_comm_test__get__comm(r1), sizeof(synchro1)); + } + if (r2->call == SIMCALL_COMM_TEST) { + MC_process_read_simple(&mc_model_checker->process, &synchro2, + simcall_comm_test__get__comm(r2), sizeof(synchro2)); + } + if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) && r2->call == SIMCALL_COMM_WAIT) { @@ -42,26 +64,25 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) : simcall_comm_irecv__get__rdv(r1); - if (rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy + if (rdv != synchro2.comm.rdv_cpy && simcall_comm_wait__get__timeout(r2) <= 0) return FALSE; - if ((r1->issuer != simcall_comm_wait__get__comm(r2)->comm.src_proc) - && (r1->issuer != simcall_comm_wait__get__comm(r2)->comm.dst_proc) + if ((r1->issuer != synchro2.comm.src_proc) + && (r1->issuer != synchro2.comm.dst_proc) && simcall_comm_wait__get__timeout(r2) <= 0) return FALSE; if ((r1->call == SIMCALL_COMM_ISEND) - && (simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND) - && (simcall_comm_wait__get__comm(r2)->comm.src_buff != + && (synchro2.comm.type == SIMIX_COMM_SEND) + && (synchro2.comm.src_buff != simcall_comm_isend__get__src_buff(r1)) && simcall_comm_wait__get__timeout(r2) <= 0) return FALSE; if ((r1->call == SIMCALL_COMM_IRECV) - && (simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE) - && (simcall_comm_wait__get__comm(r2)->comm.dst_buff != - simcall_comm_irecv__get__dst_buff(r1)) + && (synchro2.comm.type == SIMIX_COMM_RECEIVE) + && (synchro2.comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1)) && simcall_comm_wait__get__timeout(r2) <= 0) return FALSE; } @@ -74,25 +95,25 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r2) : simcall_comm_irecv__get__rdv(r2); - if (rdv != simcall_comm_wait__get__comm(r1)->comm.rdv_cpy + if (rdv != synchro1.comm.rdv_cpy && simcall_comm_wait__get__timeout(r1) <= 0) return FALSE; - if ((r2->issuer != simcall_comm_wait__get__comm(r1)->comm.src_proc) - && (r2->issuer != simcall_comm_wait__get__comm(r1)->comm.dst_proc) + if ((r2->issuer != synchro1.comm.src_proc) + && (r2->issuer != synchro1.comm.dst_proc) && simcall_comm_wait__get__timeout(r1) <= 0) return FALSE; if ((r2->call == SIMCALL_COMM_ISEND) - && (simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_SEND) - && (simcall_comm_wait__get__comm(r1)->comm.src_buff != + && (synchro1.comm.type == SIMIX_COMM_SEND) + && (synchro1.comm.src_buff != simcall_comm_isend__get__src_buff(r2)) && simcall_comm_wait__get__timeout(r1) <= 0) return FALSE; if ((r2->call == SIMCALL_COMM_IRECV) - && (simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE) - && (simcall_comm_wait__get__comm(r1)->comm.dst_buff != + && (synchro1.comm.type == SIMIX_COMM_RECEIVE) + && (synchro1.comm.dst_buff != simcall_comm_irecv__get__dst_buff(r2)) && simcall_comm_wait__get__timeout(r1) <= 0) return FALSE; @@ -122,89 +143,71 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) if (r1->call == SIMCALL_COMM_WAIT && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST) - && (simcall_comm_wait__get__comm(r1)->comm.src_proc == NULL - || simcall_comm_wait__get__comm(r1)->comm.dst_proc == NULL)) + && (synchro1.comm.src_proc == NULL || synchro1.comm.dst_proc == NULL)) return FALSE; if (r2->call == SIMCALL_COMM_WAIT && (r1->call == SIMCALL_COMM_WAIT || r1->call == SIMCALL_COMM_TEST) - && (simcall_comm_wait__get__comm(r2)->comm.src_proc == NULL - || simcall_comm_wait__get__comm(r2)->comm.dst_proc == NULL)) - return FALSE; + && (synchro2.comm.src_proc == NULL || synchro2.comm.dst_proc == NULL)) + return FALSE; if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT - && simcall_comm_wait__get__comm(r1)->comm.src_buff == - simcall_comm_wait__get__comm(r2)->comm.src_buff - && simcall_comm_wait__get__comm(r1)->comm.dst_buff == - simcall_comm_wait__get__comm(r2)->comm.dst_buff) + && synchro1.comm.src_buff == synchro2.comm.src_buff + && synchro2.comm.dst_buff == synchro2.comm.dst_buff) return FALSE; if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT - && simcall_comm_wait__get__comm(r1)->comm.src_buff != NULL - && simcall_comm_wait__get__comm(r1)->comm.dst_buff != NULL - && simcall_comm_wait__get__comm(r2)->comm.src_buff != NULL - && simcall_comm_wait__get__comm(r2)->comm.dst_buff != NULL - && simcall_comm_wait__get__comm(r1)->comm.dst_buff != - simcall_comm_wait__get__comm(r2)->comm.src_buff - && simcall_comm_wait__get__comm(r1)->comm.dst_buff != - simcall_comm_wait__get__comm(r2)->comm.dst_buff - && simcall_comm_wait__get__comm(r2)->comm.dst_buff != - simcall_comm_wait__get__comm(r1)->comm.src_buff) + && synchro1.comm.src_buff != NULL + && synchro1.comm.dst_buff != NULL + && synchro2.comm.src_buff != NULL + && synchro2.comm.dst_buff != NULL + && synchro1.comm.dst_buff != synchro2.comm.src_buff + && synchro1.comm.dst_buff != synchro2.comm.dst_buff + && synchro2.comm.dst_buff != synchro1.comm.src_buff) return FALSE; if (r1->call == SIMCALL_COMM_TEST && (simcall_comm_test__get__comm(r1) == NULL - || simcall_comm_test__get__comm(r1)->comm.src_buff == NULL - || simcall_comm_test__get__comm(r1)->comm.dst_buff == NULL)) + || synchro1.comm.src_buff == NULL + || synchro1.comm.dst_buff == NULL)) return FALSE; if (r2->call == SIMCALL_COMM_TEST && (simcall_comm_test__get__comm(r2) == NULL - || simcall_comm_test__get__comm(r2)->comm.src_buff == NULL - || simcall_comm_test__get__comm(r2)->comm.dst_buff == NULL)) + || synchro2.comm.src_buff == NULL + || synchro2.comm.dst_buff == NULL)) return FALSE; if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT - && simcall_comm_test__get__comm(r1)->comm.src_buff == - simcall_comm_wait__get__comm(r2)->comm.src_buff - && simcall_comm_test__get__comm(r1)->comm.dst_buff == - simcall_comm_wait__get__comm(r2)->comm.dst_buff) + && synchro1.comm.src_buff == synchro2.comm.src_buff + && synchro1.comm.dst_buff == synchro2.comm.dst_buff) return FALSE; if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST - && simcall_comm_wait__get__comm(r1)->comm.src_buff == - simcall_comm_test__get__comm(r2)->comm.src_buff - && simcall_comm_wait__get__comm(r1)->comm.dst_buff == - simcall_comm_test__get__comm(r2)->comm.dst_buff) + && synchro1.comm.src_buff == synchro2.comm.src_buff + && synchro1.comm.dst_buff == synchro2.comm.dst_buff) return FALSE; if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST - && simcall_comm_wait__get__comm(r1)->comm.src_buff != NULL - && simcall_comm_wait__get__comm(r1)->comm.dst_buff != NULL - && simcall_comm_test__get__comm(r2)->comm.src_buff != NULL - && simcall_comm_test__get__comm(r2)->comm.dst_buff != NULL - && simcall_comm_wait__get__comm(r1)->comm.dst_buff != - simcall_comm_test__get__comm(r2)->comm.src_buff - && simcall_comm_wait__get__comm(r1)->comm.dst_buff != - simcall_comm_test__get__comm(r2)->comm.dst_buff - && simcall_comm_test__get__comm(r2)->comm.dst_buff != - simcall_comm_wait__get__comm(r1)->comm.src_buff) + && synchro1.comm.src_buff != NULL + && synchro1.comm.dst_buff != NULL + && synchro2.comm.src_buff != NULL + && synchro2.comm.dst_buff != NULL + && synchro1.comm.dst_buff != synchro2.comm.src_buff + && synchro1.comm.dst_buff != synchro2.comm.dst_buff + && synchro2.comm.dst_buff != synchro1.comm.src_buff) return FALSE; if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT - && simcall_comm_test__get__comm(r1)->comm.src_buff != NULL - && simcall_comm_test__get__comm(r1)->comm.dst_buff != NULL - && simcall_comm_wait__get__comm(r2)->comm.src_buff != NULL - && simcall_comm_wait__get__comm(r2)->comm.dst_buff != NULL - && simcall_comm_test__get__comm(r1)->comm.dst_buff != - simcall_comm_wait__get__comm(r2)->comm.src_buff - && simcall_comm_test__get__comm(r1)->comm.dst_buff != - simcall_comm_wait__get__comm(r2)->comm.dst_buff - && simcall_comm_wait__get__comm(r2)->comm.dst_buff != - simcall_comm_test__get__comm(r1)->comm.src_buff) + && synchro1.comm.src_buff != NULL + && synchro1.comm.dst_buff != NULL + && synchro2.comm.src_buff != NULL + && synchro2.comm.dst_buff != NULL + && synchro1.comm.dst_buff != synchro2.comm.src_buff + && synchro1.comm.dst_buff != synchro2.comm.dst_buff + && synchro2.comm.dst_buff != synchro1.comm.src_buff) return FALSE; - return TRUE; } @@ -229,117 +232,179 @@ static char *buff_size_to_string(size_t buff_size) char *MC_request_to_string(smx_simcall_t req, int value) { - char *type = NULL, *args = NULL, *str = NULL, *p = NULL, *bs = NULL; - smx_synchro_t act = NULL; - size_t size = 0; + const char* type = NULL; + char *args = NULL; + + 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) + + case SIMCALL_COMM_ISEND: { + type = "iSend"; + char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req)); + char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req)); + 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); + xbt_free(bs); + xbt_free(p); break; - case SIMCALL_COMM_IRECV: - size = - simcall_comm_irecv__get__dst_buff_size(req) ? - *simcall_comm_irecv__get__dst_buff_size(req) : 0; - 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) + } + + case SIMCALL_COMM_IRECV: { + size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req); + + // size_t size = size_pointer ? *size_pointer : 0; + size_t size = 0; + if (remote_size) + MC_process_read_simple(&mc_model_checker->process, &size, + remote_size, sizeof(size)); + + type = "iRecv"; + char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req)); + char* bs = buff_size_to_string(size); + 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); + xbt_free(bs); + xbt_free(p); break; - case SIMCALL_COMM_WAIT: - act = simcall_comm_wait__get__comm(req); + } + + case SIMCALL_COMM_WAIT: { + smx_synchro_t remote_act = simcall_comm_wait__get__comm(req); + char* p; if (value == -1) { - type = xbt_strdup("WaitTimeout"); - p = pointer_to_string(act); + type = "WaitTimeout"; + p = pointer_to_string(remote_act); args = bprintf("comm=%s", p); } else { - type = xbt_strdup("Wait"); - p = pointer_to_string(act); + type = "Wait"; + p = pointer_to_string(remote_act); + + s_smx_synchro_t synchro; + MC_process_read_simple(&mc_model_checker->process, &synchro, + remote_act, sizeof(synchro)); + + smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc); + smx_process_t dst_proc = MC_smx_resolve_process(synchro.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) : ""); } + xbt_free(p); break; - case SIMCALL_COMM_TEST: - act = simcall_comm_test__get__comm(req); - if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) { - type = xbt_strdup("Test FALSE"); - p = pointer_to_string(act); + } + + case SIMCALL_COMM_TEST: { + smx_synchro_t remote_act = simcall_comm_test__get__comm(req); + s_smx_synchro_t synchro; + MC_process_read_simple(&mc_model_checker->process, &synchro, + remote_act, sizeof(synchro)); + + char* p; + if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) { + type = "Test FALSE"; + p = pointer_to_string(remote_act); args = bprintf("comm=%s", p); } else { - type = xbt_strdup("Test TRUE"); - p = pointer_to_string(act); + type = "Test TRUE"; + p = pointer_to_string(remote_act); + + smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc); + smx_process_t dst_proc = MC_smx_resolve_process(synchro.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)); } + xbt_free(p); break; + } - case SIMCALL_COMM_WAITANY: - type = xbt_strdup("WaitAny"); - if (!xbt_dynar_is_empty(simcall_comm_waitany__get__comms(req))) { - p = pointer_to_string(xbt_dynar_get_as - (simcall_comm_waitany__get__comms(req), value, - smx_synchro_t)); - args = - bprintf("comm=%s (%d of %lu)", p, value + 1, - xbt_dynar_length(simcall_comm_waitany__get__comms(req))); + case SIMCALL_COMM_WAITANY: { + type = "WaitAny"; + s_xbt_dynar_t comms; + MC_process_read_simple(&mc_model_checker->process, + &comms, simcall_comm_waitany__get__comms(req), sizeof(comms)); + if (!xbt_dynar_is_empty(&comms)) { + smx_synchro_t remote_sync; + MC_process_read_dynar_element(&mc_model_checker->process, + &remote_sync, simcall_comm_waitany__get__comms(req), value); + char* p = pointer_to_string(remote_sync); + args = bprintf("comm=%s (%d of %lu)", + p, value + 1, xbt_dynar_length(&comms)); + xbt_free(p); } else { args = bprintf("comm at idx %d", value); } break; + } case SIMCALL_COMM_TESTANY: if (value == -1) { - type = xbt_strdup("TestAny FALSE"); + type = "TestAny FALSE"; args = xbt_strdup("-"); } else { - type = xbt_strdup("TestAny"); + type = "TestAny"; args = bprintf("(%d of %lu)", value + 1, - xbt_dynar_length(simcall_comm_testany__get__comms(req))); + MC_process_read_dynar_length(&mc_model_checker->process, + simcall_comm_testany__get__comms(req))); } break; + case SIMCALL_MUTEX_LOCK: { + type = "Mutex LOCK"; + + s_smx_mutex_t mutex; + MC_process_read_simple(&mc_model_checker->process, &mutex, + simcall_mutex_lock__get__mutex(req), sizeof(mutex)); + s_xbt_swag_t mutex_sleeping; + MC_process_read_simple(&mc_model_checker->process, &mutex_sleeping, + mutex.sleeping, sizeof(mutex_sleeping)); + + args = bprintf("locked = %d, owner = %d, sleeping = %d", + mutex.locked, + mutex.owner != NULL ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1, + mutex_sleeping.count); + break; + } + case SIMCALL_MC_SNAPSHOT: - type = xbt_strdup("MC_SNAPSHOT"); + type = "MC_SNAPSHOT"; args = NULL; break; case SIMCALL_MC_COMPARE_SNAPSHOTS: - type = xbt_strdup("MC_COMPARE_SNAPSHOTS"); + type = "MC_COMPARE_SNAPSHOTS"; args = NULL; break; case SIMCALL_MC_RANDOM: - type = xbt_strdup("MC_RANDOM"); + type = "MC_RANDOM"; args = bprintf("%d", value); break; @@ -347,32 +412,55 @@ char *MC_request_to_string(smx_simcall_t req, int value) THROW_UNIMPLEMENTED; } + char* str; if (args != NULL) { 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 { 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); } - xbt_free(args); - xbt_free(type); - xbt_free(p); - xbt_free(bs); return str; } unsigned int MC_request_testany_fail(smx_simcall_t req) { - unsigned int cursor; - smx_synchro_t action; - - xbt_dynar_foreach(simcall_comm_testany__get__comms(req), cursor, action) { - if (action->comm.src_proc && action->comm.dst_proc) + // Remote xbt_dynar_foreach on simcall_comm_testany__get__comms(req). + + // Read the dynar: + s_xbt_dynar_t comms; + MC_process_read_simple(&mc_model_checker->process, + &comms, simcall_comm_testany__get__comms(req), sizeof(comms)); + + // Read ther dynar buffer: + size_t buffer_size = comms.elmsize * comms.used; + char buffer[buffer_size]; + MC_process_read_simple(&mc_model_checker->process, + buffer, comms.data, buffer_size); + + // Iterate over the elements: + assert(comms.elmsize == sizeof(smx_synchro_t)); + unsigned cursor; + for (cursor=0; cursor != comms.used; ++cursor) { + + // Get the element: + smx_synchro_t remote_action; + memcpy(buffer + comms.elmsize * cursor, &remote_action, sizeof(remote_action)); + + // Dereference the pointer: + s_smx_synchro_t action; + MC_process_read_simple(&mc_model_checker->process, + &action, remote_action, sizeof(action)); + + // Finally so something useful about it: + if (action.comm.src_proc && action.comm.dst_proc) return FALSE; } @@ -381,33 +469,38 @@ unsigned int MC_request_testany_fail(smx_simcall_t req) int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) { - smx_synchro_t act; - + smx_synchro_t remote_act = NULL; switch (req->call) { case SIMCALL_COMM_WAIT: /* FIXME: check also that src and dst processes are not suspended */ - act = simcall_comm_wait__get__comm(req); - return (act->comm.src_proc && act->comm.dst_proc); + remote_act = simcall_comm_wait__get__comm(req); break; - case SIMCALL_COMM_WAITANY: - act = - xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), idx, - smx_synchro_t); - return (act->comm.src_proc && act->comm.dst_proc); + case SIMCALL_COMM_WAITANY: { + smx_synchro_t act; + MC_process_read_dynar_element( + &mc_model_checker->process, &act, simcall_comm_waitany__get__comms(req), + idx); + } break; - case SIMCALL_COMM_TESTANY: - act = - xbt_dynar_get_as(simcall_comm_testany__get__comms(req), idx, - smx_synchro_t); - return (act->comm.src_proc && act->comm.dst_proc); + case SIMCALL_COMM_TESTANY: { + s_smx_synchro_t act; + MC_process_read_dynar_element( + &mc_model_checker->process, &act, simcall_comm_testany__get__comms(req), + idx); + } break; default: return TRUE; } + + s_smx_synchro_t synchro; + MC_process_read_simple(&mc_model_checker->process, + &synchro, remote_act, sizeof(synchro)); + return synchro.comm.src_proc && synchro.comm.dst_proc; } int MC_process_is_enabled(smx_process_t process) @@ -417,140 +510,158 @@ int MC_process_is_enabled(smx_process_t process) char *MC_request_get_dot_output(smx_simcall_t req, int value) { + char *label = NULL; - 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); + case SIMCALL_COMM_WAIT: { 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) + smx_synchro_t remote_act = simcall_comm_wait__get__comm(req); + s_smx_synchro_t synchro; + MC_process_read_simple(&mc_model_checker->process, &synchro, + remote_act, sizeof(synchro)); + + smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc); + smx_process_t dst_proc = MC_smx_resolve_process(synchro.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) + case SIMCALL_COMM_TEST: { + smx_synchro_t remote_act = simcall_comm_test__get__comm(req); + s_smx_synchro_t synchro; + MC_process_read_simple(&mc_model_checker->process, &synchro, + remote_act, sizeof(synchro)); + if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) { + 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) + case SIMCALL_COMM_WAITANY: { + unsigned long comms_size = MC_process_read_dynar_length( + &mc_model_checker->process, simcall_comm_waitany__get__comms(req)); + 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, - xbt_dynar_length(simcall_comm_waitany__get__comms(req))); + bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid, + MC_smx_process_get_host_name(issuer), value + 1, + comms_size); else label = - bprintf("[(%lu)] WaitAny [%d of %lu]", req->issuer->pid, value + 1, - xbt_dynar_length(simcall_comm_waitany__get__comms(req))); + bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1, + comms_size); 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: THROW_UNIMPLEMENTED; } - str = + char* 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;