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:
  53   void execute(Transition const& transition);
  54   void logState();
  55
  56 public: // static constructors
  57
  58   /** Create a new session by forking
  59    *
  60    *  The code is expected to `exec` the model-checker program.
  61    */
  62   static Session* fork(std::function<void(void)> code);
  63
  64   /** Create a session using `execv` */
  65   static Session* spawnv(const char *path, char *const argv[]);
  66
  67   /** Create a session using `execvp` */
  68   static Session* spawnvp(const char *path, char *const argv[]);
  69 };
  70
  71 // Temporary
  72 extern simgrid::mc::Session* session;
  73
  74 }
  75 }
  76
  77 #endif