Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Do not use reduction_mode outside of the safety algorithm
[simgrid.git] / src / mc / Session.hpp
1 /* Copyright (c) 2016. 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 SIMGRID_MC_SESSION_HPP
8 #define SIMGRID_MC_SESSION_HPP
9
10 #ifdef __linux__
11 #include <sys/prctl.h>
12 #endif
13
14 #include <sys/types.h>
15 #include <sys/socket.h>
16 #include <xbt/sysdep.h>
17 #include <xbt/system_error.hpp>
18
19 #include <functional>
20
21 #include <xbt/log.h>
22
23 #include "src/mc/mc_forward.hpp"
24 #include "src/mc/ModelChecker.hpp"
25
26 namespace simgrid {
27 namespace mc {
28
29 /** A model-checking session
30  *
31  *  This is expected to become the interface used by model-checking
32  *  algorithms to control the execution of the model-checked process
33  *  and the exploration of the execution graph. Model-checking
34  *  algorithms should be able to be written in high-level languages
35  *  (e.g. Python) using bindings on this interface.
36  */
37 class Session {
38 private:
39   std::unique_ptr<ModelChecker> modelChecker_;
40
41 private: //
42   Session(pid_t pid, int socket);
43
44   // No copy:
45   Session(Session const&) = delete;
46   Session& operator=(Session const&) = delete;
47
48 public:
49   ~Session();
50   void close();
51
52 public: // static constructors
53
54   /** Create a new session by forking
55    *
56    *  The code is expected to `exec` the model-checker program.
57    */
58   static Session* fork(std::function<void(void)> code);
59
60   /** Create a session using `execv` */
61   static Session* spawnv(const char *path, char *const argv[]);
62
63   /** Create a session using `execvp` */
64   static Session* spawnvp(const char *path, char *const argv[]);
65 };
66
67 }
68 }
69
70 #endif