분산 프로토콜 검증을 위한 시나리오 증명

분산 프로토콜의 형식적 검증은 여전히 귀납 불변성(inductive-invariant) 증명에 의해 지배되고 있으며, 여기서 핵심 과제는 도달할 수 없는 상태를 배제하는 강화 주장(strengthening assertions)을 발견하는 것입니다. 이러한 부담은 종종 프로토콜 설계자가 추론하는 방식과 맞지 않습니다. 그들은 대표적인 실행(representative executions), 인과적 이력(causal histories), 그리고 노드 간의 단계별 상호작용을 따라가면서 정확성을 설명합니다. 본 논문은 이러한 실행 중심적 추론을 형식화하는 검증 방법론인 시나리오 증명(scenario proofs)을 소개합니다. 시나리오는 고스트 변수(ghost variables)로 풍부하게 만들어진 대표적인 프로토콜 실행을 기술하는 구조화된 표현입니다. 모든 가능한 인터리빙(interleavings)을 열거하는 대신, 시나리오는 정형적 실행(canonical executions)을 설명하고, 실현 가능성(feasibility)과 최종 상태를 보존하는 재순서화(reorderings)를 처리하기 위해 건전한 반-교환 관계(sound semi-commutation relation)를 사용합니다. 검증은 두 가지 주요 의무로 나뉩니다. 커버리지(Coverage)는 모든 실현 가능한 프로토콜 실행이 시나리오가 설명하는 것과 반-교환까지 동등함을 보여줍니다. 이 의무는 안전성 속성(safety property)에 독립적이며, 프로토콜의 재사용 가능한 행동 특성화 역할을 합니다. 정확성(Correctness)은 시나리오 구조를 따라 Hoare 스타일의 가장 약한 전제 조건 추론(weakest-precondition reasoning)을 사용하여 대표적인 실행에 대해서만 원하는 안전성 속성을 증명합니다. 우리는 시나리오 언어, 그 계층적 의미론(layered semantics), 그리고 커버리지와 정확성에 대한 증명 규칙을 형식화합니다. 링 리더 선출(ring leader election), 2단계 커밋(two-phase commit), 분산 잠금(decentralized lock), 다중 서명 결제 두 가지 변형(two variants of multi-signature payment), 그리고 단일 결정 Paxos(single-decree Paxos)의 사례 연구를 통해, 시나리오 증명이 프로토콜 설계자가 비공식적으로 사용하는 인과적 및 단계 기반 주장을 어떻게 포착하는지 보여줍니다. 이러한 예시는 시나리오 증명이 거대한 불변성 발견을 대표적인 실행에 대한 구조화된 추론으로 대체할 수 있으면서도 모든 실현 가능한 프로토콜 동작과의 엄격한 연결성을 유지할 수 있음을 보여줍니다.