/* 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;
}
}
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;
/* 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();
/* 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;
}
}
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);
}
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);
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);
*/
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;
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
}
}
- SIMIX_request_pre(req);
+ SIMIX_request_pre(req, value);
MC_wait_for_requests();
/* Update statistics */
void MC_show_stack(xbt_fifo_t stack)
{
+ unsigned int value;
mc_state_t state;
xbt_fifo_item_t item;
smx_req_t req;
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);
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;
+}
#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
*/
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)
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;
}
}
/********************************* 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);
/******************************** 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;
/* 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: */
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 {
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);
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
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));
}
}
-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;
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;
}
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 */
SIMIX_request_name(issuer->request.call), issuer->request.call);
SIMIX_process_yield();
} else {
- SIMIX_request_pre(&issuer->request);
+ SIMIX_request_pre(&issuer->request, 0);
}
}
|| 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)
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:
}
}
+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:
break;
case REQ_COMM_WAITANY:
- SIMIX_pre_comm_waitany(req);
+ SIMIX_pre_comm_waitany(req, value);
break;
case REQ_COMM_WAIT:
break;
case REQ_COMM_TESTANY:
- SIMIX_pre_comm_testany(req);
+ SIMIX_pre_comm_testany(req, value);
break;
case REQ_COMM_GET_REMAINS: