X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0afab0e550e09d35a4aaaae802c7f2ea17d2b860..8a30d839e791237688f68d4047fef5a30293dfc4:/examples/msg/chord/chord.c diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c index 5061abd7bd..ca921a785b 100644 --- a/examples/msg/chord/chord.c +++ b/examples/msg/chord/chord.c @@ -204,8 +204,10 @@ static void get_mailbox(int node_id, char* mailbox) static void task_free(void* task) { // TODO add a parameter data_free_function to MSG_task_create? - xbt_free(MSG_task_get_data(task)); - MSG_task_destroy(task); + if(task != NULL){ + xbt_free(MSG_task_get_data(task)); + MSG_task_destroy(task); + } } /** @@ -269,8 +271,9 @@ 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){ + if(MC_is_active()){ periodic_stabilize_delay = 8; periodic_fix_fingers_delay = 8; periodic_check_predecessor_delay = 8; @@ -335,31 +338,67 @@ 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 (node.comm_receive && MSG_comm_test(node.comm_receive)) { - // a transfer has occured + #ifdef HAVE_MC + 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 + 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); + } + #endif + + } else { + // a transfer has occurred msg_error_t status = MSG_comm_get_status(node.comm_receive); @@ -636,16 +675,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_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); - } + // 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 @@ -723,7 +765,7 @@ static int remote_get_predecessor(node_t node, int ask_to) msg_task_t task_received = MSG_comm_get_task(node->comm_receive); task_data_t ans_data = MSG_task_get_data(task_received); - if (MC_IS_ENABLED) { + if (MC_is_active()) { MC_assert(task_received == task_sent); }