[mc] Remote support for MC_deadlock_check() using MC_MESSAGE_DEADLOCK_CHECK IPC message

diff --git a/src/mc/mc_client.c b/src/mc/mc_client.c
index 6a8d4ee..da8d8c4 100644 (file)
--- a/src/mc/mc_client.c
+++ b/src/mc/mc_client.c
@@ -22,6 +22,7 @@
 #include "mc_mmalloc.h"
 #include "mc_ignore.h"
 #include "mc_model_checker.h"
+#include "mc_private.h" // MC_deadlock_check()
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
 
@@ -44,7 +45,7 @@ void MC_client_init(void)
   int type;
   socklen_t socklen = sizeof(type);
   if (getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) != 0)
-    xbt_die("Could not check socket type: %s", strerror(errno));
+    xbt_die("Could not check socket type");
   if (type != SOCK_DGRAM)
     xbt_die("Unexpected socket type %i", type);
   XBT_DEBUG("Model-checked application found expected socket type");
@@ -85,8 +86,21 @@ void MC_client_handle_messages(void)
       xbt_die("Message is too short");
     memcpy(&message, message_buffer, sizeof(message));
     switch (message.type) {
+
+    case MC_MESSAGE_DEADLOCK_CHECK:
+      {
+        int result = MC_deadlock_check();
+        s_mc_int_message_t answer;
+        answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
+        answer.value = result;
+        if (MC_protocol_send(mc_client->fd, &answer, sizeof(answer)))
+          xbt_die("Could nor send response");
+      }
+      break;
+
     case MC_MESSAGE_CONTINUE:
       return;
+
     default:
       xbt_die("Unexpected message from model-checker %i", message.type);
     }

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 85dacbc..bf677ae 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -178,6 +178,9 @@ void MC_init_pid(pid_t pid, int socket)
     MC_ignore_global_variable("smx_total_comms");
 
     if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
+      /* Those requests are handled on the client side and propagated by message
+       * to the server: */
+
       MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
       smx_process_t process;
@@ -311,6 +314,24 @@ void MC_exit(void)
 
 int MC_deadlock_check()
 {
+  if (mc_mode == MC_MODE_SERVER) {
+    int res;
+    if ((res = MC_protocol_send_simple_message(mc_model_checker->process.socket,
+      MC_MESSAGE_DEADLOCK_CHECK)))
+      xbt_die("Could not check deadlock state: %s",strerror(res));
+    s_mc_int_message_t message;
+    ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message));
+    if (s == -1)
+      xbt_die("Could not receive message");
+    else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
+      xbt_die("Unexpected message, expected MC_MESSAGE_DEADLOCK_CHECK_REPLY %i %i vs %i %i",
+        (int) s, (int) message.type, (int) sizeof(message), (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY
+        );
+    }
+    else
+      return message.value;
+  }
+
   int deadlock = FALSE;
   smx_process_t process;
   if (xbt_swag_size(simix_global->process_list)) {

diff --git a/src/mc/mc_protocol.c b/src/mc/mc_protocol.c
index 405a61a..0034148 100644 (file)
--- a/src/mc/mc_protocol.c
+++ b/src/mc/mc_protocol.c
@@ -62,3 +62,8 @@ int MC_protocol_hello(int socket)
 
   return 0;
 }
+
+ssize_t MC_receive_message(int socket, void* message, size_t size)
+{
+  return recv(socket, message, size, 0);
+}

diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h
index 251e184..f0100fd 100644 (file)
--- a/src/mc/mc_protocol.h
+++ b/src/mc/mc_protocol.h
@@ -45,6 +45,8 @@ typedef enum {
   MC_MESSAGE_IGNORE_MEMORY,
   MC_MESSAGE_STACK_REGION,
   MC_MESSAGE_REGISTER_SYMBOL,
+  MC_MESSAGE_DEADLOCK_CHECK,
+  MC_MESSAGE_DEADLOCK_CHECK_REPLY,
 } e_mc_message_type;
 
 #define MC_MESSAGE_LENGTH 512
@@ -65,6 +67,11 @@ typedef struct s_mc_message {
   e_mc_message_type type;
 } s_mc_message_t, *mc_message_t;
 
+typedef struct s_mc_int_message {
+  e_mc_message_type type;
+  uint64_t value;
+} s_mc_int_message_t, *mc_int_message_t;
+
 typedef struct s_mc_ignore_heap_message {
   e_mc_message_type type;
   s_mc_heap_ignore_region_t region;
@@ -91,6 +98,7 @@ typedef struct s_mc_register_symbol_message {
 int MC_protocol_send(int socket, void* message, size_t size);
 int MC_protocol_send_simple_message(int socket, int type);
 int MC_protocol_hello(int socket);
+ssize_t MC_receive_message(int socket, void* message, size_t size);
 
 SG_END_DECL()