Tag: Lincheck

이 태그가 달린 글들 "Lincheck"

• 32스레드 테스트는 통과했지만 명세가 틀렸다 — Lincheck가 동시성 계약을 세 번 기각한 과정

  31 Jul, 2026

  reputation-pool의 32스레드 스트레스 테스트를 Lincheck 모델 체킹으로 확장하면서 겪은 기록입니다. Lincheck가 찾아낸 것은 단순한 구현 버그가 아니었습니다. 전역 fencing token 순서, acquire가 반환할 리소스의 정체성, block과 경합할 때의 성공 여부처럼 제가 계약이라고 믿었던 세 가지 가정이 실제 구현이 보장해야 할 계약보다 강했습니다. 실패 trace를 따라 공개 계약과 스케줄링 정책을 분리하고, 선형화로 표현할 수 없는 운영 속성은 별도의 실시간 순서 테스트로 옮긴 과정을 정리했습니다.