形式手法による分散システムの検証 〜S3 の一貫性モデルを例として〜

[y-taka-23]

セッションタイトル (必須)

• セッションのタイトルをイシュー件名に最大40文字程度で入力しました

連絡先の登録 (必須)

• 私は、こちらのフォーム に必要事項を記入してsubmitしました

セッションのアブストラクト (最大250文字) (必須)

みなさん、分散システムを「正しく」開発してますか？ 2020 年、Amazon S3 の一貫性モデルが見直され、オブジェクトに対する更新がラグなしに読み取れるようになりました。この際、巨大な分散システムである S3 に対して新しい同期プロトコルの「正しさ」を保証するために選ばれたツールこそが、形式手法の一種、P 言語です。本講演では、分散システムを愛しそして苦しむ全てのエンジニアのために、S3 を単純化したトイモデルを段階的に設計・検証する流れを追体験し、形式手法の威力と魅力を感じてもらいます。

セッションについての補足情報 (最大800文字) (任意)

形式手法とは

形式手法 (formal methods) は、システムの動作や仕様を数学的に厳密な形で記述し、静的・体系的に検査する技術です。

みなさんはアプリケーションを開発する際、単体テスト・E2E テストを実行するでしょう。しかし、分散システムには本質的なテスト困難性があります。各プロセスはそれぞれ独立して動作し、かつネットワーク遅延や偶発的な障害など、コントロールできない要素が無数に含まれます。考えるべき状況が組み合わせ的に爆発するため、いわゆる「タイミング系のバグ」の可能性は事前にテストケースとして人間が列挙できるレベルを超えています。

そしてここに、テストケースの列挙ではなく数学的記述と体系的探査による形式手法の強みがあります。今回紹介する P 言語では、システムを状態機械として定義することによって、複数のプロセスが任意のタイミングで並行して動作しても決して異常な状態に到達しないことを数学的に保証することができます。

想定受講者

• 題材は S3 ですが、インフラというよりもアプリケーション開発者向けです
• S3 の基本的な使い方や API については十分な予備知識と経験を仮定します
• 分散システムの設計・実装経験は必須ではありませんが、あればより楽しめます
• 分散システム・プロトコルや故障モデルについての学術的な予備知識は仮定しません
• 形式手法や P 言語についての予備知識は仮定しません

参考リンク

• P
• Amazon S3 data consistency model
• Amazon S3 Update – Strong Read-After-Write Consistency
• Introducing strong consistency for Amazon S3
• Diving Deep on S3 Consistency
• AWS Pi Week 2021: Amazon S3 Strong Consistency
• Amazon S3 の一貫性モデル超入門

セッション時間

45分

想定受講者の知識レベル（必須）

上級 - セッションの中心となるトピックを本番環境で利用・運用したことがある方向け

想定受講者の開発対象やロール・役割 (複数選択可) (必須)

Web バックエンド / サーバーサイド開発, その他

想定受講者の業種・業界・業態 (複数選択可) (任意)

No response

セッションのトピック (複数選択可) (必須)

Web バックエンド / サーバーサイド開発, 大規模サービス構築, アプリケーションアーキテクチャー, ソフトウェアテスト, その他

セッションの技術カテゴリー (複数選択可) (必須)

その他

セッション内で登場する主な AWS サービス (任意)

Amazon S3, Amazon DynamoDB, Amazon EMR