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 } // namespace mc
  92 } // namespace simgrid
  93
  94 #endif