[mc] DRY with mc_update_comm_pattern() (broken)

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 91c32f4..73b2701 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -317,7 +317,6 @@ void MC_modelcheck_comm_determinism(void)
   smx_simcall_t req = NULL;
   smx_process_t process = NULL;
   mc_state_t state = NULL, next_state = NULL;
-  smx_action_t current_comm;
   xbt_dynar_t current_pattern;
 
   while (xbt_fifo_size(mc_stack) > 0) {
@@ -361,19 +360,7 @@ void MC_modelcheck_comm_determinism(void)
 
       MC_SET_MC_HEAP;
       current_pattern = !initial_global_state->initial_communications_pattern_done ? initial_communications_pattern : communications_pattern; 
-      if (call == MC_CALL_TYPE_SEND) { /* Send */
-        get_comm_pattern(current_pattern, req, call);
-      } else if (call == MC_CALL_TYPE_RECV) { /* Recv */
-        get_comm_pattern(current_pattern, req, call);
-      } else if (call == MC_CALL_TYPE_WAIT) { /* Wait */
-        current_comm = simcall_comm_wait__get__comm(req);
-        if (current_comm->comm.refcount == 1)  /* First wait only must be considered */
-          complete_comm_pattern(current_pattern, current_comm);
-      } else if (call == MC_CALL_TYPE_WAITANY) { /* WaitAny */
-        current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
-        if (current_comm->comm.refcount == 1) /* First wait only must be considered */
-          complete_comm_pattern(current_pattern, current_comm);
-      }
+      mc_update_comm_pattern(call, req, value, current_pattern);
       MC_SET_STD_HEAP;
 
       /* Wait for requests (schedules processes) */

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index cec768d..92cec86 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -503,6 +503,22 @@ int MC_deadlock_check()
   return deadlock;
 }
 
+void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value, xbt_dynar_t pattern) {
+  if (call_type == MC_CALL_TYPE_SEND) { /* Send */
+    get_comm_pattern(pattern, req, call_type);
+  } else if (call_type == MC_CALL_TYPE_RECV) { /* Recv */
+    get_comm_pattern(pattern, req, call_type);
+  } else if (call_type == MC_CALL_TYPE_WAIT) { /* Wait */
+    smx_action_t current_comm = simcall_comm_wait__get__comm(req);
+    if (current_comm->comm.refcount == 1)  /* First wait only must be considered */
+      complete_comm_pattern(pattern, current_comm);
+  } else if (call_type == MC_CALL_TYPE_WAITANY) { /* WaitAny */
+    smx_action_t current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+    if (current_comm->comm.refcount == 1) /* First wait only must be considered */
+      complete_comm_pattern(pattern, current_comm);
+  }
+}
+
 /**
  * \brief Re-executes from the state at position start all the transitions indicated by
  *        a given model-checker stack.
@@ -519,7 +535,6 @@ void MC_replay(xbt_fifo_t stack, int start)
   xbt_fifo_item_t item, start_item;
   mc_state_t state;
   smx_process_t process = NULL;
-  smx_action_t current_comm;
 
   XBT_DEBUG("**** Begin Replay ****");
 
@@ -604,19 +619,7 @@ void MC_replay(xbt_fifo_t stack, int start)
 
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
         MC_SET_MC_HEAP;
-        if (call == MC_CALL_TYPE_SEND) { /* Send */
-          get_comm_pattern(communications_pattern, req, call);
-        } else if (call == MC_CALL_TYPE_RECV) { /* Recv */
-          get_comm_pattern(communications_pattern, req, call);
-        } else if (call == MC_CALL_TYPE_WAIT) { /* Wait */
-          current_comm = simcall_comm_wait__get__comm(req);
-          if (current_comm->comm.refcount == 1)  /* First wait only must be considered */
-            complete_comm_pattern(communications_pattern, current_comm);
-        } else if (call == MC_CALL_TYPE_WAITANY) { /* WaitAny */
-          current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
-          if (current_comm->comm.refcount == 1) /* First wait only must be considered */
-            complete_comm_pattern(communications_pattern, current_comm);
-        }
+        mc_update_comm_pattern(call, req, value, communications_pattern);
         MC_SET_STD_HEAP;
       }
 

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 2f886d9..4e113a0 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -735,6 +735,7 @@ static inline mc_call_type mc_get_call_type(smx_simcall_t req) {
 }
 
 void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, mc_call_type call_type);
+void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern);
 void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm);
 void MC_pre_modelcheck_comm_determinism(void);
 void MC_modelcheck_comm_determinism(void);