SG_BEGIN_DECL()
/******************************* Transitions **********************************/
-typedef enum {
- mc_isend,
- mc_irecv,
- mc_test,
- mc_wait,
- mc_waitany,
- mc_random
-} mc_trans_type_t;
-
typedef struct s_mc_transition *mc_transition_t;
SG_END_DECL()
XBT_PUBLIC(int) MC_random(int,int);
/******************************* Transitions **********************************/
-XBT_PUBLIC(mc_transition_t) MC_create_transition(mc_trans_type_t, smx_process_t, smx_rdv_t, smx_comm_t);
-XBT_PUBLIC(void) MC_transition_set_comm(mc_transition_t, smx_comm_t);
+XBT_PUBLIC(void) MC_trans_intercept_isend(smx_rdv_t);
+XBT_PUBLIC(void) MC_trans_intercept_irecv(smx_rdv_t);
+XBT_PUBLIC(void) MC_trans_intercept_wait(smx_comm_t);
+XBT_PUBLIC(void) MC_trans_intercept_test(smx_comm_t);
+XBT_PUBLIC(void) MC_trans_intercept_waitany(xbt_dynar_t);
+XBT_PUBLIC(void) MC_trans_intercept_random(int,int);
/********************************* Memory *************************************/
XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */
xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions);
xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){
if(trans->type == mc_wait
- && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
+ && (trans->wait.comm->src_proc == NULL || trans->wait.comm->dst_proc == NULL)){
xbt_setset_set_remove(initial_state->enabled_transitions, trans);
}
}
xbt_setset_add(next_state->enabled_transitions, next_state->transitions);
xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){
if(trans->type == mc_wait
- && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
+ && (trans->wait.comm->src_proc == NULL || trans->wait.comm->dst_proc == NULL)){
xbt_setset_set_remove(next_state->enabled_transitions, trans);
}
}
{
mc_state_t initial_state = NULL;
mc_transition_t trans = NULL;
- xbt_setset_cursor_t cursor = NULL;
/* Create the initial state and push it into the exploration stack */
MC_SET_RAW_MEM;
MC_schedule_enabled_processes();
MC_SET_RAW_MEM;
- xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions);
- xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){
- if(trans->type == mc_wait
- && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
- xbt_setset_set_remove(initial_state->enabled_transitions, trans);
- }
- }
+ MC_trans_compute_enabled(initial_state->enabled_transitions,
+ initial_state->transitions);
/* Fill the interleave set of the initial state with an enabled process */
trans = xbt_setset_set_choose(initial_state->enabled_transitions);
MC_execute_surf_actions(); /* Do surf's related black magic */
MC_schedule_enabled_processes();
- if(trans->type == mc_random && trans->current_value < trans->max ){
- trans->current_value++;
+ if(trans->type == mc_random && trans->random.current_value < trans->random.max){
+ trans->random.current_value++;
}else{
- trans->current_value = trans->min;
+ trans->random.current_value = trans->random.min;
xbt_setset_set_remove(mc_current_state->interleave, trans);
xbt_setset_set_insert(mc_current_state->done, trans);
}
- /* Calculate the enabled transitions set of the next state:
- -add the transition sets of the current state and the next state
- -remove the executed transition from that set
- -remove all the transitions that are disabled (mc_wait only)
- -use the resulting set as the enabled transitions of the next state */
+ /* Calculate the enabled transitions set of the next state */
MC_SET_RAW_MEM;
xbt_setset_add(next_state->transitions, mc_current_state->transitions);
xbt_setset_set_remove(next_state->transitions, trans);
- xbt_setset_add(next_state->enabled_transitions, next_state->transitions);
- xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){
- if(trans->type == mc_wait
- && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
- xbt_setset_set_remove(next_state->enabled_transitions, trans);
- }
- }
+ MC_trans_compute_enabled(next_state->enabled_transitions, next_state->transitions);
/* Choose one transition to interleave from the enabled transition set */
trans = xbt_setset_set_choose(next_state->enabled_transitions);
int MC_random(int min, int max)
{
- MC_random_create(min,max);
+ MC_trans_random_new(min,max);
SIMIX_process_yield();
if(!mc_replay_mode)
- return mc_current_state->executed_transition->current_value;
+ return mc_current_state->executed_transition->random.current_value;
else
- return mc_current_state->executed_transition->current_value - 1;
+ return mc_current_state->executed_transition->random.current_value - 1;
}
/**
#include "private.h"
+/* Creates a new iSend transition */
+mc_transition_t MC_trans_isend_new(smx_rdv_t rdv)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_isend;
+ trans->process = SIMIX_process_self();
+ trans->isend.rdv = rdv;
+ trans->name = bprintf("[%s][%s] iSend (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new iRecv transition */
+mc_transition_t MC_trans_irecv_new(smx_rdv_t rdv)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_irecv;
+ trans->process = SIMIX_process_self();
+ trans->irecv.rdv = rdv;
+ trans->name = bprintf("[%s][%s] iRecv (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new Wait transition */
+mc_transition_t MC_trans_wait_new(smx_comm_t comm)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_wait;
+ trans->process = SIMIX_process_self();
+ trans->wait.comm = comm;
+ trans->name = bprintf("[%s][%s] Wait (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new test transition */
+mc_transition_t MC_trans_test_new(smx_comm_t comm)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_test;
+ trans->process = SIMIX_process_self();
+ trans->test.comm = comm;
+ trans->name = bprintf("[%s][%s] Test (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new WaitAny transition */
+mc_transition_t MC_trans_waitany_new(xbt_dynar_t comms)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_waitany;
+ trans->process = SIMIX_process_self();
+ trans->waitany.comms = comms;
+ trans->name = bprintf("[%s][%s] WaitAny (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new Random transition */
+mc_transition_t MC_trans_random_new(int min, int max)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_random;
+ trans->process = SIMIX_process_self();
+ trans->random.min = min;
+ trans->random.max = max;
+ trans->random.current_value = min;
+ trans->name = bprintf("[%s][%s] Random (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/************************** Interception Functions ****************************/
+/* These functions intercept all the actions relevant to the model-checking
+ * process, the only difference between them is the type of transition they
+ * create. The interception works by yielding the process performer of the
+ * action, and depending on the execution mode it behaves diferently.
+ * There are two running modes, a replay (back-track process) in which no
+ * transition needs to be created, or a new state expansion, which in
+ * consecuence a transition needs to be created and added to the set of
+ * transitions associated to the current state.
+ */
+
/**
- * \brief Create a model-checker transition and add it to the set of avaiable
- * transitions of the current state, if not running in replay mode.
- * \param process The process who wants to perform the transition
- * \param comm The type of then transition (comm_send, comm_recv)
-*/
-mc_transition_t MC_create_transition(mc_trans_type_t type, smx_process_t p, smx_rdv_t rdv, smx_comm_t comm)
+ * \brief Intercept an iSend action
+ * \param rdv The rendez-vous of the iSend
+ */
+void MC_trans_intercept_isend(smx_rdv_t rdv)
{
+ mc_transition_t trans=NULL;
mc_state_t current_state = NULL;
- char *type_str = NULL;
-
if(!mc_replay_mode){
MC_SET_RAW_MEM;
- mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
-
- /* Generate a string for the "type" */
- switch(type){
- case mc_isend:
- type_str = bprintf("iSend");
- break;
- case mc_irecv:
- type_str = bprintf("iRecv");
- break;
- case mc_wait:
- type_str = bprintf("Wait");
- break;
- case mc_waitany:
- type_str = bprintf("WaitAny");
- break;
- default:
- xbt_die("Invalid transition type");
- }
-
- trans->name = bprintf("[%s][%s] %s (%p)", p->smx_host->name, p->name, type_str, trans);
- xbt_free(type_str);
-
- trans->type = type;
- trans->process = p;
- trans->rdv = rdv;
- trans->comm = comm;
- /* Push it onto the enabled transitions set of the current state */
-
- current_state = (mc_state_t)
+ trans = MC_trans_isend_new(rdv);
+ current_state = (mc_state_t)
xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
xbt_setset_set_insert(current_state->created_transitions, trans);
xbt_setset_set_insert(current_state->transitions, trans);
MC_UNSET_RAW_MEM;
- return trans;
}
- return NULL;
+ SIMIX_process_yield();
}
-void MC_random_create(int min, int max)
+/**
+ * \brief Intercept an iRecv action
+ * \param rdv The rendez-vous of the iRecv
+ */
+void MC_trans_intercept_irecv(smx_rdv_t rdv)
{
- smx_process_t p;
+ mc_transition_t trans=NULL;
+ mc_state_t current_state = NULL;
+ if(!mc_replay_mode){
+ MC_SET_RAW_MEM;
+ trans = MC_trans_irecv_new(rdv);
+ current_state = (mc_state_t)
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ xbt_setset_set_insert(current_state->created_transitions, trans);
+ xbt_setset_set_insert(current_state->transitions, trans);
+ MC_UNSET_RAW_MEM;
+ }
+ SIMIX_process_yield();
+}
+
+/**
+ * \brief Intercept a Wait action
+ * \param comm The communication associated to the wait
+ */
+void MC_trans_intercept_wait(smx_comm_t comm)
+{
+ mc_transition_t trans=NULL;
mc_state_t current_state = NULL;
- char *type_str = NULL;
-
if(!mc_replay_mode){
- p = SIMIX_process_self();
-
MC_SET_RAW_MEM;
- mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
-
- trans->name = bprintf("[%s][%s] mc_random(%d,%d) (%p)", p->smx_host->name, p->name, min, max, trans);
- xbt_free(type_str);
-
- trans->type = mc_random ;
- trans->process = p;
- trans->min = min;
- trans->max = max;
- trans->current_value = min;
-
- /* Push it onto the enabled transitions set of the current state */
+ trans = MC_trans_wait_new(comm);
current_state = (mc_state_t)
xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
xbt_setset_set_insert(current_state->created_transitions, trans);
xbt_setset_set_insert(current_state->transitions, trans);
MC_UNSET_RAW_MEM;
}
+ SIMIX_process_yield();
}
-/**
- * \brief Associate a communication to a transition
- * \param trans The transition
- * \param comm The communication
+/**
+ * \brief Intercept a Test action
+ * \param comm The communication associated to the Test
*/
-void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm)
+void MC_trans_intercept_test(smx_comm_t comm)
{
- if(trans)
- trans->comm = comm;
- return;
+ mc_transition_t trans=NULL;
+ mc_state_t current_state = NULL;
+ if(!mc_replay_mode){
+ MC_SET_RAW_MEM;
+ trans = MC_trans_test_new(comm);
+ current_state = (mc_state_t)
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ xbt_setset_set_insert(current_state->created_transitions, trans);
+ xbt_setset_set_insert(current_state->transitions, trans);
+ MC_UNSET_RAW_MEM;
+ }
+ SIMIX_process_yield();
+}
+
+/**
+ * \brief Intercept a WaitAny action
+ * \param comms The communications associated to the WaitAny
+ */
+void MC_trans_intercept_waitany(xbt_dynar_t comms)
+{
+ mc_transition_t trans=NULL;
+ mc_state_t current_state = NULL;
+ if(!mc_replay_mode){
+ MC_SET_RAW_MEM;
+ trans = MC_trans_waitany_new(comms);
+ current_state = (mc_state_t)
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ xbt_setset_set_insert(current_state->created_transitions, trans);
+ xbt_setset_set_insert(current_state->transitions, trans);
+ MC_UNSET_RAW_MEM;
+ }
+ SIMIX_process_yield();
+}
+
+/**
+ * \brief Intercept a Random action
+ * \param min The minimum value that can be returned by the Random action
+ * \param max The maximum value that can be returned by the Random action
+ */
+void MC_trans_intercept_random(int min, int max)
+{
+ mc_transition_t trans=NULL;
+ mc_state_t current_state = NULL;
+ if(!mc_replay_mode){
+ MC_SET_RAW_MEM;
+ trans = MC_trans_random_new(min, max);
+ current_state = (mc_state_t)
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ xbt_setset_set_insert(current_state->created_transitions, trans);
+ xbt_setset_set_insert(current_state->transitions, trans);
+ MC_UNSET_RAW_MEM;
+ }
+ SIMIX_process_yield();
}
/**
xbt_free(trans);
}
+/* Compute the subset of enabled transitions of the transition set */
+void MC_trans_compute_enabled(xbt_setset_set_t enabled, xbt_setset_set_t transitions)
+{
+ mc_transition_t trans = NULL;
+ xbt_setset_cursor_t cursor = NULL;
+ /* Add all the transitions to the enabled set and then remove the disabled ones */
+ xbt_setset_add(enabled, transitions);
+ xbt_setset_foreach(transitions, cursor, trans){
+ if(trans->type == mc_wait
+ && (trans->wait.comm->src_proc == NULL || trans->wait.comm->dst_proc == NULL)){
+ xbt_setset_set_remove(enabled, trans);
+ }
+ }
+}
+
/**
* \brief Determine if two transitions are dependent
* \param t1 a transition
if(t1->type != t2->type)
return FALSE;
- if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv != t2->rdv)
+ if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
return FALSE;
- if(t1->type == mc_irecv && t2->type == mc_irecv && t1->rdv != t2->rdv)
+ if(t1->type == mc_irecv && t2->type == mc_irecv && t1->irecv.rdv != t2->irecv.rdv)
return FALSE;
- if(t1->type == mc_wait && t2->type == mc_wait && t1->comm == t2->comm)
+ if(t1->type == mc_wait && t2->type == mc_wait && t1->wait.comm == t2->wait.comm)
return FALSE;
if(t1->type == mc_wait && t2->type == mc_wait
- && t1->comm->src_buff != NULL
- && t1->comm->dst_buff != NULL
- && t2->comm->src_buff != NULL
- && t2->comm->dst_buff != NULL
- && t1->comm->dst_buff != t2->comm->src_buff
- && t1->comm->dst_buff != t2->comm->dst_buff
- && t2->comm->dst_buff != t1->comm->src_buff)
+ && t1->wait.comm->src_buff != NULL
+ && t1->wait.comm->dst_buff != NULL
+ && t2->wait.comm->src_buff != NULL
+ && t2->wait.comm->dst_buff != NULL
+ && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
+ && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
+ && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)
return FALSE;
return TRUE;
/******************************* Transitions **********************************/
+typedef enum {
+ mc_isend,
+ mc_irecv,
+ mc_test,
+ mc_wait,
+ mc_waitany,
+ mc_random
+} mc_trans_type_t;
+
typedef struct s_mc_transition{
XBT_SETSET_HEADERS;
char* name;
- mc_trans_type_t type;
smx_process_t process;
- smx_rdv_t rdv;
- smx_comm_t comm; /* reference to the simix network communication */
-
- /* Used only for random transitions */
- int min; /* min random value */
- int max; /* max random value */
- int current_value; /* current value */
+ mc_trans_type_t type;
+
+ union {
+ struct {
+ smx_rdv_t rdv;
+ } isend;
+
+ struct {
+ smx_rdv_t rdv;
+ } irecv;
+
+ struct {
+ smx_comm_t comm;
+ } wait;
+
+ struct {
+ smx_comm_t comm;
+ } test;
+
+ struct {
+ xbt_dynar_t comms;
+ } waitany;
+
+ struct {
+ int min;
+ int max;
+ int current_value;
+ } random;
+ };
} s_mc_transition_t;
-void MC_random_create(int,int);
+mc_transition_t MC_trans_isend_new(smx_rdv_t);
+mc_transition_t MC_trans_irecv_new(smx_rdv_t);
+mc_transition_t MC_trans_wait_new(smx_comm_t);
+mc_transition_t MC_trans_test_new(smx_comm_t);
+mc_transition_t MC_trans_waitany_new(xbt_dynar_t);
+mc_transition_t MC_trans_random_new(int, int);
void MC_transition_delete(mc_transition_t);
int MC_transition_depend(mc_transition_t, mc_transition_t);
+void MC_trans_compute_enabled(xbt_setset_set_t, xbt_setset_set_t);
/******************************** States **************************************/
typedef struct mc_state{
void *src_buff, size_t src_buff_size, void *data)
{
smx_comm_t comm;
- mc_transition_t trans=NULL;
- if (_surf_do_model_check) {
- /* Let's intercept the communication and control it from the model-checker */
- trans = MC_create_transition(mc_isend, SIMIX_process_self(), rdv, NULL);
- SIMIX_process_yield();
- }
+ /* If running in model-checking mode then intercept the communication action.
+ * There can be two situations, this is a replay (back-track process) so no
+ * transition needs to be created, or we are expanding a new state and in
+ * consecuence a transition needs to be created and added to the set of
+ * transitions associated to the current state.
+ */
+ if (_surf_do_model_check)
+ MC_trans_intercept_isend(rdv);
/* Look for communication request matching our needs.
If it is not found then create it and push it into the rendez-vous point */
comm->src_buff = src_buff;
comm->src_buff_size = src_buff_size;
comm->data = data;
-
- /* Associate the simix communication to the mc transition */
- if (_surf_do_model_check)
- MC_transition_set_comm(trans, comm);
SIMIX_communication_start(comm);
return comm;
}
-smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_size) {
+smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_size)
+{
smx_comm_t comm;
- mc_transition_t trans=NULL;
-
- if (_surf_do_model_check) {
- /* Let's intercept the communication and control it from the model-checker */
- trans = MC_create_transition(mc_irecv, SIMIX_process_self(), rdv, NULL);
- SIMIX_process_yield();
- }
+
+ /* If running in model-checking mode then intercept the communication action.
+ * There can be two situations, this is a replay (back-track process) so no
+ * transition needs to be created, or we are expanding a new state and in
+ * consecuence a transition needs to be created and added to the set of
+ * transitions associated to the current state.
+ */
+ if (_surf_do_model_check)
+ MC_trans_intercept_irecv(rdv);
/* Look for communication request matching our needs.
- If it is not found then create it and push it into the rendez-vous point */
+ * If it is not found then create it and push it into the rendez-vous point
+ */
comm = SIMIX_rdv_get_request(rdv, comm_send);
if(!comm){
comm->dst_proc = SIMIX_process_self();
comm->dst_buff = dst_buff;
comm->dst_buff_size = dst_buff_size;
-
- /* Associate the simix communication to the mc transition */
- if (_surf_do_model_check)
- MC_transition_set_comm(trans, comm);
SIMIX_communication_start(comm);
return comm;
}
/** @brief blocks until the communication terminates or the timeout occurs */
-XBT_INLINE void SIMIX_network_wait(smx_comm_t comm, double timeout) {
- if (_surf_do_model_check) {
- /* Let's intercept the communication and control it from the model-checker */
- MC_create_transition(mc_wait, SIMIX_process_self(), comm->rdv, comm);
- SIMIX_process_yield();
- }
+XBT_INLINE void SIMIX_network_wait(smx_comm_t comm, double timeout)
+{
+ /* If running in model-checking mode then intercept the communication action.
+ * There can be two situations, this is a replay (back-track process) so no
+ * transition needs to be created, or we are expanding a new state and in
+ * consecuence a transition needs to be created and added to the set of
+ * transitions associated to the current state.
+ */
+ if (_surf_do_model_check)
+ MC_trans_intercept_wait(comm);
+
/* Wait for communication completion */
SIMIX_communication_wait_for_completion(comm, timeout);
}
/** @Returns whether the (asynchronous) communication is done yet or not */
-XBT_INLINE int SIMIX_network_test(smx_comm_t comm) {
- if (_surf_do_model_check) {
- /* Let's intercept the communication and control it from the model-checker */
- MC_create_transition(mc_test, SIMIX_process_self(), comm->rdv, comm);
- SIMIX_process_yield();
- }
+XBT_INLINE int SIMIX_network_test(smx_comm_t comm)
+{
+ /* If running in model-checking mode then intercept the communication action.
+ * There can be two situations, this is a replay (back-track process) so no
+ * transition needs to be created, or we are expanding a new state and in
+ * consecuence a transition needs to be created and added to the set of
+ * transitions associated to the current state.
+ */
+ if (_surf_do_model_check)
+ MC_trans_intercept_test(comm);
/* Copy data if the communication is done */
if(comm->sem && !SIMIX_sem_would_block(comm->sem)){
*
* @Returns the rank in the dynar of communication which finished; destroy it after identifying which one it is
*/
-unsigned int SIMIX_network_waitany(xbt_dynar_t comms) {
+unsigned int SIMIX_network_waitany(xbt_dynar_t comms)
+{
xbt_dynar_t sems = xbt_dynar_new(sizeof(smx_sem_t),NULL);
unsigned int cursor, found_comm=-1;
smx_comm_t comm,comm_finished=NULL;
- if (_surf_do_model_check) {
- /* Let's intercept the communication and control it from the model-checker */
- MC_create_transition(mc_waitany, SIMIX_process_self(), NULL, NULL);
- SIMIX_process_yield();
- }
-
+ /* If running in model-checking mode then intercept the communication action.
+ * There can be two situations, this is a replay (back-track process) so no
+ * transition needs to be created, or we are expanding a new state and in
+ * consecuence a transition needs to be created and added to the set of
+ * transitions associated to the current state.
+ */
+ if (_surf_do_model_check)
+ MC_trans_intercept_waitany(comms);
+
xbt_dynar_foreach(comms,cursor,comm)
xbt_dynar_push(sems,&(comm->sem));
/* Check for errors and cleanup the comm */
SIMIX_communication_wait_for_completion(comm_finished,-1);
return found_comm;
-}
+}
\ No newline at end of file
