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