TL;DR

  • TLA+는 시스템의 가능한 상태와 전이를 모델링하고, 모든 실행 경로가 속성을 만족하는지 검증하는 언어임.
  • 전이 시스템은 시스템 상태와 상태를 바꾸는 동작을 표현하며, 플레이그라운드에서는 테스터처럼 동작을 직접 수행해 한 가지 실행 경로를 탐색함.
  • 시간 속성은 실행 중 항상 참이어야 하는 안전성(safety)과 언젠가 참이 되어야 하는 활성성(liveness)으로 구분됨.
  • 모델 검사기 TLC는 유한한 사례에서 도달 가능한 상태를 열거하며, 속성 위반 시 구체적인 반례 실행을 제시함.
  • 안전성만으로는 동작이 멈춘 시스템을 걸러낼 수 없으며, 활성성 검증에는 공정성(fairness) 가정이 필요함.

TLA+가 표현하는 시스템

  • TLA+(Temporal Logic of Actions)는 두 종류의 대상을 기술하는 언어임.
  • 전이 시스템은 시스템이 할 수 있는 일을 나타냄. 상태는 시스템의 스냅샷으로, 후보가 누구인지, 누가 누구에게 투표했는지, 누가 리더인지를 담음.
  • 동작은 상태를 바꾸는 한 단계임. 예를 들어 ‘a가 선거를 시작함’, ‘b가 a에게 투표함’과 같은 동작임.
  • 대화형 플레이그라운드에서는 테스터처럼 단계를 직접 수행하며 가능한 실행 경로 하나를 탐색함.
  • 시간 속성은 실행이 시간에 따라 어떻게 전개되는지에 관한 진술임. 예를 들어 ‘리더가 둘인 경우는 절대 없음’, ‘언젠가 리더가 선출됨’과 같은 속성임.
  • TLA+ 모델은 합법적인 시스템 상태와 상태 사이에서 허용되는 전이를 선언함.
  • 선거 예시에서는 초기 상태에서 a, b, c 중 누구든 선거를 시작할 수 있고, 선거를 시작하면서 스스로에게 투표함. b는 a 또는 c에게 투표할 수 있음.
  • 전이 순서는 정해져 있지 않으며, 사건 발생 확률 분포도 모델링하지 않음. 메시지, 타임아웃, 사용자 동작이 여러 순서로 발생할 수 있는 분산 시스템에 적합한 추상화임.

수학적 기반과 시간 속성

  • 기반 수학은 집합, 참·거짓 진술, 관계를 사용함.
  • 시간 속성은 실행에 적용되는 연산자로 구성됨.
  • □ P(항상 P): 방문한 모든 상태에서 P가 성립함.
  • ◇ P(언젠가 P): 미래의 어느 상태에서 P가 성립함.
  • P ⇝ Q(P가 Q로 이어짐): P가 성립할 때마다 그 이후 언젠가 Q가 성립함.

안전성과 활성성

  • 안전성(safety)은 나쁜 일이 절대 발생하지 않는다는 속성임. 선거에서는 □(리더가 둘인 경우는 없음)으로 표현함.
  • 플레이그라운드의 모델 검사기는 가능한 상태를 모두 탐색함. 컴퓨터가 세 대인 모델에서는 전체 38개 상태를 확인해 속성이 성립함을 확인함.
  • 레벨 2에서는 컴퓨터가 두 번 투표할 수 있도록 규칙 하나를 바꿈. 검사기는 두 명의 리더가 생기는 지점에서 끝나는 6단계 실행을 반환함. 이 실행은 모델이 속성을 위반하는 구체적인 경로인 반례임.
  • 활성성(liveness)은 좋은 일이 언젠가 일어난다는 속성임. 아무것도 하지 않고 영원히 멈춘 시스템도 안전성만 놓고 보면 완벽하게 안전하므로, ◇(누군가가 리더임)과 같은 조건이 필요함.
  • 레벨 3은 오타로 아무 일도 일어나지 않게 되어도 안전성 검사는 통과할 수 있음을 보여줌.
  • 활성성 검증에는 공정성 가정이 필요함. 이 가정은 어떤 동작이 영원히 가능하지만 실행되지 않는 경로를 배제함.
  • 약한 공정성 WF(A)는 계속 활성화된 동작이 결국 발생한다고 규정함. 강한 공정성 SF(A)는 무한히 자주 활성화되는 동작을 다룸.

모델 검사와 증명

  • TLA+ 모델은 시스템의 가능한 실행 추적을 기술하고, 속성은 그중 어떤 추적이 허용되는지를 기술함. 검증은 가능한 모든 추적이 허용 가능한지 묻는 과정임.
  • 표준 TLA+ 모델 검사기인 TLC는 유한한 사례에서 도달 가능한 상태를 열거해 이 질문에 답함.
  • 증명은 속성이 일반적으로 성립한다는 더 강한 주장을 제시함.