Gobra による複数粒度ロック証明への挑戦

背景

Finatext でバックエンドエンジニアをしている太宰です。普段は「BaaS (Brokerage as a Service)」という証券ビジネスプラットフォームを開発しています。
半年ほど前に結成された Enabling Team の一環として「自動推論」技術について調査・検証を行っています。
これまでの詳しい経緯などは 自動推論シリーズスタート：Gobraでできること を読んでいただければと思います。

この記事で扱うこと

この記事では Gobra を用いて複数粒度ロック (Multiple granularity locking) についての証明を試みたので、その内容や工夫した点、どういった成果が得られたかについてを扱います。
Gobra を利用してどういった証明ができるかの実例について、また証明を書くにあたってどういった難しさがあるかについて伝えられればと思います。

はじめに

今回証明を試みるコードは tm8619/MGL-test です。
このリポジトリで実装されている hirelock についての証明を書くことで、実際どの程度の証明が書けるのかを検証しました。
hirelock の詳細な設計や挙動については上記リポジトリの docs ディレクトリ以下にある markdown ドキュメントを参照していただければと思います。

複数粒度ロック (Multiple granularity locking) とは

MGLでは、ロックは他のオブジェクトを含んだオブジェクトに対して設定される。MGLは「包含関係」の階層構造の性質を利用する。例えば、データベースにはファイルがあり、ファイルにはページがあり、ページにはレコードがある。これをオブジェクトの木構造と捉え、各ノードに子ノードが包含されているとする。ロックは対応するノードとその配下のノード群をまとめてロックする。

– Wikipedia:複数粒度ロック より引用

ちょっと言い換えると、上記の例でいうと以下のような階層があり、あるページをロックするときはそこに含まれる全てのレコードもまとめてロックを取る、ということです。

データベース > ファイル > ページ > レコード

複数のページは同時に排他ロックを取ることができますが、あるページの排他ロックが取られている時にそれを含むファイルの排他ロックは取ることができません。既に取られているページの排他ロックを含むためです。
上記 hirelock においてはこれを実現するために「親ノードの共有ロックを取ってから子ノードの排他ロックを取り、トランザクションのロールバックによって一気に開放する」という戦略を取っています。

今回の挑戦

データベースの並行処理において、デッドロックなどのロック制御に起因するバグを安定してテストで発見するには、ロック制御を十分に理解した上で誤った順番でロックを取るようなテストを書く必要があり、厄介な問題です。
バグがないことを証明するのはさらにやっかいで、テストで保証することを考えるとロックに関する考えられる全ての実行順についてテストを書く必要があります。
「考えられる全ての」というのが非常に厄介です。バグが発生する時にはこの点で実装時に考慮漏れを起こしていることが多く、考慮漏れしたままテストを書くと結局バグは見付けられないことになります。

そこで、今回は Gobra を用いてデッドロックしないことを証明するという挑戦を行いました。
MGLの共有ロック・排他ロックの取り方については Gobra においても表現しつつ、デッドロックが起きないことの証明については「ロック順が固定である」ことを証明することで代替としました。
上記 hirelock の戦略「親ノードの共有ロックを取ってから子ノードの排他ロックを取り、トランザクションのロールバックによって一気に開放する」において、ロック順が毎回同じであればデッドロックが起きません。
「ロック順が固定であるとデッドロックが起きないこと」そのものを証明するのは複雑になるので避け、「ロック順が固定である」ことの証明を試みます。
また、 hirelock のコードはできるだけ書き換えずにアノテーションの付加とヘルパーの追加のみで証明していくことを試みました。

これはネタバレになりますが、結論として今回は完全な証明には至ることはできませんでした。
この記事では、どういった方針で証明を試みてどこで壁にあたったのかについて共有します。

Gobra での証明において工夫したこと

Gobra を使って「データベースのロック」という副作用の強い操作を表現するにあたり、いくつか工夫を凝らしました。特に面白いのはFractional Permissions（部分アクセス権）の応用と、全順序の定義です。

1. Fractional Permissions による共有・排他ロックの表現

データベースにおける共有ロックと排他ロックを Gobra で証明するために、Gobra のメモリアクセス権限の概念である Fractional Permissions を利用しました。

Gobra では、 acc(x, 1/2) で部分的なアクセス権（読み取りのみ可能）、 acc(x, 1) で完全なアクセス権（書き込み可能）を表現します。これを以下のように DB のロックに見立てました。

• acc(Lock(…), 1/2) = 共有ロック (FOR SHARE)
• acc(Lock(…), 1) = 排他ロック (FOR UPDATE)

共有ロック同士は $1/2 + 1/2 = 1$ となり両立できますが、すでに誰かが $1$（排他ロック）を持っていると、他のトランザクションは $1/2$ すら取得できなくなります。この性質は DB のロック互換性と完全に一致します。
実際のコード（ hierlock/manager.go の Acquire メソッド）では、以下のような事後条件（ ensures ）を記述しました。

// @ ensures err == nil && result != nil && level == LevelResource ==> acc(Lock(userTarget(userID)), 1/2) && acc(Lock(accountTarget(userID, accountID)), 1/2) && acc(Lock(resourceTarget(userID, accountID, resourceID)), 1)
func (m *Manager) Acquire(ctx context.Context, level Level, userID, accountID, resourceID string) (result *LockHandle, err error) {
// ...

親階層（User, Account）には 1/2 、対象階層（Resource）には 1 のアクセス権を要求することで、MGL の制約を非常に綺麗にモデル化できました。

2. 全順序の定義

今回証明するのは「すべてのトランザクションが必ず同じ順番でロックを取得する」ことです。
これを Gobra に教え込むため、 hierlock/lock.gobra にゴーストコード（証明のためだけに存在するコード）を追加し、各ロック対象に一意の整数値を割り当てる lockLevel 関数と、順序を比較する order 関数を定義しました。

ghost
pure
decreases _
func order(t1, t2 lockTarget) bool {
        return lockLevel(t1) < lockLevel(t2)
}

この順序関係を用いて、複数のリソースをロックする際は配列が正しくソートされているという制約を記述しました。これにより、「常に一定の順序でロックを取りに行く」という挙動を数理的に表現しています。

立ちはだかった壁

ここまでの工夫は自分でも上手くやったと思っているのですが、以下の困難な壁に当たってしまい Gobra のエラーを解消しきれずに終わりました。

リソースリーク（Release の証明）の壁

ロックを取得（ Acquire ）する事後条件は書けましたが、ロックを解放（ Release ）することの証明が困難でした。
現状の LockHandle.Release() は、トランザクションをロールバックしてロックを手放します。しかし Gobra の世界では、 Acquire で獲得した Lock 述語（ゴースト状態）を Release 時に正しく「消費（Consume）」しないと、「ロックを手放していない（リソースリークしている）」と判定されてしまいます。
これを解決するには LockHandle に「自分がどのロックを保持しているか」を記録するゴーストフィールドを持たせるなどの複雑な変更が必要になり、コードのシンプルさを保ちながら証明を通すことが難航しました。

ループ不変条件（Loop Invariants）の壁

Acquire 内でロック対象のキー配列をループして順番にロックを取得していく処理があります。
Gobra に「ループが回るごとに、取得済みのロック（ Lock 述語）が蓄積されていく」ことを教えるためのループ不変条件の記述が極めて複雑になりました。「今まで処理した i 番目までのロックをすべて保持している」という状態を簡潔に表現できず、上手く証明を書くことができませんでした。

「現実世界の不確実性」と数学の不和（ハッシュ衝突）の壁

今回の実装は実運用を見据え、ロック対象を行数の上限がない実 ID ではなく、10,000,000 の固定空間のバケット（ストライプ方式）に FNV ハッシュで割り当てています。
現実には、異なる ID が同じバケットに落ちる「ハッシュ衝突（偽競合）」が起こり得ます。しかし、Gobra の証明を通すために bucket 関数に対して @ trusted を付与し、「異なる文字列からは必ず異なるバケット番号が返る」という、数学的には嘘の前提を置いてしまっています。
「衝突が起きる現実」と「衝突しないという前提を置かないと成り立たない証明」の折り合いをつける部分で、モデリングの限界を感じました。

おわりに

今回は Gobra を使って MGL という実践的な処理の証明を書くことに挑戦しました。
結果として証明しきれずに終わりましたが、この挑戦を通じて Gobra のエラーとひたすら向き合ったおかげでコードの処理を証明するということにすこしずつ慣れてきている実感があります。
一方で、事前・事後条件やループ不変条件を適切に与えることの難しさもまた実感しました。
事前・事後条件、つまり関数の入出力に関してのみ条件を与えればよいのであれば比較的簡単ですが、ループ不変条件を適切に与えようとすると実装の詳細にかなり踏み込んで証明を記載する必要があり難しいということがわかりました。
複雑な処理をしているコードこそ証明を与えたいですが、処理が複雑であるが故に証明を書けないといったケースも出てきそうです。

自動推論チームでは、今後も自動推論や形式検証といった技術とそれを実現するツールについて継続的に調査・検証を行っていきます。
今後もいくつか記事を予定していますので、ぜひ楽しみにしていただければと思います。