Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
some symbol renamings to make MC easier to understand (to me)
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sat, 20 Mar 2021 21:45:14 +0000 (22:45 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Sat, 20 Mar 2021 21:54:39 +0000 (22:54 +0100)
src/mc/mc_base.cpp
src/mc/mc_base.hpp
src/mc/mc_record.cpp
src/mc/remote/AppSide.cpp
src/mc/remote/AppSide.hpp

index da5d3bf..1ed05dc 100644 (file)
@@ -40,7 +40,7 @@ int MC_random(int min, int max)
 namespace simgrid {
 namespace mc {
 
-void wait_for_requests()
+void execute_actors()
 {
 #if SIMGRID_HAVE_MC
   xbt_assert(mc_model_checker == nullptr, "This must be called from the client");
index 30d4d15..ca4806b 100644 (file)
@@ -18,7 +18,7 @@ namespace mc {
  *  iteratively until there doesn't remain any. At this point, the function
  *  returns to the caller which can handle the visible (and ready) simcalls.
  */
-XBT_PRIVATE void wait_for_requests();
+XBT_PRIVATE void execute_actors();
 
 XBT_PRIVATE extern std::vector<double> processes_time;
 
index 46d642f..e09251e 100644 (file)
@@ -23,7 +23,7 @@ namespace mc {
 
 void replay(RecordTrace const& trace)
 {
-  simgrid::mc::wait_for_requests();
+  simgrid::mc::execute_actors();
 
   for (simgrid::mc::Transition const& transition : trace) {
     XBT_DEBUG("Executing %i$%i", transition.pid_, transition.times_considered_);
@@ -40,7 +40,7 @@ void replay(RecordTrace const& trace)
 
     // Execute the request:
     simcall->issuer_->simcall_handle(transition.times_considered_);
-    simgrid::mc::wait_for_requests();
+    simgrid::mc::execute_actors();
   }
 }
 
index f822160..3279cf1 100644 (file)
@@ -89,11 +89,7 @@ void AppSide::handle_deadlock_check(const s_mc_message_t*) const
   s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, deadlock};
   xbt_assert(channel_.send(answer) == 0, "Could not send response");
 }
-void AppSide::handle_continue(const s_mc_message_t*) const
-{
-  /* Nothing to do */
-}
-void AppSide::handle_simcall(const s_mc_message_simcall_handle_t* message) const
+void AppSide::handle_simcall_execute(const s_mc_message_simcall_handle_t* message) const
 {
   kernel::actor::ActorImpl* process = kernel::actor::ActorImpl::by_pid(message->pid_);
   xbt_assert(process != nullptr, "Invalid pid %lu", message->pid_);
@@ -115,7 +111,7 @@ void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) cons
 
 void AppSide::handle_messages() const
 {
-  while (true) {
+  while (true) { // Until we get a CONTINUE message
     XBT_DEBUG("Waiting messages from model-checker");
 
     std::array<char, MC_MESSAGE_LENGTH> message_buffer;
@@ -132,12 +128,11 @@ void AppSide::handle_messages() const
 
       case MessageType::CONTINUE:
         assert_msg_size("MESSAGE_CONTINUE", s_mc_message_t);
-        handle_continue(message);
         return;
 
       case MessageType::SIMCALL_HANDLE:
         assert_msg_size("SIMCALL_HANDLE", s_mc_message_simcall_handle_t);
-        handle_simcall((s_mc_message_simcall_handle_t*)message_buffer.data());
+        handle_simcall_execute((s_mc_message_simcall_handle_t*)message_buffer.data());
         break;
 
       case MessageType::SIMCALL_IS_VISIBLE: {
@@ -199,7 +194,7 @@ void AppSide::handle_messages() const
 void AppSide::main_loop() const
 {
   while (true) {
-    simgrid::mc::wait_for_requests();
+    simgrid::mc::execute_actors();
     xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send WAITING message to model-checker");
     this->handle_messages();
   }
index a647b32..9d5b53c 100644 (file)
@@ -31,8 +31,7 @@ public:
 
 private:
   void handle_deadlock_check(const s_mc_message_t* msg) const;
-  void handle_continue(const s_mc_message_t* msg) const;
-  void handle_simcall(const s_mc_message_simcall_handle_t* message) const;
+  void handle_simcall_execute(const s_mc_message_simcall_handle_t* message) const;
   void handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const;
 
 public: