토큰 버킷(Token Bucket) 알고리즘은 분산 시스템에서 재시도 폭주(retry storm)를 완화하는 데 효과적인 기법입니다.

**PlusCal과 TLA+**를 활용해 토큰 버킷 기반 재시도 로직을 모델링하면서, 순차적 처리 방식에서 발생하는 Head-of-Line(HOL) 블로킹 문제를 발견하였습니다. 이는 실패로 토큰이 고갈되면 재시도 쓰레드가 대기 상태에 빠져 토큰이 보충되지 않아 시스템이 교착 상태에 빠지는 현상입니다.

이를 해결하기 위해 재시도 시 토큰이 없으면 대기하지 않고 즉시 실패 처리하는 Fail-Fast 전략을 도입하여, 큐가 막히지 않고 정상적으로 동작하도록 개선하였습니다.

또한, 순차적 스레드 모델과 달리 순수 TLA+ 모델은 이벤트 기반 상태 머신으로 설계되어 HOL 블로킹 문제를 자연스럽게 회피함을 보여줍니다.

이 사례는 형식 검증 도구를 통한 설계 검증의 중요성과, 이벤트 기반 명세와 실제 순차적 구현 간의 패러다임 차이에서 발생할 수 있는 위험성을 시사합니다.