#include "msg/msg.h"
#include "xbt/log.h"
#include "xbt/asserts.h"
+#include "mc/modelchecker.h"
+#include "mc/mc.h"
XBT_LOG_NEW_DEFAULT_CATEGORY(msg_chord,
"Messages specific for this msg example");
char pred_mailbox[MAILBOX_NAME_SIZE]; // predecessor's mailbox name
int next_finger_to_fix; // index of the next finger to fix in fix_fingers()
msg_comm_t comm_receive; // current communication to receive
- xbt_dynar_t comms; // current communications being sent
double last_change_date; // last time I changed a finger or my predecessor
} s_node_t, *node_t;
*/
static int normalize(int id)
{
- // make sure id >= 0
- while (id < 0) {
- id += nb_keys;
- }
- // make sure id < nb_keys
- id = id % nb_keys;
-
- return id;
+ // like id % nb_keys, but works with negatives numbers (and faster)
+ return id & (nb_keys - 1);
}
/**
*/
int node(int argc, char *argv[])
{
+ /* Reduce the run size for the MC */
+ if(MC_IS_ENABLED){
+ periodic_stabilize_delay = 8;
+ periodic_fix_fingers_delay = 8;
+ periodic_check_predecessor_delay = 8;
+ }
+
double init_time = MSG_get_clock();
- /*m_task_t task = NULL;*/
m_task_t task_received = NULL;
- msg_comm_t comm_send = NULL;
int i;
- int index;
int join_success = 0;
double deadline;
double next_stabilize_date = init_time + periodic_stabilize_delay;
node.id = atoi(argv[1]);
get_mailbox(node.id, node.mailbox);
node.next_finger_to_fix = 0;
- node.comms = xbt_dynar_new(sizeof(msg_comm_t), NULL);
node.fingers = xbt_new0(s_finger_t, nb_bits);
node.last_change_date = init_time;
}
// see if some communications are finished
+ /*
while ((index = MSG_comm_testany(node.comms)) != -1) {
comm_send = xbt_dynar_get_as(node.comms, index, msg_comm_t);
MSG_error_t status = MSG_comm_get_status(comm_send);
xbt_dynar_remove_at(node.comms, index, &comm_send);
DEBUG3("Communication %p is finished with status %d, dynar size is now %lu",
comm_send, status, xbt_dynar_length(node.comms));
+ m_task_t task = MSG_comm_get_task(comm_send);
MSG_comm_destroy(comm_send);
+ if (status != MSG_OK) {
+ task_data_destroy(MSG_task_get_data(task));
+ MSG_task_destroy(task);
+ }
}
+ */
}
// clean unfinished comms sent
/* unsigned int cursor;
xbt_dynar_foreach(node.comms, cursor, comm_send) {
- task = MSG_comm_get_task(comm_send);
+ m_task_t task = MSG_comm_get_task(comm_send);
MSG_task_cancel(task);
task_data_destroy(MSG_task_get_data(task));
MSG_task_destroy(task);
}
// stop the simulation
- xbt_dynar_free(&node.comms);
xbt_free(node.fingers);
return 0;
}
static void handle_task(node_t node, m_task_t task) {
DEBUG1("Handling task %p", task);
- msg_comm_t comm = NULL;
- char* mailbox = NULL;
+ char mailbox[MAILBOX_NAME_SIZE];
task_data_t task_data = (task_data_t) MSG_task_get_data(task);
e_task_type_t type = task_data->type;
if (is_in_interval(task_data->request_id, node->id + 1, node->fingers[0].id)) {
task_data->type = TASK_FIND_SUCCESSOR_ANSWER;
task_data->answer_id = node->fingers[0].id;
- DEBUG3("Sending back a 'Find Successor Answer' to %s: the successor of %d is %d",
+ DEBUG4("Sending back a 'Find Successor Answer' to %s (mailbox %s): the successor of %d is %d",
task_data->issuer_host_name,
+ task_data->answer_to,
task_data->request_id, task_data->answer_id);
- comm = MSG_task_isend(task, task_data->answer_to);
- xbt_dynar_push(node->comms, &comm);
+ MSG_task_dsend(task, task_data->answer_to);
}
else {
// otherwise, forward the request to the closest preceding finger in my table
DEBUG2("Forwarding the 'Find Successor' request for id %d to my closest preceding finger %d",
task_data->request_id, closest);
get_mailbox(closest, mailbox);
- comm = MSG_task_isend(task, mailbox);
- xbt_dynar_push(node->comms, &comm);
- xbt_free(mailbox);
+ MSG_task_dsend(task, mailbox);
}
break;
DEBUG3("Sending back a 'Get Predecessor Answer' to %s via mailbox '%s': my predecessor is %d",
task_data->issuer_host_name,
task_data->answer_to, task_data->answer_id);
- comm = MSG_task_isend(task, task_data->answer_to);
- xbt_dynar_push(node->comms, &comm);
+ MSG_task_dsend(task, task_data->answer_to);
break;
case TASK_NOTIFY:
case TASK_FIND_SUCCESSOR_ANSWER:
case TASK_GET_PREDECESSOR_ANSWER:
DEBUG2("Ignoring unexpected task of type %d (%p)", type, task);
+ task_data_destroy(task_data);
+ MSG_task_destroy(task);
break;
}
}
DEBUG2("Failed to receive the answer to my 'Find Successor' request (task %p): %d",
task_sent, res);
stop = 1;
- //MSG_comm_destroy(node->comm_receive);
+ MSG_comm_destroy(node->comm_receive);
+ node->comm_receive = NULL;
}
else {
m_task_t task_received = MSG_comm_get_task(node->comm_receive);
DEBUG1("Received a task (%p)", task_received);
task_data_t ans_data = MSG_task_get_data(task_received);
+ if (MC_IS_ENABLED) {
+ MC_assert(task_received == task_sent);
+ }
+
if (task_received != task_sent) {
// this is not the expected answer
+ MSG_comm_destroy(node->comm_receive);
+ node->comm_receive = NULL;
handle_task(node, task_received);
}
else {
ans_data->request_id, task_received, id, ans_data->answer_id);
successor = ans_data->answer_id;
stop = 1;
+ MSG_comm_destroy(node->comm_receive);
+ node->comm_receive = NULL;
MSG_task_destroy(task_received);
task_data_destroy(req_data);
}
}
- MSG_comm_destroy(node->comm_receive);
- node->comm_receive = NULL;
} while (!stop);
}
DEBUG2("Failed to receive the answer to my 'Get Predecessor' request (task %p): %d",
task_sent, res);
stop = 1;
- //MSG_comm_destroy(node->comm_receive);
+ MSG_comm_destroy(node->comm_receive);
+ node->comm_receive = NULL;
}
else {
m_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) {
+ MC_assert(task_received == task_sent);
+ }
+
if (task_received != task_sent) {
+ MSG_comm_destroy(node->comm_receive);
+ node->comm_receive = NULL;
handle_task(node, task_received);
}
else {
task_received, ask_to, ans_data->answer_id);
predecessor_id = ans_data->answer_id;
stop = 1;
+ MSG_comm_destroy(node->comm_receive);
+ node->comm_receive = NULL;
MSG_task_destroy(task_received);
task_data_destroy(req_data);
}
}
- MSG_comm_destroy(node->comm_receive);
- node->comm_receive = NULL;
} while (!stop);
}
DEBUG2("Sending a 'Notify' request (task %p) to %d", task, notify_id);
char mailbox[MAILBOX_NAME_SIZE];
get_mailbox(notify_id, mailbox);
- msg_comm_t comm = MSG_task_isend(task, mailbox);
- xbt_dynar_push(node->comms, &comm);
+ MSG_task_dsend(task, mailbox);
}
/**
