TLA+ 모델링 팁
Source: Hacker News
모델을 최소화하기
작은 핵심에서 시작하고, 확장할 때마다 항상 작동하는 모델을 유지하십시오. 기본값은 생략이어야 합니다. 제외했을 때 작동하지 않는 이유를 설명할 수 있을 때만 구성 요소를 추가하십시오. 대부분의 모델은 전체 시스템 전체가 아니라 행동의 일부분에 관한 것입니다. 예: 리더 선출, 복구, 재구성. 해당 부분에 영향을 주지 않는 전체 레이어와 구성 요소는 제거하십시오. Abstraction is the art of knowing what to cut. 삭제는 기쁨을 주어야 합니다.
모델 사양, 구현이 아니라
선언적으로 작성하십시오. 어떻게 달성되는지가 아니라 무엇이 유지되어야 하는지를 명시하세요. 사양이 제어 흐름, 루프, 혹은 도우미 함수와 닮아 있다면, 그것은 코드를 시뮬레이션하는 것입니다. 이를 없애세요. 모든 변수는 그 존재 이유가 있어야 합니다. 불필요한 변수는 상태 공간(모델‑체킹 시간)을 늘리고 버그를 숨깁니다. 스스로에게 반복해서 물어보세요: 저장하는 대신 유도할 수는 없는가? 예를 들어, 기존 변수들의 상태 함수로 정의할 수 있다면 WholeSet 변수를 유지할 필요가 없습니다:
WholeSet == provisionalItems \cup nonProvisionalItems모델의 불법 지식 검토
모델을 전체적으로 읽어보고 각 프로세스가 실제로 무엇을 볼 수 있는지 확인하십시오. TLA+는 실제 분산 프로세스가 원자적으로 관찰할 수 없는 전역 상태(또는 다른 프로세스의 상태)를 쉽게 읽을 수 있게 합니다. 이는 가장 흔한 모델링 오류 중 하나입니다. 불법적인 전역 지식을 제거하기 위해 전용 검토를 수행하십시오.
Check atomicity granularity
동작을 정확성이 허용하는 한도 내에서 가능한 한 세밀하게 푸시하십시오. 지나치게 큰 원자적 동작은 경쟁 상황을 숨기고 동시성 논증을 무효화합니다. 세밀한 동작은 프로토콜이 견뎌야 하는 실제 인터리빙을 드러냅니다.
보호된 명령(guarded commands)으로 생각하라, 절차가 아니라
각 행동은 보호된 명령 스타일에서 하나의 논리적 단계를 표현해야 합니다. 가드는 이상적으로 행동의 의미를 정의합니다. 모든 활성화 조건을 가드에 넣으세요. 가드가 성립하면, 그 행동은 진정한 이벤트‑드리븐 방식으로 언제든지 실행될 수 있습니다. 이것이 제가 PlusCal보다 TLA+를 직접 쓰는 것을 선호하게 된 이유입니다: TLA+는 여러분이 보호된 명령 행동으로 생각하도록 강요하는데, 이는 분산 알고리즘이 설계되어야 하는 방식이기 때문입니다. 물론 PlusCal은 개발자가 읽기에 더 쉽지만, 순차적인 구현 형태의 사고로도 여러분을 끌어당깁니다. 최근에는 Spectacle 같은 도구 덕분에 TLA+ 사양을 공유하고 시각적으로 탐색하는 것이 훨씬 쉬워졌습니다(예시).
Step back and ask what you forgot to model
시스템에 대해 깊이 생각하는 것을 대체할 수 있는 방법은 없습니다. TLA+ 모델링은 시스템에 대해 깊이 생각하도록 돕기 위한 도구일 뿐이며, 그 자체가 생각을 대체할 수 없습니다. 실패, 메시지 재정렬, 복구, 재구성 등 모든 관련 측면을 포함했는지 확인하십시오.
TypeOK 불변식 작성
TLA+는 타입이 없으므로, TypeOK 불변식을 작성하여 타입을 명시적이고 초기에 선언해야 합니다. 좋은 TypeOK 불변식은 모델에 대한 실행 가능한 문서를 제공합니다. 이를 몇 초만에 작성하면 TLA+ 반례 로그를 통해 런타임 버그를 찾는 데 걸리는 여러 분을 절약할 수 있습니다.
가능한 한 많은 불변식을 작성하세요
속성이 중요하다면, 불변식으로 명시적으로 표현하세요. 초기에 작성하고, 시간이 지나면서 확장하세요. 불변식을 가능한 한 엄격하게 유지하려고 노력하세요. 불변식과 비불변식에 대한 학습 내용을 문서화하세요. TLA+ 사양은 커뮤니케이션 아티팩트입니다. 독자를 위해 작성하고, TLC 모델 체커를 위해 작성하지 마세요. 명확성을 위해 명시적이고 지루하게 작성하세요.
진행 속성 작성
Safety invariants alone are not enough. Check that things eventually happen: requests complete, leaders emerge, and goals are accomplished. Many “correct” models may quietly do nothing forever. Checking progress properties catches paths that stall.
성공을 의심하라
성공적인 TLC 실행은 모델이 의미 있는 동작을 탐색하지 않는 한 아무것도 증명하지 못합니다. 낮은 커버리지나 매우 작은 상태 공간은 보통 모델이 과도하게 제약되었거나 잘못되었음을 의미합니다. 사양을 일부러 깨뜨려서 실제로 작업을 수행하고 있는지, 아니면 공허하거나 사소한 방식으로 포기하고 있는지를 확인하십시오. 의도적으로 버그를 삽입하십시오. 불변 조건이 실패하지 않으면 그것은 너무 약하다는 뜻입니다. 사양을 방해함으로써 테스트하십시오.
모델‑체크 효율성 최적화 마지막
모델을 모델 체커와 분리하세요. 사양은 독립적으로 존재해야 합니다. .cfg 파일을 사용하면 적절한 구성, 제약, 카운터에 대한 경계, 대칭 항목 등을 활용하여 모델 체킹을 최적화할 수 있습니다.
많은 예제와 walkthrough는 제 블로그의 TLA+ 사양에서 확인할 수 있습니다.
TLA+ 저장소에도 더 많은 예제가 있습니다.