프로덕션에서 race condition이 떠오르기를 기다리는 건 테스트가 아니다. 성실함으로 위장한 희망이다.
앱을 몇 주씩 돌리고 metrics 대시보드를 지켜봐도, 두 개의 request가 정확히 동일한 cache eviction window에 걸릴 때만 발동하는 concurrency 버그를 그대로 배포할 수 있다. 문제는 운이 나쁜 게 아니다. 문제는 테스트 전략이 “scheduler가 나를 위해 악의적으로 작동하고, 또 내가 우연히 보고 있는 그 정확한 순간”에 의존하고 있다는 것이다.
더 나은 방법이 있다. model checking은 concurrent 로직의 가능한 모든 interleaving을 며칠이 아닌 수 초 만에 탐색할 수 있다. 테스트를 작성하지 않았던 그 race condition도 찾아낼 것이다.
model checking은 실제로 무엇을 하는가
model checking은 fuzzer가 아니다. 코드에 무작위 input을 던지고 기도하는 게 아니다. 시스템의 가능한 상태를 수학적으로 모델링하고 철저하게 순회한다.
concurrent 프로그램을 graph로 생각해라. 각 node는 상태다: 변수의 값, queue의 내용, 어떤 thread가 어떤 lock을 잡고 있는지. 각 edge는 한 step이다: thread가 값을 read하거나, mutex를 acquire하거나, message를 보내는 것. scheduler가 다음에 어떤 thread를 실행할지 선택하고, 그 선택이 graph를 분기시킨다.
model checker은 이 graph의 모든 path를 걷는다. 어떤 path가 synchronization 없이 두 thread가 같은 메모리에 write하는 상태로 이어지면, counterexample을 보고한다: 버그를 발동시키는 정확한 step의 나열이다.
핵심 통찰은 model checker이 scheduler를 제어한다는 것이다. 프로덕션에서는 운영체제의 변덕에 맡겨져 있다. model checker 안에서는 자신이 운영체제다. 중요한 라인을 실행하기 전에 thread를 pause시키고, 다른 thread가 전체 메서드를 실행하게 한 뒤, 첫 번째 thread를 resume할 수 있다. 현실에서는 cosmic ray에 network hiccup까지 필요한 interleaving도 탐색할 수 있다.
model checker이 밀리초 만에 잡아내는 race condition
고전적인 버그를 보자: 두 개의 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라는 3단계 sequence를 보고 이렇게 안다: goroutine A가 0을 read하고, goroutine B가 0을 read한 뒤, 둘 다 increment해서 1을 write하면 counter는 2가 아닌 1로 끝난다는 것을.
며칠을 돌릴 필요가 없다. 두 개의 branch만 탐색하면 된다.
자신의 코드를 model check하는 방법
model checking의 가치를 얻기 위해 전체 codebase를 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다. “두 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-grade가 아니다. 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 자체를 완전히 포기한다. 이는 하나의 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의 버그를 출하 전에 찾는 데 사용했다. 학습 곡선은 실재하지만, 중요한 시스템에 대한 return on investment는 측정 가능하다.
부드러운 시작: 위와 같은 Python 스크립트를 작성하라. 한 시간이 걸린다, 버그를 찾는다, 그리고 TLA+가 필요할 때 그것을 덜 신비롭게 만드는 직관을 기른다.
이것이 대체하지 못하는 것
model checking은 concurrent code의 logic error를 찾는다. performance regression이나 memory leak, 프로덕션 부하에서만 나타나는 버그는 찾지 못한다. mutex contention이 초당 10,000 request에서 급증하는지도 알려주지 않는다.
stress testing과 함께 쓰되, 대신 쓰지 마라. stress testing은 시스템이 부하를 견디는지 알려준다. model checking은 그 부하가 만드는 interleaving을 시스템이 견디는지 알려준다.
시작은 어디서
예전에 물어본 적 있는 concurrent component를 하나 고르라. job queue, connection pool, rate limiter 무엇이든. invariant를 plain English로 적어내고, 한 오후를 들여 작은 모델을 만들어라.
존재조차 몰랐던 버그를 찾을 수도 있다. 아니면 걱정하던 버그가 일어날 수 없다는 확신을 얻을 수도 있다. 어느 쪽이든 프로덕션 그래프를 보며 기도하는 것을 또 일주일 하는 것보다 훨씬 가치 있다.
구체적인 다음 단계를 원한다면 Learn TLA+ 튜토리얼이 주말에 분산 consensus protocol을 검증하는 단계까지 이끌어준다. Go와 Rust라면 shuttle이나 loom을 test suite에 추가해 CI에서 돌려라. code review 전에 race를 잡아준 그 첫 순간, 왜 scheduler에게 테스트를 맡겼는지 의문이 들 것이다.