X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/61c27c5a694455d748f17989be2ecf0850610a90..f53ee0c4bdeaffa3c7a781f45f640e5f32cbb480:/src/mc/mc_transition.c

diff --git a/src/mc/mc_transition.c b/src/mc/mc_transition.c
index 6b9d7f89a0..dcc1915621 100644
--- a/src/mc/mc_transition.c
+++ b/src/mc/mc_transition.c
@@ -1,107 +1,274 @@
 #include "private.h"
 
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans, mc,
+				"Logging specific to MC transitions");
+
+/* 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 value)
+{
+  mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+  trans->type = mc_random;
+  trans->process = SIMIX_process_self();
+  trans->random.value = value;
+  trans->name = bprintf("[%s][%s] Random %d (%p)", trans->process->smx_host->name, 
+                        trans->process->name, value, trans);
+
+  return trans;
+}
+
+/**
+ * \brief Deletes a transition
+ * \param trans The transition to be deleted
+ */
+void MC_transition_delete(mc_transition_t trans)
+{
+  xbt_free(trans->name);
+  xbt_free(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);
+    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;
+  }
+  SIMIX_process_yield();  
+}
 
-    /* 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) 
+/**
+ * \brief Intercept an iRecv action
+ * \param rdv The rendez-vous of the iRecv
+ */
+void MC_trans_intercept_irecv(smx_rdv_t rdv)
+{
+  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;
-    return trans;
   }
-  return NULL;
+  SIMIX_process_yield();
 }
 
-void MC_random_create(int min, int max)
+/**
+ * \brief Intercept a Wait action
+ * \param comm The communication associated to the wait
+ */
+void MC_trans_intercept_wait(smx_comm_t comm)
 {
-  smx_process_t p;
+  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 Deletes a transition
- * \param trans The transition to be deleted
+ * \brief Intercept a WaitAny action
+ * \param comms The communications associated to the WaitAny
  */
-void MC_transition_delete(mc_transition_t trans)
+void MC_trans_intercept_waitany(xbt_dynar_t comms)
 {
-  xbt_free(trans->name);
-  xbt_free(trans);
+  unsigned int cursor;
+  mc_transition_t trans = NULL;
+  mc_state_t current_state = NULL;
+  smx_comm_t comm = NULL;
+  
+  if(!mc_replay_mode){
+    MC_SET_RAW_MEM;
+    current_state = (mc_state_t) 
+      xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    xbt_dynar_foreach(comms, cursor, comm){ 
+      trans = MC_trans_wait_new(comm);
+      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)
+{
+  int i;
+  mc_transition_t trans=NULL;
+  mc_state_t current_state = NULL;
+  if(!mc_replay_mode){
+    MC_SET_RAW_MEM;
+    current_state = (mc_state_t) 
+      xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    for(i=min; i <= max; i++){    
+      trans = MC_trans_random_new(i);
+      xbt_setset_set_insert(current_state->created_transitions, trans);
+      xbt_setset_set_insert(current_state->transitions, trans);
+    }
+    MC_UNSET_RAW_MEM;
+  }
+  SIMIX_process_yield();
+}
+
+/* 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)
+{
+  unsigned int index = 0;
+  smx_comm_t comm = NULL;
+  mc_transition_t trans = NULL;
+  xbt_setset_cursor_t cursor = NULL;
+  xbt_setset_foreach(transitions, cursor, trans){
+    switch(trans->type){
+      /* Wait transitions are enabled only if the communication has both a
+         sender and receiver */
+      case mc_wait:
+        if(trans->wait.comm->src_proc && trans->wait.comm->dst_proc){
+          xbt_setset_set_insert(enabled, trans);
+          DEBUG1("Transition %p is enabled for next state", trans);
+        }
+        break;
+
+      /* WaitAny transitions are enabled if any of it's communications has both
+         a sender and a receiver */
+      case mc_waitany:
+        xbt_dynar_foreach(trans->waitany.comms, index, comm){
+          if(comm->src_proc && comm->dst_proc){
+            xbt_setset_set_insert(enabled, trans);
+            DEBUG1("Transition %p is enabled for next state", trans);
+            break;
+          }
+        }
+        break;
+
+      /* The rest of the transitions cannot be disabled */
+      default:
+        xbt_setset_set_insert(enabled, trans);
+        DEBUG1("Transition %p is enabled for next state", trans);
+        break;
+    } 
+  }
 }
 
 /**
@@ -115,27 +282,33 @@ int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
   if(t1->process == t2->process) 
     return FALSE;
 
-  if(t1->type != t2->type)
+  if(t1->type == mc_isend && t2->type == mc_irecv)
+    return FALSE;
+
+  if(t1->type == mc_irecv && t2->type == mc_isend)
     return FALSE;
   
-  if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv != t2->rdv)
+  if(t1->type == mc_random || t2->type == mc_random)
+    return FALSE;
+  
+  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;
 }
\ No newline at end of file