add_executable(random_test random_test.c)
add_executable(bugged1_liveness bugged1_liveness.c)
add_executable(bugged2_liveness bugged2_liveness.c)
+ add_executable(chord_liveness chord_liveness.c)
add_executable(test/snapshot_comparison_liveness1 test/snapshot_comparison_liveness1.c)
add_executable(test/snapshot_comparison_liveness2 test/snapshot_comparison_liveness2.c)
add_executable(test/snapshot_comparison_liveness3 test/snapshot_comparison_liveness3.c)
target_link_libraries(random_test simgrid m )
target_link_libraries(bugged1_liveness simgrid m )
target_link_libraries(bugged2_liveness simgrid m )
+ target_link_libraries(chord_liveness simgrid m )
target_link_libraries(test/snapshot_comparison_liveness1 simgrid m )
target_link_libraries(test/snapshot_comparison_liveness2 simgrid m )
target_link_libraries(test/snapshot_comparison_liveness3 simgrid m )
${CMAKE_CURRENT_SOURCE_DIR}/deploy_mutex.xml
${CMAKE_CURRENT_SOURCE_DIR}/deploy_random_test.xml
${CMAKE_CURRENT_SOURCE_DIR}/platform.xml
+ ${CMAKE_CURRENT_SOURCE_DIR}/deploy_chord_liveness.xml
${CMAKE_CURRENT_SOURCE_DIR}/test/deploy_snapshot_comparison.xml
PARENT_SCOPE
)
${CMAKE_CURRENT_SOURCE_DIR}/random_test.c
${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.h
${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h
+ ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness.c
+ ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness.h
${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness1.c
${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness2.c
${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness3.c
${CMAKE_CURRENT_SOURCE_DIR}/parse_dwarf
${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged1_liveness
${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness
+ ${CMAKE_CURRENT_SOURCE_DIR}/promela_chord_liveness
${CMAKE_CURRENT_SOURCE_DIR}/test/promela
PARENT_SCOPE
)
--- /dev/null
+
+/* Copyright (c) 2010. The SimGrid Team.
+ * All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <stdio.h>
+#include "msg/msg.h"
+#include "xbt/log.h"
+#include "xbt/asserts.h"
+#include "simgrid/modelchecker.h"
+#include "chord_liveness.h"
+#include "mc/mc.h"
+
+/** @addtogroup MSG_examples
+ *
+ * - <b>chord/chord.c: Classical Chord P2P protocol</b>
+ * This example implements the well known Chord P2P protocol. Its
+ * main advantage is that it constitute a fully working non-trivial
+ * example. In addition, its implementation is rather efficient, as
+ * demonstrated in http://hal.inria.fr/inria-00602216/
+ */
+
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(chord_liveness,
+ "Messages specific for this example");
+
+#define COMM_SIZE 10
+#define COMP_SIZE 0
+#define MAILBOX_NAME_SIZE 10
+
+static int nb_bits = 24;
+static int nb_keys = 0;
+static int timeout = 50;
+static int max_simulation_time = 1000;
+static int periodic_stabilize_delay = 20;
+static int periodic_fix_fingers_delay = 120;
+static int periodic_check_predecessor_delay = 120;
+static int periodic_lookup_delay = 10;
+
+//extern long int smx_total_comms;
+
+/*
+ * Finger element.
+ */
+typedef struct s_finger {
+ int id;
+ char mailbox[MAILBOX_NAME_SIZE]; // string representation of the id
+} s_finger_t, *finger_t;
+
+/*
+ * Node data.
+ */
+typedef struct s_node {
+ int id; // my id
+ char mailbox[MAILBOX_NAME_SIZE]; // my mailbox name (string representation of the id)
+ s_finger_t *fingers; // finger table, of size nb_bits (fingers[0] is my successor)
+ int pred_id; // predecessor id
+ 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
+ double last_change_date; // last time I changed a finger or my predecessor
+} s_node_t, *node_t;
+
+/**
+ * Types of tasks exchanged between nodes.
+ */
+typedef enum {
+ TASK_FIND_SUCCESSOR,
+ TASK_FIND_SUCCESSOR_ANSWER,
+ TASK_GET_PREDECESSOR,
+ TASK_GET_PREDECESSOR_ANSWER,
+ TASK_NOTIFY,
+ TASK_SUCCESSOR_LEAVING,
+ TASK_PREDECESSOR_LEAVING
+} e_task_type_t;
+
+/*
+ * Data attached with the tasks sent and received
+ */
+typedef struct s_task_data {
+ e_task_type_t type; // type of task
+ int request_id; // id paramater (used by some types of tasks)
+ int request_finger; // finger parameter (used by some types of tasks)
+ int answer_id; // answer (used by some types of tasks)
+ char answer_to[MAILBOX_NAME_SIZE]; // mailbox to send an answer to (if any)
+ const char* issuer_host_name; // used for logging
+} s_task_data_t, *task_data_t;
+
+static int *powers2;
+
+// utility functions
+static void chord_initialize(void);
+static void chord_exit(void);
+static int normalize(int id);
+static int is_in_interval(int id, int start, int end);
+static void get_mailbox(int host_id, char* mailbox);
+static void task_free(void* task);
+static void print_finger_table(node_t node);
+static void set_finger(node_t node, int finger_index, int id);
+static void set_predecessor(node_t node, int predecessor_id);
+
+// process functions
+static int node(int argc, char *argv[]);
+static void handle_task(node_t node, msg_task_t task);
+
+// Chord core
+static void create(node_t node);
+static int join(node_t node, int known_id);
+static void leave(node_t node);
+static int find_successor(node_t node, int id);
+static int remote_find_successor(node_t node, int ask_to_id, int id);
+static int remote_get_predecessor(node_t node, int ask_to_id);
+static int closest_preceding_node(node_t node, int id);
+static void stabilize(node_t node);
+static void notify(node_t node, int predecessor_candidate_id);
+static void remote_notify(node_t node, int notify_to, int predecessor_candidate_id);
+static void fix_fingers(node_t node);
+static void check_predecessor(node_t node);
+static void random_lookup(node_t);
+static void quit_notify(node_t node);
+
+/* Global variable corresponding to atomic proposition */
+int node_join = 0;
+
+/**
+ * \brief Global initialization of the Chord simulation.
+ */
+static void chord_initialize(void)
+{
+ // compute the powers of 2 once for all
+ powers2 = xbt_new(int, nb_bits);
+ int pow = 1;
+ int i;
+ for (i = 0; i < nb_bits; i++) {
+ powers2[i] = pow;
+ pow = pow << 1;
+ }
+ nb_keys = pow;
+ XBT_DEBUG("Sets nb_keys to %d", nb_keys);
+}
+
+static void chord_exit(void)
+{
+ xbt_free(powers2);
+}
+
+/**
+ * \brief Turns an id into an equivalent id in [0, nb_keys).
+ * \param id an id
+ * \return the corresponding normalized id
+ */
+static int normalize(int id)
+{
+ // like id % nb_keys, but works with negatives numbers (and faster)
+ return id & (nb_keys - 1);
+}
+
+/**
+ * \brief Returns whether an id belongs to the interval [start, end].
+ *
+ * The parameters are noramlized to make sure they are between 0 and nb_keys - 1).
+ * 1 belongs to [62, 3]
+ * 1 does not belong to [3, 62]
+ * 63 belongs to [62, 3]
+ * 63 does not belong to [3, 62]
+ * 24 belongs to [21, 29]
+ * 24 does not belong to [29, 21]
+ *
+ * \param id id to check
+ * \param start lower bound
+ * \param end upper bound
+ * \return a non-zero value if id in in [start, end]
+ */
+static int is_in_interval(int id, int start, int end)
+{
+ id = normalize(id);
+ start = normalize(start);
+ end = normalize(end);
+
+ // make sure end >= start and id >= start
+ if (end < start) {
+ end += nb_keys;
+ }
+
+ if (id < start) {
+ id += nb_keys;
+ }
+
+ return id <= end;
+}
+
+/**
+ * \brief Gets the mailbox name of a host given its chord id.
+ * \param node_id id of a node
+ * \param mailbox pointer to where the mailbox name should be written
+ * (there must be enough space)
+ */
+static void get_mailbox(int node_id, char* mailbox)
+{
+ snprintf(mailbox, MAILBOX_NAME_SIZE - 1, "%d", node_id);
+}
+
+/**
+ * \brief Frees the memory used by a task.
+ * \param task the MSG task to destroy
+ */
+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);
+ task = NULL;
+}
+
+/**
+ * \brief Displays the finger table of a node.
+ * \param node a node
+ */
+static void print_finger_table(node_t node)
+{
+ if (XBT_LOG_ISENABLED(chord_liveness, xbt_log_priority_verbose)) {
+ int i;
+ XBT_VERB("My finger table:");
+ XBT_VERB("Start | Succ ");
+ for (i = 0; i < nb_bits; i++) {
+ XBT_VERB(" %3d | %3d ", (node->id + powers2[i]) % nb_keys, node->fingers[i].id);
+ }
+ XBT_VERB("Predecessor: %d", node->pred_id);
+ }
+}
+
+/**
+ * \brief Sets a finger of the current node.
+ * \param node the current node
+ * \param finger_index index of the finger to set (0 to nb_bits - 1)
+ * \param id the id to set for this finger
+ */
+static void set_finger(node_t node, int finger_index, int id)
+{
+ if (id != node->fingers[finger_index].id) {
+ node->fingers[finger_index].id = id;
+ get_mailbox(id, node->fingers[finger_index].mailbox);
+ node->last_change_date = MSG_get_clock();
+ XBT_DEBUG("My new finger #%d is %d", finger_index, id);
+ }
+}
+
+/**
+ * \brief Sets the predecessor of the current node.
+ * \param node the current node
+ * \param id the id to predecessor, or -1 to unset the predecessor
+ */
+static void set_predecessor(node_t node, int predecessor_id)
+{
+ if (predecessor_id != node->pred_id) {
+ node->pred_id = predecessor_id;
+
+ if (predecessor_id != -1) {
+ get_mailbox(predecessor_id, node->pred_mailbox);
+ }
+ node->last_change_date = MSG_get_clock();
+
+ XBT_DEBUG("My new predecessor is %d", predecessor_id);
+ }
+}
+
+/**
+ * \brief Node Function
+ * Arguments:
+ * - my id
+ * - the id of a guy I know in the system (except for the first node)
+ * - the time to sleep before I join (except for the first node)
+ */
+int node(int argc, char *argv[])
+{
+ /* Reduce the run size for the MC */
+ if(MC_is_active()){
+ periodic_stabilize_delay = 8;
+ periodic_fix_fingers_delay = 8;
+ periodic_check_predecessor_delay = 8;
+ }
+
+ double init_time = MSG_get_clock();
+ msg_task_t task_received = NULL;
+ int i;
+ int join_success = 0;
+ double deadline;
+ double next_stabilize_date = init_time + periodic_stabilize_delay;
+ double next_fix_fingers_date = init_time + periodic_fix_fingers_delay;
+ double next_check_predecessor_date = init_time + periodic_check_predecessor_delay;
+ double next_lookup_date = init_time + periodic_lookup_delay;
+
+ xbt_assert(argc == 3 || argc == 5, "Wrong number of arguments for this node");
+
+ // initialize my node
+ s_node_t node = {0};
+ node.id = atoi(argv[1]);
+ get_mailbox(node.id, node.mailbox);
+ node.next_finger_to_fix = 0;
+ node.fingers = xbt_new0(s_finger_t, nb_bits);
+ node.last_change_date = init_time;
+
+ for (i = 0; i < nb_bits; i++) {
+ node.fingers[i].id = -1;
+ set_finger(&node, i, node.id);
+ }
+
+ if (argc == 3) { // first ring
+ deadline = atof(argv[2]);
+ create(&node);
+ join_success = 1;
+ }
+ else {
+ int known_id = atoi(argv[2]);
+ //double sleep_time = atof(argv[3]);
+ deadline = atof(argv[4]);
+
+ /*
+ // sleep before starting
+ XBT_DEBUG("Let's sleep during %f", sleep_time);
+ MSG_process_sleep(sleep_time);
+ */
+ XBT_DEBUG("Hey! Let's join the system.");
+
+ join_success = join(&node, known_id);
+
+ if(join_success){
+ XBT_INFO("Node %d joined the ring", node.id);
+ node_join = 1;
+ //MC_compare();
+ }
+ }
+
+ if (join_success) {
+
+ while (MSG_get_clock() < init_time + deadline
+// && MSG_get_clock() < node.last_change_date + 1000
+ && MSG_get_clock() < max_simulation_time) {
+
+ if (node.comm_receive == NULL) {
+ task_received = NULL;
+ node.comm_receive = MSG_task_irecv(&task_received, node.mailbox);
+ // FIXME: do not make MSG_task_irecv() calls from several functions
+ }
+
+ 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);
+ }
+ }else{
+
+ if (node.comm_receive) {
+
+ XBT_INFO("A transfer has occured");
+
+ //MC_compare();
+
+ // a transfer has occured
+
+ msg_error_t status = MSG_comm_get_status(node.comm_receive);
+
+ if (status != MSG_OK) {
+ XBT_INFO("Failed to receive a task. Nevermind.");
+ MSG_comm_destroy(node.comm_receive);
+ node.comm_receive = NULL;
+ }
+ else {
+ // the task was successfully received
+ XBT_INFO("The task was successfully received by node %d", node.id);
+ MSG_comm_destroy(node.comm_receive);
+ node.comm_receive = NULL;
+ handle_task(&node, task_received);
+ }
+ }
+ }
+ }
+
+ if (node.comm_receive) {
+ MSG_comm_destroy(node.comm_receive);
+ node.comm_receive = NULL;
+ }
+
+ // leave the ring
+ leave(&node);
+ }
+
+ // stop the simulation
+ xbt_free(node.fingers);
+ return 0;
+}
+
+/**
+ * \brief This function is called when the current node receives a task.
+ * \param node the current node
+ * \param task the task to handle (don't touch it then:
+ * it will be destroyed, reused or forwarded)
+ */
+static void handle_task(node_t node, msg_task_t task) {
+
+ XBT_DEBUG("Handling task %p", task);
+ 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;
+
+ switch (type) {
+
+ case TASK_FIND_SUCCESSOR:
+ XBT_DEBUG("Receiving a 'Find Successor' request from %s for id %d",
+ task_data->issuer_host_name, task_data->request_id);
+ // is my successor the successor?
+ 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;
+ XBT_DEBUG("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);
+ MSG_task_dsend(task, task_data->answer_to, task_free);
+ }
+ else {
+ // otherwise, forward the request to the closest preceding finger in my table
+ int closest = closest_preceding_node(node, task_data->request_id);
+ XBT_DEBUG("Forwarding the 'Find Successor' request for id %d to my closest preceding finger %d",
+ task_data->request_id, closest);
+ get_mailbox(closest, mailbox);
+ MSG_task_dsend(task, mailbox, task_free);
+ }
+ break;
+
+ case TASK_GET_PREDECESSOR:
+ XBT_DEBUG("Receiving a 'Get Predecessor' request from %s", task_data->issuer_host_name);
+ task_data->type = TASK_GET_PREDECESSOR_ANSWER;
+ task_data->answer_id = node->pred_id;
+ XBT_DEBUG("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);
+ MSG_task_dsend(task, task_data->answer_to, task_free);
+ break;
+
+ case TASK_NOTIFY:
+ // someone is telling me that he may be my new predecessor
+ XBT_DEBUG("Receiving a 'Notify' request from %s", task_data->issuer_host_name);
+ notify(node, task_data->request_id);
+ task_free(task);
+ break;
+
+ case TASK_PREDECESSOR_LEAVING:
+ // my predecessor is about to quit
+ XBT_DEBUG("Receiving a 'Predecessor Leaving' message from %s", task_data->issuer_host_name);
+ // modify my predecessor
+ set_predecessor(node, task_data->request_id);
+ task_free(task);
+ /*TODO :
+ >> notify my new predecessor
+ >> send a notify_predecessors !!
+ */
+ break;
+
+ case TASK_SUCCESSOR_LEAVING:
+ // my successor is about to quit
+ XBT_DEBUG("Receiving a 'Successor Leaving' message from %s", task_data->issuer_host_name);
+ // modify my successor FIXME : this should be implicit ?
+ set_finger(node, 0, task_data->request_id);
+ task_free(task);
+ /* TODO
+ >> notify my new successor
+ >> update my table & predecessors table */
+ break;
+
+ case TASK_FIND_SUCCESSOR_ANSWER:
+ case TASK_GET_PREDECESSOR_ANSWER:
+ XBT_DEBUG("Ignoring unexpected task of type %d (%p)", (int)type, task);
+ task_free(task);
+ break;
+ }
+}
+
+/**
+ * \brief Initializes the current node as the first one of the system.
+ * \param node the current node
+ */
+static void create(node_t node)
+{
+ XBT_DEBUG("Create a new Chord ring...");
+ set_predecessor(node, -1); // -1 means that I have no predecessor
+ print_finger_table(node);
+}
+
+/**
+ * \brief Makes the current node join the ring, knowing the id of a node
+ * already in the ring
+ * \param node the current node
+ * \param known_id id of a node already in the ring
+ * \return 1 if the join operation succeeded, 0 otherwise
+ */
+static int join(node_t node, int known_id)
+{
+ XBT_INFO("Joining the ring with id %d, knowing node %d", node->id, known_id);
+ set_predecessor(node, -1); // no predecessor (yet)
+
+ /*
+ int i;
+ for (i = 0; i < nb_bits; i++) {
+ set_finger(node, i, known_id);
+ }
+ */
+
+ int successor_id = remote_find_successor(node, known_id, node->id);
+ if (successor_id == -1) {
+ XBT_INFO("Cannot join the ring.");
+ }
+ else {
+ set_finger(node, 0, successor_id);
+ print_finger_table(node);
+ }
+
+ return successor_id != -1;
+}
+
+/**
+ * \brief Makes the current node quit the system
+ * \param node the current node
+ */
+static void leave(node_t node)
+{
+ XBT_DEBUG("Well Guys! I Think it's time for me to quit ;)");
+ quit_notify(node);
+}
+
+/*
+ * \brief Notifies the successor and the predecessor of the current node
+ * of the departure
+ * \param node the current node
+ */
+static void quit_notify(node_t node)
+{
+ char mailbox[MAILBOX_NAME_SIZE];
+ //send the PREDECESSOR_LEAVING to our successor
+ task_data_t req_data = xbt_new0(s_task_data_t,1);
+ req_data->type = TASK_PREDECESSOR_LEAVING;
+ req_data->request_id = node->pred_id;
+ get_mailbox(node->id, req_data->answer_to);
+ req_data->issuer_host_name = MSG_host_get_name(MSG_host_self());
+
+ msg_task_t task_sent = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data);
+ XBT_DEBUG("Sending a 'PREDECESSOR_LEAVING' to my successor %d",node->fingers[0].id);
+ MSG_task_send_with_timeout(task_sent, node->fingers[0].mailbox, timeout);
+
+ //send the SUCCESSOR_LEAVING to our predecessor
+ get_mailbox(node->pred_id, mailbox);
+ task_data_t req_data_s = xbt_new0(s_task_data_t,1);
+ req_data_s->type = TASK_SUCCESSOR_LEAVING;
+ req_data_s->request_id = node->fingers[0].id;
+ req_data_s->request_id = node->pred_id;
+ get_mailbox(node->id, req_data_s->answer_to);
+ req_data_s->issuer_host_name = MSG_host_get_name(MSG_host_self());
+
+ msg_task_t task_sent_s = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data_s);
+ XBT_DEBUG("Sending a 'SUCCESSOR_LEAVING' to my predecessor %d",node->pred_id);
+ MSG_task_send_with_timeout(task_sent_s, mailbox, timeout);
+
+}
+
+/**
+ * \brief Makes the current node find the successor node of an id.
+ * \param node the current node
+ * \param id the id to find
+ * \return the id of the successor node, or -1 if the request failed
+ */
+static int find_successor(node_t node, int id)
+{
+ // is my successor the successor?
+ if (is_in_interval(id, node->id + 1, node->fingers[0].id)) {
+ return node->fingers[0].id;
+ }
+
+ // otherwise, ask the closest preceding finger in my table
+ int closest = closest_preceding_node(node, id);
+ return remote_find_successor(node, closest, id);
+}
+
+/**
+ * \brief Asks another node the successor node of an id.
+ * \param node the current node
+ * \param ask_to the node to ask to
+ * \param id the id to find
+ * \return the id of the successor node, or -1 if the request failed
+ */
+static int remote_find_successor(node_t node, int ask_to, int id)
+{
+ int successor = -1;
+ int stop = 0;
+ char mailbox[MAILBOX_NAME_SIZE];
+ get_mailbox(ask_to, mailbox);
+ task_data_t req_data = xbt_new0(s_task_data_t, 1);
+ req_data->type = TASK_FIND_SUCCESSOR;
+ req_data->request_id = id;
+ get_mailbox(node->id, req_data->answer_to);
+ req_data->issuer_host_name = MSG_host_get_name(MSG_host_self());
+
+ // send a "Find Successor" request to ask_to_id
+ msg_task_t task_sent = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data);
+ XBT_DEBUG("Sending a 'Find Successor' request (task %p) to %d for id %d", task_sent, ask_to, id);
+ msg_error_t res = MSG_task_send_with_timeout(task_sent, mailbox, timeout);
+
+ if (res != MSG_OK) {
+ XBT_DEBUG("Failed to send the 'Find Successor' request (task %p) to %d for id %d",
+ task_sent, ask_to, id);
+ task_free(task_sent);
+ }
+ else {
+
+ // receive the answer
+ XBT_DEBUG("Sent a 'Find Successor' request (task %p) to %d for key %d, waiting for the answer",
+ task_sent, ask_to, id);
+
+ do {
+ if (node->comm_receive == NULL) {
+ msg_task_t task_received = NULL;
+ node->comm_receive = MSG_task_irecv(&task_received, node->mailbox);
+ }
+
+ res = MSG_comm_wait(node->comm_receive, timeout);
+
+ if (res != MSG_OK) {
+ XBT_DEBUG("Failed to receive the answer to my 'Find Successor' request (task %p): %d",
+ task_sent, (int)res);
+ stop = 1;
+ MSG_comm_destroy(node->comm_receive);
+ node->comm_receive = NULL;
+ }
+ else {
+ msg_task_t task_received = MSG_comm_get_task(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_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);
+ }
+
+ 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 {
+ // this is our answer
+ XBT_DEBUG("Received the answer to my 'Find Successor' request for id %d (task %p): the successor of key %d is %d",
+ 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;
+ task_free(task_received);
+ }
+ }
+ } while (!stop);
+ }
+
+ return successor;
+}
+
+/**
+ * \brief Asks another node its predecessor.
+ * \param node the current node
+ * \param ask_to the node to ask to
+ * \return the id of its predecessor node, or -1 if the request failed
+ * (or if the node does not know its predecessor)
+ */
+static int remote_get_predecessor(node_t node, int ask_to)
+{
+ int predecessor_id = -1;
+ int stop = 0;
+ char mailbox[MAILBOX_NAME_SIZE];
+ get_mailbox(ask_to, mailbox);
+ task_data_t req_data = xbt_new0(s_task_data_t, 1);
+ req_data->type = TASK_GET_PREDECESSOR;
+ get_mailbox(node->id, req_data->answer_to);
+ req_data->issuer_host_name = MSG_host_get_name(MSG_host_self());
+
+ // send a "Get Predecessor" request to ask_to_id
+ XBT_DEBUG("Sending a 'Get Predecessor' request to %d", ask_to);
+ msg_task_t task_sent = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data);
+ msg_error_t res = MSG_task_send_with_timeout(task_sent, mailbox, timeout);
+
+ if (res != MSG_OK) {
+ XBT_DEBUG("Failed to send the 'Get Predecessor' request (task %p) to %d",
+ task_sent, ask_to);
+ task_free(task_sent);
+ }
+ else {
+
+ // receive the answer
+ XBT_DEBUG("Sent 'Get Predecessor' request (task %p) to %d, waiting for the answer on my mailbox '%s'",
+ task_sent, ask_to, req_data->answer_to);
+
+ do {
+ if (node->comm_receive == NULL) { // FIXME simplify this
+ msg_task_t task_received = NULL;
+ node->comm_receive = MSG_task_irecv(&task_received, node->mailbox);
+ }
+
+ res = MSG_comm_wait(node->comm_receive, timeout);
+
+ if (res != MSG_OK) {
+ XBT_DEBUG("Failed to receive the answer to my 'Get Predecessor' request (task %p): %d",
+ task_sent, (int)res);
+ stop = 1;
+ MSG_comm_destroy(node->comm_receive);
+ node->comm_receive = NULL;
+ }
+ else {
+ 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_active()) {
+ 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 {
+ XBT_DEBUG("Received the answer to my 'Get Predecessor' request (task %p): the predecessor of node %d is %d",
+ 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;
+ task_free(task_received);
+ }
+ }
+ } while (!stop);
+ }
+
+ return predecessor_id;
+}
+
+/**
+ * \brief Returns the closest preceding finger of an id
+ * with respect to the finger table of the current node.
+ * \param node the current node
+ * \param id the id to find
+ * \return the closest preceding finger of that id
+ */
+int closest_preceding_node(node_t node, int id)
+{
+ int i;
+ for (i = nb_bits - 1; i >= 0; i--) {
+ if (is_in_interval(node->fingers[i].id, node->id + 1, id - 1)) {
+ return node->fingers[i].id;
+ }
+ }
+ return node->id;
+}
+
+/**
+ * \brief This function is called periodically. It checks the immediate
+ * successor of the current node.
+ * \param node the current node
+ */
+static void stabilize(node_t node)
+{
+ XBT_DEBUG("Stabilizing node");
+
+ // get the predecessor of my immediate successor
+ int candidate_id;
+ int successor_id = node->fingers[0].id;
+ if (successor_id != node->id) {
+ candidate_id = remote_get_predecessor(node, successor_id);
+ }
+ else {
+ candidate_id = node->pred_id;
+ }
+
+ // this node is a candidate to become my new successor
+ if (candidate_id != -1
+ && is_in_interval(candidate_id, node->id + 1, successor_id - 1)) {
+ set_finger(node, 0, candidate_id);
+ }
+ if (successor_id != node->id) {
+ remote_notify(node, successor_id, node->id);
+ }
+}
+
+/**
+ * \brief Notifies the current node that its predecessor may have changed.
+ * \param node the current node
+ * \param candidate_id the possible new predecessor
+ */
+static void notify(node_t node, int predecessor_candidate_id) {
+
+ if (node->pred_id == -1
+ || is_in_interval(predecessor_candidate_id, node->pred_id + 1, node->id - 1)) {
+
+ set_predecessor(node, predecessor_candidate_id);
+ print_finger_table(node);
+ }
+ else {
+ XBT_DEBUG("I don't have to change my predecessor to %d", predecessor_candidate_id);
+ }
+}
+
+/**
+ * \brief Notifies a remote node that its predecessor may have changed.
+ * \param node the current node
+ * \param notify_id id of the node to notify
+ * \param candidate_id the possible new predecessor
+ */
+static void remote_notify(node_t node, int notify_id, int predecessor_candidate_id) {
+
+ task_data_t req_data = xbt_new0(s_task_data_t, 1);
+ req_data->type = TASK_NOTIFY;
+ req_data->request_id = predecessor_candidate_id;
+ req_data->issuer_host_name = MSG_host_get_name(MSG_host_self());
+
+ // send a "Notify" request to notify_id
+ msg_task_t task = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data);
+ XBT_DEBUG("Sending a 'Notify' request (task %p) to %d", task, notify_id);
+ char mailbox[MAILBOX_NAME_SIZE];
+ get_mailbox(notify_id, mailbox);
+ MSG_task_dsend(task, mailbox, task_free);
+ }
+
+/**
+ * \brief This function is called periodically.
+ * It refreshes the finger table of the current node.
+ * \param node the current node
+ */
+static void fix_fingers(node_t node) {
+
+ XBT_DEBUG("Fixing fingers");
+ int i = node->next_finger_to_fix;
+ int id = find_successor(node, node->id + powers2[i]);
+ if (id != -1) {
+
+ if (id != node->fingers[i].id) {
+ set_finger(node, i, id);
+ print_finger_table(node);
+ }
+ node->next_finger_to_fix = (i + 1) % nb_bits;
+ }
+}
+
+/**
+ * \brief This function is called periodically.
+ * It checks whether the predecessor has failed
+ * \param node the current node
+ */
+static void check_predecessor(node_t node)
+{
+ XBT_DEBUG("Checking whether my predecessor is alive");
+ // TODO
+}
+
+/**
+ * \brief Performs a find successor request to a random id.
+ * \param node the current node
+ */
+static void random_lookup(node_t node)
+{
+ int id = 1337; // TODO pick a pseudorandom id
+ XBT_DEBUG("Making a lookup request for id %d", id);
+ find_successor(node, id);
+}
+
+int predJoin(void){
+ return node_join;
+}
+
+
+/**
+ * \brief Main function.
+ */
+int main(int argc, char *argv[])
+{
+ MSG_init(&argc, argv);
+ /*if (argc < 3) {
+ printf("Usage: %s [-nb_bits=n] [-timeout=t] platform_file deployment_file\n", argv[0]);
+ printf("example: %s ../msg_platform.xml chord.xml\n", argv[0]);
+ exit(1);
+ }*/
+
+ char **options = &argv[0];
+ while (!strncmp(options[0], "-", 1)) {
+
+ int length = strlen("-nb_bits=");
+ if (!strncmp(options[0], "-nb_bits=", length) && strlen(options[0]) > length) {
+ nb_bits = atoi(options[0] + length);
+ XBT_DEBUG("Set nb_bits to %d", nb_bits);
+ }
+ else {
+
+ length = strlen("-timeout=");
+ if (!strncmp(options[0], "-timeout=", length) && strlen(options[0]) > length) {
+ timeout = atoi(options[0] + length);
+ XBT_DEBUG("Set timeout to %d", timeout);
+ }
+ else {
+ xbt_die("Invalid chord option '%s'", options[0]);
+ }
+ }
+ options++;
+ }
+
+ //const char* platform_file = options[0];
+ //const char* application_file = options[1];
+
+ chord_initialize();
+
+ MSG_config("model-check/property","promela_chord_liveness");
+ MC_automaton_new_propositional_symbol("join", &predJoin);
+
+ MSG_create_environment("../msg_platform.xml");
+
+ MSG_function_register("node", node);
+ MSG_launch_application("deploy_chord_liveness.xml");
+
+ msg_error_t res = MSG_main();
+ //XBT_CRITICAL("Messages created: %ld", smx_total_comms);
+ XBT_INFO("Simulated time: %g", MSG_get_clock());
+
+ chord_exit();
+
+ if (res == MSG_OK)
+ return 0;
+ else
+ return 1;
+}
--- /dev/null
+#ifndef _CHORD_LIVENESS_H
+#define _CHORD_LIVENESS_H
+
+int predJoin(void);
+
+#endif
--- /dev/null
+<?xml version='1.0'?>
+<!DOCTYPE platform SYSTEM "http://simgrid.gforge.inria.fr/simgrid.dtd">
+<platform version="3">
+
+ <process host="Jean_Yves" function="node">
+ <argument value="14"/> <!-- my id -->
+ <argument value="1"/> <!-- known id -->
+ <argument value="400"/> <!-- time to sleep before it starts-->
+ <argument value ="600"/> <!-- deadline -->
+ </process>
+
+ <process host="Boivin" function="node">
+ <argument value="8"/> <!-- my id -->
+ <argument value="1"/> <!-- known id -->
+ <argument value="300"/> <!-- time to sleep before it starts-->
+ <argument value ="600"/> <!-- deadline -->
+ </process>
+
+ <process host="Jacquelin" function="node">
+ <argument value="1"/> <!-- my id -->
+ <argument value ="600"/> <!-- deadline -->
+ </process>
+
+</platform>
--- /dev/null
+never { /* !(!(GFjoin)) */
+T0_init : /* init */
+ if
+ :: (join) -> goto accept_S1
+ :: (1) -> goto T0_init
+ fi;
+accept_S1 : /* 1 */
+ if
+ :: (join) -> goto accept_S1
+ :: (1) -> goto T0_init
+ fi;
+}
\ No newline at end of file
MSG_process_sleep(1);
char *toto = xbt_malloc(5);
- XBT_INFO("Toto value %s", toto);
+ XBT_INFO("Toto allocated");
void *snap2 = MC_snapshot();
XBT_INFO("**** End test ****");
+ xbt_free(toto);
+
return 0;
}
XBT_INFO("**** Start test ****");
XBT_INFO("Malloc and free after first snapshot");
+ char *toto = NULL;
+
void *snap1 = MC_snapshot();
MSG_process_sleep(1);
- char *toto = NULL;
toto = xbt_malloc(5);
- XBT_INFO("Toto value %s", toto);
+ XBT_INFO("Toto allocated");
xbt_free(toto);
toto = NULL;
+ XBT_INFO("Toto free");
MSG_process_sleep(1);
void *snap2 = MC_snapshot();
- int res = MC_compare_snapshots(snap1, snap2);
+ MC_ignore_stack("snap2", "test");
+ MC_ignore_stack("snap1", "test");
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+ XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
XBT_INFO("**** End test ****");
XBT_INFO("Free after first snapshot");
char *toto = xbt_malloc(5);
- XBT_INFO("Toto value %s", toto);
+ XBT_INFO("Toto allocated");
void *snap1 = MC_snapshot();
MSG_process_sleep(1);
xbt_free(toto);
+ XBT_INFO("Toto free");
void *snap2 = MC_snapshot();
MSG_process_sleep(1);
+
+ MC_ignore_stack("snap2", "test");
+ MC_ignore_stack("snap1", "test");
- int res = MC_compare_snapshots(snap1, snap2);
-
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+ XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
XBT_INFO("**** End test ****");
MSG_process_sleep(1);
- int res = MC_compare_snapshots(snap1, snap2);
+ MC_ignore_stack("snap2", "test");
+ MC_ignore_stack("snap1", "test");
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+ XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
XBT_INFO("**** End test ****");
int is_free_area(void *area, xbt_mheap_t heap);
+size_t mmalloc_get_chunks_used(xbt_mheap_t);
+
#endif /* MMALLOC_H */
/*********** Structures for snapshot comparison **************************/
-typedef struct s_mc_ignore_region{
+typedef struct s_mc_heap_ignore_region{
int block;
int fragment;
void *address;
size_t size;
-}s_mc_ignore_region_t, *mc_ignore_region_t;
+}s_mc_heap_ignore_region_t, *mc_heap_ignore_region_t;
+
+typedef struct s_mc_stack_ignore_variable{
+ char *var_name;
+ char *frame;
+}s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
+
+typedef struct s_mc_data_bss_ignore_variable{
+ void *address;
+ size_t size;
+}s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
typedef struct s_stack_region{
void *address;
extern char*_surf_mc_property_file; /* fixme: better location? */
-extern xbt_dynar_t mc_comparison_ignore;
+extern xbt_dynar_t mc_heap_comparison_ignore;
extern xbt_dynar_t stacks_areas;
/********************************* Global *************************************/
void _mc_cfg_cb_reduce(const char *name, int pos);
void _mc_cfg_cb_checkpoint(const char *name, int pos);
void _mc_cfg_cb_property(const char *name, int pos);
+void _mc_cfg_cb_timeout(const char *name, int pos);
XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
void MC_automaton_load(const char *file);
-XBT_PUBLIC(void) MC_ignore(void *address, size_t size);
-void MC_new_stack_area(void *stack, char *name, void *context);
+/****************************** MC ignore **********************************/
+XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size);
+XBT_PUBLIC(void) MC_ignore_stack(const char *var_name, const char *frame);
+XBT_PUBLIC(void) MC_ignore_data_bss(void *address, size_t size);
+void MC_new_stack_area(void *stack, char *name, void *context, size_t size);
/********************************* Memory *************************************/
XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */
XBT_PUBLIC(void) MC_memory_exit(void);
-/********************************* Snapshot comparison test *************************************/
-void MC_test_heap_comparison(void);
-
/* Trigger for state equality detection (check potential cycle in application) */
void MC_compare(void);
void *start_plt_libsimgrid, *end_plt_libsimgrid;
void *start_plt_binary, *end_plt_binary;
char *libsimgrid_path;
-void *start_data_libsimgrid;
+void *start_data_libsimgrid, *start_bss_libsimgrid;
+void *start_data_binary, *start_bss_binary;
void *start_text_binary;
void *end_raw_heap;
} else {
if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
start_data_libsimgrid = reg.start_addr;
+ i++;
+ reg = maps->regions[i];
+ if(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize)
+ start_bss_libsimgrid = reg.start_addr;
+ }else if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
+ start_data_binary = reg.start_addr;
+ i++;
+ reg = maps->regions[i];
+ if(reg.pathname == NULL && (reg.prot & PROT_WRITE) && reg.start_addr != std_heap && reg.start_addr != raw_heap && i < maps->mapsize){
+ start_bss_binary = reg.start_addr;
+ i++;
+ }
}
}
}else if ((reg.prot & PROT_READ)){
nb_reg++;
i++;
reg = maps->regions[i];
- while(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize){
+ if(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize){
MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
- i++;
reg = maps->regions[i];
+ i++;
nb_reg++;
}
} else {
if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
nb_reg++;
+ i++;
+ reg = maps->regions[i];
+ if(reg.pathname == NULL && (reg.prot & PROT_WRITE) && reg.start_addr != std_heap && reg.start_addr != raw_heap && i < maps->mapsize){
+ MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
+ reg = maps->regions[i];
+ nb_reg++;
+ }
+ }else{
+ i++;
}
- i++;
}
}
}else if ((reg.prot & PROT_READ)){
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
"Logging specific to mc_compare");
-static int data_program_region_compare(void *d1, void *d2, size_t size);
-static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size);
+static int data_bss_program_region_compare(void *d1, void *d2, size_t size);
+static int data_bss_libsimgrid_region_compare(void *d1, void *d2, size_t size);
static int heap_region_compare(void *d1, void *d2, size_t size);
static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *sp2, void *heap1, void *heap2, xbt_dynar_t equals);
static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2);
-static size_t ignore(void *address);
+static size_t heap_ignore_size(void *address);
+static size_t data_bss_ignore_size(void *address);
static void stack_region_free(stack_region_t s);
static void heap_equality_free(heap_equality_t e);
+static int is_stack_ignore_variable(char *frame, char *var_name);
static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals);
-static size_t ignore(void *address){
+static size_t heap_ignore_size(void *address){
unsigned int cursor = 0;
int start = 0;
- int end = xbt_dynar_length(mc_comparison_ignore) - 1;
- mc_ignore_region_t region;
+ int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+ mc_heap_ignore_region_t region;
while(start <= end){
cursor = (start + end) / 2;
- region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t);
+ region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
if(region->address == address)
return region->size;
if(region->address < address)
return 0;
}
-static int data_program_region_compare(void *d1, void *d2, size_t size){
- int distance = 0;
+static size_t data_bss_ignore_size(void *address){
+ unsigned int cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
+ mc_data_bss_ignore_variable_t var;
+
+ while(start <= end){
+ cursor = (start + end) / 2;
+ var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
+ if(var->address == address)
+ return var->size;
+ if(var->address < address)
+ start = cursor + 1;
+ if(var->address > address)
+ end = cursor - 1;
+ }
+
+ return 0;
+}
+
+static int data_bss_program_region_compare(void *d1, void *d2, size_t size){
+
size_t i = 0;
int pointer_align;
void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
if((addr_pointed1 > start_plt_binary && addr_pointed1 < end_plt_binary) || (addr_pointed2 > start_plt_binary && addr_pointed2 < end_plt_binary)){
continue;
}else{
- XBT_DEBUG("Different byte (offset=%zu) (%p - %p) in data program region", i, (char *)d1 + i, (char *)d2 + i);
- distance++;
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)){
+ XBT_VERB("Different byte (offset=%zu) (%p - %p) in data program region", i, (char *)d1 + i, (char *)d2 + i);
+ XBT_VERB("Addresses pointed : %p - %p\n", addr_pointed1, addr_pointed2);
+ }
+ return 1;
}
}
}
- XBT_INFO("Hamming distance between data program regions : %d", distance);
-
- return distance;
+ return 0;
}
-static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
- int distance = 0;
+static int data_bss_libsimgrid_region_compare(void *d1, void *d2, size_t size){
+
size_t i = 0, ignore_size = 0;
int pointer_align;
void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
for(i=0; i<size; i++){
if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
- if((ignore_size = ignore((char *)start_data_libsimgrid+i)) > 0){
+ if((ignore_size = data_bss_ignore_size((char *)start_data_libsimgrid+i)) > 0){
+ i = i + ignore_size;
+ continue;
+ }else if((ignore_size = data_bss_ignore_size((char *)start_bss_libsimgrid+i)) > 0){
i = i + ignore_size;
continue;
}
}else if(addr_pointed1 >= raw_heap && addr_pointed1 <= end_raw_heap && addr_pointed2 >= raw_heap && addr_pointed2 <= end_raw_heap){
continue;
}else{
- XBT_DEBUG("Different byte (offset=%zu) (%p - %p) in data libsimgrid region", i, (char *)d1 + i, (char *)d2 + i);
- XBT_DEBUG("Addresses pointed : %p - %p\n", addr_pointed1, addr_pointed2);
- distance++;
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)){
+ XBT_VERB("Different byte (offset=%zu) (%p - %p) in libsimgrid region", i, (char *)d1 + i, (char *)d2 + i);
+ XBT_VERB("Addresses pointed : %p - %p\n", addr_pointed1, addr_pointed2);
+ }
+ return 1;
}
}
}
- XBT_INFO("Hamming distance between data libsimgrid regions : %d", distance); fflush(NULL);
-
- return distance;
+ return 0;
}
static int heap_region_compare(void *d1, void *d2, size_t size){
- int distance = 0;
size_t i = 0;
for(i=0; i<size; i++){
if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
- XBT_DEBUG("Different byte (offset=%zu) (%p - %p) in heap region", i, (char *)d1 + i, (char *)d2 + i);
- distance++;
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)){
+ XBT_VERB("Different byte (offset=%zu) (%p - %p) in heap region", i, (char *)d1 + i, (char *)d2 + i);
+ }
+ return 1;
}
}
- XBT_INFO("Hamming distance between heap regions : %d (total size : %zu)", distance, size);
-
- return distance;
+ return 0;
}
static void stack_region_free(stack_region_t s){
MC_SET_RAW_MEM;
- int errors = 0, i;
- xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
- xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
- xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp);
+ int errors = 0, i = 0;
- void *heap1 = NULL, *heap2 = NULL;
-
if(s1->num_reg != s2->num_reg){
- XBT_DEBUG("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg);
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)){
+ XBT_VERB("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg);
+ }
return 1;
}
- for(i=0 ; i< s1->num_reg ; i++){
-
- if(s1->regions[i]->type != s2->regions[i]->type){
- XBT_DEBUG("Different type of region");
- errors++;
- }
-
+ int heap_index = 0, data_libsimgrid_index = 0, data_program_index = 0;
+
+ /* Get index of regions */
+ while(i < s1->num_reg){
switch(s1->regions[i]->type){
- case 0 :
- /* Compare heapregion */
- if(s1->regions[i]->size != s2->regions[i]->size){
- XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return 1;
- }
- if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return 1;
- }
- if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[i]->data, (xbt_mheap_t)s2->regions[i]->data, &stacks1, &stacks2, &equals)){
- XBT_INFO("Different heap (mmalloc_compare)");
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return 1;
- }
- heap1 = s1->regions[i]->data;
- heap2 = s2->regions[i]->data;
+ case 0:
+ heap_index = i;
+ i++;
break;
- case 1 :
- /* Compare data libsimgrid region */
- if(s1->regions[i]->size != s2->regions[i]->size){
- XBT_DEBUG("Different size of libsimgrid (data) (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return 1;
- }
- if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- XBT_DEBUG("Different start addr of libsimgrid (data) (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return 1;
- }
- if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
- XBT_INFO("Different memcmp for data in libsimgrid");
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return 1;
- }
+ case 1:
+ data_libsimgrid_index = i;
+ i++;
+ while( i < s1->num_reg && s1->regions[i]->type == 1)
+ i++;
break;
+ case 2:
+ data_program_index = i;
+ i++;
+ while( i < s1->num_reg && s1->regions[i]->type == 2)
+ i++;
+ break;
+ }
+ }
+
+ xbt_os_timer_t global_timer = xbt_os_timer_new();
+ xbt_os_timer_t timer = xbt_os_timer_new();
+
+ xbt_os_timer_start(global_timer);
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
+ xbt_os_timer_start(timer);
+
+ /* Compare number of blocks/fragments used in each heap */
+ size_t chunks_used1 = mmalloc_get_chunks_used((xbt_mheap_t)s1->regions[heap_index]->data);
+ size_t chunks_used2 = mmalloc_get_chunks_used((xbt_mheap_t)s2->regions[heap_index]->data);
+ if(chunks_used1 != chunks_used2){
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ XBT_DEBUG("Different number of chunks used in each heap : %zu - %zu", chunks_used1, chunks_used2);
+ errors++;
+ }else{
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ XBT_VERB("Different number of chunks used in each heap : %zu - %zu", chunks_used1, chunks_used2);
+
+ xbt_os_timer_free(timer);
+ xbt_os_timer_stop(global_timer);
+ xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+ xbt_os_timer_free(global_timer);
+
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
+
+ return 1;
+ }
+ }
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ xbt_os_timer_stop(timer);
+ xbt_dynar_push_as(initial_state_liveness->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+ XBT_DEBUG("Chunks used comparison : %f", xbt_os_timer_elapsed(timer));
+
+ xbt_os_timer_start(timer);
+ }
+
+ /* Compare size of stacks */
+ unsigned int cursor = 0;
+ void *addr_stack1, *addr_stack2;
+ void *sp1, *sp2;
+ size_t size_used1, size_used2;
+ while(cursor < xbt_dynar_length(stacks_areas)){
+ addr_stack1 = (char *)s1->regions[heap_index]->data + ((char *)((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->address - (char *)std_heap);
+ addr_stack2 = (char *)s2->regions[heap_index]->data + ((char *)((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->address - (char *)std_heap);
+ sp1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->stack_pointer;
+ sp2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->stack_pointer;
+ size_used1 = ((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->size - ((char*)sp1 - (char*)addr_stack1);
+ size_used2 = ((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->size - ((char*)sp2 - (char*)addr_stack2);
+ if(size_used1 != size_used2){
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ XBT_DEBUG("Different size used in stacks : %zu - %zu", size_used1, size_used2);
+ errors++;
+ }else{
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
+
+ xbt_os_timer_free(timer);
+ xbt_os_timer_stop(global_timer);
+ xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+ xbt_os_timer_free(global_timer);
- case 2 :
- /* Compare data program region */
- if(s1->regions[i]->size != s2->regions[i]->size){
- XBT_DEBUG("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
return 1;
}
- if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- XBT_DEBUG("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
+ }
+ cursor++;
+ }
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ xbt_os_timer_stop(timer);
+ xbt_dynar_push_as(initial_state_liveness->stacks_sizes_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+ XBT_DEBUG("Stacks sizes comparison : %f", xbt_os_timer_elapsed(timer));
+
+ xbt_os_timer_start(timer);
+ }
+
+ /* Compare program data segment(s) */
+ i = data_program_index;
+ while(i < s1->num_reg && s1->regions[i]->type == 2){
+ if(data_bss_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ XBT_DEBUG("Different memcmp for data in program");
+ errors++;
+ }else{
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ XBT_VERB("Different memcmp for data in program");
+
+ xbt_os_timer_free(timer);
+ xbt_os_timer_stop(global_timer);
+ xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+ xbt_os_timer_free(global_timer);
+
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
return 1;
}
- if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
- XBT_INFO("Different memcmp for data in program");
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
+ }
+ i++;
+ }
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ xbt_os_timer_stop(timer);
+ xbt_dynar_push_as(initial_state_liveness->program_data_segment_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+ XBT_DEBUG("Program data segment comparison : %f", xbt_os_timer_elapsed(timer));
+
+ xbt_os_timer_start(timer);
+ }
+
+ /* Compare libsimgrid data segment(s) */
+ i = data_libsimgrid_index;
+ while(i < s1->num_reg && s1->regions[i]->type == 1){
+ if(data_bss_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ XBT_DEBUG("Different memcmp for data in libsimgrid");
+ errors++;
+ }else{
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ XBT_VERB("Different memcmp for data in libsimgrid");
+
+ xbt_os_timer_free(timer);
+ xbt_os_timer_stop(global_timer);
+ xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+ xbt_os_timer_free(global_timer);
+
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
return 1;
}
- break;
-
}
+ i++;
+ }
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ xbt_os_timer_stop(timer);
+ xbt_dynar_push_as(initial_state_liveness->libsimgrid_data_segment_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+ XBT_DEBUG("Libsimgrid data segment comparison : %f", xbt_os_timer_elapsed(timer));
+
+ xbt_os_timer_start(timer);
+ }
+ /* Compare heap */
+ xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
+ xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
+ xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp);
+
+ void *heap1 = s1->regions[heap_index]->data, *heap2 = s2->regions[heap_index]->data;
+
+ if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[heap_index]->data, (xbt_mheap_t)s2->regions[heap_index]->data, &stacks1, &stacks2, &equals)){
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ XBT_DEBUG("Different heap (mmalloc_compare)");
+ errors++;
+ }else{
+
+ xbt_os_timer_free(timer);
+ xbt_dynar_free(&stacks1);
+ xbt_dynar_free(&stacks2);
+ xbt_dynar_free(&equals);
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ XBT_VERB("Different heap (mmalloc_compare)");
+
+ xbt_os_timer_stop(global_timer);
+ xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+ xbt_os_timer_free(global_timer);
+
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ }
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ xbt_os_timer_stop(timer);
+ xbt_dynar_push_as(initial_state_liveness->heap_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+ XBT_DEBUG("Heap comparison : %f", xbt_os_timer_elapsed(timer));
+
+ xbt_os_timer_start(timer);
}
/* Stacks comparison */
- unsigned int cursor = 0;
+ cursor = 0;
stack_region_t stack_region1, stack_region2;
- void *sp1, *sp2;
int diff = 0, diff_local = 0;
while(cursor < xbt_dynar_length(stacks1)){
- XBT_DEBUG("Stack %d", cursor + 1);
stack_region1 = (stack_region_t)(xbt_dynar_get_as(stacks1, cursor, stack_region_t));
stack_region2 = (stack_region_t)(xbt_dynar_get_as(stacks2, cursor, stack_region_t));
sp1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->stack_pointer;
sp2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->stack_pointer;
diff = compare_stack(stack_region1, stack_region2, sp1, sp2, heap1, heap2, equals);
- if(diff >0){
+ if(diff > 0){ /* Differences may be due to padding */
diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, equals);
if(diff_local > 0){
- XBT_INFO("Different local variables between stacks");
- xbt_dynar_free(&stacks1);
- xbt_dynar_free(&stacks2);
- xbt_dynar_free(&equals);
- if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
- return 1;
- }else{
- XBT_INFO("Local variables are equals in stack %d", cursor + 1);
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ XBT_DEBUG("Different local variables between stacks %d", cursor + 1);
+ errors++;
+ }else{
+ xbt_dynar_free(&stacks1);
+ xbt_dynar_free(&stacks2);
+ xbt_dynar_free(&equals);
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ XBT_VERB("Different local variables between stacks %d", cursor + 1);
+
+ xbt_os_timer_free(timer);
+ xbt_os_timer_stop(global_timer);
+ xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+ xbt_os_timer_free(global_timer);
+
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
+
+ return 1;
+ }
}
- }else{
- XBT_INFO("Hamming distance between stacks %d : %d", cursor + 1, diff);
}
cursor++;
}
xbt_dynar_free(&stacks1);
xbt_dynar_free(&stacks2);
xbt_dynar_free(&equals);
+
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+ xbt_os_timer_stop(timer);
+ xbt_dynar_push_as(initial_state_liveness->stacks_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+ XBT_DEBUG("Stacks comparison : %f", xbt_os_timer_elapsed(timer));
+
+ xbt_os_timer_free(timer);
+ }
+
+ xbt_os_timer_stop(global_timer);
+ xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+ xbt_os_timer_free(global_timer);
+
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
- return 0;
+
+ return errors > 0;
}
+static int is_stack_ignore_variable(char *frame, char *var_name){
+
+ unsigned int cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
+ mc_stack_ignore_variable_t current_var;
+
+ while(start <= end){
+ cursor = (start + end) / 2;
+ current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
+ if(strcmp(current_var->frame, frame) == 0){
+ if(strcmp(current_var->var_name, var_name) == 0)
+ return 1;
+ if(strcmp(current_var->var_name, var_name) < 0)
+ start = cursor + 1;
+ if(strcmp(current_var->var_name, var_name) > 0)
+ end = cursor - 1;
+ }
+ if(strcmp(current_var->frame, frame) < 0)
+ start = cursor + 1;
+ if(strcmp(current_var->frame, frame) > 0)
+ end = cursor - 1;
+ }
+
+ return 0;
+}
+
static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){
xbt_dynar_t tokens1 = xbt_str_split(s1, NULL);
xbt_dynar_t s_tokens1, s_tokens2;
unsigned int cursor = 0;
void *addr1, *addr2;
-
- int diff = 0;
+ char *ip1 = NULL, *ip2 = NULL;
while(cursor < xbt_dynar_length(tokens1)){
s_tokens1 = xbt_str_split(xbt_dynar_get_as(tokens1, cursor, char *), "=");
s_tokens2 = xbt_str_split(xbt_dynar_get_as(tokens2, cursor, char *), "=");
if(xbt_dynar_length(s_tokens1) > 1 && xbt_dynar_length(s_tokens2) > 1){
- if(strcmp(xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)) != 0){
+ if((strcmp(xbt_dynar_get_as(s_tokens1, 0, char *), "ip") == 0) && (strcmp(xbt_dynar_get_as(s_tokens2, 0, char *), "ip") == 0)){
+ ip1 = strdup(xbt_dynar_get_as(s_tokens1, 1, char *));
+ ip2 = strdup(xbt_dynar_get_as(s_tokens2, 1, char *));
+ /*if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ XBT_VERB("Instruction pointer : %s, Instruction pointer : %s", ip1, ip2);*/
+ }
+ if(strcmp(xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)) != 0){
+ /* Ignore this variable ? */
+ if(is_stack_ignore_variable(ip1, xbt_dynar_get_as(s_tokens1, 0, char *)) && is_stack_ignore_variable(ip2, xbt_dynar_get_as(s_tokens2, 0, char *))){
+ xbt_dynar_free(&s_tokens1);
+ xbt_dynar_free(&s_tokens2);
+ cursor++;
+ continue;
+ }
addr1 = (void *) strtoul(xbt_dynar_get_as(s_tokens1, 1, char *), NULL, 16);
addr2 = (void *) strtoul(xbt_dynar_get_as(s_tokens2, 1, char *), NULL, 16);
if(is_heap_equality(heap_equals, addr1, addr2) == 0){
- if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
- XBT_DEBUG("Variable %s is different between stacks : %s - %s", xbt_dynar_get_as(s_tokens1, 0, char *), xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
- else
- XBT_INFO("Variable %s is different between stacks", xbt_dynar_get_as(s_tokens1, 0, char *));
- diff++;
+ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+ XBT_VERB("Variable %s is different between stacks : %s - %s", xbt_dynar_get_as(s_tokens1, 0, char *), xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
+ xbt_dynar_free(&s_tokens1);
+ xbt_dynar_free(&s_tokens2);
+ return 1;
}
}
}
xbt_dynar_free(&tokens1);
xbt_dynar_free(&tokens2);
- return diff;
+ return 0;
}
static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *sp2, void *heap1, void *heap2, xbt_dynar_t equals){
- size_t k = 0, nb_diff = 0;
+ size_t k = 0;
size_t size_used1 = s1->size - ((char*)sp1 - (char*)s1->address);
size_t size_used2 = s2->size - ((char*)sp2 - (char*)s2->address);
int pointer_align;
void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
-
- if(size_used1 == size_used2){
-
- while(k < size_used1){
- if(memcmp((char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k, 1) != 0){
- pointer_align = ((size_used1 - k) / sizeof(void*)) * sizeof(void*);
- addr_pointed1 = *((void **)(((char*)s1->address + (s1->size - size_used1)) + pointer_align));
- addr_pointed2 = *((void **)(((char*)s2->address + (s2->size - size_used2)) + pointer_align));
- if(is_heap_equality(equals, addr_pointed1, addr_pointed2) == 0){
- if((addr_pointed1 > std_heap) && (addr_pointed1 < (void *)((char *)std_heap + STD_HEAP_SIZE)) && (addr_pointed2 > std_heap) && (addr_pointed2 < (void *)((char *)std_heap + STD_HEAP_SIZE))){
- if(is_free_area(addr_pointed1, (xbt_mheap_t)heap1) == 0 || is_free_area(addr_pointed2, (xbt_mheap_t)heap2) == 0){
- //XBT_INFO("Difference at offset %zu (%p - %p)", k, (char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k);
- nb_diff++;
- }
- }else{
- //XBT_INFO("Difference at offset %zu (%p - %p)", k, (char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k);
- nb_diff++;
- }
- }
- }
- k++;
- }
-
- }else{
- XBT_INFO("Different size used between stacks");
- return 1;
+
+ while(k < size_used1){
+ if(memcmp((char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k, 1) != 0){
+ pointer_align = ((size_used1 - k) / sizeof(void*)) * sizeof(void*);
+ addr_pointed1 = *((void **)(((char*)s1->address + (s1->size - size_used1)) + pointer_align));
+ addr_pointed2 = *((void **)(((char*)s2->address + (s2->size - size_used2)) + pointer_align));
+ if(is_heap_equality(equals, addr_pointed1, addr_pointed2) == 0){
+ if((addr_pointed1 > std_heap) && (addr_pointed1 < (void *)((char *)std_heap + STD_HEAP_SIZE)) && (addr_pointed2 > std_heap) && (addr_pointed2 < (void *)((char *)std_heap + STD_HEAP_SIZE))){
+ if(is_free_area(addr_pointed1, (xbt_mheap_t)heap1) == 0 || is_free_area(addr_pointed2, (xbt_mheap_t)heap2) == 0){
+ return 1;
+ }
+ }else{
+ return 1;
+ }
+ }
+ }
+ k++;
}
-
- return nb_diff;
+
+ return 0;
}
int MC_compare_snapshots(void *s1, void *s2){
xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
}
+void _mc_cfg_cb_timeout(const char *name, int pos) {
+ if (_surf_init_status && !_surf_do_model_check) {
+ xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _surf_mc_timeout= xbt_cfg_get_int(_surf_cfg_set, name);
+ xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+
/* MC global data structures */
xbt_dict_t mc_local_variables = NULL;
/* Ignore mechanism */
-extern xbt_dynar_t mc_comparison_ignore;
+xbt_dynar_t mc_stack_comparison_ignore;
+xbt_dynar_t mc_data_bss_comparison_ignore;
+extern xbt_dynar_t mc_heap_comparison_ignore;
extern xbt_dynar_t stacks_areas;
xbt_automaton_t _mc_property_automaton = NULL;
/* mc_time refers to clock for each process -> ignore it for heap comparison */
int i;
for(i = 0; i<simix_process_maxpid; i++)
- MC_ignore(&(mc_time[i]), sizeof(double));
+ MC_ignore_heap(&(mc_time[i]), sizeof(double));
compare = 0;
xbt_dict_t libsimgrid_location_list = MC_get_location_list(ls_path);
MC_get_local_variables(ls_path, libsimgrid_location_list, &mc_local_variables);
+ initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+ initial_state_liveness->snapshot_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+ initial_state_liveness->chunks_used_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+ initial_state_liveness->stacks_sizes_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+ initial_state_liveness->program_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+ initial_state_liveness->libsimgrid_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+ initial_state_liveness->heap_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+ initial_state_liveness->stacks_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+
MC_UNSET_RAW_MEM;
MC_init_memory_map_info();
*/
void MC_replay(xbt_fifo_t stack, int start)
{
- raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem = (mmalloc_get_current_heap() == raw_heap);
int value, i = 1;
char *req_str;
}
XBT_DEBUG("**** End Replay ****");
- if(raw_mem_set)
+ if(raw_mem)
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
{
- raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem = (mmalloc_get_current_heap() == raw_heap);
int value;
char *req_str;
XBT_DEBUG("**** End Replay ****");
- if(raw_mem_set)
+ if(raw_mem)
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
//XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
XBT_INFO("Expanded / Visited = %lf",
(double) stats->visited_pairs / stats->expanded_pairs);
- /*XBT_INFO("Exploration coverage = %lf",
- (double)stats->expanded_states / stats->state_size); */
+
+ if(mmalloc_get_current_heap() == raw_heap)
+ MC_UNSET_RAW_MEM;
}
void MC_assert(int prop)
/************ MC_ignore ***********/
-void MC_ignore(void *address, size_t size){
+void MC_ignore_heap(void *address, size_t size){
raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
- if(mc_comparison_ignore == NULL)
- mc_comparison_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL);
+ if(mc_heap_comparison_ignore == NULL)
+ mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), NULL);
- mc_ignore_region_t region = NULL;
- region = xbt_new0(s_mc_ignore_region_t, 1);
+ mc_heap_ignore_region_t region = NULL;
+ region = xbt_new0(s_mc_heap_ignore_region_t, 1);
region->address = address;
region->size = size;
}
unsigned int cursor = 0;
- mc_ignore_region_t current_region;
- xbt_dynar_foreach(mc_comparison_ignore, cursor, current_region){
+ mc_heap_ignore_region_t current_region;
+ xbt_dynar_foreach(mc_heap_comparison_ignore, cursor, current_region){
if(current_region->address > address)
break;
}
- xbt_dynar_insert_at(mc_comparison_ignore, cursor, ®ion);
+ xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
MC_UNSET_RAW_MEM;
MC_SET_RAW_MEM;
}
-void MC_new_stack_area(void *stack, char *name, void* context){
+void MC_ignore_data_bss(void *address, size_t size){
+
+ raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ if(mc_data_bss_comparison_ignore == NULL)
+ mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), NULL);
+
+ if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
+
+ mc_data_bss_ignore_variable_t var = NULL;
+ var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
+ var->address = address;
+ var->size = size;
+
+ xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
+
+ }else{
+
+ unsigned int cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
+ mc_data_bss_ignore_variable_t current_var = NULL;
+
+ while(start <= end){
+ cursor = (start + end) / 2;
+ current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
+ if(current_var->address == address){
+ MC_UNSET_RAW_MEM;
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ return;
+ }
+ if(current_var->address < address)
+ start = cursor + 1;
+ if(current_var->address > address)
+ end = cursor - 1;
+ }
+
+ mc_data_bss_ignore_variable_t var = NULL;
+ var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
+ var->address = address;
+ var->size = size;
+
+ if(current_var->address > address)
+ xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
+ else
+ xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
+
+ }
+
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+}
+void MC_ignore_stack(const char *var_name, const char *frame){
+
raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
+ if(mc_stack_comparison_ignore == NULL)
+ mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), NULL);
+
+ if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
+
+ mc_stack_ignore_variable_t var = NULL;
+ var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
+ var->var_name = strdup(var_name);
+ var->frame = strdup(frame);
+
+ xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
+
+ }else{
+
+ unsigned int cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
+ mc_stack_ignore_variable_t current_var = NULL;
+
+ while(start <= end){
+ cursor = (start + end) / 2;
+ current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
+ if(strcmp(current_var->frame, frame) == 0){
+ if(strcmp(current_var->var_name, var_name) == 0){
+ MC_UNSET_RAW_MEM;
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ return;
+ }
+ if(strcmp(current_var->var_name, var_name) < 0)
+ start = cursor + 1;
+ if(strcmp(current_var->var_name, var_name) > 0)
+ end = cursor - 1;
+ }
+ if(strcmp(current_var->frame, frame) < 0)
+ start = cursor + 1;
+ if(strcmp(current_var->frame, frame) > 0)
+ end = cursor - 1;
+ }
+
+ mc_stack_ignore_variable_t var = NULL;
+ var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
+ var->var_name = strdup(var_name);
+ var->frame = strdup(frame);
+
+ if(strcmp(current_var->frame, frame) < 0)
+ xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
+ else
+ xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
+
+ }
+
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+}
+
+void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
+
+ raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
if(stacks_areas == NULL)
stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
region->address = stack;
region->process_name = strdup(name);
region->context = context;
+ region->size = size;
xbt_dynar_push(stacks_areas, ®ion);
MC_UNSET_RAW_MEM;
dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
new_element->type = e_dw_bregister_op;
new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
- new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, 2, char*));
+ new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, 1, char*));
xbt_dynar_push(loc->location.compose, &new_element);
}else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
MC_UNSET_RAW_MEM;
- if(xbt_dynar_is_empty(reached_pairs) || !compare){
+ if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
MC_SET_RAW_MEM;
/* New pair reached */
xbt_dynar_push(reached_pairs, &new_pair);
MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
return 0;
if(raw_mem_set)
MC_SET_RAW_MEM;
- else
- MC_UNSET_RAW_MEM;
-
+
compare = 0;
return 0;
if(raw_mem_set)
MC_SET_RAW_MEM;
- else
- MC_UNSET_RAW_MEM;
}
/********************* Double-DFS stateless *******************/
void pair_stateless_free(mc_pair_stateless_t pair){
+ xbt_free(pair->graph_state->system_state);
+ xbt_free(pair->graph_state->proc_status);
+ xbt_free(pair->graph_state);
xbt_free(pair);
}
successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
/* Save the initial state */
- initial_state_liveness = xbt_new0(s_mc_global_t, 1);
initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
MC_UNSET_RAW_MEM;
mc_pair_stateless_t next_pair = NULL;
mc_pair_stateless_t pair_succ;
+
+ mc_pair_stateless_t remove_pair;
+ mc_pair_reached_t remove_pair_reached;
if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
next_graph_state = MC_state_pair_new();
/* Get enabled process and insert it in the interleave set of the next graph_state */
+
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
+ }
+ }
+
xbt_swag_foreach(process, simix_global->process_list){
if(MC_process_is_enabled(process)){
MC_state_interleave_process(next_graph_state, process);
}
+ }else{
+
+ XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
+
+ MC_SET_RAW_MEM;
+
+ /* Create the new expanded graph_state */
+ next_graph_state = MC_state_pair_new();
+
+ xbt_dynar_reset(successors);
+
+ MC_UNSET_RAW_MEM;
+
+
+ cursor= 0;
+ xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+
+ res = MC_automaton_evaluate_label(transition_succ->label);
+
+ if(res == 1){ // enabled transition in automaton
+ MC_SET_RAW_MEM;
+ next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ xbt_dynar_push(successors, &next_pair);
+ MC_UNSET_RAW_MEM;
+ }
+
+ }
+
+ cursor = 0;
+
+ xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+
+ res = MC_automaton_evaluate_label(transition_succ->label);
+
+ if(res == 2){ // true transition in automaton
+ MC_SET_RAW_MEM;
+ next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ xbt_dynar_push(successors, &next_pair);
+ MC_UNSET_RAW_MEM;
+ }
+
+ }
+
+ cursor = 0;
+
+ xbt_dynar_foreach(successors, cursor, pair_succ){
+
+ if(search_cycle == 1){
+
+ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
+
+ if(reached(pair_succ->automaton_state)){
+
+ XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
+
+ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+ XBT_INFO("| ACCEPTANCE CYCLE |");
+ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+ XBT_INFO("Counter-example that violates formula :");
+ MC_show_stack_liveness(mc_stack_liveness);
+ MC_dump_stack_liveness(mc_stack_liveness);
+ MC_print_statistics_pairs(mc_stats_pair);
+ exit(0);
+
+ }else{
+
+ XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
+
+ XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
+
+ MC_ddfs(search_cycle);
+
+ }
+
+ }else{
+
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
+
+ MC_ddfs(search_cycle);
+
+ }
+
+
+ }else{
+
+ if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+
+ set_pair_reached(pair_succ->automaton_state);
+
+ search_cycle = 1;
+
+ XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+
+ }
+
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
+
+ MC_ddfs(search_cycle);
+
+ }
+
+ /* Restore system before checking others successors */
+ if(cursor != xbt_dynar_length(successors) - 1)
+ MC_replay_liveness(mc_stack_liveness, 1);
+
+ }
+
}
}else{
MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_stack_liveness);
+ remove_pair = xbt_fifo_shift(mc_stack_liveness);
+ xbt_fifo_remove(mc_stack_liveness, remove_pair);
+ remove_pair = NULL;
if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
- xbt_dynar_pop(reached_pairs, NULL);
+ remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
+ pair_reached_free(remove_pair_reached);
+ remove_pair_reached = NULL;
}
MC_UNSET_RAW_MEM;
if(raw_mem_set)
MC_SET_RAW_MEM;
- else
- MC_UNSET_RAW_MEM;
}
typedef struct s_mc_global_t{
mc_snapshot_t initial_snapshot;
+ xbt_dynar_t snapshot_comparison_times;
+ xbt_dynar_t chunks_used_comparison_times;
+ xbt_dynar_t stacks_sizes_comparison_times;
+ xbt_dynar_t program_data_segment_comparison_times;
+ xbt_dynar_t libsimgrid_data_segment_comparison_times;
+ xbt_dynar_t heap_comparison_times;
+ xbt_dynar_t stacks_comparison_times;
}s_mc_global_t, *mc_global_t;
void MC_take_snapshot(mc_snapshot_t);
extern void *end_plt_libsimgrid;
extern void *start_plt_binary;
extern void *end_plt_binary;
+extern xbt_dynar_t mc_stack_comparison_ignore;
+extern xbt_dynar_t mc_data_bss_comparison_ignore;
+extern void *start_bss_libsimgrid;
typedef struct s_mc_pair{
mc_snapshot_t system_state;
extern int _surf_mc_checkpoint;
extern char* _surf_mc_property_file;
+extern int _surf_mc_timeout;
/****** Core dump ******/
* communication is not ready, it can timeout and won't block.
* On the other hand if it hasn't a timeout, check if the comm is ready.*/
if(req->comm_wait.timeout >= 0){
- return TRUE;
+ if(_surf_mc_timeout == 1){
+ return TRUE;
+ }else{
+ act = req->comm_wait.comm;
+ return (act->comm.src_proc && act->comm.dst_proc);
+ }
}else{
act = req->comm_wait.comm;
return (act->comm.src_proc && act->comm.dst_proc);
if(MC_is_active()){
/* Ignore total amount of messages sent during the simulation for heap comparison */
- MC_ignore(&(msg_global->sent_msg), sizeof(msg_global->sent_msg));
+ MC_ignore_heap(&(msg_global->sent_msg), sizeof(msg_global->sent_msg));
}
#ifdef HAVE_TRACING
{
xbt_ex_t e;
int finished = 0;
+
+ /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
+ if (MC_is_active()){
+ MC_ignore_stack("e", "MSG_comm_test");
+ MC_ignore_stack("__ex_cleanup", "MSG_comm_test");
+ }
+
TRY {
finished = simcall_comm_test(comm->s_comm);
/* Store the address of the stack in heap to compare it apart of heap comparison */
if(MC_is_active())
- MC_ignore(context, size);
+ MC_ignore_heap(context, size);
/* If the user provided a function for the process then use it.
Otherwise, it is the context for maestro and we should set it as the
raw_maestro_context = context;
if(MC_is_active())
- MC_ignore(&(raw_maestro_context->stack_top), sizeof(raw_maestro_context->stack_top));
+ MC_ignore_heap(&(raw_maestro_context->stack_top), sizeof(raw_maestro_context->stack_top));
}
}
if(MC_is_active() && code)
- MC_new_stack_area(context, ((smx_process_t)((smx_context_t)context)->data)->name, &(context->uc));
+ MC_new_stack_area(context, ((smx_process_t)((smx_context_t)context)->data)->name, &(context->uc), size);
return (smx_context_t) context;
}
smx_context_t next_context;
unsigned long int i = sysv_process_index++;
+ if(MC_is_active()){
+ MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
+ MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
+ }
+
if (i < xbt_dynar_length(simix_global->process_to_run)) {
/* execute the next process */
XBT_DEBUG("Run next process");
{
rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free);
if(MC_is_active())
- MC_ignore(&smx_total_comms, sizeof(smx_total_comms));
+ MC_ignore_data_bss(&smx_total_comms, sizeof(smx_total_comms));
}
void SIMIX_network_exit(void)
self->doexception = 0;
SMX_THROW();
}
+
+ /* Ignore some local variables from xbt/ex.c for stacks comparison */
+ if(MC_is_active()){
+ MC_ignore_stack("ctx", "SIMIX_process_yield");
+ MC_ignore_stack("_throw_ctx", "SIMIX_process_yield");
+ MC_ignore_stack("_log_ev", "SIMIX_process_yield");
+ }
}
/* callback: context fetching */
"Specify the kind of exploration reduction (either none or DPOR)",
xbt_cfgelm_string, &default_value, 0, 1,
_mc_cfg_cb_reduce, NULL);
+
+ /* Enable/disable timeout for wait requests with model-checking */
+ default_value_int = 1;
+ xbt_cfg_register(&_surf_cfg_set, "model-check/timeout",
+ "Enable/Disable timeout for wait requests",
+ xbt_cfgelm_int, &default_value, 0, 1,
+ _mc_cfg_cb_timeout, NULL);
#endif
/* do verbose-exit */
extern char *xbt_binary_name;
-xbt_dynar_t mc_comparison_ignore;
+xbt_dynar_t mc_heap_comparison_ignore;
xbt_dynar_t stacks_areas;
static void heap_area_pair_free(heap_area_pair_t pair);
static void match_equals(xbt_dynar_t list, xbt_dynar_t *equals);
static int in_mc_comparison_ignore(int block, int fragment);
-static size_t heap_comparison_ignore(void *address);
+static size_t heap_comparison_ignore_size(void *address);
static void add_heap_equality(xbt_dynar_t *equals, void *a1, void *a2);
static void remove_heap_equality(xbt_dynar_t *equals, int address, void *a);
}
-void *s_heap, *heapbase1, *heapbase2;
-malloc_info *heapinfo1, *heapinfo2;
-size_t heaplimit, heapsize1, heapsize2;
+void *s_heap = NULL, *heapbase1 = NULL, *heapbase2 = NULL;
+malloc_info *heapinfo1 = NULL, *heapinfo2 = NULL;
+size_t heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
-int ignore_done;
+int ignore_done = 0;
int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stack1, xbt_dynar_t *stack2, xbt_dynar_t *equals){
void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
void *real_addr_block1, *real_addr_block2;
char *stack_name;
- int nb_block1=0, nb_frag1=0, nb_block2=0, nb_frag2=0;
xbt_dynar_t previous = xbt_dynar_new(sizeof(heap_area_pair_t), heap_area_pair_free_voidp);
int equal, res_compare;
- ignore_done = 0;
-
/* Init equal information */
i1 = 1;
while(i1<=heaplimit){
if(heapinfo1[i1].type == 0){
- if(heapinfo1[i1].busy_block.busy_size > 0)
- nb_block1++;
heapinfo1[i1].busy_block.equal_to = NULL;
}
if(heapinfo1[i1].type > 0){
for(j1=0; j1 < (size_t) (BLOCKSIZE >> heapinfo1[i1].type); j1++){
- if(heapinfo1[i1].busy_frag.frag_size[j1] > 0)
- nb_frag1++;
heapinfo1[i1].busy_frag.equal_to[j1] = NULL;
}
}
while(i2<=heaplimit){
if(heapinfo2[i2].type == 0){
- if(heapinfo2[i2].busy_block.busy_size > 0)
- nb_block2++;
heapinfo2[i2].busy_block.equal_to = NULL;
}
if(heapinfo2[i2].type > 0){
for(j2=0; j2 < (size_t) (BLOCKSIZE >> heapinfo2[i2].type); j2++){
- if(heapinfo2[i2].busy_frag.frag_size[j2] > 0)
- nb_frag2++;
heapinfo2[i2].busy_frag.equal_to[j2] = NULL;
}
}
i2++;
}
- if(nb_block1 != nb_block2 || nb_frag1 != nb_frag2){
- XBT_DEBUG("Different number of busy blocks (%d - %d) or busy fragments (%d - %d)", nb_block1, nb_block2, nb_frag1, nb_frag2);
- return 1;
- }
-
/* Check busy blocks*/
i1 = 1;
add_heap_area_pair(previous, current_block, -1, current_block, -1);
- if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+ if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){
if(in_mc_comparison_ignore((int)current_block, -1))
res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 1);
else
/* Comparison */
add_heap_area_pair(previous, i1, -1, i2, -1);
- if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+ if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){
if(in_mc_comparison_ignore((int)i1, -1))
res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 1);
else
add_heap_area_pair(previous, current_block, current_fragment, current_block, current_fragment);
- if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+ if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){
if(in_mc_comparison_ignore((int)current_block, (int)current_fragment))
res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[current_block].busy_frag.frag_size[current_fragment], previous, 1);
else
/* Comparison */
add_heap_area_pair(previous, i1, j1, i2, j2);
- if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+ if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){
if(in_mc_comparison_ignore((int)i1, (int)j1))
res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 1);
else
XBT_DEBUG("Different blocks or fragments in heap2 : %d", nb_diff2);
xbt_dynar_free(&previous);
+ ignore_done = 0;
+ s_heap = NULL, heapbase1 = NULL, heapbase2 = NULL;
+ heapinfo1 = NULL, heapinfo2 = NULL;
+ heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
return ((nb_diff1 > 0) || (nb_diff2 > 0));
unsigned int cursor = 0;
int start = 0;
- int end = xbt_dynar_length(mc_comparison_ignore) - 1;
- mc_ignore_region_t region;
+ int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+ mc_heap_ignore_region_t region;
while(start <= end){
cursor = (start + end) / 2;
- region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t);
+ region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
if(region->block == block){
if(region->fragment == fragment)
return 1;
return 0;
}
-static size_t heap_comparison_ignore(void *address){
+static size_t heap_comparison_ignore_size(void *address){
unsigned int cursor = 0;
int start = 0;
- int end = xbt_dynar_length(mc_comparison_ignore) - 1;
- mc_ignore_region_t region;
+ int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+ mc_heap_ignore_region_t region;
while(start <= end){
cursor = (start + end) / 2;
- region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t);
+ region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
if(region->address == address)
return region->size;
if(region->address < address)
if(check_ignore){
current_area1 = (char*)((xbt_mheap_t)s_heap)->heapbase + ((((char *)area1) + i) - (char *)heapbase1);
- if((ignore1 = heap_comparison_ignore(current_area1)) > 0){
+ if((ignore1 = heap_comparison_ignore_size(current_area1)) > 0){
current_area2 = (char*)((xbt_mheap_t)s_heap)->heapbase + ((((char *)area2) + i) - (char *)heapbase2);
- if((ignore2 = heap_comparison_ignore(current_area2)) == ignore1){
+ if((ignore2 = heap_comparison_ignore_size(current_area2)) == ignore1){
i = i + ignore2;
ignore_done++;
continue;
if(add_heap_area_pair(previous, block_pointed1, -1, block_pointed2, -1)){
- if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+ if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){
if(in_mc_comparison_ignore(block_pointed1, -1))
res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 1);
else
if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){
- if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+ if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){
if(in_mc_comparison_ignore(block_pointed1, frag_pointed1))
res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 1);
else
if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){
- if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+ if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){
if(in_mc_comparison_ignore(block_pointed1, frag_pointed1))
res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 1);
else
static void add_heap_equality(xbt_dynar_t *equals, void *a1, void *a2){
- heap_equality_t he = xbt_new0(s_heap_equality_t, 1);
- he->address1 = a1;
- he->address2 = a2;
-
if(xbt_dynar_is_empty(*equals)){
+ heap_equality_t he = xbt_new0(s_heap_equality_t, 1);
+ he->address1 = a1;
+ he->address2 = a2;
+
xbt_dynar_insert_at(*equals, 0, &he);
}else{
if(current_equality->address1 > a1)
end = cursor - 1;
}
+
+ heap_equality_t he = xbt_new0(s_heap_equality_t, 1);
+ he->address1 = a1;
+ he->address2 = a2;
if(current_equality->address1 < a1)
xbt_dynar_insert_at(*equals, cursor + 1 , &he);
// mmalloc_detach(__mmalloc_default_mdp);
xbt_mheap_destroy_no_free(__mmalloc_default_mdp);
}
+
+size_t mmalloc_get_chunks_used(xbt_mheap_t heap){
+ return ((struct mdesc *)heap)->heapstats.chunks_used;
+}
int _surf_do_model_check = 0;
int _surf_mc_checkpoint=0;
char* _surf_mc_property_file=NULL;
+int _surf_mc_timeout=0;
/* Declare xbt_preinit and xbt_postexit as constructor/destructor of the library.
* This is crude and rather compiler-specific, unfortunately.
