DSLabs: 분산 시스템 교육용 모델 체킹 프레임워크
Source
Evernote/Inbox/Teaching rigorous distributed systems with efficient model checking – the morning paper.md
Summary
본 문서는 워싱턴 대학교의 분산 시스템 교육용 오픈소스 프레임워크인 DSLabs(Distributed Systems Labs)를 소개합니다. DSLabs는 학생들이 RPC, Paxos, 키-값 저장소 등 핵심 분산 시스템을 구현하고 테스트할 수 있도록 설계되었습니다. 기존 테스트의 한계를 극복하기 위해 DSLabs는 Java 기반 개발 환경에 경량 모델 체킹(Model Checking)을 통합하여, 비결정론적 네트워크 환경(메시지 지연, 손실, 중복 등)에서 발생할 수 있는 잠재적 버그를 체계적으로 탐지합니다. 특히 TLA+와 같은 형식적 검증 도구의 높은 학습 곡선을 피하면서도, 모델 체킹 친화적인 시스템 설계(결정론적 핸들러, 제한된 랜덤성)를 통해 교육 및 실무 모두에 유용한 검증 환경을 제공합니다.
Key Points
- DSLabs는 분산 시스템 교육용 오픈소스 프레임워크로, RPC, Primary-Backup, Paxos, 트랜잭션 키-값 저장소 구현을 위한 4단계 과제를 제공합니다.
- 기존 테스트의 한계(특히 희귀한 경합 조건 버그 탐지 실패)를 해결하기 위해 경량 모델 체킹을 통합하여 모든 가능한 실행 경로를 체계적으로 탐색합니다.
- TLA+와 같은 별도 형식적 검증 언어의 학습 부담을 줄이기 위해, Java 구현 코드 자체를 모델 체킹 대상으로 하는 통합 환경을 제공합니다.
- 모델 체킹의 효율성을 위해 시스템은 단일 스레드 이벤트 루프 기반의 결정론적 핸들러로 구성되며, 랜덤성은 타이머 만료 시간에만 제한적으로 허용됩니다.
- 비동기 네트워크 모델(메시지 순서 무질서, 지연, 손실, 중복 허용)과 크래시-스톱 실패 모델을 가정하여 현실적인 분산 시스템 환경을 시뮬레이션합니다.