src/mc/checker/SimcallObserver.cpp

   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 #include "src/mc/checker/SimcallObserver.hpp"
   7 #include "simgrid/s4u/Host.hpp"
   8 #include "src/kernel/activity/MutexImpl.hpp"
   9 #include "src/kernel/actor/ActorImpl.hpp"
  10
  11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation");
  12
  13 namespace simgrid {
  14 namespace mc {
  15
  16 std::string SimcallObserver::to_string(int /*time_considered*/) const
  17 {
  18   return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(),
  19                                      issuer_->get_cname());
  20 }
  21
  22 std::string SimcallObserver::dot_label() const
  23 {
  24   if (issuer_->get_host())
  25     return xbt::string_printf("[(%ld)%s] ", issuer_->get_pid(), issuer_->get_cname());
  26   return xbt::string_printf("[(%ld)] ", issuer_->get_pid());
  27 }
  28
  29 std::string RandomSimcall::to_string(int time_considered) const
  30 {
  31   return SimcallObserver::to_string(time_considered) + "MC_RANDOM(" + std::to_string(time_considered) + ")";
  32 }
  33
  34 std::string RandomSimcall::dot_label() const
  35 {
  36   return SimcallObserver::dot_label() + "MC_RANDOM(" + std::to_string(next_value_) + ")";
  37 }
  38
  39 void RandomSimcall::prepare(int times_considered)
  40 {
  41   next_value_ = min_ + times_considered;
  42   XBT_DEBUG("MC_RANDOM(%d, %d) will return %d after %d times", min_, max_, next_value_, times_considered);
  43 }
  44
  45 int RandomSimcall::get_max_consider() const
  46 {
  47   return max_ - min_ + 1;
  48 }
  49
  50 std::string MutexUnlockSimcall::to_string(int time_considered) const
  51 {
  52   return SimcallObserver::to_string(time_considered) + "Mutex UNLOCK";
  53 }
  54
  55 std::string MutexUnlockSimcall::dot_label() const
  56 {
  57   return SimcallObserver::dot_label() + "Mutex UNLOCK";
  58 }
  59
  60 std::string MutexLockSimcall::to_string(int time_considered) const
  61 {
  62   std::string res = SimcallObserver::to_string(time_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
  63   res += "(locked = " + std::to_string(mutex_->is_locked());
  64   res += ", owner = " + std::to_string(mutex_->get_owner() ? mutex_->get_owner()->get_pid() : -1);
  65   res += ", sleeping = n/a)";
  66   return res;
  67 }
  68
  69 std::string MutexLockSimcall::dot_label() const
  70 {
  71   return SimcallObserver::dot_label() + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
  72 }
  73
  74 bool MutexLockSimcall::is_enabled() const
  75 {
  76   return not blocking_ || mutex_->get_owner() == nullptr || mutex_->get_owner() == get_issuer();
  77 }
  78
  79 std::string SemAcquireSimcall::to_string(int time_considered) const
  80 {
  81   return SimcallObserver::to_string(time_considered) + "Sem ACQUIRE";
  82 }
  83
  84 std::string SemAcquireSimcall::dot_label() const
  85 {
  86   return SimcallObserver::dot_label() + "Sem ACQUIRE";
  87 }
  88
  89 bool SemAcquireSimcall::is_enabled() const
  90 {
  91   static bool warned = false;
  92   if (not warned) {
  93     XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
  94     warned = true;
  95   }
  96   return true;
  97 }
  98 } // namespace mc
  99 } // namespace simgrid