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   std::shared_ptr<simgrid::mc::Snapshot> initialSnapshot_;
  41
  42 private:
  43   Session(pid_t pid, int socket);
  44
  45   // No copy:
  46   Session(Session const&) = delete;
  47   Session& operator=(Session const&) = delete;
  48
  49 public:
  50   ~Session();
  51   void close();
  52
  53 public:
  54   void initialize();
  55   void execute(Transition const& transition);
  56   void logState();
  57
  58   void restoreInitialState();
  59
  60 public: // static constructors
  61
  62   /** Create a new session by forking
  63    *
  64    *  This sets up the environment for the model-checked process
  65    *  (environoment variables, sockets, etc.).
  66    *
  67    *  The code is expected to `exec` the model-checker program.
  68    */
  69   static Session* fork(std::function<void(void)> code);
  70
  71   /** Spawn a model-checked process
  72    *
  73    *  @param path full path of the executable
  74    *  @param argv arguments for the model-checked process (NULL-terminated)
  75    */
  76   static Session* spawnv(const char *path, char *const argv[]);
  77
  78   /** Spawn a model-checked process (using PATH)
  79    *
  80    *  @param file file name of the executable (found using `PATH`)
  81    *  @param argv arguments for the model-checked process (NULL-terminated)
  82    */
  83   static Session* spawnvp(const char *file, char *const argv[]);
  84 };
  85
  86 // Temporary
  87 extern simgrid::mc::Session* session;
  88
  89 }
  90 }
  91
  92 #endif