model-checker : fix MC_RANDOM simcall

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

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index c3fe12c..42b74ca 100644 (file)
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -335,28 +335,44 @@ int node(int argc, char *argv[])
       if (!MSG_comm_test(node.comm_receive)) {
 
         // no task was received: make some periodic calls
-        if (MSG_get_clock() >= next_stabilize_date) {
-          stabilize(&node);
-          next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
-        }
-        else if (MSG_get_clock() >= next_fix_fingers_date) {
-          fix_fingers(&node);
-          next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
-        }
-        else if (MSG_get_clock() >= next_check_predecessor_date) {
-          check_predecessor(&node);
-          next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
-        }
-        else if (MSG_get_clock() >= next_lookup_date) {
-          random_lookup(&node);
-          next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
-        }
-        else {
-          // nothing to do: sleep for a while
-          MSG_process_sleep(5);
+
+        if(MC_is_active()){
+          if(MC_random()){
+            stabilize(&node);
+          }else if(MC_random()){
+            fix_fingers(&node);
+          }else if(MC_random()){
+            check_predecessor(&node);
+          }else if(MC_random()){
+            random_lookup(&node);
+          }else{
+            MSG_process_sleep(5);
+          }
+        }else{
+          if (MSG_get_clock() >= next_stabilize_date) {
+            stabilize(&node);
+            next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
+          }
+          else if (MSG_get_clock() >= next_fix_fingers_date) {
+            fix_fingers(&node);
+            next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
+          }
+          else if (MSG_get_clock() >= next_check_predecessor_date) {
+            check_predecessor(&node);
+            next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
+          }
+          else if (MSG_get_clock() >= next_lookup_date) {
+            random_lookup(&node);
+            next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
+          }
+          else {
+            // nothing to do: sleep for a while
+            MSG_process_sleep(5);
+          }
         }
+
       } else {
-        // a transfer has occured
+        // a transfer has occurred
 
         msg_error_t status = MSG_comm_get_status(node.comm_receive);
 
@@ -633,16 +649,19 @@ static int remote_find_successor(node_t node, int ask_to, int id)
         XBT_DEBUG("Received a task (%p)", task_received);
         task_data_t ans_data = MSG_task_get_data(task_received);
 
-        if (MC_is_active()) {
-          // 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);
-        }
+       // Once upon a time, our code assumed that here, task_received != task_sent all the time
+       // 
+       // This assumption is wrong (as messages from differing round can interleave), leading to a bug in our code.
+       // We failed to find this bug directly, as it only occured on large platforms, leading to hardly usable traces.
+       // Instead, we used the model-checker to track down the issue by adding the following test here in the code:
+       //   if (MC_is_active()) {
+       //      MC_assert(task_received == task_sent);
+        //   }
+       // That explained the bug in a snap, with a very cool example and everything.
+       // 
+       // This MC_assert is now desactivated as the case is now properly handled in our code and we don't want the
+       //   MC to fail any further under that condition, but this comment is here to as a memorial for this first 
+       //   brillant victory of the model-checking in the SimGrid community :)
 
         if (task_received != task_sent) {
           // this is not the expected answer