src/mc/Session.hpp

   1 /* Copyright (c) 2016-2019. The SimGrid Team. All rights reserved.          */
   2
   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. */
   5
   6 #ifndef SIMGRID_MC_SESSION_HPP
   7 #define SIMGRID_MC_SESSION_HPP
   8
   9 #ifdef __linux__
  10 #include <sys/prctl.h>
  11 #endif
  12
  13 #include "xbt/sysdep.h"
  14 #include "xbt/system_error.hpp"
  15 #include <sys/socket.h>
  16 #include <sys/types.h>
  17
  18 #include <functional>
  19
  20 #include "xbt/log.h"
  21
  22 #include "src/mc/mc_forward.hpp"
  23 #include "src/mc/ModelChecker.hpp"
  24
  25 namespace simgrid {
  26 namespace mc {
  27
  28 /** A model-checking session
  29  *
  30  *  This is expected to become the interface used by model-checking
  31  *  algorithms to control the execution of the model-checked process
  32  *  and the exploration of the execution graph. Model-checking
  33  *  algorithms should be able to be written in high-level languages
  34  *  (e.g. Python) using bindings on this interface.
  35  */
  36 class Session {
  37 private:
  38   std::unique_ptr<ModelChecker> modelChecker_;
  39   std::shared_ptr<simgrid::mc::Snapshot> initialSnapshot_;
  40
  41   Session(pid_t pid, int socket);
  42
  43   // No copy:
  44   Session(Session const&) = delete;
  45   Session& operator=(Session const&) = delete;
  46
  47 public:
  48   ~Session();
  49   void close();
  50
  51   void initialize();
  52   void execute(Transition const& transition);
  53   void logState();
  54
  55   void restoreInitialState();
  56
  57   // static constructors
  58
  59   /** Create a new session by forking
  60    *
  61    *  This sets up the environment for the model-checked process
  62    *  (environment variables, sockets, etc.).
  63    *
  64    *  The code is expected to `exec` the model-checker program.
  65    */
  66   static Session* fork(const std::function<void()>& code);
  67
  68   /** Spawn a model-checked process
  69    *
  70    *  @param path full path of the executable
  71    *  @param argv arguments for the model-checked process (NULL-terminated)
  72    */
  73   static Session* spawnv(const char *path, char *const argv[]);
  74
  75   /** Spawn a model-checked process (using PATH)
  76    *
  77    *  @param file file name of the executable (found using `PATH`)
  78    *  @param argv arguments for the model-checked process (NULL-terminated)
  79    */
  80   static Session* spawnvp(const char *file, char *const argv[]);
  81 };
  82
  83 // Temporary
  84 extern simgrid::mc::Session* session;
  85
  86 }
  87 }
  88
  89 #endif