Increase the frequency of chord's getrequest operations when running the mc.

[simgrid.git] / examples / msg / chord / chord.c

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index 9071378..f7f145a 100644 (file)
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -10,6 +10,7 @@
 #include "xbt/log.h"
 #include "xbt/asserts.h"
 #include "mc/modelchecker.h"
+#include "mc/mc.h"
 XBT_LOG_NEW_DEFAULT_CATEGORY(msg_chord,
                              "Messages specific for this msg example");
 
@@ -130,14 +131,8 @@ static void chord_initialize(void)
  */
 static int normalize(int id)
 {
-  // make sure id >= 0
-  while (id < 0) {
-    id += nb_keys;
-  }
-  // make sure id < nb_keys
-  id = id % nb_keys;
-
-  return id;
+  // like id % nb_keys, but works with negatives numbers (and faster)
+  return id & (nb_keys - 1);
 }
 
 /**
@@ -255,6 +250,13 @@ static void set_predecessor(node_t node, int predecessor_id)
  */
 int node(int argc, char *argv[])
 {
+  /* Reduce the run size for the MC */
+  if(MC_IS_ENABLED){
+    periodic_stabilize_delay = 3;
+    periodic_fix_fingers_delay = 3;
+    periodic_check_predecessor_delay = 3;
+  }
+
   double init_time = MSG_get_clock();
   m_task_t task_received = NULL;
   msg_comm_t comm_send = NULL;
@@ -335,7 +337,7 @@ int node(int argc, char *argv[])
        }
         else {
           // nothing to do: sleep for a while
-          MSG_process_sleep(5);
+          MSG_process_sleep(3);
         }
       }
       else {
@@ -649,7 +651,9 @@ static int remote_find_successor(node_t node, int ask_to, int id)
         DEBUG1("Received a task (%p)", task_received);
         task_data_t ans_data = MSG_task_get_data(task_received);
 
-        MC_assert(task_received == task_sent);
+       if (MC_IS_ENABLED) {
+         MC_assert(task_received == task_sent);
+       }
 
         if (task_received != task_sent) {
           // this is not the expected answer
@@ -729,7 +733,9 @@ static int remote_get_predecessor(node_t node, int ask_to)
         m_task_t task_received = MSG_comm_get_task(node->comm_receive);
         task_data_t ans_data = MSG_task_get_data(task_received);
 
-        MC_assert(task_received == task_sent);
+       if (MC_IS_ENABLED) {
+         MC_assert(task_received == task_sent);
+       }
 
         if (task_received != task_sent) {
          MSG_comm_destroy(node->comm_receive);