1 /* Copyright (c) 2015-2017. The SimGrid Team. All rights reserved. */
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. */
6 #ifndef SIMGRID_MC_PROTOCOL_H
7 #define SIMGRID_MC_PROTOCOL_H
13 #include "mc/datatypes.h"
14 #include "simgrid/forward.h"
18 // ***** Environment variables for passing context to the model-checked process
20 /** Environment variable name set by `simgrid-mc` to enable MC support in the
21 * children MC processes
23 #define MC_ENV_VARIABLE "SIMGRID_MC"
25 /** Environment variable name used to pass the communication socket */
26 #define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
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,
41 MC_MESSAGE_SIMCALL_HANDLE,
42 MC_MESSAGE_ASSERTION_FAILED,
43 // MCer request to finish the restoration:
45 MC_MESSAGE_ACTOR_ENABLED,
46 MC_MESSAGE_ACTOR_ENABLED_REPLY
49 #define MC_MESSAGE_LENGTH 512
51 /** Basic structure for a MC message
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.
57 * Moreover the protocol is not stable. The same version of the library should be used
58 * for the client and the server.
61 /* Basic structure: all message start with a message type */
63 e_mc_message_type type;
65 typedef struct s_mc_message mc_message_t;
67 struct s_mc_message_int {
68 e_mc_message_type type;
71 typedef struct s_mc_message_int mc_message_int_t;
74 struct s_mc_message_ignore_heap {
75 e_mc_message_type type;
81 typedef struct s_mc_message_ignore_heap s_mc_message_ignore_heap_t;
83 struct s_mc_message_ignore_memory {
84 e_mc_message_type type;
88 typedef struct s_mc_message_ignore_memory s_mc_message_ignore_memory_t;
90 struct s_mc_message_stack_region {
91 e_mc_message_type type;
92 s_stack_region_t stack_region;
94 typedef struct s_mc_message_stack_region s_mc_message_stack_region_t;
96 struct s_mc_message_register_symbol {
97 e_mc_message_type type;
99 int (*callback)(void*);
102 typedef struct s_mc_message_register_symbol s_mc_message_register_symbol_t;
104 /* Server -> client */
105 struct s_mc_message_simcall_handle {
106 e_mc_message_type type;
110 typedef struct s_mc_message_simcall_handle s_mc_message_simcall_handle_t;
112 struct s_mc_message_restore {
113 e_mc_message_type type;
116 typedef struct s_mc_message_restore s_mc_message_restore_t;
118 struct s_mc_message_actor_enabled {
119 e_mc_message_type type;
120 aid_t aid; // actor ID
122 typedef struct s_mc_message_actor_enabled s_mc_message_actor_enabled_t;
124 XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type);