src/mc/remote/mc_protocol.h

   1 /* Copyright (c) 2015-2017. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #ifndef SIMGRID_MC_PROTOCOL_H
   7 #define SIMGRID_MC_PROTOCOL_H
   8
   9 #include <stdint.h>
  10
  11 #include <xbt/base.h>
  12
  13 #include "mc/datatypes.h"
  14 #include "simgrid/forward.h"
  15
  16 SG_BEGIN_DECL()
  17
  18 // ***** Environment variables for passing context to the model-checked process
  19
  20 /** Environment variable name set by `simgrid-mc` to enable MC support in the
  21  *  children MC processes
  22  */
  23 #define MC_ENV_VARIABLE "SIMGRID_MC"
  24
  25 /** Environment variable name used to pass the communication socket */
  26 #define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
  27
  28 // ***** Messages
  29
  30 enum e_mc_message_type {
  31   MC_MESSAGE_NONE,
  32   MC_MESSAGE_CONTINUE,
  33   MC_MESSAGE_IGNORE_HEAP,
  34   MC_MESSAGE_UNIGNORE_HEAP,
  35   MC_MESSAGE_IGNORE_MEMORY,
  36   MC_MESSAGE_STACK_REGION,
  37   MC_MESSAGE_REGISTER_SYMBOL,
  38   MC_MESSAGE_DEADLOCK_CHECK,
  39   MC_MESSAGE_DEADLOCK_CHECK_REPLY,
  40   MC_MESSAGE_WAITING,
  41   MC_MESSAGE_SIMCALL_HANDLE,
  42   MC_MESSAGE_ASSERTION_FAILED,
  43   // MCer request to finish the restoration:
  44   MC_MESSAGE_RESTORE,
  45   MC_MESSAGE_ACTOR_ENABLED,
  46   MC_MESSAGE_ACTOR_ENABLED_REPLY
  47 };
  48
  49 #define MC_MESSAGE_LENGTH 512
  50
  51 /** Basic structure for a MC message
  52  *
  53  *  The current version of the client/server protocol sends C structures over `AF_LOCAL`
  54  *  `SOCK_SEQPACKET` sockets. This means that the protocol is ABI/architecture specific:
  55  *  we currently can't model-check a x86 process from a x86_64 process.
  56  *
  57  *  Moreover the protocol is not stable. The same version of the library should be used
  58  *  for the client and the server.
  59  */
  60
  61 /* Basic structure: all message start with a message type */
  62 struct s_mc_message_t {
  63   enum e_mc_message_type type;
  64 };
  65
  66 struct s_mc_message_int_t {
  67   enum e_mc_message_type type;
  68   uint64_t value;
  69 };
  70
  71 /* Client->Server */
  72 struct s_mc_message_ignore_heap_t {
  73   enum e_mc_message_type type;
  74   int block;
  75   int fragment;
  76   void* address;
  77   size_t size;
  78 };
  79
  80 struct s_mc_message_ignore_memory_t {
  81   enum e_mc_message_type type;
  82   uint64_t addr;
  83   size_t size;
  84 };
  85
  86 struct s_mc_message_stack_region_t {
  87   enum e_mc_message_type type;
  88   s_stack_region_t stack_region;
  89 };
  90
  91 struct s_mc_message_register_symbol_t {
  92   enum e_mc_message_type type;
  93   char name[128];
  94   int (*callback)(void*);
  95   void* data;
  96 };
  97
  98 /* Server -> client */
  99 struct s_mc_message_simcall_handle_t {
 100   enum e_mc_message_type type;
 101   unsigned long pid;
 102   int value;
 103 };
 104
 105 struct s_mc_message_restore_t {
 106   enum e_mc_message_type type;
 107   int index;
 108 };
 109
 110 struct s_mc_message_actor_enabled_t {
 111   enum e_mc_message_type type;
 112   aid_t aid; // actor ID
 113 };
 114
 115 XBT_PRIVATE const char* MC_message_type_name(enum e_mc_message_type type);
 116
 117 SG_END_DECL()
 118
 119 #endif