src/mc/Transition.hpp

   1 /* Copyright (c) 2015-2022. 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_TRANSITION_HPP
   8 #define SIMGRID_MC_TRANSITION_HPP
   9
  10 #include "simgrid/forward.h" // aid_t
  11 #include "src/kernel/actor/SimcallObserver.hpp"
  12 #include "src/mc/remote/RemotePtr.hpp"
  13 #include <string>
  14
  15 namespace simgrid {
  16 namespace mc {
  17
  18 /** An element in the recorded path
  19  *
  20  *  At each decision point, we need to record which process transition
  21  *  is triggered and potentially which value is associated with this
  22  *  transition. The value is used to find which communication is triggered
  23  *  in things like waitany and for associating a given value of MC_random()
  24  *  calls.
  25  */
  26 class Transition {
  27   /* Textual representation of the transition, to display backtraces */
  28   static unsigned long executed_transitions_;
  29   static unsigned long replayed_transitions_;
  30
  31   friend State; // FIXME remove this once we have a proper class to handle the statistics
  32
  33 protected:
  34   std::string textual_ = "";
  35
  36 public:
  37   aid_t aid_ = 0;
  38
  39   /* Which transition was executed for this simcall
  40    *
  41    * Some simcalls can lead to different transitions:
  42    *
  43    * * waitany/testany can trigger on different messages;
  44    *
  45    * * random can produce different values.
  46    */
  47   int times_considered_ = 0;
  48
  49   Transition() = default;
  50   Transition(aid_t issuer, int times_considered) : aid_(issuer), times_considered_(times_considered) {}
  51
  52   void init(aid_t aid, int times_considered);
  53
  54   virtual std::string to_string(bool verbose = false);
  55   const char* to_cstring(bool verbose = false);
  56
  57   /* Moves the application toward a path that was already explored, but don't change the current transition */
  58   void replay() const;
  59
  60   virtual bool depends(const Transition* other) const { return true; }
  61
  62   /* Returns the total amount of transitions executed so far (for statistics) */
  63   static unsigned long get_executed_transitions() { return executed_transitions_; }
  64   /* Returns the total amount of transitions replayed so far while backtracing (for statistics) */
  65   static unsigned long get_replayed_transitions() { return replayed_transitions_; }
  66 };
  67
  68 class CommSendTransition;
  69 class CommRecvTransition;
  70
  71 class CommWaitTransition : public Transition {
  72   bool timeout_;
  73   void* comm_;
  74   aid_t sender_;
  75   aid_t receiver_;
  76   unsigned mbox_;
  77   void* src_buff_;
  78   void* dst_buff_;
  79   size_t size_;
  80   friend CommSendTransition;
  81   friend CommRecvTransition;
  82
  83 public:
  84   CommWaitTransition(aid_t issuer, int times_considered, char* buffer);
  85   std::string to_string(bool verbose) override;
  86   bool depends(const Transition* other) const override;
  87 };
  88
  89 class CommRecvTransition : public Transition {
  90   unsigned mbox_;
  91   void* dst_buff_;
  92
  93 public:
  94   CommRecvTransition(aid_t issuer, int times_considered, char* buffer);
  95   std::string to_string(bool verbose) override;
  96   bool depends(const Transition* other) const override;
  97 };
  98
  99 class CommSendTransition : public Transition {
 100   unsigned mbox_;
 101   void* src_buff_;
 102   size_t size_;
 103
 104 public:
 105   CommSendTransition(aid_t issuer, int times_considered, char* buffer);
 106   std::string to_string(bool verbose) override;
 107   bool depends(const Transition* other) const override;
 108 };
 109
 110 /** Make a new transition from serialized description */
 111 Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
 112                             char* buffer);
 113
 114 } // namespace mc
 115 } // namespace simgrid
 116
 117 #endif