Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
chord: avoid duplicate call of MSG_comm_test()
[simgrid.git] / examples / msg / chord / chord.c
index e0787cb..ec12796 100644 (file)
@@ -355,10 +355,7 @@ int node(int argc, char *argv[])
           // nothing to do: sleep for a while
           MSG_process_sleep(5);
         }
-      }
-
-      if (node.comm_receive && MSG_comm_test(node.comm_receive)) {
-
+      } else {
         // a transfer has occured
 
         msg_error_t status = MSG_comm_get_status(node.comm_receive);
@@ -637,6 +634,13 @@ static int remote_find_successor(node_t node, int ask_to, int id)
         task_data_t ans_data = MSG_task_get_data(task_received);
 
         if (MC_IS_ENABLED) {
+          // the model-checker is expected to find a counter-example here. 
+         // 
+         // As you can see in the test right below, task_received is not always equal to task_sent 
+         // (as messages from differing round can interleave). But the previous version of this code 
+         // wrongly assumed that, leading to problems. But this only occured on large platforms,
+         // leading to hardly usable traces. So we used the model-checker to track down the issue, 
+         // and we came down to this test, that explained the bug in a snap.
           MC_assert(task_received == task_sent);
         }
 
@@ -917,7 +921,6 @@ int main(int argc, char *argv[])
   XBT_CRITICAL("Messages created: %ld", smx_total_comms);
   XBT_INFO("Simulated time: %g", MSG_get_clock());
 
-  MSG_clean();
   chord_exit();
 
   if (res == MSG_OK)