1 /* Copyright (c) 2015. The SimGrid Team.
2 * All rights reserved. */
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. */
10 #include <xbt/string.hpp>
12 #include "src/simix/smx_private.h"
14 #include "src/mc/mc_smx.h"
15 #include "ModelChecker.hpp"
17 using simgrid::mc::remote;
22 void MC_smx_process_info_clear(mc_smx_process_info_t p)
29 xbt_dynar_t MC_smx_process_info_list_new(void)
32 sizeof(s_mc_smx_process_info_t),
33 ( void_f_pvoid_t) &MC_smx_process_info_clear);
37 bool is_in_dynar(smx_process_t p, xbt_dynar_t dynar)
39 return (uintptr_t) p >= (uintptr_t) dynar->data
40 && (uintptr_t) p < ((uintptr_t) dynar->data + dynar->used * dynar->elmsize);
44 mc_smx_process_info_t MC_smx_process_get_info(smx_process_t p)
46 assert(is_in_dynar(p, mc_model_checker->process().smx_process_infos)
47 || is_in_dynar(p, mc_model_checker->process().smx_old_process_infos));
48 mc_smx_process_info_t process_info =
49 (mc_smx_process_info_t)
50 ((char*) p - offsetof(s_mc_smx_process_info_t, copy));
54 /** Load the remote swag of processes into a dynar
56 * @param process MCed process
57 * @param target Local dynar (to be filled with copies of `s_smx_process_t`)
58 * @param remote_swag Address of the process SWAG in the remote list
60 static void MC_process_refresh_simix_process_list(
61 simgrid::mc::Process* process,
62 xbt_dynar_t target, xbt_swag_t remote_swag)
64 // swag = REMOTE(*simix_global->process_list)
66 process->read_bytes(&swag, sizeof(swag), remote(remote_swag));
69 xbt_dynar_reset(target);
71 // Load each element of the dynar from the MCed process:
73 for (p = (smx_process_t) swag.head; p; ++i) {
75 s_mc_smx_process_info_t info;
79 process->read_bytes(&info.copy, sizeof(info.copy), remote(p));
80 xbt_dynar_push(target, &info);
82 // Lookup next process address:
83 p = (smx_process_t) xbt_swag_getNext(&info.copy, swag.offset);
85 assert(i == swag.count);
88 void MC_process_smx_refresh(simgrid::mc::Process* process)
90 xbt_assert(mc_mode == MC_MODE_SERVER);
91 if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
94 // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
96 // simix_global_p = REMOTE(simix_global);
97 smx_global_t simix_global_p;
98 process->read_variable("simix_global", &simix_global_p, sizeof(simix_global_p));
100 // simix_global = REMOTE(*simix_global)
101 s_smx_global_t simix_global;
102 process->read_bytes(&simix_global, sizeof(simix_global),
103 remote(simix_global_p));
105 MC_process_refresh_simix_process_list(
106 process, process->smx_process_infos, simix_global.process_list);
107 MC_process_refresh_simix_process_list(
108 process, process->smx_old_process_infos, simix_global.process_to_destroy);
110 process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
113 /** Get the issuer of a simcall (`req->issuer`)
115 * In split-process mode, it does the black magic necessary to get an address
116 * of a (shallow) copy of the data structure the issuer SIMIX process in the local
119 * @param process the MCed process
120 * @param req the simcall (copied in the local process)
122 smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req)
124 if (mc_mode == MC_MODE_CLIENT)
127 MC_process_smx_refresh(&mc_model_checker->process());
129 // This is the address of the smx_process in the MCed process:
130 void* address = req->issuer;
133 mc_smx_process_info_t p;
135 // Lookup by address:
136 xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, i, p)
137 if (p->address == address)
139 xbt_dynar_foreach_ptr(mc_model_checker->process().smx_old_process_infos, i, p)
140 if (p->address == address)
143 xbt_die("Issuer not found");
146 smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address)
148 if (!process_remote_address)
150 if (mc_mode == MC_MODE_CLIENT)
151 return process_remote_address;
153 mc_smx_process_info_t process_info = MC_smx_resolve_process_info(process_remote_address);
155 return &process_info->copy;
160 mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address)
162 if (mc_mode == MC_MODE_CLIENT)
163 xbt_die("No process_info for local process is not enabled.");
166 mc_smx_process_info_t process_info;
167 xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, index, process_info)
168 if (process_info->address == process_remote_address)
170 xbt_dynar_foreach_ptr(mc_model_checker->process().smx_old_process_infos, index, process_info)
171 if (process_info->address == process_remote_address)
173 xbt_die("Process info not found");
176 const char* MC_smx_process_get_host_name(smx_process_t p)
178 if (mc_mode == MC_MODE_CLIENT)
179 return sg_host_get_name(p->host);
181 simgrid::mc::Process* process = &mc_model_checker->process();
183 /* Horrible hack to find the offset of the id in the simgrid::s4u::Host.
185 Offsetof is not supported for non-POD types but this should
186 work in pratice for the targets currently supported by the MC
187 as long as we do not add funny features to the Host class
188 (such as virtual base).
190 We are using a (C++11) unrestricted union in order to avoid
191 any construction/destruction of the simgrid::s4u::Host.
194 simgrid::s4u::Host host;
199 const size_t offset = (char*) &foo.host.name() - (char*) &foo.host;
201 // Read the simgrid::xbt::string in the MCed process:
202 mc_smx_process_info_t info = MC_smx_process_get_info(p);
203 simgrid::xbt::string_data remote_string;
204 auto remote_string_address = remote(
205 (simgrid::xbt::string_data*) ((char*) p->host + offset));
206 process->read_bytes(&remote_string, sizeof(remote_string), remote_string_address);
207 char hostname[remote_string.len];
208 process->read_bytes(hostname, remote_string.len + 1, remote(remote_string.data));
209 info->hostname = mc_model_checker->get_host_name(hostname);
210 return info->hostname;
213 const char* MC_smx_process_get_name(smx_process_t p)
215 simgrid::mc::Process* process = &mc_model_checker->process();
216 if (mc_mode == MC_MODE_CLIENT)
221 mc_smx_process_info_t info = MC_smx_process_get_info(p);
223 info->name = process->read_string(p->name);
229 int MC_smpi_process_count(void)
231 if (mc_mode == MC_MODE_CLIENT)
232 return smpi_process_count();
235 mc_model_checker->process().read_variable("process_count",
242 unsigned long MC_smx_get_maxpid(void)
244 unsigned long maxpid;
245 mc_model_checker->process().read_variable("simix_process_maxpid",
246 &maxpid, sizeof(maxpid));