チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

VPC Reachability Analyzer と形式手法

こんにちは、チェシャ猫です。

先日開催された AWS Dev Day Online Japan 2021 で、AWSVPC Reachability Analyzer とそのバックエンドである Tiros について発表してきました。公募 CFP 枠です。

講演概要

このプレゼンの大きな目標は、VPC Reachability Analyzer のバックエンドである検査エンジン Tiros の論文 [Bac19] を解説することです。そのための道筋として、Section 1 で VPC Reachability Analyzer の機能を簡単に紹介した後、Section 2 でその要素技術である SMT ソルバの仕組みを解説し、最後に Section 3 として VPC ネットワークの意味論を SMT ソルバ用にエンコーディングする方針について解説します。

VPC Reachability Analyzer

AWS 上でネットワークが意図通りの挙動を示さない時、トラブルシュートには二つの方針があります。一つは nc をはじめとするネットワーク形のコマンドを用いて実際にパケットを送信してみることであり、もう一つは AWS マネジメントコンソールから設定ミスを見つけることです。しかし、実際にこの辺りのトラブルシュートを経験したことがある方はご存知の通り、いずれもそれなりの前提知識が必要で、いわゆる「職人芸」になりがちな部分でもあります。

2020 年 12 月、そんなトラブルシューティングに便利な機能が AWS から発表されました。VPC Reachability Analyzer です。この機能では、通信の送信元と送信先を指定することで、その間の通信が到達可能になるかどうかを自動的に判定することができます。また、到達可能でない場合には原因となっているコンポーネントの特定も可能です。

f:id:y_taka_23:20210930211652p:plain
VPC Reachability Analyzer による到達可能性の判定

VPC Reachability Analyzer が面白いのは、Packet Probing と呼ばれる実際にパケットの送信を行うタイプの古典的な検査とは異なり、設定項目のみからを読み取って推論を行うところです。いわば AWS のネットワーク設定が持つ「意味」を理解して結論を出しているとも言えます。この特徴があるため、実際のプロダクション環境で検査を行っても帯域に悪影響を与えることがなく、また到達不可能な場合に「どこを修正すれば到達できるか」まで含めた情報を得ることができます。

VPC Reachability Analyzer については、今回解説する論文の他にも AWS からいくつか資料が出てきます。

SAT ソルバと SMT ソルバ

それでは、VPC Reachability Analyzer が実際の通信を行うことなく到達性を「推論」できるのはなぜでしょうか? この秘密は内部で SMT ソルバを呼び出していることにあります。

SMT ソルバの前提として、まず SAT ソルバについて押さえておきましょう。SAT ソルバは命題論理式の充足可能性(SATisfiability)、すなわち各変数にうまい真偽値を割り当てることで与えられた式の全体が真にできるかどうかを判定するソルバです。SAT 問題とそのソルバのアルゴリズムは古くから研究される対象であり、さまざまな高速化が知られています。反面、命題論理式しか扱うことができないため、現実の問題をエンコードすると問題のサイズが大きくなりすぎたり、元の問題の構造を失ってしまうために非効率になることも少なくありません。

このような SAT ソルバの欠点を補完して実用を意図したパフォーマンスを出すツールとして、SMT ソルバがあります。SMT ソルバでは特定の理論のソルバを別途用意します。理論に関連した部分式を命題変数に抽象化した上で、論理演算の部分のみ SAT ソルバが解き、結果を理論ソルバに渡すことで残りの部分式を解かせるという連携を行います。

f:id:y_taka_23:20210930212857p:plain
SMT ソルバにおける SAT ソルバと理論ソルバの連携

実際には、現代の実用的な SMT ソルバでは SAT 部分と理論部分は完全に独立して動作するわけではなく、SAT ソルバが命題変数への真偽割り当てを探索する過程で理論ソルバのアルゴリズムが介入することで探索空間を減らし、パフォーマンスを上げる工夫が入っています。このようなタイプの SMT ソルバは Lazy SMT と呼ばれたりします。

このあたりの詳細に興味がある人は、参考文献 [Seb07] を参照してください。Lazy SMT に関する包括的なサーベイ論文です。

MonoSAT によるエンコーディング

AWS の内部でも SMT ソルバが使用されています。冒頭に挙げた VPC Reachability Analyzer もその一つで、Tiros と呼ばれる内部のエンジンが SMT ソルバの一種である MonoSAT をバックエンドとして使用しています。

論文中には、Tiros は MonoSAT 以外の実装の候補として、Datalog 処理系 Soufflé [Sub19] と一階述語論理の自動定理証明器 Vampire [Kot18] が提案されており、それぞれが VPC をどのようにモデル化したのかについて述べられています。大規模ベンチマークの結果としては MonoSAT が多くの場合に最速ですが、Soufflé では MonoSAT では実装できないタイプのクエリが存在する点に言及されています。具体的には純粋なネットワークの接続以外の、例えば EC2 インスタンスのタグに言及するようなクエリがその例です。

Tiros が MonoSAT を用いて VPC ネットワークの意味論を検査するさいには、MonoSAT が持っているグラフ理論用の理論ソルバを使用します。具体的には EC2 インスタンスや ENI、セキュリティグループなどのコンポーネントをノードとし、ENI とセキュリティブループ間のようなアタッチ関係をエッジとします。このとき、やはり MonoSAT が持つビットベクトルの理論ソルバを使ってコンポーネントを通過できるパケット条件を記述することで、パケットの到達可能性はグラフの到達可能性として検査することが可能になります。

f:id:y_taka_23:20210930212020p:plain
ビットベクトルによる Security Group の表現

ところで、MonoSAT が持つグラフ理論の理論ソルバは、汎用の SMT ソルバとしては特殊なものです。逆に言えばなぜ MonoSAT はグラフの理論ソルバを実装しているのでしょうか?

この答えは MonoSAT の提案論文である参考文献 [Bay15] に述べられています。ここで鍵になるのはと Boolean Monotonic Theories と呼ばれる理論のクラスです。Boolean Monotonic な理論では述語や関数の引数が真偽値に限定されており、かつ述語 p に対して以下の性質が成り立ちます。


    p(..., s_{i-1}, 0, s_{i+1}, ...) \rightarrow p(..., s_{i-1}, 1, s_{i+1}, ...)

つまり、その述語がある変数を偽としたときに成立するのであれば、その変数を真に変えたときでもやはり成立する、という性質です。

今回考えているグラフの到達可能性は、この Monotonic の性質を満たす述語です。実際、あるエッジが偽(接続しない)の状態で到達可能なノード同士は、そのエッジを真(接続する)に変更したとしてもやはり到達可能です。また、MonoSAT が実装している到達性以外の述語、例えば最小スパニング木の生成などについてもこの性質が成り立ちます。

理論が Monotonic である場合、理論ソルバ側の原子命題への部分的な真偽割り当てが与えられた段階で、残りをすべて真で埋めてしまって理論ソルバで検証することが可能になります。なぜなら、そうして得られた結果が充足不可能であれば、部分的な割り当ての時点で既に充足不可能であることがわかるからです。逆に、すべて偽で埋めた状況で充足可能が確定すれば、残りの変数の真偽はどちらでも問題ないことがわかります。いわば、上下からおおざっぱな評価をしてみて情報を引き出していると言えるでしょう。これを利用して探索空間を絞るのが MonoSAT の、ひいては Tiros の戦略です。

Blocked Path の検出

これは当日のプレゼンに入れられなかった補足なのですが、今年に入ってから Tiros の機能を拡張する論文 [Bay21] が出ており、しかもこの論文は VPC Reachability Analyzer に直接関係しています。具体的には、接続できない場合に原因となっているコンポーネントを検出する方法について示した論文です。

一般には、MonoSAT で到達不可能であることが示された場合、何が原因であるかは明らかではありません。理論ソルバ側が充足不可能だった場合には矛盾が生じた式の集合を返してくるため、そこから修正すべき原因を引き出してユーザに情報を提示することになります。

ここで一筋縄でいかないのは、最終的な出力として何を残す必要があるかによってアルゴリズムが変わることです。前述の論文ではこの「到達不可能な原因」を以下の 3 種類に分類しています。

  • ユーザがコンポーネントの設定を変更できるもの
  • Local Route など、変更できないが情報としては必要なもの
  • 検査の過程で機械的に変換された変数など、提示する意味がないもの

そして、それぞれに対して「最小の矛盾集合」を段階的に得るアルゴリズムとその正当性を示す流れが論文の骨子です。

サンプル構成

今回サンプルとして使用した EC2 インスタンス 3 個からなる構成は、以下の CloudFormation テンプレートから作成することができます。なお、このテンプレートを使用することで生じた問題には一切責任は持てません。特に、小さいとはいえ実際のインスタンスを立てること、また VPC Reachability Analyzer の実行には安くない料金(0.1 USD / 検査)がかかることに注意してください。

---
Description: 'Demo for AWS Dev Day 2021: Breakout Session G-4'
AWSTemplateFormatVersion: 2010-09-09

Mappings:
  RegionMap:
    ap-northeast-1:
      execution: ami-02892a4ea9bfa2192

Resources:
  VPC:
    Type: AWS::EC2::VPC
    Properties:
      CidrBlock: 172.0.0.0/16

  SubnetX:
    Type: AWS::EC2::Subnet
    Properties:
      VpcId: !Ref VPC
      CidrBlock: 172.0.1.0/24

  SubnetY:
    Type: AWS::EC2::Subnet
    Properties:
      VpcId: !Ref VPC
      CidrBlock: 172.0.2.0/24

  SecurityGroup1:
    Type: AWS::EC2::SecurityGroup
    Properties:
      GroupDescription: 'Allow SSH from inside of the VPC'
      VpcId: !Ref VPC
      SecurityGroupIngress:
        - CidrIp: !GetAtt VPC.CidrBlock
          IpProtocol: "tcp"
          FromPort: 22
          ToPort: 22
      SecurityGroupEgress:
        - CidrIp: 0.0.0.0/0
          IpProtocol: "-1"

  SecurityGroup2:
    Type: AWS::EC2::SecurityGroup
    Properties:
      GroupDescription: 'Deny all incomming accesses'
      VpcId: !Ref VPC
      SecurityGroupEgress:
        - CidrIp: 0.0.0.0/0
          IpProtocol: "-1"

  InstanceA:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetX
      SecurityGroupIds:
        - !Ref SecurityGroup1
      Tags:
        - Key: Name
          Value: InstanceA

  InstanceB:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetY
      SecurityGroupIds:
        - !Ref SecurityGroup1
      Tags:
        - Key: Name
          Value: InstanceB

  InstanceC:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetY
      SecurityGroupIds:
        - !Ref SecurityGroup2
      Tags:
        - Key: Name
          Value: InstanceC

  ReachablePath:
    Type: AWS::EC2::NetworkInsightsPath
    Properties:
      Source: !Ref InstanceA
      Destination: !Ref InstanceB
      DestinationPort: 22
      Protocol: tcp

  UnreachablePath:
    Type: AWS::EC2::NetworkInsightsPath
    Properties:
      Source: !Ref InstanceA
      Destination: !Ref InstanceC
      DestinationPort: 22
      Protocol: tcp

まとめ

以上、AWSVPC ネットワークにおいて、トラブルシューティングを自動化するのに便利な機能 VPC Reachability Analyzer と、そのバックエンドである Tiros、さらにその背後にある SMT ソルバ MonoSAT の特性について解説しました。

ところで、ベンチマークのスライドで述べている通り、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.
  • [Bay15] Bayless, Sam, Noah Bayless, Holger Hoos, and Alan Hu. 2015. “SAT Modulo Monotonic Theories.” Proceedings of the AAAI Conference on Artificial Intelligence 29 (1). https://ojs.aaai.org/index.php/AAAI/article/view/9755.
  • [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.
  • [Kot18] Kotelnikov, Evgenii. 2018. “Automated Theorem Proving with Extensions of First-Order Logic.” search.proquest.com. https://search.proquest.com/openview/2407fa8ebeb24157d4348884a5d03dd5/1?pq-origsite=gscholar&cbl=18750&diss=y.
  • [Seb07] Sebastiani, Roberto. 2007. “Lazy Satisfiability Modulo Theories.” Journal on Satisfiability, Boolean Modeling and Computation 3 (3-4): 141–224.
  • [Sub19] Subotic, Pavle. 2019. “Scalable Logic Defined Static Analysis.” Doctoral, UCL (University College London). https://discovery.ucl.ac.uk/id/eprint/10067190/.

CI/CD Conference 2021 で Zelkova の論文について話してきました

こんにちは、チェシャ猫です。

先日開催された CI/CD Conference 2021 で、AWS の IAM Access Anazlyer のバックエンドとして使用されている検査エンジン Zelkova、およびその元となった論文について発表してきました。公募 CFP 枠です。

発表の大筋は、少し前に July Tech Festa 2021 で登壇した際のものと共通です。関連リンク集などは以下の記事にまとめてあるので、よかったらこちらも合わせてお読みください。

ccvanishing.hateblo.jp

内容面では、前回の発表時間 20 分に対して今回は 40 分の枠をもらっていたので、

  • Level 1-3 として定式化した「検査水準」とツールの対応を明確にすること
  • Zelkova による IAM Policy の SMT エンコードについてより具体的に述べること

の 2 点を中心に内容の整理・再構成を行いました。特に後者についてはスライドの構成に大幅に手を入れたので、前回よりかなり分かりやすいプレゼンになったのではないかと自負しています。

なお、スライド中にも宣伝を入れた通り、AWS の「もう一つの推論エンジン」であるネットワーク検査エンジン Tiros については、AWS Dev Day Online 2021 で詳しくお話しする予定です。Z3 のみをバックエンドとする Zelkova と異なり、Tiros では MonoSATSoufflé、そして Vampire という複数のソルバを組み合わせて推論を行うのですが、それはまた別の話。

aws.amazon.com

July Tech Festa 2021 で IAM Access Analyzer と Zelkova について話してきました

こんにちは、チェシャ猫です。

先日開催された July Tech Festa 2021 で、AWS のアクセス制御検査ツール Zelkova について発表してきました。公募 CFP 枠です。

techfesta.connpass.com

講演概要

www.youtube.com

一般に、AWS 上のリソース設定を変更したときに何が起こるのかを事前に検査するのは難しい作業です。特に、複数の設定がマージされた結果として最終的なアクセス許可が決まるような場合、単独の項目をルールベースでチェックするだけでは限界があります。

今回の発表中では、インフラに対する検査の水準を以下の 3 つのレベルに分けて定式化しました。

  • Level 1:構文論的な検査。テンプレートが文法的に正しいかどうかを確かめる
  • Level 2ヒューリスティックな検査。意図した性質が成り立つかどうかを、特定の設定項目に関する条件として書き下した上で、その条件を確かめる
  • Level 3:意味論的な検査。意図した性質が成り立つかどうかを直接確かめる

ここで言う Level 3 の検査を実現するのが Automated Reasoning と呼ばれる技術です。設定ファイルの個別の項目をテストするのではなく、設定ファイルに記述された内容から最終的に意図した性質が成り立つかどうかを「自動的に推論」してくれます。

今回紹介した IAM Access Analyzer は、エンドユーザが Automated Reasoning を利用できる面白い機能です。例えば S3 BucketBucket Policy を変更したい場合、適用する前にプレビューの段階で、外部からの不用意なアクセスが許可されているなどのセキュリティ的な問題を検出できます。

IAM Access Analyzer の基礎になっているのは Zelkova と呼ばれるエンジンで、さらにその内部では SMT ソルバである Z3 が検査を行っています。発表中に述べた Zelkova の実装に関する情報は、以下の論文に基づきます。

ieeexplore.ieee.org

参考リンク

IAM Access Analyzer

IAM Access Analyzer 自体は無料で利用することができます。いくつかのリソースに対してアクセス権限の検査ができるようになっていますが、実験する場合は S3 BucketBucket Policy で試すのが最も簡単で、結果もわかりやすいと思います。

docs.aws.amazon.com

aws.amazon.com

例えば、Bucket Policy を用いてアクセス元として 11.22.33.0/24 を Allow し、11.22.33.44/32 を Deny した場合、Deny の方が CIDR の狭いため Access Analyzer はこれを過剰なアクセス許可としてプレビュー段階で検知します。しかしこれを逆にして 11.22.33.44/32 を Allow し 11.22.33.0/24 を Deny するよう書き換えると、今度は Deny の方が Allow を覆い隠す形になるため指摘は消えます。

このことから、Access Analyzer は CIDR 指定を単なる文字列として比較しているわけではなく、包含関係を考慮した上で最終的な権限の状態を推論していることがわかります。

f:id:y_taka_23:20210719070838p:plain
IAM Access Analyzer による意味論的検査 (スライド p.9)

SMT ソルバ

SAT ソルバや SMT ソルバの仕組みについては、以下のスライドがわかりやすく非常におすすめです。

www.slideshare.net

今回紹介した Zelkova には、SMT ソルバとして Z3 が組み込まれています。Z3 は Microsoft Research により開発されたソルバで、SMT ソルバとしては CVC と並んで非常にメジャーなものです。

github.com

オンラインで Z3 を実行できるチュートリアルサイトもあります。Zelkova で使用されている文字列やビットベクトルの理論もチュートリアルに含まれているので、実際に動作させてみると理解が深まるでしょう。

rise4fun.com

Zelkova / Tiros

発表中に名前を挙げた Zelkova や Tiros のような、数学的なバックグラウンドに立脚した AWS のセキュリティ検証の取り組みは、Provable Security というくくりで特設サイトにまとめられています。

aws.amazon.com

Zelkova に関連した記事はいくつかありますが、とりあえずのとっかかりとしてはこの記事から目を通すとよいです。

www.allthingsdistributed.com

文章よりも動画が好きだ、という人は以下のふたつをどうぞ。前者はビジネス層向けにポップにまとめられ CMクリップ、後者は re:Inforce 2019 のフルセッションです。

www.youtube.com

www.youtube.com

冒頭にも挙げましたが、今回の発表の後半部分は以下の Zelkova の論文が元になっています。発表中に盛り込めなかった SMT エンコーディングのディティールや具体例も載っています。検索すれば PDF も見つかります。

ieeexplore.ieee.org

まとめ

以上、簡単ですが July Tech Festa 2021 の登壇報告と、関連情報のリンクをまとめました。

AWS の検査エンジン Zelkova は、IAM Policy を SMT ソルバ用にエンコーディングすることで、実際のアクセスを伴わずに AWS リソースに対するアクセス権限の検査を行うことができます。またエンドユーザの立場では、IAM Access Analyzer を介して Zelkova に問い合わせることで、設定を変更する前にセキュリティ的な問題の有無を確認することが可能です。

今回は時間の都合もあって Zelkova をメインに据えましたが、Tiros も面白い技術です。SMT ソルバ(とその拡張)で完結している Zelkova と異なり、Tiros では SMT ソルバ MonoSAT 以外に、Datalog 互換のソルバ Soufflé と古典一階述語論理の証明器 Vampire を合わせた三種類を用途に応じて使い分けます。こちらも機会があれば是非どこかでお話ししたいのですが、それはまた別の話。

DevOpsDays Tokyo 2021 で Infrastructure as Code のテストについて話してきました

こんにちは、チェシャ猫です。

先日開催された DevOpsDays Tokyo 2021 で Infrastructure as Code のテストについて発表してきました。公募 CFP 枠です。

今回の発表は、昨年の CloudOperatorDays Tokyo 2020 での講演をほぼそのまま再現しています。内容については前回登壇時に詳細な解説記事を書いたので、こちらもご参照ください。

ccvanishing.hateblo.jp

オンサイト登壇

ここしばらく、どのカンファレンスもリモート開催がデフォルトになっていましたが、今回は久しぶりに会場まで行って登壇してきました。最後にオンサイトでプレゼンしたのが 2020 年の 3 月 26 日 なので、実に 1 年ぶりです。

f:id:y_taka_23:20210416164012j:plain

実際には会場で参加していたのはほぼ関係者オンリーで、各ホールに数人ずつといった程度の人数でした。ただ登壇する側としてはマイクを持って物理的に対面して話すのことの効果は大きく、久々に自分の本来のペースが出せたので非常に良かったです。個人的には、他のイベントでもせめて登壇側はオンサイトで話せる仕組みができると良いなと感じます。*1

前回からの差分

昨年 CloudOperatorDays の登壇からやや時間は経っていますが、主たるテーマである「IaC はなぜ辛いのか」「それを解決するために何をテストすべきか」という問題意識は今も変わっていないため、スライドも大部分は前回と同じものを使用しています。

ただし、CloudFormation Guard が 2020 年 10 月に一般利用可能 (GA) になったことを受けて記述をマイナーチェンジしました。前回の時点では開発プレビュー版だったこともあり、cfn-guard コマンドのインストールには Rust のソースコードからのビルドが必要でした。現在はバイナリリリース版が利用可能で、またセキュリティ用の設定が必要であればサンプルファイルも提供されています。

github.com

cfn-nag と CloudFormation Guard を比較する上で最も大きな差はルールのカスタマイズ性です。とりあえずセキュリティのベストプラクティスだけでも網羅的に当てておきたければ cfn-nag を、ルール追加やカスタマイズが必要であれば CloudFormation Guard を、という感じになるかなと思います。

なお、CloudFormation Guard は既存の Template からルールを生成する機能を持っていますが、これはあまり期待しない方がよいです。ポリシーとして記述したいであろう内容と、cfn-guard機械的に検出した条件はニュアンスが一致しないことも多いため、実用に足るポリシーはやはり人間が確認した上で書くことになりそうです。

まとめ

以上、簡単ではありますが DevOpsDays Tokyo 2021 での登壇報告でした。

余談ですが、講演後チャットで GCP + Terraform の場合はどうなるのかという質問を頂きました。AWS CDK の姉妹プロジェクトとして Hashicorp 社によって「Terraform 用の CDK」も開発されています。さらに、今回紹介した Conftest は、HCL や Dockerfile など YAML 以外のファイル形式もサポートしています。

github.com

というわけで、今回お話ししたような内容と Terraform との組み合わせもどこかで話せたら面白いかなと思っていますが、それはまた別の話。

*1:ただしその分、今回のように参加費が高くなるのも事実。

July Tech Festa 2021 winter で CockroachDB と TLA+ について話してきました

こんにちは、チェシャ猫です。

インフラ技術のカンファレンス July Tech Festa 2021 winter で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。

www.youtube.com

今回の登壇は、昨年の CloudNative Days Tokyo 2020 と同じ題材を扱っています。ただ、前回より持ち時間が長くなった分、前回のスライドで説明不足だった部分を拡充してあります。特に、CockroachDB 以外の TLA+ 採用事例や、分散システムにおける Chaos Engineering の位置付けについて解説を追加しました。

なお、前回の登壇報告は以下の記事をご参照ください。

ccvanishing.hateblo.jp

当日出た質問

実時間を含む性質

今回の時相論理では「いつか成り立つ」という性質を記述していたが、時間制限をつけて「n 分以内に成り立つ」いう記述は可能ですか?

いいえ、TLA+ では「何らかの条件 B が成り立つより前に A が成り立つ」という記述はできますが、「n 分以内」のような実際の時間に言及するような記述はサポートしていません。

ただ TLA+ 以外だとこのような性質を記述・検査できるツールも存在します。実時間モデル検査と呼ばれる分野で、有名なツールとしては商用製品ですが UPPAAL が挙げられます。スライド中で「ベースとする数学的対象によってツールの性質が変わる」という話を出しましたが、UPPAAL は時間オートマトン (Timed Automata) をベースにしています。

事例の詳細

その他の TLA+ 採用事例についてもう少し具体的に知りたいです

スライド中に挙げた事例については、以下のリンクが参考になると思います。

AWS DynamoDB

cacm.acm.org

Azure Cosmos DB

github.com

TiDB / TiKV

github.com

Elasticsearch

github.com

学習リソース

形式手法の勉強をしようとすると情報が少なくて困るのですが、TLA+ を勉強する際に良い資料はありますか?

本家である Lamport が自身の Web ページ上にチュートリアルを公開しています。ご本人による動画による解説付きです。やや題材が硬派というか地味な感じですが、TLA+ の機能は最もしっかり解説されているように思います。

また、とりあえず動かしてみて雰囲気を掴みたいということであれば、以下のチュートリアルサイトも小綺麗で良い感じです。このサイトの作者 Hillel Wayne はCockroach Lab 社で TLA+ のセミナーを開催したとのことで、まさに今回の CockroachDB の事例のきっかけを作った人物です。

まとめ

以上、簡単ではありますが、July Tech Festa 2021 winter での登壇と、当日出た質問についてまとめました。

なお、今回の講演で解説した内容は、説明を簡略化するために実際の仕組みを省略している部分がいくつか存在します。もしオリジナル版に興味がある方は、GitHub で公開されている TLA+ 仕様記述を読み解いてみるのも面白いでしょう。

github.com

ところで、講演中に OSS の事例として挙げた TiDB と Elasticsearch は、「TLA+ だけでなく他の手法と組み合わせて検証を行なっている」という点でも興味深いプロジェクトです。TiDB が Chaos Mesh を開発していることはスライドに述べた通り、また Elasticsearch は Isablle というまた毛色の違う形式手法ツールを併用しています。

今回 CockroachDB を扱ったので、他のプロジェクトについてもいつかメインで取り上げたいと思っていますが、それはまた別の話。

Kubernetes: kube-scheduler をソースコードレベルで理解する

はじめに

Kubernetes において、Pod を配置するための Node を決定する手続きをスケジューリングと呼び、デフォルトのクラスタでは kube-scheduler がその責務を担っています。本記事ではこの kube-scheduler のソースコードを時系列に沿って追いつつ、どのようなロジックで Pod を配置する Node が決定されるのかを解説します。

なお、本記事は Kubernetes の内部実装について学ぶ勉強会 Kubernetes Internal #3 の補足資料を意図して執筆されました。本文中で参照しているソースコードのバージョンは v1.19.4 です。

スケジューラの概要

ソースコードを読むに先立つ予備知識として、スケジューリングの大まかな流れと Scheduling Framework の概要に触れておきます。

スケジューリングの流れ

ReplicaSet や Job によって作成されたばかりの Pod は、配置先の Node が未定の状態になっています。この Node を決定するのが kube-scheduler の役割であり、さらにその結果を各 Node で稼働している kubelet が見て、自 Node に割り当てられた Pod を実際に立ち上げる、というのが Kubernetes の動作原理です。

配置先が決まっていない Pod がキューに格納されていると考えてください。kube-scheduler のメイン部分は以下のように動作します。

  1. Pod を一つ、キューから取り出す
  2. 取り出した Pod が配置できる可能性がある Node をフィルタリングする
  3. 可能性のある Node のうち最も良いものを選ぶ
  4. API Server 経由で Bind リソースを作成する

1 から 3 までをスケジューリングサイクル、4 をバインディングサイクルと呼びます。スケジューリングサイクルは直列化されており常に Pod を一つずつ扱いますが、バインディングサイクルは Pod ごとに goroutine 上で実行されます。スケジューリングサイクルは 3 で Node が確定してバインディングサイクルの goroutine を起動させたあと、完了を待たずに次の Pod のスケジュールサイクルを開始します。

なお、2 で条件にあった Node のみフィルタリングする際、場合によっては一つも残らないことがあります。このような場合に Kubernetes は、 その Pod よりも Priority が低い稼働中 Pod を削除することで Node に空きを作ろうとします。この手続きを Preemption と呼びます。

f:id:y_taka_23:20201203044922p:plain
スケジューリングサイクルの模式図

Scheduler Extender

上で述べた流れに対して、追加ロジックを差し込むことができる機構が用意されています。あらかじめ kube-scheduler に設定を加えておくとスケジューリングの特定のポイントで HTTP リクエストが外部サーバに送信され、それにレスポンスすることで kube-scheduler の挙動を変えることができます。

拡張できるのは以下の 4 点です。

  • Filter: Node をフィルタリングした結果を受け取り、さらに候補を絞る
  • Prioritize: Node を選択する際の優先度付け関数を追加する
  • Bind: バインディングサイクル内で追加で他の処理を行う
  • Preempt: Preemption で犠牲となる予定の Pod を受け取り、その中に削除されたくない Pod があれば外す

Scheduling Framework

Extender を利用したスケジューリングロジックのカスタマイズには、いくつか問題点が指摘されていました。

まず単純に拡張点が少なく、カスタマイズの余地に制限があること。また、外部サーバに JSON Webhook を投げるという実装上パフォーマンスが落ちること。さらに、Webhook サーバが外部にあることで、拡張点をまたいだ情報の受け渡しやエラー時のハンドリングがスケジューラ側ではコントロールできないこと。

さらに kube-scheduler の実装自体も種々の拡張により肥大化が進んでおり、外部で新たなカスタムスケジューラを実装しようとするとかなりの部分が kube-scheduler の再実装にならざるを得ませんでした。

この問題に対して、コントロールフロー部分だけを提供しロジックを差し替えたスケジューラを作成できるようにする仕組みが Scheduling Framework です。Scheduling Framework では、以下の拡張点を定義しています。

  • スケジューリング待ちキューに作用するもの
    • QueueSort: 優先度付きキューの優先度関数を変更する
  • フィルタリングに作用するもの
    • PreFilter
    • FIlter
  • スコアリングに作用するもの
    • PreScore
    • Score
    • NormalieScore
  • バインドに作用するもの
    • Reserve: バインド前に Node や Volume などの確保をキャッシュに登録する
    • Permit: バインディングサイクルの先頭で Pod を一旦待機させる
    • PreBind
    • Bind
    • PostBind

今回のコードリーディングでは、これらの拡張点がどのように実装されているかも含め、スケジューリングの流れを追いつつ確認していきます。

f:id:y_taka_23:20201203041559p:plain
Scheduler Framework の拡張点 (https://github.com/kubernetes/enhancements/tree/master/keps/sig-scheduling/624-scheduling-framework)

プラグインの実装

Scheduling Framework のプラグインは、Name を返す Plugin interface の他、各拡張点に対応した interface を実装している必要があります。以下は Pod を配置できる可能性がある Node をフィルタリングする Filter プラグインの interface です。

type FilterPlugin interface {
    Plugin
    Filter(ctx context.Context, state *CycleState, pod *v1.Pod, nodeInfo *NodeInfo) *Status
}

あらかじめ実装が提供されている Scheduling Framework のプラグインpkg/scheduler/framework/plugins に配置されています。

プラグインは一般には複数個の拡張点をサポートしています。例えば pkg/scheduling/framework/plugins/node_affinity.go にある NodeAffinity プラグインFilterScore の両方のメソッドを実装しており、両方の拡張点での挙動に影響を与えます。

var _ framework.FilterPlugin = &NodeAffinity{}
var _ framework.ScorePlugin = &NodeAffinity{}

また、上に示した Filter を見て取れるように、プラグインのメソッドは *CycleState を引数に取ります。この CycleState は排他制御付きの map であり、複数の拡張点やプラグインの間でデータを共有するために使用できます。ただし、CycleState はその名の通り、スケジューリングサイクルが開始されるごとにリセットされるため、データが共有できるのはあくまでも一つの Pod のスケジューリング内です。

f:id:y_taka_23:20201203053752p:plain
拡張点・プラグイン間の相互作用

スケジューリングサイクルの実装

スケジューリングサイクルの本体は pkg/scheduler/scheduler.go で実装されています。kube-scheduler は実行されると SchedulingQueue を起動させた上で、scheduleOne の無限ループに入ります。

func (sched *Scheduler) Run(ctx context.Context) {
    if !cache.WaitForCacheSync(ctx.Done(), sched.scheduledPodsHasSynced) {
        return
    }
    sched.SchedulingQueue.Run()
    wait.UntilWithContext(ctx, sched.scheduleOne, 0)
    sched.SchedulingQueue.Close()
}

この scheduleOne こそがスケジューラのロジックのコア部分であり、前述したスケジューリングの流れにほぼそのまま対応しています。以下、実装にい沿って詳細を見ていきましょう。

Pod の取り出し

冒頭、NextPod によりスケジューリングの対象となる Pod をキューからひとつ取り出します。後述しますが、このキューは Pod の Priority による優先度付きキューとして振る舞います。

podInfo := sched.NextPod()

次に、profileForPod で取り出した Pod に対応する Scheduling Profile を取得してどのようなロジックを採用するのかを決めます。また、削除中であったり、すでに配置先が決まっていた Node を再度見つけた場合は skipPodUpdate(pod) でスキップし、何も行いません。

pod := podInfo.Pod
prof, err := sched.profileForPod(pod)
(snip)
if sched.skipPodSchedule(prof, pod) {
    return
}

最後に、スケジューリングサイクルを始めるにあたって、プラグインのデータ置き場である CycleState をリセットしておきます。

state := framework.NewCycleState()

配置先 Node の決定

先に概要として述べた通りmPod を配置する Node を決定するにあたっては、

  1. 候補となる Node を絞る
  2. 残った Node に優先度をつける
  3. 一番優先度の高い Node を選択する

という手続きが行われます。これら一連の動作は pkg/scheduler/core/generic_scheduler.go で定義された Schedule メソッドで行われます。

scheduleResult, err := sched.Algorithm.Schedule(schedulingCycleCtx, prof, state, pod)

この中で、上記の「候補となる Node を絞る」を行うのが findNodesThatFitPod、「残った Node に優先度をつける」を行うのが prioritizeNodes、「一番優先度の高い Node を選択する」を行うのが selectHost です。

feasibleNodes, filteredNodesStatuses, err := g.findNodesThatFitPod(ctx, prof, state, pod)
priorityList, err := g.prioritizeNodes(ctx, prof, state, pod, feasibleNodes)
host, err := g.selectHost(priorityList)

Node のフィルタリング

ではさらに findNodesThatFitPod の中身を確認していきます。まず、PreFilter プラグインが呼び出されます。

s := prof.RunPreFilterPlugins(ctx, state, pod)

そして実際に Node をフィルタリングする処理はさらに二つの処理からなります。

まず一段階目は Filter プラグインによる findNodesThatFitPod です。

feasibleNodes, err := g.findNodesThatPassFilters(ctx, prof, state, pod, filteredNodesStatuses)

findNodesThatFitPod の内部では、各 Node に対して Pod との相性が並行してチェックされるようになっています。checkNode がチェックする処理で、さらにその内部で呼ばれている PodPassesFiltersOnNode が実際に Filter プラグインを呼び出す部分になっています。

parallelize.Until(ctx, len(allNodes), checkNode)
checkNode := func(i int) {
    // We check the nodes starting from where we left off in the previous scheduling cycle,
    // this is to make sure all nodes have the same chance of being examined across pods.
    nodeInfo := allNodes[(g.nextStartNodeIndex+i)%len(allNodes)]
    fits, status, err := PodPassesFiltersOnNode(ctx, prof.PreemptHandle(), state, pod, nodeInfo)
    //(snip)
}

冒頭でも提示しましたが、Filter プラグインFilter メソッドにより定義される interface になっています。PodPassesFiltersOnNode の内部では RunFilterPlugin が実行されており、これが各プラグインの Filter 結果を統合して一つでも失敗した Node は候補から外される仕組みになっています。処理の本体は pkg/scheduler/framework/runtime/framework.go にあります。

また、二段階目の findNodesThatPassExtenders では Extender による判定が行われます。

feasibleNodes, err = g.findNodesThatPassExtenders(pod, feasibleNodes, filteredNodesStatuses)

もし、この段階で候補となる Node が見つからなかった場合は、Preemotion の手続きに進みます。ここでは一旦、一つ以上の Node が見つかったとして話を続けましょう。

Node のスコアリング

prioritizeNodes でフィルタリングの結果生き残った Node に優先順序をつけます。Filter のときと同じく、ここでもまず PreScore プラグインが呼び出されます。

preScoreStatus := prof.RunPreScorePlugins(ctx, state, pod, nodes)

そしてやはり Filter の時と同じく、スコアリングもプラグインによるものと Extender によるものを合わせて考えます。まず、Score プラグインによるスコアの算出です。プラグイン名とそのプラグインによる Node の採点結果が map になって返されます。NormalizeScore プラグインによる正規化もここで行われます。

scoresMap, scoreStatus := prof.RunScorePlugins(ctx, state, pod, nodes)

そして、この結果に Extender によるスコアを足し込みます。Extender が複数登録されている場合、各 Extender ごとに並行して計算されます。

for i := range g.extenders {
    // (snip)
    go func(extIndex int) {
        // (snip)
        prioritizedList, weight, err := g.extenders[extIndex].Prioritize(pod, nodes)
        mu.Lock()
        for i := range *prioritizedList {
            host, score := (*prioritizedList)[i].Host, (*prioritizedList)[i].Score
            // (snip)
            combinedScores[host] += score * weight
        }
        mu.Unlock()
    }(i)
}

なお、プラグインによるスコアと Extender によるスコアの合算の際にはスケール調整を行っています。

result[i].Score += combinedScores[result[i].Name] * (framework.MaxNodeScore / extenderv1.MaxExtenderPriority)

Node の選択

最後に、selectHost が Node ごとのスコアの結果 priorityList を受け取って Node を一つ選択します。selectHost の中身は単純にループを回して最大値を選択する(同点の場合はランダム)だけです。

host, err := g.selectHost(priorityList)

バインディングサイクルの実装

Pod の配置先 Node が決定したあと、実際に Pod の Status を書き換えて配置を行う操作は Pod ごとに goroutine を発行することで行われます。これは、Volume のプロビジョニングの待ち時間や後述の CoScheduling によって Pod がすぐに起動できない場合であっても、先に次の Pod のスケジューリングサイクルを開始するためです。

まず、処理が goroutine として分岐する前に、Reserve プラグインと Permit プラグインが呼び出されます。

if sts := prof.RunReservePlugins(schedulingCycleCtx, state, assumedPod, scheduleResult.SuggestedHost); !sts.IsSuccess() {...}
runPermitStatus := prof.RunPermitPlugins(schedulingCycleCtx, state, assumedPod, scheduleResult.SuggestedHost)

この次、Permit プラグインの呼び出しが終わったあとの処理を見ると、goroutine で無名関数を実行していることがわかります。

go func() {
    bindingCycleCtx, cancel := context.WithCancel(ctx)
    defer cancel()
    // (snip)
}()

この goroutine の中で最初に実行されるのが WaitOnPermit です。Permit プラグインによって許可が行われるまで Pod は待機状態になります。goroutine として分岐した後なので、ここで Pod が待たされている間も後続の Pod は次のスケジューリングサイクルに入ることができます。

waitOnPermitStatus := prof.WaitOnPermit(bindingCycleCtx, assumedPod)

Pod が待機状態から解放されると、まず PreBInd プラグインが呼び出されます。

preBindStatus := prof.RunPreBindPlugins(bindingCycleCtx, state, assumedPod, scheduleResult.SuggestedHost)

そして実際のバインド処理は bind が実行されます。bind の中身は Filter や Score と同じくプラグインと Extender の両方が使用されますが、今回は Extender の実行が先で、かつその時点でバインドが成功すればプラグインには処理が渡らないようになっています。

func (sched *Scheduler) bind(ctx context.Context, prof *profile.Profile, assumed *v1.Pod, targetNode string, state *framework.CycleState) (err error) {
    // (snip)
    bound, err := sched.extendersBinding(assumed, targetNode)
    if bound {
        return err
    }
    bindStatus := prof.RunBindPlugins(ctx, state, assumed, targetNode)
    // (snip)
}

最後に PostBind プラグインを呼び出して一連の処理が終了です。

prof.RunPostBindPlugins(bindingCycleCtx, state, assumedPod, scheduleResult.SuggestedHost)

なお、Reserve プラグイン呼び出し後の Volume 操作やプラグイン呼び出しでエラーが発生した場合、Reserve を取り消す必要があります。そのため、各エラーハンドリング内では Reserve プラグインを呼び出して取り消し処理を行うようになっています。

prof.RunReservePluginsUnreserve(bindingCycleCtx, state, assumedPod, scheduleResult.SuggestedHost)

Preemption

ここまで、最初のフィルタリングの段階で少なくとも一つの Node が見つかった場合の流れについて解説してきました。しかし実際の運用中には必ずしも候補となる Node が存在するとは限りません。

では、条件に合う Node が全く見つからなかった場合の処理も見ていきましょう。このとき ScheduleFitError を返すことにより Preemption の手続きが開始されます。

scheduleResult, err := sched.Algorithm.Schedule(schedulingCycleCtx, prof, state, pod)
if err != nil {
    nominatedNode := ""
    if fitError, ok := err.(*core.FitError); ok {
        if !prof.HasPostFilterPlugins() {
            klog.V(3).Infof("No PostFilter plugins are registered, so no preemption will be performed.")
        } else {
            // Run PostFilter plugins to try to make the pod schedulable in a future scheduling cycle.
            result, status := prof.RunPostFilterPlugins(ctx, state, pod, fitError.FilteredNodesStatuses)
            if status.IsSuccess() && result != nil {
                nominatedNode = result.NominatedNodeName
            }
        }
    // (snip)
}

ここで、nominatedNode には、Preemption の結果 Pod が立ち退かされて空きができた Node の名前が記録されます。ただし、最終的に Pod がこの nominatedNode に配置されるとは限りません。再度スケジューリングサイクルを通過する間に他の Pod に埋められてしまう可能性もあり得ます。

Preemption 処理のロジックは PostFilter プラグインが担当します。

result, status := prof.RunPostFilterPlugins(ctx, state, pod, fitError.FilteredNodesStatuses)

デフォルトの状態では PostFilter は DefaultPreemption プラグインのみが実装しています。 ソースコードpkg/scheduler/framework/plugins/default/preemption/default_preemption.go です。

処理の本体は preempt メソッドであり、以下の処理が行われます。

  1. そもそもその Pod が Preempt 対象かどうか調べる
  2. 削除できる可能性のある Pod をリストアップする
  3. Extender に問い合わせて除外すべき Node がないかどうか調べる
  4. もっとも影響が軽い Node を選択する
  5. 実際に Pod を削除する

ロジックの中心となっているのは「候補となる Node をリストアップする」を行う selectVictimsOnNode です。大まかに

  1. まず、各 Node 上で、考えている Pod より Priority が低い Pod を全部削除した状態を考える
  2. そこから Pod を一つづつ戻してみる。PodDisruptionBudget に影響される Pod を優先して戻す
  3. それ以上戻せない、すなわち新しい Pod を配置するために必要な最低限の犠牲がどの Pod になるかを調べる

という順序で処理が行われます。

参考文献

過去のスライド

公式ドキュメント

まとめ

Kubernetes において、Pod を配置するための Node を選択する手続きをスケジューリングと呼びます。本記事では、デフォルトのスケジューラである kube-scheduler のソースコードを追うことで、Node がどのように選択されるのかの内部アルゴリズムを解説しました。特に最新の kube-scheduler では、Scheduling Framework を用いることでアルゴリズム中のロジックを差し替え可能になっているのが特徴です。

なお、今回大きくは扱いませんでしたが、運用上スケジューラのパフォーマンスに大きく影響する仕組みとして、スケジューリングキューとキャッシュが挙げられます。いつか機会があればこれらのトピックについても解説したいと思いますが、それはまた別の話。

安全性-活性分解定理とその関連研究

こんにちは、チェシャ猫です。先日行われた第 7 回 Web System Architecture 研究会で形式手法について発表してきました。

普段、形式手法について登壇する際は具体例な検証例を出すことが多いですが、今回は理論側に寄せたサーベイになっています。

はじめに

本セッションでは、安全性-活性分解 (safety-liveness decomposition) と呼ばれる一連の結果について解説する。安全性-活性分解は、システムの仕様が与えられた時、それを安全性 (safety) および活性 (liveness) と呼ばれる、よりシンプルな特徴付けを持つクラスに分解して扱うための方法論である。さらにセッションの後半では、安全性と活性の組み合わせ以外にも提案されている派生的な特徴付けについても述べる。

Web アプリケーションと形式手法

システムやプログラムの性質を何らかの数学的な対象を通して表現、検証する方法論を形式手法 (formal methods) と呼ぶ。

期待される入力と出力を人間が具体的に与える従来のテストと比較し、形式手法では理論的な背景に基づいた抜けや漏れのない検証が可能であり、また並行性のようなコントロールが困難な性質についても網羅的な検証を行うことができる。また、実装に依存せず設計段階でその意図を表現・検証できるというメリットもある。一方、形式手法を扱えるプログラマは多くなく、また一般には記述コストが通常のテストに比べて高くなるというデメリットも存在する。

伝統的には形式手法は、例えば航空宇宙関連の組み込みプログラムのような、高コストを支払ってでもそれを上回る信頼性が必要となる分野で用いられてきた。しかし近年では分散システムが身近になったことに起因し、Web アプリケーション開発において形式手法が採用される事例も見られる。一例としてここでは Amazon Web Service による S3 および DynamoDB のレプリケーションを検証した事例 [CRZ15]、および CockroachDB の分散トランザクションの最適化を検証した事例 [TSM20] を挙げておく。

安全性と活性

システムやプログラムの仕様を表現するにあたって、安全性と活性の二種類の仕様があることは古くから経験的に知られてきた。非形式的な表現で述べるなら、安全性とは「何か悪いことが決して起こらない性質」であり、活性とは「何か良いことがいつかは起こる性質」である。

シンプルな例として排他制御を考える。二つのプロセスが並行して動作し、各々が実行中にクリティカルセクションに入る必要があるとする。直感的にイメージされる性質は「二つのプロセスが同時にクリティカルセクションに入ることがない」であり、これは安全性に属する性質である。

しかし実はこの記述には不足があり、システムとして要求される性質を完全には表現していない。各プロセスが一度もクリティカルセッションに入らないようなシステムであってもこの安全性を満たすからである。したがって「各プロセスが実行中にいずれクリティカルプロセスに入る」という条件が必要であり、これが活性に相当する。

このことからもわかる通り、システムに要求される性質を記述する上では、安全性だけでなく活性を与えることが本質的に必要である。

分解定理

システムを検証するに当たって、前提としてその動作や期待する性質を何らかの形で記述する必要がある。停止するプログラムであれば入力-出力の関係としてその性質を記述することも考えられるが、システムサーバのような動き続けるシステムを記述するにはこの形式は不向きである。

このような場合、システムの状態を要素とする無限列を考えることが一般的である。例えば、システムに関与する各プロセスのプログラムカウンタの位置と各変数に代入された値の組はそのシステムの状態とみなすことができる。状態の無限列をパス (path) あるいは振る舞い (behaviour)と呼び、パス全体がなす集合の部分集合を性質 (property) と呼ぶ。

ここで、パスの定義は「実際にそのシステムが動作中に実現しうるもの」に限られない点に注意されたい。最終的な目標となる「システムが要求された性質を満たすことの検証」とはすなわち、「パスのうちシステムが実現しうるもの集合が要求したい性質の集合に含まれていること」に他ならない。

二つのパスに対して「最初 n 個目までの状態までが一致する」という関係はパス間の距離を定義する。したがって、パス全体の集合に対して、この距離が誘導する位相構造を考えることができる。

Alpern と Schneider [AS85] はこの位相構造を用いて、安全性と活性にエレガントな定義を与えている。特に活性については、これが最初の理論的な定義である。

定義:閉な部分集合を安全性 (safety property)、稠密な部分集合を活性 (liveness property) と呼ぶ

非形式的な表現に直すなら、安全性とは「要求に違反する無限列があったとしたら最初の有限個の状態ですでに違反している」性質であり、活性とは「最初の有限個がどんな状態であっても、その後続をうまく取れば全体としては要求を満たすことができる」性質である。これは前項で述べた安全性および活性の直感的な理解とよく一致する。

ところで、一般に位相空間において、任意の集合は閉集合と稠密集合の共通部分として表現することができる。このことから以下の定理が従うことがわかる [AS85]。

定理:任意の性質 P に対して、安全性 S と活性 L が存在して P = S \cap L

言い換えれば、システムに要求される任意の性質は、安全性に属する部分と活性に属する部分に分解できることがわかる。この定理は分解定理あるいは Alpern-Schneider 型定理と呼ばれ、以降に述べるような様々な派生的な研究のきっかけとなっている。

f:id:y_taka_23:20201114205820p:plain
安全性-活性分解の直感的証明

サブクラスに対する分解

上に示した分解定理は、任意の性質  P に対して成立するという意味では適用範囲が広いが、具体的に性質を記述したり判定を行ったりする目的には向かない。実用上はより具体的な記述の形式や分解の手続きが必要である。さらに、分解した結果を効率的に運用するためには、あるクラスに属する性質を分解した結果もそのクラスに閉じていること望ましい。ここでは知られている例として、Büchi オートマトンに対する結果および線形時相論理式に対する結果を取り上げる。

Büchi オートマトンに対する分解

Büchi オートマトンは有限状態オートマトンのある意味での拡張である。有限状態オートマトンが正規言語に対応するように、Büchi オートマトンは ω-正則言語と呼ばれる記号列のクラスに対応する。有限状態オートマトンを用いて記号の有限列が条件にマッチするかどうかを定義できるのと同様、Büchi オートマトンは与えられた記号の無限列が条件にマッチするかどうかを定義する。

非形式的な表現で述べれば、有限の記号列がある有限状態オートマトンに受理されるとは、記号に応じてオートマトンの遷移を辿っていった際、最終状態が受理状態であることを指す。これに対して無限の記号列がある Büchi オートマトンに受理されるとは、記号に応じてオートマトンの遷移を辿っていった際、受理状態を無限回通過することを指す。

今、考えているシステムのパスとは状態の無限列のことであり、システムの性質とはパス全体がなす集合の部分集合であった。つまり記号の集合として状態の集合を考えると、Büchi オートマトン m に対して m が受理するパスの集合 L(m) が定まり、これは何らかの性質を定義しているとみなすことができる。

Alpern と Schneider は先ほどの抽象的な分解に加えて、与えられた Büchi オートマトン m から二つの Büchi オートマトン Safe(m)Live(m) を構成する手続きを示した [AS87]。

定理:任意の既約 Büchi オートマトン m に対して、L(Safe(m)) および L(Live(m)) はそれぞれ安全性と活性となる。さらに L(m) = L(Safe(m)) \cap L(Live(m)) が成り立つ

この定理は先に述べた位相を利用して得られる定理と同様、性質を安全性と活性とに分解する記述を与えている。ただしその分解の対象は性質の中でも特に Büchi オートマトンにより定義できるものに限られ、その代わり分解のための具体的な手続きを提供する。

線形時相論理式に対する分解

線形時相論理 (linear temporal logic, LTL) は、時相論理と呼ばれる時間的な広がりを持った条件を記述することができる諸体系の一部である。 時相論理には複数のクラスがあり、LTL の他にも計算木論理 (computational tree logic, CTL) や、LTL と CTL の両者を内包する CTL* などの体系が知られている。木構造の分岐を扱うことができる CTL に対して、時間発展を直線的なモデル、すなわち状態列として扱うのが LTL の特徴である。

一般に時相論理おける論理式は、単一の状態に対する通常の命題論理に時相論理用の演算子を追加して記述される。どの記号がどの位置に出現することを許すかによって時相論理の中でも上記のバリエーションが生まれるが、LTL として妥当な演算子とその非形式的な意味は以下の二つである。

\bigcirc \phi:次の状態で \phi が成立する

\phi \mathbf{U} \psi:今後いつかは \psi が成立し、かつそれまでの間は \phi が成立する

実用上の文脈では、これらの演算子を用いてさらに定義される

 \Diamond \phi = true \mathbf{U} \phi

 \Box \phi = \neg \Diamond \neg \phi

が使用されることが多い。非形式的には  \Diamond \phi は「今後、いつかは \phi が成立する」 、 \Box \phi は「今後、常に \phi が成立する」といったような意味になる。

LTL 論理式は無限列に対してその真偽が判定できるため、やはり何らかの性質を表現しているとみなすことができる。Maretić らはこの LTL で表される性質のクラスに対する結果として以下を示した [MDB14]。前述の Büchi オートマトンに関する結果と同じく、与えられた性質を安全性と活性に分解する形式になっている。

定理:任意の LTL 論理式 \phi に対して、安全性を表現する LTL 論理式 \sigma と活性を表現する LTL 論理式 \lambda が存在して \phi = \sigma \land \lambda

なお、LTL 論理式で表現できる性質は Büchi オートマトンでも表現できるが、逆は成り立たない。LTL 論理式の表現力は Büchi オートマトンの中でも特に counter-free と呼ばれるクラスに属しているものに等しく [DG08]、これは Büchi オートマトン全体より真に狭い [W83]。つまり LTL 論理式に対する上記の定理は、LTL 論理式が分解について閉じていることを意味している。

性質に対する分類の拡張

ここまでに述べてきた結果は、対象とする性質のクラスに差はあるが、いずれも Alpern-Schneider により定式化された安全性と活性という分類に基づいたものであった。やや方向性が異なる研究として、従来とは異なる新たな分類手法を提案した文献を二つ取り上げる。

束論を用いた特徴付け

\langle L, \leq \rangle に対して、以下の条件を満たす作用素 cl: L \rightarrow L を閉包作用素と呼ぶ。

  1. a \leq cl(a)
  2. cl(a) = cl(cl(a))
  3. a \leq b ならば cl(a) \leq cl(b)

ある集合が与えられた時、その部分集合の全体に包含関係で順序を入れたものは束になり、位相の意味での閉包を取る操作は閉包作用素の条件を満たす。このため、位相を用いて定義された安全性と活性の概念は、束を用いて再定義することができる。

Manolios と Trefler はこの着想に基づき、束上で定義される安全性と活性の類似物について論じている [MR03]。具体的には以下のような定義である。

定義:可補モジュラー束 \langle L, \land, \lor, 0, 1 \rangle 上の閉包演算子 cl: L \rightarrow L が与えられたとする。a = cl(a) を満たすような元 acl-安全性 (cl-safety)、cl(a) = 1 を満たすような元  acl-活性 (cl-live) と呼ぶ

cl として位相的な閉包を取る操作を考えると、これらの定義は先に挙げたものの一般化になっている。さらにこの方針の面白い性質は、分解された各部分を特徴づける際に共通の cl を用いる必要がないという事実である。以下の定理からわかるように、特定の条件下さえ満たされれば、安全性と活性の定義に異なる cl を使用することができる。

定理 cl1cl2 を可補モジュラー束 \langle L, \land, \lor, 0, 1 \rangle 上の閉包作用素とし、任意の x \in L に対して cl1(x) \leq cl2(x) が成り立つとする。このとき cl1-安全性 y \in Lcl1-活性 z \in L が存在して x = y \land z が成り立つ

この一般化を利用して論文中では、分岐時間的 (branching-time) な性質、すなわちここまで見てきたような状態の直線的な無限列ではなく、状態をノードとするような木構造に対して定義された性質についても、従来と類似の分解定理が成立することが示されている。

定理:任意の分岐時間的な性質は、existentially safe な性質と existentially live な性質の共通部分、universally safe な性質と universally live の共通部分、existentially safe な性質と universally live な性質の共通部分、のすべてのパターンに分解可能である

ここで existentially および universally の具体的な定義は省略するが、それぞれ別の閉包作用素を通じて定義される性質である。非形式的な表現でいえば、状態がなす木構造において、existentially safe は「うまいルートの辿り方をすれば悪いことが起こらない」性質、universally safe は「どんなルートを辿ったとしても悪いことが起こらない」性質といった意味になる。

分岐時間的な分解定理は先に挙げた束上の分解定理の直接的な系であり cl1 が existentially、cl2 が universally に対応している。universally safe と existentially live の組み合わせだけが抜けているのは条件 cl1(x) \leq cl2(x) が満たされないためであり、実際にこの組み合わせでは分解できない反例が存在する。

またこの分岐時間の例は、束論による定義が位相による定義の真の拡張になっていることを示す例でもある。実際、universally を定義する閉包作用素は位相的な意味でも閉包を与えるが、existantially を定義する閉包作用素は位相的な意味では閉包にはならない。

階層的な特徴付け

また別の観点からの定式化を用いたシステムの性質の分類として、Chang らによる研究が知られている [CMP93]。従来の Alpern-Schneider 型の研究では性質を安全性と活性に二分していたが、Chang らは階層的なモデルを提案している。

既に述べた通り、Alpern と Schneider による分類は閉集合を安全性、稠密集合を活性とするものであった。Chang らの論文中では複数の視点から同値な定義が与えられているが、対応がわかりやすいように位相による定義を用いて彼らの分類を述べると以下のようになる。

定義閉集合、開集合、加算個の閉集合の和、加算個の開集合の共通部分として特徴付けられるクラスをそれぞれ Safety、Guarantee、Response、Persistence と呼ぶ

さらに、副次的なクラスとして Safety と Guarantee の両方に属するクラスを Obligation、Response と Persistence の両方に属するクラスを Reactivity として定義している。

面白いのは、理論的に自然な階層として定義されたこれらの性質と、システムに求められる要件の階層がよく対応しているように見えることである。例えば Persistence を定義する「加算個の開集合の共通部分」というクラスは、F_{\sigma} とも表され集合論では古くからよく知られた研究対象であるが、これは非形式的な表現では「いつかは成立し、かつ一度成立するとその後は成立したままになる」という状況に対応している。

なお、Chang らによる Safety の定義は Alpern-Schendier 型の安全性と共通しているが、他のクラスは活性とは直行する概念である。実際、Guarantee、Obligation、Response、Persistence、Reactivity のいずれかを \kappa で表すと、以下の分解定理が成立する。

定理:クラス \kappa に属する任意の性質 \Pi に対して、Safety に属する \Pi_{S}\kappaかつ活性に属する \Pi_{L} が存在して \Pi=\Pi_{S} \cap \Pi_{L}

参考文献

[AS85] B. Alpern, and F. B. Schneider. 1985. “Defining Liveness.” Information Processing Letters 21 (4): 181–85.

[AS87] B. Alpern, and F. B. Schneider. 1987. “Recognizing Safety and Liveness.” Distributed Computing 2 (3): 117–26.

[CMP93] E. Chang, Z. Manna, and A. Pnueli. 1993. “The Safety-Progress Classification.” In Logic and Algebra of Specification, 143–202. Springer Berlin Heidelberg.

[CRZ15] N. Chris, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff. 2015. “How Amazon Web Services Uses Formal Methods.” Communications of the ACM 58 (4): 66–73.

[DG08] V. Diekert, and P. Gastin. 2008. “First-Order Definable Languages.” Logic and Automata 2: 261–306.

[MR03] P. Manolios, and R. Trefler. 2003. “A Lattice-Theoretic Characterization of Safety and Liveness.” In Proceedings of the Twenty-Second Annual Symposium on Principles of Distributed Computing, 325–33. PODC ’03. New York, NY, USA: Association for Computing Machinery.

[MDB14] G. P. Maretić, M. T. Dashti, and D. Basin. 2014. “LTL Is Closed under Topological Closure.” Information Processing Letters 114 (8): 408–13.

[TSM20] R. Taft, I. Sharif, A. Matei, N. VanBenschoten, J. Lewis, T. Grieger, K. Niemi, et al. 2020. “CockroachDB: The Resilient Geo-Distributed SQL Database.” In Proceedings of the 2020 ACM SIGMOD International Conference on Management of Data, 1493–1509. SIGMOD ’20. New York, NY, USA: Association for Computing Machinery.

[W83] P. Wolper. 1983. “Temporal Logic Can Be More Expressive.” Information and Control 56 (1): 72–99.