From 635188886cb9b98f353a1c3869dee898f9b73b8b Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Wed, 24 Oct 2012 15:13:41 +0200 Subject: [PATCH] Desactivate an historical MC_assert so that model-checking Chord get a chance to work Leave a comment on this first historical battle for MC in SimGrid in the source code :) --- examples/msg/chord/chord.c | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c index c3fe12cff4..a3b7830071 100644 --- a/examples/msg/chord/chord.c +++ b/examples/msg/chord/chord.c @@ -633,16 +633,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 -- 2.20.1