From 7a25b8e6a7aae6d40849189e58495aee0d8f726f Mon Sep 17 00:00:00 2001 From: cristianrosa Date: Wed, 5 Jan 2011 09:02:47 +0000 Subject: [PATCH] Add suport for TestAny and WaitAny requests to the model-checker. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@9358 48e7efb5-ca39-0410-a469-dd3cf9ba447f --- src/mc/mc_dpor.c | 20 +++++------ src/mc/mc_global.c | 12 +++---- src/mc/mc_request.c | 27 ++++++++++++++ src/mc/mc_state.c | 70 +++++++++++++++++++++++-------------- src/mc/private.h | 20 +++++------ src/simix/network_private.h | 4 +-- src/simix/smurf_private.h | 3 +- src/simix/smx_global.c | 2 +- src/simix/smx_network.c | 30 ++++++++++++++-- src/simix/smx_smurf.c | 38 +++++++++++++++----- 10 files changed, 158 insertions(+), 68 deletions(-) diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 1970b9cdf6..bc37c91bca 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -33,7 +33,7 @@ void MC_dpor_init() /* Get an enabled process and insert it in the interleave set of the initial state */ xbt_swag_foreach(process, simix_global->process_list){ if(SIMIX_process_is_enabled(process)){ - MC_state_add_to_interleave(initial_state, process); + MC_state_interleave_process(initial_state, process); break; } } @@ -52,7 +52,7 @@ void MC_dpor_init() void MC_dpor(void) { char *req_str; - char value; + unsigned int value; smx_req_t req = NULL; mc_state_t state = NULL, prev_state = NULL, next_state = NULL; smx_process_t process = NULL; @@ -80,15 +80,15 @@ void MC_dpor(void) /* Debug information */ if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){ req_str = MC_request_to_string(req); - DEBUG1("Execute: %s", req_str); + DEBUG2("Execute: %s (%u)", req_str, value); xbt_free(req_str); } - MC_state_set_executed_request(state, req); + MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; /* Answer the request */ - SIMIX_request_pre(req); /* After this call req is no longer usefull */ + SIMIX_request_pre(req, value); /* After this call req is no longer usefull */ /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@ -102,7 +102,7 @@ void MC_dpor(void) /* Get an enabled process and insert it in the interleave set of the next state */ xbt_swag_foreach(process, simix_global->process_list){ if(SIMIX_process_is_enabled(process)){ - MC_state_add_to_interleave(next_state, process); + MC_state_interleave_process(next_state, process); break; } } @@ -136,12 +136,12 @@ void MC_dpor(void) executed before it. If it does then add it to the interleave set of the state that executed that previous request. */ while ((state = xbt_fifo_shift(mc_stack)) != NULL) { - req = MC_state_get_executed_request(state); + req = MC_state_get_executed_request(state, &value); xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) { - if(MC_request_depend(req, MC_state_get_executed_request(prev_state))){ + if(MC_request_depend(req, MC_state_get_executed_request(prev_state, &value))){ if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){ DEBUG0("Dependent Transitions:"); - req_str = MC_request_to_string(MC_state_get_executed_request(prev_state)); + req_str = MC_request_to_string(MC_state_get_executed_request(prev_state, &value)); DEBUG2("%s (state=%p)", req_str, prev_state); xbt_free(req_str); req_str = MC_request_to_string(req); @@ -150,7 +150,7 @@ void MC_dpor(void) } if(!MC_state_process_is_done(prev_state, req->issuer)) - MC_state_add_to_interleave(prev_state, req->issuer); + MC_state_interleave_process(prev_state, req->issuer); else DEBUG1("Process %p is in done set", req->issuer); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index de02e74da1..50b1c7415f 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -79,9 +79,7 @@ void MC_wait_for_requests(void) SIMIX_context_runall(simix_global->process_to_run); while((req = SIMIX_request_pop())){ if(!SIMIX_request_is_visible(req)) - SIMIX_request_pre(req); - else if(req->call == REQ_COMM_WAITANY) - THROW_UNIMPLEMENTED; + SIMIX_request_pre(req, 0); else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ req_str = MC_request_to_string(req); DEBUG1("Got: %s", req_str); @@ -115,6 +113,7 @@ int MC_deadlock_check() */ void MC_replay(xbt_fifo_t stack) { + unsigned int value; char *req_str; smx_req_t req = NULL, saved_req = NULL; xbt_fifo_item_t item; @@ -134,7 +133,7 @@ void MC_replay(xbt_fifo_t stack) item = xbt_fifo_get_prev_item(item)) { state = (mc_state_t) xbt_fifo_get_item_content(item); - saved_req = MC_state_get_executed_request(state); + saved_req = MC_state_get_executed_request(state, &value); if(saved_req){ /* because we got a copy of the executed request, we have to fetch the @@ -149,7 +148,7 @@ void MC_replay(xbt_fifo_t stack) } } - SIMIX_request_pre(req); + SIMIX_request_pre(req, value); MC_wait_for_requests(); /* Update statistics */ @@ -178,6 +177,7 @@ void MC_dump_stack(xbt_fifo_t stack) void MC_show_stack(xbt_fifo_t stack) { + unsigned int value; mc_state_t state; xbt_fifo_item_t item; smx_req_t req; @@ -186,7 +186,7 @@ void MC_show_stack(xbt_fifo_t stack) for (item = xbt_fifo_get_last_item(stack); (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item))) : (NULL)); item = xbt_fifo_get_prev_item(item)) { - req = MC_state_get_executed_request(state); + req = MC_state_get_executed_request(state, &value); if(req){ req_str = MC_request_to_string(req); INFO1("%s", req_str); diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 6ee8336ba9..3aaa2665c4 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -67,11 +67,38 @@ char *MC_request_to_string(smx_req_t req) act->comm.src_proc ? act->comm.src_proc->name : "", act->comm.dst_proc ? act->comm.dst_proc->name : ""); break; + + case REQ_COMM_WAITANY: + type = bprintf("WaitAny"); + args = bprintf("-"); + /* FIXME: improve output */ + break; + + case REQ_COMM_TESTANY: + type = bprintf("TestAny"); + args = bprintf("-"); + /* FIXME: improve output */ + break; + default: THROW_UNIMPLEMENTED; } + str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args); xbt_free(type); xbt_free(args); return str; } + +unsigned int MC_request_testany_fail(smx_req_t req) +{ + unsigned int cursor; + smx_action_t action; + + xbt_dynar_foreach(req->comm_testany.comms, cursor, action){ + if(action->comm.src_proc && action->comm.dst_proc) + return FALSE; + } + + return TRUE; +} diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index 74f5a54b7d..e289fd1688 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -2,8 +2,6 @@ #include "xbt/fifo.h" #include "private.h" -static void MC_state_add_transition(mc_state_t state, mc_transition_t trans); - /** * \brief Creates a state data structure used by the exploration algorithm */ @@ -29,10 +27,10 @@ void MC_state_delete(mc_state_t state) xbt_free(state); } -void MC_state_add_to_interleave(mc_state_t state, smx_process_t process) +void MC_state_interleave_process(mc_state_t state, smx_process_t process) { state->proc_status[process->pid].state = MC_INTERLEAVE; - state->proc_status[process->pid].num_to_interleave = 1; + state->proc_status[process->pid].interleave_count = 0; } unsigned int MC_state_interleave_size(mc_state_t state) @@ -51,43 +49,63 @@ int MC_state_process_is_done(mc_state_t state, smx_process_t process){ return state->proc_status[process->pid].state == MC_DONE ? TRUE : FALSE; } -void MC_state_set_executed_request(mc_state_t state, smx_req_t req) +void MC_state_set_executed_request(mc_state_t state, smx_req_t req, unsigned int value) { + state->executed_value = value; state->executed = *req; } -smx_req_t MC_state_get_executed_request(mc_state_t state) +smx_req_t MC_state_get_executed_request(mc_state_t state, unsigned int *value) { + *value = state->executed_value; return &state->executed; } -smx_req_t MC_state_get_request(mc_state_t state, char *value) +smx_req_t MC_state_get_request(mc_state_t state, unsigned int *value) { - unsigned int i; smx_process_t process = NULL; mc_procstate_t procstate = NULL; - for(i=0; i < state->max_pid; i++){ - procstate = &state->proc_status[i]; - - if(procstate->state == MC_INTERLEAVE){ - if(procstate->num_to_interleave-- > 1) - *value = procstate->requests_indexes[procstate->num_to_interleave]; + xbt_swag_foreach(process, simix_global->process_list){ + procstate = &state->proc_status[process->pid]; - /* If the are no more requests to interleave for process i then it is done */ - if(procstate->num_to_interleave == 0) - procstate->state = MC_DONE; - - /* FIXME: SIMIX should implement a process table indexed by pid */ - /* So we should use that instead of traversing the swag */ - xbt_swag_foreach(process, simix_global->process_list){ - if(process->pid == i) - break; + if(procstate->state == MC_INTERLEAVE){ + if(SIMIX_process_is_enabled(process)){ + switch(process->request.call){ + case REQ_COMM_WAITANY: + while(procstate->interleave_count < xbt_dynar_length(process->request.comm_waitany.comms)){ + if(SIMIX_request_is_enabled_by_idx(&process->request, procstate->interleave_count++)){ + *value = procstate->interleave_count - 1; + return &process->request; + } + } + procstate->state = MC_DONE; + break; + + case REQ_COMM_TESTANY: + if(MC_request_testany_fail(&process->request)){ + procstate->state = MC_DONE; + *value = (unsigned int)-1; + return &process->request; + } + + while(procstate->interleave_count < xbt_dynar_length(process->request.comm_waitany.comms)){ + if(SIMIX_request_is_enabled_by_idx(&process->request, procstate->interleave_count++)){ + *value = procstate->interleave_count - 1; + return &process->request; + } + } + procstate->state = MC_DONE; + break; + + default: + procstate->state = MC_DONE; + *value = 0; + return &process->request; + break; + } } - - if(SIMIX_process_is_enabled(process)) - return &process->request; } } diff --git a/src/mc/private.h b/src/mc/private.h index a1720fdef2..7c13977da7 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -52,6 +52,8 @@ void MC_dump_stack(xbt_fifo_t stack); /********************************* Requests ***********************************/ int MC_request_depend(smx_req_t req1, smx_req_t req2); char* MC_request_to_string(smx_req_t req); +unsigned int MC_request_testany_fail(smx_req_t req); +int MC_waitany_is_enabled_by_comm(smx_req_t req, unsigned int comm); /********************************** DPOR **************************************/ void MC_dpor_init(void); @@ -61,7 +63,7 @@ void MC_dpor_exit(void); /******************************** States **************************************/ /* Possible exploration status of a process in a state */ typedef enum { - MC_NOT_INTERLEAVE = 0, /* Do not interleave (do not execute) */ + MC_NOT_INTERLEAVE=0, /* Do not interleave (do not execute) */ MC_INTERLEAVE, /* Interleave the process (one or more request) */ MC_DONE /* Already interleaved */ } e_mc_process_state_t; @@ -69,11 +71,8 @@ typedef enum { /* On every state, each process has an entry of the following type */ typedef struct mc_procstate{ e_mc_process_state_t state; /* Exploration control information */ - unsigned int num_to_interleave; /* Number of request to interleave */ - /* If a process has a request with multiple possible responses like a */ - /* "WaitAny", then the following vector with the indexes to interleave */ - /* is additionally used. */ - unsigned int *requests_indexes; /* Indexes of the requests to interleave */ + unsigned int interleave_count; /* Number of times that the process was + interleaved */ } s_mc_procstate_t, *mc_procstate_t; /* An exploration state is composed of: */ @@ -81,18 +80,19 @@ typedef struct mc_state { unsigned long max_pid; /* Maximum pid at state's creation time */ mc_procstate_t proc_status; /* State's exploration status by process */ s_smx_req_t executed; /* The executed request of the state */ + unsigned int executed_value; /* The value associated to the request */ } s_mc_state_t, *mc_state_t; extern xbt_fifo_t mc_stack; mc_state_t MC_state_new(void); void MC_state_delete(mc_state_t state); -void MC_state_add_to_interleave(mc_state_t state, smx_process_t process); +void MC_state_interleave_process(mc_state_t state, smx_process_t process); unsigned int MC_state_interleave_size(mc_state_t state); int MC_state_process_is_done(mc_state_t state, smx_process_t process); -void MC_state_set_executed_request(mc_state_t state, smx_req_t req); -smx_req_t MC_state_get_executed_request(mc_state_t state); -smx_req_t MC_state_get_request(mc_state_t state, char *value); +void MC_state_set_executed_request(mc_state_t state, smx_req_t req, unsigned int value); +smx_req_t MC_state_get_executed_request(mc_state_t state, unsigned int *value); +smx_req_t MC_state_get_request(mc_state_t state, unsigned int *value); /****************************** Statistics ************************************/ typedef struct mc_stats { diff --git a/src/simix/network_private.h b/src/simix/network_private.h index a66b5d946d..292e6562d0 100644 --- a/src/simix/network_private.h +++ b/src/simix/network_private.h @@ -39,10 +39,10 @@ smx_action_t SIMIX_comm_irecv(smx_process_t dst_proc, smx_rdv_t rdv, void SIMIX_comm_destroy(smx_action_t action); void SIMIX_comm_destroy_internal_actions(smx_action_t action); void SIMIX_pre_comm_wait(smx_req_t req); -void SIMIX_pre_comm_waitany(smx_req_t req); +void SIMIX_pre_comm_waitany(smx_req_t req, unsigned int idx); void SIMIX_post_comm(smx_action_t action); void SIMIX_pre_comm_test(smx_req_t req); -void SIMIX_pre_comm_testany(smx_req_t req); +void SIMIX_pre_comm_testany(smx_req_t req, unsigned int idx); void SIMIX_comm_cancel(smx_action_t action); double SIMIX_comm_get_remains(smx_action_t action); e_smx_state_t SIMIX_comm_get_state(smx_action_t action); diff --git a/src/simix/smurf_private.h b/src/simix/smurf_private.h index f150f85d62..f9659fc9d4 100644 --- a/src/simix/smurf_private.h +++ b/src/simix/smurf_private.h @@ -474,10 +474,11 @@ void SIMIX_request_destroy(void); void SIMIX_request_push(void); smx_req_t SIMIX_request_pop(void); void SIMIX_request_answer(smx_req_t); -void SIMIX_request_pre(smx_req_t); +void SIMIX_request_pre(smx_req_t, unsigned int); void SIMIX_request_post(smx_action_t); int SIMIX_request_is_visible(smx_req_t req); int SIMIX_request_is_enabled(smx_req_t req); +int SIMIX_request_is_enabled_by_idx(smx_req_t req, unsigned int idx); XBT_INLINE smx_req_t SIMIX_req_mine(void); #endif diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c index 9fcfa67862..d0e2c53314 100644 --- a/src/simix/smx_global.c +++ b/src/simix/smx_global.c @@ -176,7 +176,7 @@ void SIMIX_run(void) SIMIX_context_runall(simix_global->process_to_run); while ((req = SIMIX_request_pop())) { DEBUG1("Handling request %p", req); - SIMIX_request_pre(req); + SIMIX_request_pre(req, 0); } } while (xbt_dynar_length(simix_global->process_to_run)); diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c index c5a62db9b3..41192b6e23 100644 --- a/src/simix/smx_network.c +++ b/src/simix/smx_network.c @@ -359,11 +359,25 @@ void SIMIX_pre_comm_test(smx_req_t req) } } -void SIMIX_pre_comm_testany(smx_req_t req) +void SIMIX_pre_comm_testany(smx_req_t req, unsigned int idx) { unsigned int cursor; smx_action_t action; + xbt_dynar_t actions = req->comm_testany.comms; req->comm_testany.result = -1; + + if (MC_IS_ENABLED){ + if((int)idx == -1){ + SIMIX_request_answer(req); + }else{ + action = xbt_dynar_get_as(actions, idx, smx_action_t); + xbt_fifo_push(action->request_list, req); + action->state = SIMIX_DONE; + SIMIX_comm_finish(action); + } + return; + } + xbt_dynar_foreach(req->comm_testany.comms,cursor,action) { if (action->state != SIMIX_WAITING && action->state != SIMIX_RUNNING) { req->comm_testany.result = cursor; @@ -375,15 +389,26 @@ void SIMIX_pre_comm_testany(smx_req_t req) SIMIX_request_answer(req); } -void SIMIX_pre_comm_waitany(smx_req_t req) +void SIMIX_pre_comm_waitany(smx_req_t req, unsigned int idx) { smx_action_t action; unsigned int cursor = 0; xbt_dynar_t actions = req->comm_waitany.comms; + + if (MC_IS_ENABLED){ + action = xbt_dynar_get_as(actions, idx, smx_action_t); + xbt_fifo_push(action->request_list, req); + req->comm_waitany.result = idx; + action->state = SIMIX_DONE; + SIMIX_comm_finish(action); + return; + } + xbt_dynar_foreach(actions, cursor, action){ /* Associate this request to the action */ xbt_fifo_push(action->request_list, req); if (action->state != SIMIX_WAITING && action->state != SIMIX_RUNNING){ + req->comm_waitany.result = cursor; SIMIX_comm_finish(action); break; } @@ -456,7 +481,6 @@ void SIMIX_comm_finish(smx_action_t action) return it as the result of the call */ if (req->call == REQ_COMM_WAITANY) { SIMIX_waitany_req_remove_from_actions(req); - req->comm_waitany.result = xbt_dynar_search(req->comm_waitany.comms, &action); } /* If the action is still in a rendez-vous point then remove from it */ diff --git a/src/simix/smx_smurf.c b/src/simix/smx_smurf.c index 8c4b3705a8..3f2045d8af 100644 --- a/src/simix/smx_smurf.c +++ b/src/simix/smx_smurf.c @@ -47,7 +47,7 @@ void SIMIX_request_push() SIMIX_request_name(issuer->request.call), issuer->request.call); SIMIX_process_yield(); } else { - SIMIX_request_pre(&issuer->request); + SIMIX_request_pre(&issuer->request, 0); } } @@ -77,7 +77,8 @@ int SIMIX_request_is_visible(smx_req_t req) || req->call == REQ_COMM_IRECV || req->call == REQ_COMM_WAIT || req->call == REQ_COMM_WAITANY - || req->call == REQ_COMM_TEST; + || req->call == REQ_COMM_TEST + || req->call == REQ_COMM_TESTANY; } int SIMIX_request_is_enabled(smx_req_t req) @@ -89,10 +90,8 @@ int SIMIX_request_is_enabled(smx_req_t req) case REQ_COMM_WAIT: /* FIXME: check also that src and dst processes are not suspended */ - if (req->comm_wait.comm->comm.src_proc - && req->comm_wait.comm->comm.dst_proc) - return TRUE; - return FALSE; + act = req->comm_wait.comm; + return (act->comm.src_proc && act->comm.dst_proc); break; case REQ_COMM_WAITANY: @@ -109,8 +108,29 @@ int SIMIX_request_is_enabled(smx_req_t req) } } +int SIMIX_request_is_enabled_by_idx(smx_req_t req, unsigned int idx) +{ + smx_action_t act; + + switch (req->call) { + + case REQ_COMM_WAIT: + /* FIXME: check also that src and dst processes are not suspended */ + act = req->comm_wait.comm; + return (act->comm.src_proc && act->comm.dst_proc); + break; + + case REQ_COMM_WAITANY: + act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t); + return (act->comm.src_proc && act->comm.dst_proc); + break; + + default: + return TRUE; + } +} -void SIMIX_request_pre(smx_req_t req) +void SIMIX_request_pre(smx_req_t req, unsigned int value) { switch (req->call) { case REQ_NO_REQ: @@ -359,7 +379,7 @@ void SIMIX_request_pre(smx_req_t req) break; case REQ_COMM_WAITANY: - SIMIX_pre_comm_waitany(req); + SIMIX_pre_comm_waitany(req, value); break; case REQ_COMM_WAIT: @@ -371,7 +391,7 @@ void SIMIX_request_pre(smx_req_t req) break; case REQ_COMM_TESTANY: - SIMIX_pre_comm_testany(req); + SIMIX_pre_comm_testany(req, value); break; case REQ_COMM_GET_REMAINS: -- 2.20.1