src/mc/explo/odpor/WakeupTree.cpp

   1 /* Copyright (c) 2008-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 #include "src/mc/explo/odpor/WakeupTree.hpp"
   7 #include "src/mc/explo/odpor/Execution.hpp"
   8 #include "xbt/asserts.h"
   9
  10 #include <algorithm>
  11 #include <exception>
  12 #include <queue>
  13
  14 namespace simgrid::mc::odpor {
  15
  16 WakeupTree::WakeupTree() : WakeupTree(std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode({}))) {}
  17 WakeupTree::WakeupTree(std::unique_ptr<WakeupTreeNode> root) : root_(root.get())
  18 {
  19   this->insert_node(std::move(root));
  20 }
  21
  22 WakeupTree WakeupTree::new_subtree_rooted_at(WakeupTreeNode* root)
  23 {
  24   if (not root->is_single_process()) {
  25     throw std::invalid_argument("Selecting subtrees is only defined for single-process nodes");
  26   }
  27
  28   const aid_t p = (*(root->get_sequence().begin()))->aid_;
  29
  30   // Perform a BFS search to perform a deep copy of the portion
  31   // of the tree underneath and including `root`. Note that `root`
  32   // is contained within the context of a *different* wakeup tree;
  33   // hence, we have to be careful to update each node's children
  34   // appropriately
  35   auto subtree                    = WakeupTree();
  36   WakeupTreeNode* root_equivalent = subtree.make_node(root->get_sequence());
  37
  38   std::list<std::pair<WakeupTreeNode*, WakeupTreeNode*>> frontier{std::make_pair(root, root_equivalent)};
  39   while (not frontier.empty()) {
  40     auto [node_in_other_tree, subtree_equivalent] = frontier.front();
  41     frontier.pop_front();
  42
  43     // For each child of the node corresponding to that in `subtree`,
  44     // make clones of each of its children and add them to `frontier`
  45     // to that their children are added, and so on. Note that the subtree
  46     // **explicitly** removes the first process from each child
  47     for (WakeupTreeNode* child_in_other_tree : node_in_other_tree->get_ordered_children()) {
  48       auto p_w           = child_in_other_tree->get_sequence();
  49       const auto p_again = p_w.front()->aid_;
  50
  51       // INVARIANT: A nodes of a wakeup tree form a prefix-closed set;
  52       // this means that any child node `c` of a node `n` must contain
  53       // `n.get_sequence()` as a prefix of `c.get_sequence()`
  54       xbt_assert(p_again == p,
  55                  "Invariant Violation: The wakeup tree from which a subtree with actor "
  56                  "`%ld` is being taken is not prefix free! The child node starts with "
  57                  "`%ld` while the parent is `%ld`! This indicates that there "
  58                  "is a bug in the insertion logic for the wakeup tree",
  59                  p, p_again, p);
  60       p_w.pop_front();
  61
  62       WakeupTreeNode* child_equivalent = subtree.make_node(p_w);
  63       subtree_equivalent->add_child(child_equivalent);
  64       frontier.push_back(std::make_pair(child_in_other_tree, child_equivalent));
  65     }
  66   }
  67   return subtree;
  68 }
  69
  70 WakeupTreeNode* WakeupTree::make_node(const PartialExecution& u)
  71 {
  72   auto node                 = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(u));
  73   auto* node_handle         = node.get();
  74   this->nodes_[node_handle] = std::move(node);
  75   return node_handle;
  76 }
  77
  78 void WakeupTree::insert_node(std::unique_ptr<WakeupTreeNode> node)
  79 {
  80   auto* node_handle         = node.get();
  81   this->nodes_[node_handle] = std::move(node);
  82 }
  83
  84 void WakeupTree::insert(const Execution& E, const PartialExecution& w)
  85 {
  86   // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details
  87
  88   // Find the first node `v` in the tree such that
  89   // `v ~_[E] w` and `v`  is not a leaf node
  90   for (WakeupTreeNode* node : *this) {
  91     if (const auto shortest_sequence = E.get_shortest_odpor_sq_subset_insertion(node->get_sequence(), w);
  92         shortest_sequence.has_value()) {
  93       // Insert the sequence as a child of `node`, but only
  94       // if the node is not already a leaf
  95       if (not node->is_leaf()) {
  96         WakeupTreeNode* new_node = this->make_node(shortest_sequence.value());
  97         node->add_child(new_node);
  98       }
  99       // Since we're following the post-order traversal of the tree,
 100       // the first such node we see is the smallest w.r.t "<"
 101       return;
 102     }
 103   }
 104 }
 105
 106 } // namespace simgrid::mc::odpor