examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp

   1 /* Copyright (c) 2012-2023. 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 /***************** Centralized Mutual Exclusion Algorithm *******************/
   7 /* This example implements a centralized mutual exclusion algorithm.        */
   8 /* Bug : CS requests of client 1 not satisfied                              */
   9 /* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok)          */
  10 /****************************************************************************/
  11
  12 #ifdef GARBAGE_STACK
  13 #include <fcntl.h>
  14 #include <sys/stat.h>
  15 #include <unistd.h>
  16 #endif
  17
  18 #include <simgrid/modelchecker.h>
  19 #include <simgrid/s4u.hpp>
  20 #include <xbt/dynar.h>
  21
  22 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
  23 namespace sg4 = simgrid::s4u;
  24
  25 class Message {
  26 public:
  27   enum class Kind { GRANT, REQUEST, RELEASE };
  28   Kind kind                             = Kind::GRANT;
  29   sg4::Mailbox* return_mailbox          = nullptr;
  30   explicit Message(Message::Kind kind, sg4::Mailbox* mbox) : kind(kind), return_mailbox(mbox) {}
  31 };
  32
  33 int r  = 0;
  34 int cs = 0;
  35
  36 #ifdef GARBAGE_STACK
  37 /** Do not use a clean stack */
  38 static void garbage_stack(void)
  39 {
  40   const size_t size = 256;
  41   int fd            = open("/dev/urandom", O_RDONLY);
  42   char foo[size];
  43   read(fd, foo, size);
  44   close(fd);
  45 }
  46 #endif
  47
  48 static void coordinator()
  49 {
  50   bool CS_used = false;
  51   std::queue<sg4::Mailbox*> requests;
  52
  53   sg4::Mailbox* mbox = sg4::Mailbox::by_name("coordinator");
  54
  55   while (true) {
  56     auto m = mbox->get_unique<Message>();
  57     if (m->kind == Message::Kind::REQUEST) {
  58       if (CS_used) {
  59         XBT_INFO("CS already used. Queue the request.");
  60         requests.push(m->return_mailbox);
  61       } else {
  62         if (m->return_mailbox->get_name() != "1") {
  63           XBT_INFO("CS idle. Grant immediately");
  64           m->return_mailbox->put(new Message(Message::Kind::GRANT, mbox), 1000);
  65           CS_used = true;
  66         }
  67       }
  68     } else {
  69       if (not requests.empty()) {
  70         XBT_INFO("CS release. Grant to queued requests (queue size: %zu)", requests.size());
  71         sg4::Mailbox* req = requests.front();
  72         requests.pop();
  73         if (req->get_name() != "1") {
  74           req->put(new Message(Message::Kind::GRANT, mbox), 1000);
  75         } else {
  76           requests.push(req);
  77           CS_used = false;
  78         }
  79       } else {
  80         XBT_INFO("CS release. resource now idle");
  81         CS_used = false;
  82       }
  83     }
  84   }
  85 }
  86
  87 static void client(int id)
  88 {
  89   aid_t my_pid = sg4::this_actor::get_pid();
  90
  91   sg4::Mailbox* my_mailbox = sg4::Mailbox::by_name(std::to_string(id));
  92
  93   while (true) {
  94     XBT_INFO("Ask the request");
  95     sg4::Mailbox::by_name("coordinator")->put(new Message(Message::Kind::REQUEST, my_mailbox), 1000);
  96
  97     if (id == 1) {
  98       r  = 1;
  99       cs = 0;
 100       XBT_INFO("Propositions changed : r=1, cs=0");
 101     }
 102
 103     auto grant = my_mailbox->get_unique<Message>();
 104     xbt_assert(grant->kind == Message::Kind::GRANT);
 105
 106     if (id == 1) {
 107       cs = 1;
 108       r  = 0;
 109       XBT_INFO("Propositions changed : r=0, cs=1");
 110     }
 111
 112     XBT_INFO("%d got the answer. Sleep a bit and release it", id);
 113
 114     sg4::this_actor::sleep_for(1);
 115
 116     sg4::Mailbox::by_name("coordinator")->put(new Message(Message::Kind::RELEASE, my_mailbox), 1000);
 117
 118     sg4::this_actor::sleep_for(static_cast<double>(my_pid));
 119
 120     if (id == 1) {
 121       cs = 0;
 122       r  = 0;
 123       XBT_INFO("Propositions changed : r=0, cs=0");
 124     }
 125   }
 126 }
 127
 128 static void raw_client(int id)
 129 {
 130 #ifdef GARBAGE_STACK
 131   // At this point the stack of the callee (client) is probably filled with
 132   // zeros and uninitialized variables will contain 0. This call will place
 133   // random byes in the stack of the callee:
 134   garbage_stack();
 135 #endif
 136   client(id);
 137 }
 138
 139 int main(int argc, char* argv[])
 140 {
 141   sg4::Engine e(&argc, argv);
 142
 143   MC_automaton_new_propositional_symbol_pointer("r", &r);
 144   MC_automaton_new_propositional_symbol_pointer("cs", &cs);
 145
 146   e.load_platform(argv[1]);
 147
 148   sg4::Actor::create("coordinator", e.host_by_name("Tremblay"), coordinator)
 149       ->set_kill_time(argc > 3 ? std::stod(argv[3]) : -1.0);
 150   if (std::stod(argv[2]) == 0) {
 151     sg4::Actor::create("client", e.host_by_name("Boivin"), raw_client, 1);
 152     sg4::Actor::create("client", e.host_by_name("Fafard"), raw_client, 2);
 153   } else { // "Visited" case
 154     sg4::Actor::create("client", e.host_by_name("Boivin"), raw_client, 2);
 155     sg4::Actor::create("client", e.host_by_name("Fafard"), raw_client, 1);
 156   }
 157   e.run();
 158
 159   return 0;
 160 }