Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
a33d00ec1c5bf5877ea6ee4b62906a6532f0a0f9
[simgrid.git] / src / mc / mc_protocol.h
1 /* Copyright (c) 2015. The SimGrid Team.
2  * All rights reserved.                                                     */
3
4 /* This program is free software; you can redistribute it and/or modify it
5  * under the terms of the license (GNU LGPL) which comes with this package. */
6
7 #ifndef MC_PROTOCOL_H
8 #define MC_PROTOCOL_H
9
10 #include <xbt/misc.h>
11
12 #include "mc/datatypes.h"
13
14 SG_BEGIN_DECL()
15
16 // ***** Environment variables for passing context to the model-checked process
17
18 /** Environment variable name set by `simgrid-mc` to enable MC support in the
19  *  children MC processes
20  */
21 #define MC_ENV_VARIABLE "SIMGRIC_MC"
22
23 /** Environment variable name used to pass the communication socket */
24 #define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
25
26 // ***** MC mode
27
28 typedef enum {
29   MC_MODE_NONE = 0,
30   MC_MODE_STANDALONE,
31   MC_MODE_CLIENT,
32   MC_MODE_SERVER
33 } e_mc_mode_t;
34
35 extern e_mc_mode_t mc_mode;
36
37 // ***** Messages
38
39 typedef enum {
40   MC_MESSAGE_NONE,
41   MC_MESSAGE_HELLO,
42   MC_MESSAGE_CONTINUE,
43   MC_MESSAGE_IGNORE_HEAP,
44   MC_MESSAGE_UNIGNORE_HEAP,
45   MC_MESSAGE_IGNORE_MEMORY,
46   MC_MESSAGE_STACK_REGION,
47 } e_mc_message_type;
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_DGRAM` 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  *  This is the basic structure shared by all messages: all message start with a message
61  *  type.
62  */
63 typedef struct s_mc_message {
64   e_mc_message_type type;
65 } s_mc_message_t, *mc_message_t;
66
67 typedef struct s_mc_ignore_heap_message {
68   e_mc_message_type type;
69   s_mc_heap_ignore_region_t region;
70 } s_mc_ignore_heap_message_t, *mc_ignore_heap_message_t;
71
72 typedef struct s_mc_ignore_memory_message {
73   e_mc_message_type type;
74   void *addr;
75   size_t size;
76 } s_mc_ignore_memory_message_t, *mc_ignore_memory_message_t;
77
78 typedef struct s_mc_stack_region_message {
79   e_mc_message_type type;
80   s_stack_region_t stack_region;
81 } s_mc_stack_region_message_t, *mc_stack_region_message_t;
82
83 int MC_protocol_send(int socket, void* message, size_t size);
84 int MC_protocol_send_simple_message(int socket, int type);
85 int MC_protocol_hello(int socket);
86
87 SG_END_DECL()
88
89 #endif