- XBT_DEBUG("Inside the parent process");
- if (simgrid::mc::server)
- xbt_die("MC server already present");
- try {
- mc_mode = MC_MODE_SERVER;
- simgrid::mc::server = new simgrid::mc::Server(child, socket);
- simgrid::mc::server->start();
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- MC_modelcheck_comm_determinism();
- else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
- MC_modelcheck_safety();
- else
- MC_modelcheck_liveness();
- simgrid::mc::server->shutdown();
- simgrid::mc::server->exit();
- }
- catch(std::exception& e) {
- XBT_ERROR("Exception: %s", e.what());
- }
- exit(SIMGRID_ERROR);
+ // Create a AF_LOCAL socketpair used for exchanging messages
+ // bewteen the model-checker process (ourselves) and the model-checked
+ // process:
+ int res;
+ int sockets[2];
+ res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
+ if (res == -1)
+ throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
+
+ pid_t pid = do_fork([&] {
+ close(sockets[1]);
+ int res = exec_model_checked(sockets[0], argv);
+ XBT_DEBUG("Error in the child process creation");
+ exit(res);
+ });
+
+ // Parent (model-checker):
+ close(sockets[0]);
+ return std::make_pair(pid, sockets[1]);