src/mc/checker/SimcallObserver.hpp

   1 /* Copyright (c) 2019-2021. 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_SIMCALL_OBSERVER_HPP
   7 #define SIMGRID_MC_SIMCALL_OBSERVER_HPP
   8
   9 #include "simgrid/forward.h"
  10
  11 #include <string>
  12
  13 namespace simgrid {
  14 namespace mc {
  15
  16 class SimcallObserver {
  17   kernel::actor::ActorImpl* const issuer_;
  18
  19 public:
  20   explicit SimcallObserver(kernel::actor::ActorImpl* issuer) : issuer_(issuer) {}
  21   kernel::actor::ActorImpl* get_issuer() const { return issuer_; }
  22   /** Whether this transition can currently be taken without blocking.
  23    *
  24    * For example, a mutex_lock is not enabled when the mutex is not free.
  25    * A comm_receive is not enabled before the corresponding send has been issued.
  26    */
  27   virtual bool is_enabled() const { return true; }
  28
  29   /** Returns the amount of time that this transition can be used.
  30    *
  31    * If it's 1 (as with send/wait), there is no need to fork the state space exploration on this point.
  32    * If it's more than one (as with mc_random or waitany), we need to consider this transition several times to start
  33    * differing branches
  34    */
  35   virtual int get_max_consider() const { return 1; }
  36
  37   /** Prepares the simcall to be used.
  38    *
  39    * For most simcalls, this does nothing. Once enabled, there is nothing to do to prepare a send().
  40    *
  41    * It is useful only for the simcalls that can be used several times, such as waitany() or random().
  42    * For them, prepare() selects the right outcome for the time being considered.
  43    *
  44    * The first time a simcall is considered, times_considered is 0, not 1.
  45    */
  46   virtual void prepare(int times_considered) { /* Nothing to do by default */}
  47
  48   /** Some simcalls may only be observable under some circumstances.
  49    * Most simcalls are not visible from the MC because they don't have an observer at all. */
  50   virtual bool is_visible() const { return true; }
  51   virtual std::string to_string(int times_considered) const = 0;
  52   virtual std::string dot_label() const                     = 0;
  53 };
  54
  55 class RandomSimcall : public SimcallObserver {
  56   const int min_;
  57   const int max_;
  58   int next_value_ = 0;
  59
  60 public:
  61   RandomSimcall(smx_actor_t actor, int min, int max) : SimcallObserver(actor), min_(min), max_(max) {}
  62   int get_max_consider() const override;
  63   void prepare(int times_considered) override;
  64   std::string to_string(int times_considered) const override;
  65   std::string dot_label() const override;
  66   int get_value() const { return next_value_; }
  67 };
  68
  69 class MutexUnlockSimcall : public SimcallObserver {
  70   using SimcallObserver::SimcallObserver;
  71
  72 public:
  73   std::string to_string(int times_considered) const override;
  74   std::string dot_label() const override;
  75 };
  76
  77 class MutexLockSimcall : public SimcallObserver {
  78   kernel::activity::MutexImpl* const mutex_;
  79   const bool blocking_;
  80
  81 public:
  82   MutexLockSimcall(smx_actor_t actor, kernel::activity::MutexImpl* mutex, bool blocking = true)
  83       : SimcallObserver(actor), mutex_(mutex), blocking_(blocking)
  84   {
  85   }
  86   bool is_enabled() const override;
  87   std::string to_string(int times_considered) const override;
  88   std::string dot_label() const override;
  89   kernel::activity::MutexImpl* get_mutex() const { return mutex_; }
  90 };
  91
  92 class ConditionWaitSimcall : public SimcallObserver {
  93   kernel::activity::ConditionVariableImpl* const cond_;
  94   kernel::activity::MutexImpl* const mutex_;
  95   const double timeout_;
  96
  97 public:
  98   ConditionWaitSimcall(smx_actor_t actor, kernel::activity::ConditionVariableImpl* cond,
  99                        kernel::activity::MutexImpl* mutex, double timeout = -1.0)
 100       : SimcallObserver(actor), cond_(cond), mutex_(mutex), timeout_(timeout)
 101   {
 102   }
 103   bool is_enabled() const override;
 104   bool is_visible() const override { return false; }
 105   std::string to_string(int times_considered) const override;
 106   std::string dot_label() const override;
 107   kernel::activity::ConditionVariableImpl* get_cond() const { return cond_; }
 108   kernel::activity::MutexImpl* get_mutex() const { return mutex_; }
 109   double get_timeout() const { return timeout_; }
 110 };
 111
 112 class SemAcquireSimcall : public SimcallObserver {
 113   kernel::activity::SemaphoreImpl* const sem_;
 114   const double timeout_;
 115
 116 public:
 117   SemAcquireSimcall(smx_actor_t actor, kernel::activity::SemaphoreImpl* sem, double timeout = -1.0)
 118       : SimcallObserver(actor), sem_(sem), timeout_(timeout)
 119   {
 120   }
 121   bool is_enabled() const override;
 122   bool is_visible() const override { return false; }
 123   std::string to_string(int times_considered) const override;
 124   std::string dot_label() const override;
 125   kernel::activity::SemaphoreImpl* get_sem() const { return sem_; }
 126   double get_timeout() const { return timeout_; }
 127 };
 128
 129 class ExecutionWaitanySimcall : public SimcallObserver {
 130   const std::vector<kernel::activity::ExecImpl*>* const execs_;
 131   const double timeout_;
 132
 133 public:
 134   ExecutionWaitanySimcall(smx_actor_t actor, const std::vector<kernel::activity::ExecImpl*>* execs, double timeout)
 135       : SimcallObserver(actor), execs_(execs), timeout_(timeout)
 136   {
 137   }
 138   bool is_visible() const override { return false; }
 139   std::string to_string(int times_considered) const override;
 140   std::string dot_label() const override;
 141   const std::vector<kernel::activity::ExecImpl*>* get_execs() const { return execs_; }
 142   double get_timeout() const { return timeout_; }
 143 };
 144 } // namespace mc
 145 } // namespace simgrid
 146
 147 #endif