Kubernetes の Service に対するトラフィックを、ネットワーク的に近い Pod に対してルーティングする機能、Topology Aware Hints を解説しています。具体的には Node に対する Label で表現された各 Zone に対して、その Zone に存在する Node の CPU 数の比によってトラフィックのルーティング先が決まります。ルーティングのロジックはやや複雑ですが、もし興味があればスライドを参照してください。
ところで、Speaker Deck のスライドページをご覧いただくと分かる通り、今年の登壇はスライド閲覧数が異様に少ないのも特徴です。特に CloudNative Days Tokyo 2022 のスライド は、大規模イベントかつ Twitter 上でそれなりに Like されているにもかかわらず、スライド閲覧数が以前の LT の水準にすら達していません。
Backes, John, Sam Bayless, Byron Cook, Catherine Dodge, Andrew Gacek, Alan J. Hu, Temesghen Kahsai, et al. 2019. “Reachability Analysis for AWS-Based Networks.” In Computer Aided Verification, 231–41. Springer International Publishing. https://doi.org/10.1007/978-3-030-25543-5_14
Bayless, S., J. Backes, D. DaCosta, B. F. Jones, N. Launchbury, P. Trentin, K. Jewell, S. Joshi, M. Q. Zeng, and N. Mathews. 2021. “Debugging Network Reachability with Blocked Paths.” In Computer Aided Verification, 851–62. Springer International Publishing. https://doi.org/10.1007/978-3-030-81688-9_39
SMT ソルバの前提として、まず SAT ソルバについて押さえておきましょう。SAT ソルバは命題論理式の充足可能性(SATisfiability)、すなわち各変数にうまい真偽値を割り当てることで与えられた式の全体が真にできるかどうかを判定するソルバです。SAT 問題とそのソルバのアルゴリズムは古くから研究される対象であり、さまざまな高速化が知られています。反面、命題論理式しか扱うことができないため、現実の問題をエンコードすると問題のサイズが大きくなりすぎたり、元の問題の構造を失ってしまうために非効率になることも少なくありません。
このような SAT ソルバの欠点を補完して実用を意図したパフォーマンスを出すツールとして、SMT ソルバがあります。SMT ソルバでは特定の理論のソルバを別途用意します。理論に関連した部分式を命題変数に抽象化した上で、論理演算の部分のみ SAT ソルバが解き、結果を理論ソルバに渡すことで残りの部分式を解かせるという連携を行います。
ところで、ベンチマークのスライドで述べている通り、MonoSAT は複数の経路が存在するようなケースで性能が悪化することが知られています。これは MonoSAT に限らず、一般に SMT ソルバベースのソリューションで見られる傾向です。このような場合に極力パフォーマンスを悪化させないために、Header Space Analysis と呼ばれる手法も知られているのですが、それはまた別の話。
参考文献
[Bac19] Backes, John, Sam Bayless, Byron Cook, Catherine Dodge, Andrew Gacek, Alan J. Hu, Temesghen Kahsai, et al. 2019. “Reachability Analysis for AWS-Based Networks.” In Computer Aided Verification, 231–41. Springer International Publishing.
[Bay21] Bayless, S., J. Backes, D. DaCosta, B. F. Jones, N. Launchbury, P. Trentin, K. Jewell, S. Joshi, M. Q. Zeng, and N. Mathews. 2021. “Debugging Network Reachability with Blocked Paths.” In Computer Aided Verification, 851–62. Springer International Publishing.