productionでrace conditionが出るのを待つのは、テストじゃない。勤勉のフリをした希望だ。
アプリを何週間も走らせ、metrics dashboardを見張っていても、2つのrequestがまさに同じcache eviction windowに突入したときだけ発火するconcurrency bugをリリースする可能性は残る。問題は運が悪いからじゃない。問題は、テスト戦略が「schedulerが自分のために悪意を持って動き、しかも自分がちょうど見ているその瞬間」に依存していることだ。
もっとまともな方法がある。model checkingなら、concurrent logicのありとあらゆるinterleavingを数日ではなく数秒で探索できる。テストを書くのを忘れていたあのrace conditionも見つけてくれる。
model checkingは実際に何をやるのか
model checkingはfuzzerじゃない。ランダムなinputをコードにぶつけて祈るようなものではない。システムのありうるstateを数学的にモデル化し、網羅的に走査する。
concurrent programをgraphとして考えろ。各nodeはstateだ：変数の値、queueの中身、どのthreadがどのlockを持っているか。各edgeはstepだ：threadが値をreadした、mutexをacquireした、messageを送った。schedulerが次にどのthreadを動かすか選び、その選択がgraphを分岐させる。
model checkerはこのgraphのすべてのpathを歩く。あるpathが2つのthreadがsynchronizationなしに同じmemoryにwriteする状態に至ったら、counterexampleを報告する：bugを発火させる正確なstepの列だ。
核心的な洞察は、model checkerがschedulerを支配するということだ。productionではOSの気まぐれに任されている。model checkerの中では、自分がOSだ。重要な行を実行する前にthreadをpauseし、別のthreadにメソッド全体を走らせ、最初のthreadをresumeできる。現実世界ではcosmic rayに加えてnetwork hiccupが必要なようなinterleavingも探索できる。
model checkerがミリ秒で捕まえるrace condition
古典的なbugを見せよう：2つのgoroutineがshared counterをincrementする。
package main
import (
"fmt"
"sync"
)
func main() {
var counter int
var wg sync.WaitGroup
for i := 0; i < 2; i++ {
wg.Add(1)
go func() {
defer wg.Done()
// Read, increment, write: three steps
val := counter
val++
counter = val
}()
}
wg.Wait()
fmt.Println(counter) // Expected 2, often prints 1
}これを千回走らせても、毎回2が出力されるかもしれない。schedulerはお前の都合で敵になってくれない。だがmodel checkerはread-increment-writeという3stepの列を見て、こう判断する：goroutine Aが0をreadし、次にgoroutine Bが0をreadし、両方がincrementして1をwriteすれば、counterは2ではなく1で終わる、と。
数日待つ必要はない。2つのbranchを探索するだけだ。
自分のコードをmodel checkする方法
model checkingの価値を得るために、コードベース全体をformal verificationする必要はない。ほとんどのチームは、concurrencyが実際に問題になる20%のコードをモデル化するだけで、80%の効果を得ている。
ワークフローはこうだ：
-
concurrent componentを隔離する。 HTTP handler、database query、loggingを削ぎ落とせ。state machineに集中しろ：どのthreadやgoroutineが存在し、どのshared stateに触れ、どのsynchronization primitiveを使うのか。
-
abstract modelを書く。 実際のdata structureを、関心のある振る舞いを捉える単純化された版に置き換える。job queueをチェックするなら、実際のjob payloadは不要だ。queueとworker、そしてjobが進行中かどうかを示すflagがあればいい。
-
維持したいpropertyを定義する。 それがinvariantだ。「2つのworkerが同じjobを処理することはない」「jobが失われることはない」「cacheとdatabaseが食い違うことはない」。
-
model checkerを走らせる。 結果は「すべてのinvariantが成立」か、counterexample traceの提示だ。
以下は、シンプルなexplicit-state checkerを使ったPythonでの最小モデルだ：
from collections import namedtuple
# Abstract model of a counter with two threads
State = namedtuple('State', ['counter', 'pc1', 'pc2'])
def successors(state):
"""Return all states reachable in one step."""
results = []
c, pc1, pc2 = state
# Thread 1: three-step increment
if pc1 == 0:
results.append(State(c, 1, pc2)) # read
elif pc1 == 1:
results.append(State(c, 2, pc2)) # increment
elif pc1 == 2:
results.append(State(c + 1, 3, pc2)) # write
# Thread 2: three-step increment
if pc2 == 0:
results.append(State(c, pc1, 1))
elif pc2 == 1:
results.append(State(c, pc1, 2))
elif pc2 == 2:
results.append(State(c + 1, pc1, 3))
return results
def check():
initial = State(0, 0, 0)
visited = set()
stack = [initial]
while stack:
state = stack.pop()
if state in visited:
continue
visited.add(state)
# Invariant: if both threads finished, counter must be 2
if state.pc1 == 3 and state.pc2 == 3 and state.counter != 2:
print(f"BUG: counter={state.counter}")
return
stack.extend(successors(state))
print("No race condition found in model.")
check()これはproduction-readyではない。ideaを示す20行のPythonだ。TLA+やSpin、mCRL2のような本物のmodel checkerはstate deduplicationやtemporal logic property、partial-order reductionを扱い、数百万のstateを持つシステムもチェックできる。だがmental modelは同じだ：systemをencodeし、invariantを宣言し、探索する。
落とし穴：state space explosion
model checkingはタダじゃない。4つのthreadがあり、それぞれに10個の可能な次stepがあるなら、state graphは指数的に膨張する。64-bit integerを追加すれば、state spaceは文字通りチェック不能になる。
解決策はabstractionだ。実際のcacheをモデル化しない。「cacheにkeyがある」「cacheにkeyがない」としてモデル化する。実際のdatabaseをモデル化しない。「committed」か「uncommitted」としてモデル化する。
ここで人が躓く。実コードをmodel checkしようとしてcheckerが永遠に走り続ける。そしてmodel checking自体を放棄する。これは、1つのtest caseでアプリ全体をテストしようとして失敗したからunit testを放棄するのと同じだ。
鉄則はこうだ：concurrencyをモデル化し、business logicはモデル化するな。race conditionがuser IDの正確な値に依存しているなら、すでに負けている。race conditionはinterleavingで起きるもので、data valueで起きるものではない。
実際に機能するツール
本物のコードをmodel checkし始めたいなら、選択肢はある。
Go向け： gosimは、model checkerから制御できるdeterministic schedulerでGoプログラムを走らせられる。sync.Mutexの想定を破るinterleavingを見つけてくれる。
Rust向け： shuttleはAWS Labsのdeterministic concurrency testing frameworkだ。asyncコードを異なるscheduler選択で何千回も走らせ、memory modelレベルでチェックするloom（これも優秀なツール）が見つけるraceを発見する。
分散システム向け： TLA+はindustrial-strengthの選択肢だ。AmazonはDynamoDBやS3のbugを出荷前に見つけるのに使った。学習曲線は本物だが、クリティカルなシステムへのreturn on investmentは測定可能だ。
手軽に始めるなら： 上記のようなPythonスクリプトを書け。1時間かかる、bugを見つける、そしてTLA+が必要になったときにそれを謎めかしくなくする直感を養える。
これが代替しないもの
model checkingはconcurrent codeのlogic errorを見つける。performance regressionやmemory leak、production load下でのみ現れるbugは見つけられない。mutex contentionが1秒間に10,000 requestで急増することも教えてくれない。
stress testingと併用し、置き換えるな。stress testingはsystemが負荷を生き延びるかを教えてくれる。model checkingは、その負荷が生み出すinterleavingをsystemが生き延びるかを教えてくれる。
始める場所
過去に噛まれたことのあるconcurrent componentを1つ選べ。job queueでもconnection poolでもrate limiterでもいい。invariantをplain Englishで書き出し、その後ひと午後を使ってちっちゃなモデルを組め。
存在すら知らなかったbugが見つかるかもしれない。あるいは、心配していたbugが起き得ないという確信が得られるかもしれない。どちらの結果も、production graphを見張って祈るのをもう1週間続けるよりはるかに価値がある。
具体的な次のステップが欲しいなら、Learn TLA+チュートリアルで、週末にdistributed consensus protocolをゼロからチェックできるようになる。GoやRustなら、shuttleかloomをtest suiteに追加してCIで走らせろ。code reviewの前にraceを捕まえてくれたその瞬間、なぜschedulerにテストを任せていたのかと思うだろう。