Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add suport for TestAny and WaitAny requests to the model-checker.
authorcristianrosa <cristianrosa@48e7efb5-ca39-0410-a469-dd3cf9ba447f>
Wed, 5 Jan 2011 09:02:47 +0000 (09:02 +0000)
committercristianrosa <cristianrosa@48e7efb5-ca39-0410-a469-dd3cf9ba447f>
Wed, 5 Jan 2011 09:02:47 +0000 (09:02 +0000)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@9358 48e7efb5-ca39-0410-a469-dd3cf9ba447f

src/mc/mc_dpor.c
src/mc/mc_global.c
src/mc/mc_request.c
src/mc/mc_state.c
src/mc/private.h
src/simix/network_private.h
src/simix/smurf_private.h
src/simix/smx_global.c
src/simix/smx_network.c
src/simix/smx_smurf.c

index 1970b9c..bc37c91 100644 (file)
@@ -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);
 
index de02e74..50b1c74 100644 (file)
@@ -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);
index 6ee8336..3aaa266 100644 (file)
@@ -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;
+}
index 74f5a54..e289fd1 100644 (file)
@@ -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;
     }
   }
 
index a1720fd..7c13977 100644 (file)
@@ -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 {
index a66b5d9..292e656 100644 (file)
@@ -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);
index f150f85..f9659fc 100644 (file)
@@ -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
index 9fcfa67..d0e2c53 100644 (file)
@@ -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));
 
index c5a62db..41192b6 100644 (file)
@@ -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 */
index 8c4b370..3f2045d 100644 (file)
@@ -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: