src/mc/checker/SimcallInspector.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_INSPECTOR_HPP
   7 #define SIMGRID_MC_SIMCALL_INSPECTOR_HPP
   8
   9 #include "simgrid/forward.h"
  10
  11 #include <string>
  12
  13 namespace simgrid {
  14 namespace mc {
  15
  16 class SimcallInspector {
  17   kernel::actor::ActorImpl* issuer_;
  18
  19 public:
  20   SimcallInspector(kernel::actor::ActorImpl* issuer) : issuer_(issuer) {}
  21   kernel::actor::ActorImpl* get_issuer() { 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() { return true; }
  28
  29   /** Check whether the simcall will still be firable on this execution path
  30    *
  31    * Return true if the simcall can be fired another time, and false if it gave all its content already.
  32    *
  33    * This is not to be mixed with is_enabled(). Even if is_pending() returns true,
  34    * is_enabled() may return false at a given point but will eventually return true further
  35    * on that execution path.
  36    *
  37    * If is_pending() returns false the first time, it means that the execution path is not branching
  38    * on that transition. Only one execution path goes out of that simcall.
  39    *
  40    * is_pending() is to decide whether we should branch a new execution path with this transition while
  41    * is_enabled() is about continuing the current execution path with that transition or saving it for later.
  42    *
  43    * This function should also do the choices that the platform would have done in non-MC settings.
  44    * For example if it's a waitany, pick the communication that should finish first.
  45    * If it's a random(), choose the next value to explore.
  46    */
  47   virtual bool is_pending(int times_considered) { return false; }
  48
  49   /** Some simcalls may only be observable under some circumstances.
  50    * Most simcalls are not visible from the MC because they don't have an inspector at all. */
  51   virtual bool is_visible() { return true; }
  52   virtual std::string to_string(int times_considered);
  53   virtual std::string dot_label() = 0;
  54 };
  55
  56 class RandomSimcall : public SimcallInspector {
  57   int min_;
  58   int max_;
  59   int next_value_ = 0;
  60
  61 public:
  62   RandomSimcall(smx_actor_t actor, int min, int max) : SimcallInspector(actor), min_(min), max_(max) {}
  63   bool is_pending(int times_considered) override;
  64   std::string to_string(int times_considered) override;
  65   std::string dot_label() override;
  66   int get_value();
  67 };
  68 } // namespace mc
  69 } // namespace simgrid
  70
  71 #endif