16년 숨어 있던 SQLite WAL 버그, 수백 줄짜리 TLA+ 명세가 몇 분 만에 잡아냈어요

세상에서 가장 많이 테스트된 코드에도 버그는 숨어 있어요

SQLite는 아마 지구상에서 가장 널리 배포된 소프트웨어일 거예요. 여러분 스마트폰에도, 브라우저에도 들어 있죠. 테스트 코드가 본체 코드보다 수백 배 많기로 유명한 프로젝트이기도 하고요. 그런데 2025년에 SQLite 개발팀이 WAL 모드에 약 16년 동안, 그러니까 2010년 WAL 도입 시점부터 숨어 있던 버그를 공개했어요. 그리고 최근 캐노니컬(우분투 만드는 회사)의 dqlite 팀이 '우리 제품도 영향받나?'를 확인하려고 TLA+라는 형식 검증 도구를 동원한 이야기를 블로그에 풀었는데요, 이게 정말 교과서적인 사례예요.

먼저 WAL이 뭔지부터 짚고 갈게요

WAL(Write-Ahead Logging)이 뭐냐면, 데이터를 원본 DB 파일에 바로 쓰지 않고 별도의 로그 파일(WAL 파일)에 먼저 순서대로 기록하는 방식이에요. 가계부 원장에 바로 쓰는 대신 포스트잇에 먼저 적어두는 느낌이랄까요. 이렇게 하면 읽는 사람과 쓰는 사람이 서로를 덜 막아서 동시성이 좋아지거든요. 그리고 주기적으로 '체크포인트'라는 작업이 포스트잇 내용을 원장에 옮겨 적고 WAL 파일을 처음부터 다시 쓰도록 리셋해요.

버그는 바로 이 리셋 순간에 있었어요. 체크포인트가 WAL을 리셋한 직후, 아주 특정한 타이밍으로 스레드들이 엇갈리면, 오래된 wal-index 헤더(WAL의 목차 역할을 하는 공유 메모리)를 들고 있던 읽기 트랜잭션이 이전 세대의 WAL 프레임을 읽어버릴 수 있었던 거예요. 쉽게 말해 리셋 전의 낡은 포스트잇을 최신 내용인 줄 알고 읽는 거죠. 스냅샷 격리가 깨지는, 데이터베이스에서는 꽤 심각한 종류의 버그예요. 다만 체크포인트, 동시 쓰기, 그리고 정확한 순서로 락을 잡는 리더가 맞물려야 해서 실제로 터질 확률은 천문학적으로 낮았고, 그래서 16년을 버틴 거고요.

TLA+로 버그를 '재현'한다는 것

dqlite 팀은 이 버그를 TLA+로 모델링했어요. TLA+가 뭐냐면, 시스템의 동작 규칙을 수학적 명세로 적으면 모델 체커(TLC)가 가능한 모든 실행 순서를 전부 탐색해서 규칙 위반을 찾아주는 도구예요. 테스트가 '몇 가지 시나리오를 돌려보는 것'이라면, 모델 체킹은 '정해진 범위 안의 모든 시나리오를 빠짐없이 확인하는 것'이거든요.

팀은 wal-index 헤더, 읽기 마크와 락, 쓰기 락, RESTART/TRUNCATE 체크포인트 동작까지 WAL 프로토콜을 수백 줄의 TLA+로 명세했어요. 그리고 리더 2명, 라이터 1명, 체크포인터 1명이라는 작은 범위로 돌렸더니, 몇 분 만에 '리더가 잘못된 세대의 프레임을 읽는' 불변식 위반이 재현됐대요. 초정밀 테스트로도 16년간 못 잡은 인터리빙을요. 참고로 업스트림 SQLite의 수정은 헤더를 읽을 때의 메모리 배리어 순서를 조정해서, 리더가 WAL 리셋을 감지하면 재시도하도록 하는 방식이었어요.

그래서 dqlite는 영향받았을까요?

결론부터 말하면 영향 없음이에요. dqlite는 SQLite에 Raft 합의 알고리즘을 얹어 분산 DB로 만든 건데(LXD, MicroK8s에서 쓰여요), 쓰기가 전부 Raft를 거쳐 단일 스레드로 적용되고 체크포인트도 동시 리더가 없는 통제된 시점에만 일어나거든요. 문제의 인터리빙 자체가 발생할 수 없는 구조예요. 팀은 TLA+ 모델에 dqlite의 제약을 반영해서 그 나쁜 상태에 도달 불가능함을 확인했어요. 감으로 '괜찮을 것 같다'가 아니라 수학적으로 보여준 거죠.

한국 개발자에게 주는 시사점

형식 검증이라고 하면 학계나 항공우주 같은 데서나 쓰는 거라고 생각하기 쉬운데, AWS가 S3와 DynamoDB 설계에 TLA+를 쓴 이후로 실무 도입 사례가 꾸준히 늘고 있어요. 이번 사례의 교훈은 '시스템 전체가 아니라 까다로운 프로토콜 한 조각만 작게 모델링해도 충분히 남는 장사'라는 거예요. 분산 락, 캐시 무효화, 결제 상태 머신처럼 동시성 순서가 꼬이면 큰일 나는 로직을 다루고 있다면, 테스트로는 도달할 수 없는 영역이 있다는 걸 기억해 둘 만해요. 게다가 명세 자체가 프로토콜의 살아 있는 문서 역할도 하고요.

한줄 요약: 테스트는 있는 버그를 몇 개 찾아주지만, 모델 체킹은 범위 안의 모든 타이밍을 뒤져서 '없다'는 것까지 말해준다.

여러분 프로젝트에서 '이건 타이밍 문제라 재현이 안 돼요'라며 덮어둔 버그, 혹시 없으신가요? 형식 검증까지는 아니어도 동시성 버그를 잡는 자기만의 방법이 있다면 공유해 주세요.