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;
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)) {
+ 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);
+ }
+ }
- // a transfer has occured
+ } else {
+ // a transfer has occurred
msg_error_t status = MSG_comm_get_status(node.comm_receive);
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
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);
}
