비즈니스 로직을 클라우드 서비스로 만드는 과정에서, 상태 기반의 비즈니스 로직을 개발하는 경우가 많습니다.
이 때, 만드는 시스템에 설계 상 결함이 없는지를 알아내기 위해 다양한 테스트 기법을 도입하여 안정성을 보장하려는 시도를 많이 합니다. 그럼에도, 근본 설계가 타당한지, 정말 모델링이 잘 된 설계인지 아는 것은 쉽지 않습니다.
이것을 수학적인 모델링을 통해 검증하는 도구로 TLA+ 이야기가 나와서 조금 찾아봤는데, Azure, AWS 등 주요 클라우드 서비스 엔지니어링 팀이 이미 절찬리에 많이 사용하고 있는 도구라는 것을 알게 되어 공유해봅니다.
아래는 Microsoft에서 이야기하는 TLA+에 대한 후기들입니다.
TLA+는 2004년경부터 Microsoft에서 산발적으로 사용되었습니다. 다음은 고인이 된 Chuck Thacker가 보고한 그러한 사용 사례 중 하나입니다.
Xbox 360을 개발하는 동안 저는 엔지니어링 그룹과 함께 메모리 일관성 프로토콜을 작업했습니다. 인턴과 함께 프로토콜에 대한 TLA+ 모델을 개발했습니다. 이 과정에서 매우 미묘한 버그를 발견했습니다. IBM에 보고했고, 그들은 그럴 수 없다고 말했습니다. 몇 주 후, 그들은 양보하여 버그가 실제일 뿐만 아니라 회귀 테스트에서 발견되지 않았을 것이라고 말했습니다. 그들이 버그를 수정하지 않았다면 약 4시간 사용 후 교착 상태가 될 칩을 우리에게 배송했을 것입니다. [이런 일이] 발생했다면 크리스마스 출시 일정을 거의 확실히 놓쳤을 것입니다.
2015년경부터 Microsoft에서 사용이 증가했습니다. 특히 Microsoft의 클라우드 서비스인 Azure에서 그렇습니다. 다음은 Azure 팀 구성원이 작성한 TLA+ 사용에 대한 요약 및 약간 편집된 설명입니다. 언급된 TLA+ 사양 중 일부는 실제로 PlusCal에서 작성되었습니다.
Azure 네트워킹의 기업 부사장인 Albert Greenberg는 다음과 같이 말합니다.
저희 엔지니어링 프로세스는 엔지니어링 수명 주기에서 가능한 한 일찍 검증을 진행합니다. 저희는 위험을 줄이고 민첩성을 높이며 개발자에게 빠른 피드백을 제공하기 위해 오류를 더 빨리 감지하기 위해 노력합니다. 저희가 사용하는 주요 도구 중 하나는 TLA+ 사양 언어입니다. 이를 통해 구성 요소를 간단한 수학으로 공식적으로 설명할 수 있으며, 수학을 정확하게 작성하는 데 필요한 것 이상의 오버헤드를 최소화할 수 있습니다.
저희는 TLA+가 특히 동시 및 분산 시스템의 고수준 사양을 작성하는 데 적합하다는 것을 발견했습니다. 구체적으로 문제를 정의하고, 원하는 구현에 가까운 사양을 제공하고, 연속적인 개선을 통해 사양을 구현한다는 것을 증명하거나, 그렇지 않으면 결함을 찾아 설계를 수정합니다. Azure Networking에서 TLA+를 적용한 프로젝트로는 Azure DNS(레코드 전파), RingMaster(분산형 글로벌 복제 및 검사점 조정), Distributed Load Shedding, Macsec(암호화 키 롤오버 오케스트레이션) 등이 있습니다. 예를 들어 RingMaster에서 단위 테스트의 간헐적 실패에서 나타났지만 코드에서 지역화하기가 엄청나게 어려운 버그를 식별했습니다. 원하는 동작에 대한 특정 TLA+ 사양을 작성하고 논리적 설계에서 버그를 빠르게 찾아 코드를 수정했습니다.
Microsoft Technical Fellow인 Dharma Shukla는 Microsoft의 글로벌 분산 데이터베이스 서비스인 Azure Cosmos DB에서 TLA+를 사용하는 것에 대해 다음과 같이 적었습니다.
Cosmos DB 엔지니어링 팀은 TLA+를 사용하여 핵심 알고리즘의 정확성과 시스템이 고객에게 제공하는 5가지 일관성 모델의 상위 수준 사양을 지정하고 검증했습니다. TLA+는 두 가지 기본적인 면에서 매우 유용하다는 것을 알게 되었습니다.
분산 알고리즘을 설계하는 경우. 예를 들어, 다중 위치 쓰기 기능에 대한 알고리즘을 설계하는 동안 시스템의 중요한 안전 속성을 위반하는 중요한 정확성 버그를 발견했습니다. 이 버그는 TLA+ 사양을 작성하는 동안 발견되었으며, 코드 한 줄도 작성하기 전에 문제를 수정할 수 있었습니다.
알고리즘이나 시스템이 제공하는 보장을 정확하게 지정합니다. 예를 들어, Cosmos DB는 TLA+를 사용하여 서비스가 사용자에게 제공하는 5가지 일관성 모델이 제공하는 보장을 지정했습니다. 이러한 사양은 사용자에게 제공됩니다.
Principle Software Engineer Manager인 Cheng Huang은 다음과 같이 썼습니다.
TLA+는 가장 확신하는 구현에서도 안전 위반을 발견했습니다. 우리는 신중하게 설계 및 구현되고, 철저한 코드 검토를 거쳤으며, 여러 날 동안 스트레스 하에서 테스트된 잠금 없는 데이터 구조 구현을 가졌습니다. 그 결과, 구현에 대한 확신이 컸습니다. 결국 정확성을 검증하기 위해서가 아니라 팀원들이 PlusCal을 배우고 연습할 수 있도록 TLA+ 사양을 작성하기로 결정했습니다. 그래서 모델 검사자가 안전 위반을 보고했을 때, 우리는 정말 놀랐습니다. 이 경험은 많은 팀원들에게 아하 순간이 되었고, TLA+에 대한 그들의 사실상의 증언이 되었습니다.저희 시스템은 많은 Paxos 링을 관리하고 이러한 링을 즉시 동적으로 재구성합니다. TLA+는 우리가 이것을 올바르게 하는 것이 보이는 것보다 훨씬 더 미묘하다는 것을 깨닫도록 도와주었습니다. 정전에서 복구하는 동안 특정 순서의 이벤트 시퀀스에 따라 데이터 손실(고객에게)을 초래했을 안전 위반을 발견하게 되어 매우 기뻤습니다. 이것이 저희의 어떤 테스트 노력을 통해서도 발견될 수 있을 것이라고는 상상할 수 없었습니다.
TLA+는 아직 Microsoft에서 채용의 전제 조건이 아닙니다. 그러나 후보자의 TLA+에 대한 지식은 저희의 평가에서 상당한 가중치를 둡니다. 저희에게는 이것이 품질과 정확성을 진정으로 중시하는 사람들을 나타내는 훌륭한 지표입니다.
요구 사항 구현이나 시스템 설계 때문에 모두가 바쁜 것은 사실이지만, 따로 시간을 내어 TLA+에 대해 알아보고 적용할 기회를 탐색해보는 것은 무척 유익할 것이란 생각이 드네요!
