TLA+ の Refinement で実装が仕様を満たすことを確認する

TLA+

この記事は、CYBOZU SUMMER BLOG FES '25の記事です。

こんにちは、クラウド基盤本部の向井です。

システム開発において、「具体的な実装」が「抽象的な仕様」を満たしていることを保証することは重要な課題です。TLA+ の Refinement（詳細化）は、この課題に対する解決策の一つです。本記事では、上書き可能なオブジェクトストレージを使って上書き不可能なオブジェクトストレージを実装する例を通じて、TLA+ の Refinement の使い方を紹介します。コードを完全に理解するためにはある程度の TLA+ の知識が必要ですが、そうでなくても流れは理解できるように書いたつもりです。

TLA+ とは？

TLA+ は、Leslie Lamport 氏によって開発された、分散システムやアルゴリズムの設計と検証のための形式仕様記述言語です。TLA+ の特徴は、システムの振る舞いを厳密に記述し、モデル検査器（TLC）を使って自動的に検証できることです。これにより、実装前の段階で設計の問題を発見し、修正することができます。

TLA+ についてこれから学びたい方には Lamport 氏の Video Course がおすすめです。実例を交えながら基礎から応用まで体系的に学ぶことができます。この記事のテーマである Refinement についてのより正確かつより詳細な内容の Lecture もあります。

TLA+ の Refinement とは？

システム開発では、まず「何を実現したいか」という抽象的な仕様を定義し、次に「どう実現するか」という具体的な実装を設計することが多いと思います。しかし、実装が複雑になるにつれて、本当に元の仕様を満たしているか確認することが困難になります。例えば、「データは一度だけ書き込める」という単純な仕様でも、並行処理や分散システムでは実装が複雑になり、バグが入り込みやすくなります。

Refinement は、この問題を解決する強力な手法です。具体的な実装が抽象的な仕様の振る舞いを正しく実現していることを形式的に検証できます。具体的には、以下のような利点があります。

  • 段階的な詳細化：シンプルな仕様から始めて、徐々に実装の詳細を追加できる。
  • 正しさの保証：各段階で仕様との整合性を自動検証できる。
  • 設計の見通し向上：複雑な実装でも、元の仕様との関係が明確になる。

Refinement の活用例

ここからは「上書き可能なオブジェクトストレージ」を利用して「上書き不可能なオブジェクトストレージ」を実装する例を通し、Refinement を活用して抽象的な仕様を満たす実装を段階的に詳細化していく流れを見てゆきましょう。

抽象的な仕様

まずは上書き不可能なオブジェクトストレージの仕様を決め、TLA+ で記述しましょう。上書き不可能なので、許可される操作はオブジェクトのアップロードだけとします。通常、オブジェクトストレージにはバケットやオブジェクトを特定するためのキーのような概念がありますが、特定のバケットの特定のキーにだけ着目したと考え、これらを明に書かないことにします。

アップロードできるオブジェクトはどのようなものでしょうか。例えば AWS S3 では一つのオブジェクトの最大サイズは5TBだそうです。つまりアップロードできるオブジェクトの種類は高々有限ということになります。高々有限ではありますが、モデル検査では現れる状態の数が計算時間に直結するため、同じだけの種類をアップロードできる仕様を検証するのは難しいでしょう。そこで、我々の仕様では思い切ってアップロードできるオブジェクトは3通りということにしましょう。それらを d1、d2、d3 とし、これらの集合を Data とします。

---- MODULE Immutable ----
CONSTANTS Data, NotFound

VARIABLES object
vars == <<object>>

Init == object = NotFound

Put(data) ==
  /\ object = NotFound
  /\ object' = data

Next == \E d \in Data: Put(d)

Spec == Init /\ [][Next]_vars

TypeOK == object \in {NotFound} \cup Data

Immutability ==
    [][object # NotFound => object' = object]_vars
====

Immutablity が「一度オブジェクトがアップロードされると、そのオブジェクトが変更されることはない」という性質を表しています。この性質は Put(data) というアクションで object = NotFound という条件を満たす場合、つまりまだオブジェクトがアップロードされていない場合だけ object' が変更されることにより実現されるはずです。実際、この性質は以下のように Immutability が常に満たされることを確認するように設定してモデル検査を行うことで確かめられます。

SPECIFICATION Spec

CONSTANTS
    Data = {d1, d2, d3}
    NotFound = NotFound

INVARIANTS
    TypeOK

PROPERTIES
    Immutability

CHECK_DEADLOCK FALSE

ここからはデータの保存に上書き可能なオブジェクトストレージを利用して、上記の抽象的な仕様を満たすプログラムを実装することを考えましょう。

一つのプロセスの場合

まずは一つのプロセス内の複数のスレッド（t1, t2, t3）が並行してリクエストを処理する場合を考えます。この実装でデータの保存に利用しているストレージは上書きが可能であり、上書きしないようにするためにはすでにオブジェクトがアップロードされているかどうかを確かめてから、アップロードされていない場合のみアップロードするということが必要そうです。

以下にこの実装の仕様を示します。上書き可能なオブジェクトストレージを store という名前で利用しています。

---- MODULE SingleProcess ----
CONSTANTS Data, NotFound, Threads

VARIABLES pc, store
vars == <<pc, store>>

Init ==
    /\ pc = [ t \in Threads |-> "accept" ]
    /\ store = NotFound

CheckStoreOK(t) ==
    /\ pc[t] = "accept"
    /\ store = NotFound
    /\ pc' = [ pc EXCEPT ![t] = "checked_store" ]
    /\ UNCHANGED store

CheckStoreFail(t) ==
    /\ pc[t] = "accept"
    /\ store # NotFound
    /\ pc' = [ pc EXCEPT ![t] = "done" ]
    /\ UNCHANGED store

Put(t, d) ==
    /\ pc[t] = "checked_store"
    /\ pc' = [ pc EXCEPT ![t] = "done" ]
    /\ store' = d

Terminated ==
    /\ \A t \in Threads: pc[t] = "done"
    /\ UNCHANGED vars

Next ==
    \E t \in Threads:
        \/ CheckStoreOK(t)
        \/ CheckStoreFail(t)
        \/ \E d \in Data: Put(t, d)
    \/ Terminated

Spec == Init /\ [][Next]_vars

TypeOK == store \in {NotFound} \cup Data
====

この実装が抽象的な仕様を満たしているか検証してみましょう。一つの方法は抽象的な仕様が満たしていた性質（例えば Immutablity）をこの実装も満たしているかどうか調べるというものがあります。しかし、抽象的な仕様が満たすべき性質の数が多い場合はどうでしょうか。仕様が満たしていた性質を全て実装でも満たすかどうかを調べるのは大変になりますし、二度手間にも感じます。

ここで便利なのが Refinement です。この手法では、実装が抽象的な仕様の詳細化になっているかどうかを調べることができます。

object == store
Immutable == INSTANCE Immutable WITH object <- object
Refinement == Immutable!Spec

このコードの意味は以下の通りです。

  • object == store：実装の store 変数を抽象仕様の object 変数にマッピングする。
  • INSTANCE Immutable WITH object <- object：抽象仕様モジュールをインポートし、変数をマッピングする。
  • Refinement == Immutable!Spec：実装が抽象仕様 Spec を満たすことを表すプロパティを定義する。

Refinement プロパティを検証することで、実装のすべての実行パスが抽象仕様で許可された実行パスに対応することを確認できます。

SPECIFICATION Spec

CONSTANTS
    Data = {d1, d2, d3}
    NotFound = NotFound
    Threads = {t1, t2, t3}

INVARIANTS
    TypeOK

PROPERTIES
    Refinement

実行すると、以下のように Immutable の性質が満たされないということと、その反例が示されます。1

TLC Model Checker による Immutable プロパティの検証結果
TLC Model Checker が検出した反例：store が d1 から d2 に上書きされている

この反例では以下の流れで抽象的な仕様では起こらなかったことが起こっています。

  1. スレッド t1 が store を確認し、アップロードされていないとわかる。
  2. スレッド t2 が store を確認し、アップロードされていないとわかる。
  3. スレッド t1 が store に d1 をアップロードする。
  4. スレッド t2 が store に d2 をアップロードする。

これは典型的な TOCTOU 問題ですね。チェック時点では条件を満たしていても、使用時点では別のスレッドによって状態が変更されている可能性があります。今は一つのプロセス内で動作する複数のスレッドを考えているので、store を読み書きする前にプロセス内でロックを取るとよさそうです。このように改修したものが次の実装です。

-VARIABLES pc, store
-vars == <<pc, store>>
+VARIABLES pc, lock, store
+vars == <<pc, lock, store>>

 Init ==
     /\ pc = [ t \in Threads |-> "accept" ]
+    /\ lock = FALSE
     /\ store = NotFound

-CheckStoreOK(t) ==
+AcquireLock(t) ==
     /\ pc[t] = "accept"
+    /\ lock = FALSE
+    /\ pc' = [ pc EXCEPT ![t] = "acquired_lock" ]
+    /\ lock' = TRUE
+    /\ UNCHANGED store
+
+CheckStoreOK(t) ==
+    /\ pc[t] = "acquired_lock"
     /\ store = NotFound
     /\ pc' = [ pc EXCEPT ![t] = "checked_store" ]
-    /\ UNCHANGED store
+    /\ UNCHANGED <<store, lock>>

 CheckStoreFail(t) ==
-    /\ pc[t] = "accept"
+    /\ pc[t] = "acquired_lock"
     /\ store # NotFound
     /\ pc' = [ pc EXCEPT ![t] = "done" ]
+    /\ lock' = FALSE
     /\ UNCHANGED store

 Put(t, d) ==
     /\ pc[t] = "checked_store"
     /\ pc' = [ pc EXCEPT ![t] = "done" ]
+    /\ lock' = FALSE
     /\ store' = d

 Next ==
     \E t \in Threads:
+        \/ AcquireLock(t)
         \/ CheckStoreOK(t)
         \/ CheckStoreFail(t)
         \/ \E d \in Data: Put(t, d)

これを先ほどと同じ設定ファイルで検証すると、エラーは報告されなくなります。この実装が抽象的な仕様と同じ振る舞いをすることが確かめられました。

複数のプロセスの場合

実環境で運用する場合、スケーラビリティや耐障害性を考えると、複数のプロセスに処理を分散できるとよいでしょう。しかし、プロセスが複数になると、一般にプロセス内のロックに頼ることができなくなります。代替案はいろいろありそうですが、ここで ACID 特性を持つデータベースのトランザクションを使う例を考えてみましょう。

以下のようなアルゴリズムでアップロードを行うことを考えます。簡単のため、各プロセスは一つだけのリクエストを処理することにします。

  1. 各プロセスはアップロード対象のオブジェクトを上書き可能なオブジェクトストレージの一時領域（リクエスト毎に固有な場所）にアップロードする。
  2. データベースのトランザクション内で以下を実行する。
    • まだコミットされていなければ、そのプロセスの一時領域を正式な保存場所として記録し、コミットする。
    • すでにコミットされていれば、トランザクションを中止し、一時領域をクリーンアップする。

このアプローチにより、複数のプロセスが同時にオブジェクトをアップロードしようとしても、データベースのトランザクション機能により一つだけが成功することが保証されます。

以下にこの仕様に対応する TLA+ のコードを示します。

---- MODULE Distributed ----
CONSTANTS Data, NotFound, Processes

VARIABLES pc, database, store
vars == <<pc, database, store>>

Init ==
    /\ pc = [ p \in Processes |-> "accept" ]
    /\ database = [ committed |-> FALSE ]
    /\ store = [ p \in Processes |-> NotFound ]

CreateTemp(p, d) ==
    /\ pc[p] = "accept"
    /\ pc' = [ pc EXCEPT ![p] = "created_temp" ]
    /\ store' = [ store EXCEPT ![p] = d ]
    /\ UNCHANGED database

Commit(p) ==
    /\ pc[p] = "created_temp"
    /\ ~database.committed
    /\ pc' = [ pc EXCEPT ![p] = "done" ]
    /\ database' = [ committed |-> TRUE, process |-> p ]
    /\ UNCHANGED store

Abort(p) ==
    /\ pc[p] = "created_temp"
    /\ database.committed
    /\ pc' = [ pc EXCEPT ![p] = "done" ]
    /\ store' = [ store EXCEPT ![p] = NotFound ]
    /\ UNCHANGED database

Terminated ==
    /\ \A p \in Processes: pc[p] = "done"
    /\ UNCHANGED vars

Next ==
    \E p \in Processes:
        \/ \E d \in Data: CreateTemp(p, d)
        \/ Commit(p)
        \/ Abort(p)
    \/ Terminated

Spec == Init /\ [][Next]_vars

TypeOK == \A p \in Processes: store[p] \in {NotFound} \cup Data

このとき、「データベースでコミット済みであれば保存されたオブジェクトの場所にあるオブジェクトがアップロード済み、コミット済みでなければまだアップロードされていない」とみなせば抽象的な仕様を満たせるでしょうか。この場合の Refinement は一つのプロセスの場合のように単純なマッピングではありませんが、以下のように書くことができます。

object ==
    IF database.committed
    THEN store[database.process]
    ELSE NotFound
Immutable == INSTANCE Immutable WITH object <- object
Refinement == Immutable!Spec

この仕様を以下の設定ファイルで検証することで、抽象的な仕様を満たすことを確認できます。

SPECIFICATION Spec

CONSTANTS
    Data = {d1, d2, d3}
    NotFound = NotFound
    Processes = {p1, p2, p3}

INVARIANTS
    TypeOK

PROPERTIES
    Refinement

まとめ

この記事では TLA+ の Refinement を使って、抽象的な仕様を満たす実装を段階的に詳細化していく手法について紹介しました。具体的には以下の流れで進めました。

  1. 抽象仕様の定義：イミュータブルストレージの本質的な性質を記述
  2. 単一プロセスでの実装：TOCTOU問題の発見とロックによる解決
  3. 分散システムでの実装：データベーストランザクションを使った実装

Refinement を活用し、各実装段階で正しさを保証しながらシステムを複雑化していくイメージをお伝えできていれば幸いです。

  1. このスクリーンショットは Visual Studio Code の TLA+ (Temporal Logic of Actions) という拡張を利用してモデル検査を行い作成しました。↩
#CYBOZU SUMMER BLOG FES '25

yellow-sabotech

関連記事
このエントリーをはてなブックマークに追加