見出し画像
Photo by ayakonishihara

[TLA+] 分散システムを設計する際に形式仕様を導入してみた

hden

こんにちは、トレタの鄧（でん）です。

今回はトレタ社内でシステムを設計する際に導入した形式仕様（formal specification）、あるいは形式手法（formal method）についてお話したいと思います。

なぜ形式仕様が必要なのか？

モバイルアプリや Web アプリ、またはマイクロサービスなどの普及により基本分散型のサービスが主流になりつつあると思いますが、その分散型のシステムを設計する際に複数のシステムの状態推移や整合性を担保するシステム設計はそのシステムの複雑度に比例して難しくなっていると感じております。

例えば：

  • エンドユーザーがアクションを起こせば隅々のシステムまで正しく一回のみ実行されてますか？

  • A と B という二つのシステムがある場合、A システムが OO ステータスになった場合、B システムも必ず XX ステータスに遷移することを担保できますか？時間差などによっては予想外のステータスに遷移しませんか？

  • ネットワークの一時的な障害やユーザー起因のブラウザバックが発生した場合、冪等性は担保されてますでしょうか？

トレタでは残念ながら過去ネットワータイムアウトやその他リトライ処理のミスよってお客様にご迷惑をおかけしたこともあり、システム設計においての堅牢性を担保する活動の一環として形式仕様言語の TLA+ / PlusCal を使って設計者の補助をおこなっております。

形式仕様とは本実装とは別に、仕様、例えばシーケンス図、ステータス遷移、DB トランザクションなどの設計に対して、数学的に論理的矛盾、考慮もれ、因果関係、蓋然性などの検証を手伝ってくれるツールです。

特に一つの API シーケンスに関わるサービスが増えた場合（Stripe など外部のシステムを使っている以上必然的に増える）、あるいは非同期処理など処理が走るタイミングが前後する場合など、システム全体的に到達できるステートは指数的に増えるのでアーキテクトが頭で考えることによって検証することはシステムが複雑化することによって徐々に現実的ではなくなります。

そこでトレタでは形式仕様言語の TLA+ / PlusCal を使って機械的に全ての可能性や前後関係をスキャンして、設計上の抜け漏れを洗い出す作用を手伝ってもらってます。

TLA+ と PlusCal

Amazon が Dynamo DB を設計する際に利用した(1)ことや、SQUARE ENIX が Final Fantasy 15 Pocket Edition を設計する際に使ったこと(1)が有名ですが、TLA+ は本質的には数理モデルを表現するツールだと認識しております。

TLA+ のパパである Leslie Lamport が数学家である影響もあり、TLA+ を扱う際のマインドセットとしては仕様や挙動を数式、関数、あるいは集合として表現することです。（一部 Tuples など、比較的高度なデータ構造も扱えます）

細かい数式や文法の説明するのは本記事の目的ではないので割愛しますが、概念としては例えばプリンターとキューの間の API を設計している際に

  • プリンターが複数台存在していて、同じキューを共有している

  • 各プリンターのインスタンスは API を通してキューからジョブを取り出して印刷を試し、成功や失敗もまた API を通してキューに知らせます

  • もちろん現実的なプリンターは紙詰まりも起こすし、場合によっては印刷中に故障することもあります

  • そんな中、キューの中のジョブは必ず一回印刷されることを担保できるのか？（印刷漏れや重複印刷が発生しないことを担保できるのか）

プリンターが一台しか無い場合は頑張ってリトライをする条件などを考えて抜け漏れがないことを脳内でイメージすることができますが、プリンターの台数が増える、あるいはネットワークの要素や非同期処理の前後などが発生する場合、どうしても考慮漏れが発生しやすくなります。

そこで数学的に全ての可能性を考慮して検証を手伝ってくれるのが TLA+ ですが、あまりにも数学的な表現が多いのでエンジニアにとってはとっつきにくい言語になります。そこでの解決案として PlusCal が存在しており、C に近い文法（C-syntax）あるいは Pascal に近い文法（P-syntax）で式を表現すると自動的に TLA+ に翻訳してくれるのです。

そこでトレタでは大まかなシーケンス図や ER 図を一旦仮で書いて、PlusCal と TLA+ を使ってこのような API を数式でモデリングして、複数台のプリンターが同時並行で稼働する（非同期によって API リクエストは前後する）、あるいは成功・失敗など分岐する可能性があるシナリオを全てスキャンして、設計時点で抜け漏れがないか、あるいはどの辺りの前提が崩れると求められている条件を達成できなくなるのかなど、設計や仕様の蓋然性や弱みを把握するようにしております。

形式仕様を導入した恩恵は？

正直、元々数学がものすごく得意なわけでもないし、完全に使いこなせている自信もないのですが、普段はふんわりした概念を式として清書する作業自体、ラバーダッキングの効果があり、仕様の言語化に役立っております。

そこに加えて、普段は現実的に全ての可能性を検証することは現実的ではないのに対して、TLA+ を導入した結果、意図しないステータス遷移が発生した場合や仕様違反を起こした際には再現手順もご丁寧にステップバイステップで教えてくれますので、仕様のバグ潰しが捗ります。

形式仕様は銀の弾丸なのか

TLA+ は学習コストがあるし、仕様のモデリングには時間がかかるので、結論から言うと全てのシステムに対して導入するのはお薦めできませんが、複雑且つ失敗してはいけない部分（俗に言うミッションクリティカル）などは上記ラバーダッキングの効果や言語化の恩恵があるので、厳密なモデリングじゃなくても十分お役に立てると考えております。

TLA+ や PlusCal 以外にも形式仕様言語は多く存在しますので、使いこなせばシステム設計の際には十分お役に立てるのではないかと思います。

参考資料

  1. TLA+と形式仕様言語

  2. Learn TLA+

  3. PlusCal (P-Syntax) マニュアル日本語版


この記事が気に入ったらサポートをしてみませんか？