윤상호조

프로젝트 개요

기술개발 과제

국문 : ZooKeeper Atomic Broadcast 프로토콜의 형식적 명세

영문 : Formally Specifying ZooKeeper Atomic Broadcast Protocol

과제 팀명

윤상호

지도교수

이병정 교수님

개발기간

2019년 3월 ~ 2019년 6월 (총 4개월)

구성원 소개

서울시립대학교 컴퓨터과학부 2016920064 윤상호

서론

ZooKeeper는 Yahoo! Research에서 만들어진 분산 설정 관리 시스템이다. 한 대의 물리장비로 이루어진 시스템은 전력 손실이나 통신 두절 등의 이유로 서비스 실패의 가능성을 가지고 있으므로 실패를 줄이고 높은 사용성을 이루기 위해선 데이터를 물리적으로 독립된 여러 저장소에 복제해야 한다. ZooKeeper는 데이터의 복제를 통한 높은 가용성과 읽기 요청이 많은 경우에 대해 높은 성능을 가질 것을 목적으로 설계되었으며 Yahoo!의 크롤러나 Facebook의 설정 관리 시스템, Twitter의 서비스 발견 시스템 등에서 사용되고 있다. ZooKeeper가 내부적으로 사용하는 프로토콜은 크게 두 가지인데 첫 번째는 시스템을 구성하는 클러스터의 리더를 선출하는 프로토콜이고 두 번째는 데이터의 정합성을 보장하는 ZAB(ZooKeeper Atomic Broadcast)이다. ZAB이 프로토콜 진행 중 리더 선출 프로토콜을 사용하는 형태이며 따라서 ZAB이 클러스터 간 데이터의 정합성을 보장한다는 속성을 확인하는 것은 인터넷 규모의 트래픽을 소화하는 시스템에서 사용되기에 높은 가용성과 성능이 요구되는 시스템들이 핵심적으로 의존하고 있는 ZooKeeper를 위해 선행되어야 한다고 볼 수 있다. 기존 연구에서는 ZAB이 가지는 속성과 그 증명을 다루지만 형식 언어로 작성되어 있지 않기 때문에 기계적으로 검증해 볼 수 없다는 한계를 가지고 있다. 이 논문에서는 ZooKeeper의 주요 동기화 프로토콜인 ZooKeeper Atomic Broadcast를 TLA+로 모델링하고 프로토콜이 보장하는 가용성과 정합성이 모델에서 충족될 수 있는지 모델 체킹 기법을 통해 확인한다.

개발 과제의 개요

개발 과제 요약

ZooKeeper는 여러 분산 소프트웨어 시스템이 의존하고 있는 설정 관리 시스템이며 ZooKeepr Atomic Broadcast 프로토 콜은 ZooKeeper의 핵심 프로토콜이다. 그렇기 때문에 프로토콜의 정확성에 대한 보증이 먼저 이루어져야 한다고 볼 수 있으며 기존 의 연구에서는 형식적이지 않은 방식으로 이루어진 증명으로 인해 해당 증명이 정말로 올바른지 확인하기 위해서는 사람의 이해가 선행되어야 한다는 한계를 가지고 있다. 이 연구에서는 TLA+를 통한 프로토콜과 프로토콜의 속성에 대한 형식적인 명세를 통해 기계적으로 검증 가능한 모델을 만들어 프로토콜의 정확성과 안정 성에 대한 확신을 위해 필요한 증명의 이해에 드는 비용을 줄이는 작업을 진행했다. 프로토콜의 세 페이즈에 대한 모델을 만들었고 4가지의 속성을 명세하고 모델 체킹함으로써 만들어진 모델이 속 성을 만족하는 것을 확인할 수 있었다.

개발 과제의 배경

• Model Checking

모델 체킹이란 소프트웨어 또는 하드웨어 시스템의 모델과 명세(Specification)가 주어졌을 때 시스템의 모델이 가질 수 있는 상태를 전부 탐색하여 모델이 명세에 명시된 속성들을 만족하는지 도구를 활용해 자동으로, 빠짐없이 확인하는 행위이다. 모델과 명세를 작성하는 언어는 기계적으로 체크되어야 하기 때문에 문법과 의미가 수학적으로 엄밀히 정의된 형식 언어여야 하고 이 논문에서는 TLA+(Temporal Logic of Actions)라는 형식 언어와 이 언어로 작성된 모델과 명세를 확인할 수 있는 소프트웨어인 TLC를 사용한다.

• Temporal Logic of Actions

1977년 Pnueli가 시간 논리(temporal logic)를 통해 기존 논리 체계에 "영원히"라는 논리 한정자를 도입한 것을 시작으로 "next", "until" 그리고 "since"와 같은 논리 한정자가 추가되기 시작했는데 Lesslie Lamport는 Pnueli의 시간 논리에서 상태 하나에 대한 선언과 actions(여러 개의 상태)에 대한 선언을 추가한 Temporal Logic of Actions(TLA)를 제안하여 동시성을 가진 소프트웨어에 대한 추론의 많은 부분을 시간 논리를 사용하는 것에서 actions에 대한 추론만을 사용하는 것으로 바꾸게 되었다.

• TLA+

TLA+는 Temporal Logic of Actions와 ZF 집합론을 사용해 만든 분산 시스템을 위한 고수준 명세 언어이며 언어를 실행할 수 있는 도구를 포함한다. TLA를 통해 비형식적인 방법으로 소프트웨어에 대한 증명을 시도하던 과정에서 기계적인 검증을 위해 만들어진 언어이기에 일반적인 프로그래밍 언어와는 달리 기초적인 논리 표현식을 바탕으로 하고있으며 모델링의 대상이 되는 시스템의 상태 공간을 정의하고 시스템의 초기 상태와 상태 전이 규칙, 그리고 safety속성과 liveness속성을 정의하면 TLA+는 시스템이 도달 가능한 모든 상태를 탐색하여 주어진 속성을 만족하는지 확인하게 된다.

• PlusCal

PlusCal은 TLA+가 프로그래밍 언어의 형태를 닮지 않아 엔지니어가 접근하기 어렵다는 문제를 해결하기 위해 만들어진 언어이다. 절차적인 방식으로 알고리즘을 기술할 수 있도록 설계되었으며 동시성을 가진 알고리즘을 기술하기 쉽도록 관련된 언어 기능들이 추가되어있다. 모든 PlusCal 프로그램은 TLA+로 변환될 수 있기에 TLA+와 마찬가지로 PlusCal도 집합론과 일차 논리로 표현할 수 있는 모든 수학적인 명제를 표현할 수 있으며 추가적으로 if, while, goto와 같은 제어문과 동시성을 가진 소프트웨어의 모델링을 위한 process 선언 기능을 제공한다.

• TLC

TLC는 TLA+로 작성된 명세의 유한 상태 공간에 대해 safety 속성과 liveness 속성을 체크하는 소프트웨어이다. 동시성을 가진 소프트웨어 시스템의 디자인을 돕기위해 고수준 명세에 대한 유한 상태 공간 모델을 탐색하는 방식을 사용하며 이 논문에서는 PlusCal로 작성한 명세를 TLA+로 변환한 후 TLC를 통해 모델 체킹을 하게 된다. 모델 체킹을 위해 TLC가 받는 입력은 두 가지이며 하나는 PlusCal 또는 TLA+로 작성된 시스템의 명세(specification)이고 다른 하나는 명세가 부합해야 할 시스템의 모델이다. 명세가 PlusCal로 작성되었을 경우 먼저 TLC에서 제공하는 기능을 통해 PlusCal을 TLA+로 변환해야 하며 모델 값을 설정하면 TLC가 입력으로 받은 명세가 입력으로 받은 모델에 부합하는지 모든 상태 공간을 탐색하는 방법으로 확인하게 된다.

개발 과제의 목표 및 내용

계층적 키-값 정보를 저장하는 분산 시스템인 Apache ZooKeeper의 핵심 프로토콜인 ZooKeeper Atomic Broadcast 프로토콜의 형식적 명세를 작성해 프로토콜의 핵심적인 조건을 만족하는지 확인한다.

관련 기술의 현황

관련 기술의 현황 및 분석(State of art)

• 전 세계적인 기술현황

Leesatapornwongsa, Tanakorn, et al. "{SAMC}: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems." 11th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 14). 2014.

SAMC(Semantic-Aware Model Checking) 시스템은 분산 시스템 모델 체커(distributed systems model checker) 중 하나로, Model Checking기법을 활용해 ZooKeeper를 포함한 MapReduce와 Cassandra를 정적 검사한 시스템이다. SAMC에서는 모델 체킹을 통해 식별한 버그를 재현하기 위한 스텝이 길 경우 해당 버그를 DeepBug로 정의하고 분석 대상 시스템에서 SAMC가 식별할 수 있는 DeepBug가 얼마나 존재하는지, 그리고 알려진 버그도 SAMC가 잡아낼 수 있는지를 논한다. 기존 분산 시스템 모델 체커와는 다르게 시스템의 프로토콜만을 모델링하는 것이 아닌 시스템이 크래시되고 복구되는 경우, 시스템이 리붓 후 동기화를 맞추는 경우를 포함한 문맥 정보를 추가해 더 많은 버그를 식별할 수 있다고 주장하며 문맥 정보를 도입함으로써 발생하는 부하를 어떤 기법을 통해 줄일 수 있었는지 다룬다.

Hawblitzel, Chris, et al. "IronFleet: proving practical distributed systems correct." Proceedings of the 25th Symposium on Operating Systems Principles. ACM, 2015.

IronFleet은 올바름을 보일 명세만 작성하는 것이 아니라 명세에 대한 구현까지 작성한 후 이 구현이 명세를 만족하는지에 대한 완전한 형식적 검증이 가능하다. IronFleet은 이를 이루기 위해 소프트웨어 시스템의 명세와 구현을 프로토콜 층위, 명세 층위 그리고 구현 층위로 나누었고 프로토콜 층위의 정제(refinement)가 명세 층위가 되고 다시 명세 층위의 정제가 구현 층위가 된다는 것을 증명하는 기법을 사용했고 프로토콜 층위에서 분산 시스템의 liveness 속성을 증명하기 위해 이 과제에서 사용할 TLA(Temportal Logic of Actions)를 IronFleet이 사용하는 언어인 Dafny에 내재(embed)시켰다. TLA를 내재하는 과정에서 SMT와 함께 복합적인 사용을 어떻게 구현할 수 있었는지와 함께 Dafny에 존재하지 않는 네트워크 라이브러리를 어떻게 만들었고 이를 통해 작성한 UDP통신이 바이트 레벨에서 전부 올바르도록 어떻게 구현할 수 있었는지에 대해서 다룬다.

Wilcox, James R., et al. "Verdi: a framework for implementing and formally verifying distributed systems." ACM SIGPLAN Notices. Vol. 50. No. 6. ACM, 2015.

Verdi는 분산 시스템을 형식적으로 검증하기 위한 Coq 프레임워크이다. IronFleet과 마찬가지로 시스템의 명세뿐 아니라 구현까지 같이 작성할 수 있으며 구현이 명세를 만족하는지에 대한 검증도 할 수 있다. Verdi의 사용자는 Coq라는 증명 보조기(Proof Assistant)를 사용해 시스템의 명세 및 시스템이 만족해야 할 속성을 기술할 수 있고 마찬가지로 Coq가 지원하는 증명 언어인 tactic을 사용해 속성에 대한 증명을 작성할 수 있다. 작성된 명세와 증명은 Coq에서 제공하는 추출기를 통해 OCaml이라는 함수형 프로그래밍 언어로 추출되며 이 OCaml이 OCaml 컴파일러에 의해 최종적으로 실행 가능한 바이너리로 변환되는 구조이다. 논문에서는 분산 시스템의 특징은 fault-tolerance를 Verdi가 어떻게 모델링하고 있는지 이야기하며 Raft라는 분산 프로토콜을 Verdi로 명세하고 구현한 사례를 다루기도 한다. Raft는 ZooKeeper Atomic Broadcast, Paxos와 비슷한 추상 레벨을 가진 프로토콜이며 Raft의 사례에서 분산 프로토콜의 명세를 어떻게 명세하는지 참고하여 과제를 진행할 수 있을 것이다.

Newcombe, Chris, et al. "How Amazon web services uses formal methods." Communications of the ACM 58.4 (2015): 66-73.

아마존이 자사의 클라우드 서비스인 S3(Simple Storage Service)와 DynamoDB, EBS(Elastic Block Store), Internal distributed lock manager를 대상으로 TLA+ 모델링을 한 후 결과를 보고하는 논문이다. 형식적 방법론(formal methods)의 필요성에 대해서 이야기한 후 여러 가지 기법들 중 왜 TLA+를 선택했는지와 함께 TLA+를 통해 모델링한 시스템들에서 어떤 버그를 발견할 수 있었는지에 대해서 다룬다. S3 서비스의 Fault-tolerant low-level network algorithm은 804줄의 PlusCal로 모델링할 수 있었고 2개의 버그를 발견할 수 있었으며 동일 서비스의 Background redistribution of data 컴포넌트는 645줄의 PlusCal로 모델링할 수 있었고 1개의 버그를 발견할 수 있었다고 보고한다. 이와 비슷하게 EBS, DynamoDB, Internal distributed lock manager의 몇 개 컴포넌트들도 PlusCal 또는 TLA+를 통해 모델링했고 각각 3, 3, 1개의 버그를 발견했다고 보고한다. 논문에서는 TLA+로 작성된 명세사항을 “Exhaustively testable pseudo-code” 라고 표현하며 사내 엔지니어들에게 시스템 디자인을 위해 TLA+ 사용을 장려한다는 이야기도 다루어진다.

• 특허조사 및 특허 전략 분석

ZooKeeper는 Apache 오픈소스 라이선스를 사용하고 있기 때문에 ZooKeeper의 일부인 ZAB과 관련된 특허는 존재하지 않을 것이라 생각하며 ZooKeeper를 기반으로 하는 분산 시스템에서 순서가 매겨진 숫자를 생성하는 방식에 대한 특허는 존재하는 것으로 보인다

• 기술 로드맵

ZAB 프로토콜 및 invariant들의 명세

기술의 기초를 위해서 먼저 ZAB프로토콜이 무엇인지에 대한 명세와 그 프로토콜이 만족해야 하는 성질이 무엇인지 TLA+로 표현하는 작업이 필요하다. 필요할 경우 속성에 대한 증명도 작성해야 하며 정의, 속성, 증명이 TLC를 통해 Model checking이 되어야 올바른 명세와 속성을 완성했다고 판단할 수 있다.

Fast Leader Election 프로토콜 및 Invariant들의 명세

위의 명세가 완료되었다면 ZAB에 추가된 Fast Leader Election 프로토콜의 검증도 생각해 볼 수 있다. Fast Leader Election은 ZAB의 구현 과정에서 성능 상의 이점을 취하기 위해 몇 가지 변경사항을 도입한 프로토콜이며 기존의 프로토콜 검증 관련된 연구들은 Fast Leader Election이 도입되기 전에 진행되었기 때문에 검증의 완전함을 갖추기 위해 Fast Leader Elect 프로토콜을 대상으로 검증해야 할 사항들이 존재할 것이라 예상한다.

Formal verification으로의 확장

이 과제에서는 ZAB의 형식적 명세에서 그치지만 ZAB의 형식적 검증으로도 확장될 수 있다. 그 방식은 크게 두 가지인데 하나는 명세를 먼저 작성하고 이 명세가 Java로 구현된 ZooKeeper의 구현과 일치하는지 확인하는 것이고 두 번째 방식은 명세를 작성한 후 그 명세로부터 Verdi나 IronFleet의 접근 방식처럼 실행 가능한 바이너리를 추출하는 것이다. 첫 번째는 Java 프로그램을 분석하기 위한 기법들이 필요할 것이라 예상되고 두 번째 방식은 실행 가능한 바이너리를 추출하는 데에 성공했다 하더라도 표준 ZooKeeper 구현의 성능을 따라잡을 수 있는지에 대한 평가가 이루어져야 할 것이다.

시장상황에 대한 분석

• 경쟁제품 조사 비교

Apache ZooKeeper ZooKeeper는 Yahoo! Research에서 개발되어 Yahoo의 configuration management, membership service등 내부 시스템의 coordination시스템으로써 사용되다 2007년 처음으로 SourceForge에 오픈소스로 공개되었고 그 이후 Apache Hadoop의 서브프로젝트로써 포함되어 현재는 Apache 재단의 최고 레벨 프로젝트로 관리되고 있다. ZooKeeper는 오늘날 Twitter , Facebook , Reddit , eBay , LINE 등의 회사에서 사용되고 있으며 같은 Apache 재단 프로젝트인 Kafka와 Hadoop에서도 클러스터 설정 관리 시스템으로써 사용되고 있다.

Google Chubby Chubby는 2006년에 Google에서 공개된 분산 시스템을 위한 락(lock) 서비스이다. 구글도 Yahoo와 마찬가지로 여러 대의 장비로 구성된 분산 시스템이 상호 작용하는, 조율이 필요한 환경에 노출되어 있었고 조율 문제를 해결하기 위해 락을 사용하는 Chubby 서비스를 만들었다. Chubby는 ZooKeeper와 비슷하게 적은 양의 정보, 특히 시스템의 설정에 관련된 정보 혹은 클러스터의 구성같은 메타 정보등을 여러 대의 장비 또는 서비스에서 동기화할 수 있는 기능을 제공하며 구글의 핵심 시스템인 GFS(Google File System), BigTable외에도 내부적으로 조율이 필요한 곳에서 사용되고 있다.

• 마케팅 전략 제시

마케팅 전략은 존재하지 않는다.

개발과제의 기대효과

기술적 기대효과

ZooKeeper Atomic Broadcast 프로토콜 버그의 발견

TLA+로 ZAB을 명세하고 TLC를 통해 기계적으로 확인하는 접근을 선택한 논문이 존재하지 않으므로 이 과제에서 사용된 접근법을 통해 ZAB의 모델링에 성공할 경우, 기존 연구들이 확인하지 못했던 시스템의 동작 공간을 탐색해 새로운 버그를 발견할 수 있을 것을 기대해 볼 수 있다. 특히 최근에 추가된 Fast Leader Election 프로토콜은 구현만 존재하고 형식적 증명은 이루어지지 않았기 때문에 Fast Leader Election 프로토콜의 명세에도 성공할 경우 관련된 버그를 찾을 수 있다고 기대할 수 있다.

ZooKeeper Atomic Broadcast 프로토콜의 올바름의 새로운 확증

이 과제를 통해 성공적인 명세가 이루어지고 TLC도 통과하게 되면 이미 업계에서 널리 사용 중인 ZAB이 프로토콜 레벨에서 버그가 없다는 사실을 다시 한번 확인해 ZAB을 사용하는 분산 시스템들의 reliability를 높이는 효과를 기대할 수 있다.

Formal method 기법의 확장

TLA+를 통한 형식적 명세의 작성은 프로그램이 올바른지 확인하는 기법인 formal method의 일종이며 ZooKeeper라는 실용적인 시스템의 핵심을 이루는 ZAB 프로토콜의 형식적 명세를 통한 기계적 검증은 현실 세계의 문제에 적용된 formal method로써의 의미를 가질 수 있고 과제의 결과에 따라 formal method기법이 적용될 곳을 늘릴 수 있다는 확장 효과를 기대할 수 있다.

경제적, 사회적 기대 및 파급효과

ZooKeeper Atomic Broadcast 프로토콜의 버그가 발견되었을 경우 대형 소프트웨어 시스템의 coordination 서비스로써 동작하는 Zookeeeper의 내부 프로토콜인 ZAB의 버그가 발견되었을 경우 보안 취약점으로써 활용될 수 있고 이 취약점은 대형 소프트웨어 시스템의 공격에 활용될 수 있다. 특히 공격의 대상인 시스템이 상업적 용도를 가지고 있을 경우 정보 탈취를 통한 시스템 사용자들의 경제에 악영향을 미칠 수 있을 것이라고 생각한다.

기술개발 일정 및 추진체계

개발 일정

3,4월: TLA+ 학습

4,5월: ZAB 학습

5,6월: 논문 작성

구성원 및 추진체계

윤상호

설계

설계사양

제품의 요구사항

번호	요구사항	D or W	비고
1	기존 논문에서 증명된 속성의 명세	D
2	Temporal 속성의 명세	W
3	ZAB이 사용하는 리더 선출 프로토콜의 명세	W
4	ZAB의 Java구현이 사용하는 Fast 리더 선출 프토콜의 명세	W
5	대칭 집합 모델 등의 모델 체킹 최적화 기법 적용	W

설계 사양

ZAB 프로토콜이 수행되는 시스템은 크래시가 발생할 수 있으나 영속적인 저장장치를 가져서 크래시로부터 복구될 수 있는 여러 개의 프로세스로 구성되어 있다. 시스템을 S = {p1, p2, ..., pn}(pn = process)라 했을 때 어떤 프로세스 pn 가 크래시되지 않은 상태라면 up process라 부르고 크래시 가 발생했다면 down process라 부른다. 프로토콜의 실행을 위해 프로세스 간 커뮤니케이션이 필수적이며 커뮤니케이션 방식은 메세지 전달 방식을 사용한다. 프로토콜이 수행되기 위해서 언젠가는(eventually) 충분히 많은 숫자의 프로세스가 충분히 오랜 시간동안 up상태에 놓여있을 것이라는 사실을 가정한다.

개념설계안

• 프로세스 모델

ZAB 프로토콜에서 하나의 프로세스는 leader, follower의 두 가지 역할 중 하나 이상을 수행하게 된다. 각각의 프로세스는 영속적인 저장장치에 아래 4 개의 정보를 저장 할 수 있기에 동작 중 크래시가 발생하더라도 정보가 유지될 수 있다고 가정한다.

• • history: 수락된 트랜잭션들의 로그
  • acceptedEpoch: 마지막으로 수락된 NEWEPOCH 메시지의 epoch
  • currentEpoch: 마지막으로 수락된 NEWLEADER 메시지의 epoch
  • lastZxid: history의 마지막 트랜잭션의 zxid

추가로 아래 2개의 변수도 가각의 프로세스가 가지고 있다고 가정한다.

• • loracle: 현재 리더 프로세스가 몇 번 프로세스인지에 대 한 정보
  • isReady: 프로세스가 브로드캐스트를 하기 위한 준비가 되어 있는지에 대한 상태

• 채널 모델

프로세스간 통신은 채널을 통해 이루어지며 어떤 프로세스 p_i와 p_j의 통신을 위한 채널을 c_ij로 나타낸다. 각각의 프로세스는 자신이 참여하고 있는 채널마다 입력 버퍼와 출력 버퍼를 가지고 있으며 p_i가 p_j로 메세지 m을 보낸다고 가정하면 먼저 메세지 m은 p_i의 출력 버퍼에 입력되고 채널을 통해 전달된 m은 p_j의 입력 버퍼에 쌓이게 된다. 프로세스 p_j에게 메세지 m을 보내는 이벤트는 send(m, p_j)로 나타내며 p_j의 입력 버퍼로부터 메시지 m을 받는 이벤트는 recv(m p_i)로 나타낸다. ZAB 프로토콜은 리더가 교체되었을 경우 새로운 이터레이션을 시작해야 하고 새 이터레이션은 새로운 채널을 수립해야 하므로 각각의 채널은 고유한 이터레이션에 속하게 된다.

상세설계 내용

• 브로드캐스트 프로토콜

브로드캐스트 프로토콜은 일반적으로 여러 프로세스로 구성되며, 그 중 특정 프로세스 하나가 프로토콜에 참여하는 다른 프로세스들에게 메시지를 전달하는 구조이다. 원자적(atomic) 브로드캐스트 프로토콜이란 전달되는 메시지가 모든 프로세스에게 전달되거나 아예 전달되지 않는다는 성질을 보장하는 프로토콜을 의미한다.\cite{tap}

• 트랜잭션

트랜잭션이란 브로드캐스트를 통해 전파되는 상태의 변화 하나를 의미한다. 트랜잭션 <v, z>는 두 개의 원소로 이루어진 튜플이다. v는 트랜잭션을 통해 전파되는 값을 나타내며 z는 트랜잭션 식별자(zxid)를 의미한다. 트랜잭션 식별자는 <e, c>로 정의되며 e는 epoch을 의미하고 c는 카운터를 의미한다. 두 트랜잭션 식별자 $z = <v, <e, c>>, $z' = <v', <e', c'>>는 비교가 가능하며 z < z'일 경우 e < e'이거나 e = e' & c < c'임을 의미하며 z가 z'를 선행한다라고 표현한다.

• Quorum

다수의 프로세스로 이루어진 시스템이 하나의 값을 결정한다는 것은 과반수 이상의 프로세스가 동일한 값을 가진다는 것을 의미하고 이 때 과반수 이상의 프로세스의 집합을 quorum이라 정의한다. PlusCal의 모델에서는 toLeader, toFollower변수와 같이 전역 변수로써 설정되고 정의는 quorum = 1..N \ {loracle}로 정의해 리더 프로세스를 제외한 follower 프로세스 전체로 모델링하고 있다.

• Request의 개수 크기

ZAB의 트랜잭션은 시스템 사용자의 요청에 의해서 발생하기에 ZAB을 모델링하기 위해선 시스템 사용자의 요청을 모델링 할 필요가 있다. 이 명세에서는 프로세스의 개수 $N$과 비슷하게 사용자 요청의 개수 R이라는 모델 값을 만들고 파라미터로써 설정하는 방식을 선택한 후 PlusCal에서 R의 크기 만큼의 사용자 요청을 처리하는 형태로 프로토콜을 모델링했다.

• 프로토콜 페이즈

각각의 프로세스는 한 번에 하나의 페이즈를 실행하며 프로세스가 실행 중 down process가 되어 다시 시작될 경우 현재의 페이즈를 포기하고 첫 번째 페이즈부터 다시 시작할 수 있다. 리더의 역할을 수행 중인 프로세스일 경우 Follower의 역할도 동시에 수행되게 된다. 프로토콜을 이루는 3개의 페이즈는 발견, 동기화, 브로드캐스트이며 PlusCal로의 모델링은 각각의 프로세스에서의 분기를 통한 결정 방식을 사용한다.

CONSTANTS N
process (Peer \in 1..N)
    variables requests = 0,
              history = << >>,
              last_zxid = -1,
              accepted_epoch = -1,
              current_epoch = -1;
{
    p1: while (requests < R) {
          if (self = loracle) {
                 if (phase[self] = 1) {
                     (* Execute leader phase 1 *)
                 } else if (phase[self] = 2) {
                     (* Execute leader phase 2 *)
                 } else if (phase[self] = 3) {
                     (* Execute leader phase 3 *)
                 }
           } else {
                 if (phase[self] = 1) {
                     (* Execute follower phase 1 *)
                 } else if (phase[self] = 2) {
                     (* Execute follower phase 2 *)
                 } else if (phase[self] = 3) {
                     (* Execute follower phase 3 *)
                 }
         }
   }
}

history, last_zxid, accepted_epoch, current_epoch 변수는 프로세스의 지역 변수이고 request는 개별 프로세스가 자신이 현재 몇 번째 유저 요청을 처리하고 있는지를 나타내는 변수이다. 총 R개의 유저 요청이 처리되었을 경우 프로세스는 종료되게 된다.

• 프로토콜 속성

ZAB이 원자적 브로드캐스트 프로토콜이기 위해서는 아래의 네 가지 성질을 만족해야 한다.

• • Validity: 올바른 프로세스가 메시지를 전달한다면 모든 올바른 프로세스는 해당 메시지를 언젠가는 전달받는다.
  • Agreement: 어떤 프로세스 p₁이 <v,z>을 전달받았고 다른 프로세스 p₂가 <v',z'>을 전달받았다면 p₁이 <v',z'>을 전달받거나 p₂가 <v,z>을 전달받는다.
  • Integrity: 어떤 메시지 m의 발신자를 s라 하면 모든 프로세스는 m을 최대 한 번 전달받는다.
  • Total Order: 어떤 프로세스 p와 q가 두 개의 메시지 m, m'을 전달 받았을 경우, p가 m' 보다 전에 m을 전달 받았다면 q도 m' 보다 전에 m을 전달받아야 하며 반대의 경우도 마찬가지이다.

• 프로토콜 속성의 TLA+ 표현

• • Agreement: 기본 아이디어는 먼저 임의의 두 프로세스 p₁, p₂의 history에서 서로 다른 두 개의 트랜잭션 쌍 <t₁, t₂>을 찾은 다음 t₁이 p₂의 history에 속해있거나 t₂가 p₁의 history에 속해있는지를 확인하는 것이며 TLA+ 식으로 나타내면 다음과 같다. $\forall x,y \in quorum : Len(history[x]) > 0 \land Len(history[y]) > 0 \Rightarrow (\forall i \in 1..Len(history[x]), j \in 1..Len(history[y]) : history[x][i] /= history[y][j] \Rightarrow (\exists ix \in 1..Len(history[x]) : history[x][ix] = history[y][j]) \lor (\exists jy \in 1..Len(history[y]) : history[y][jy] = history[x][i])) $

• • Total Order: 두 개 이상의 트랜잭션($t_1, t_2, ...$)을 가지고 있는 $history$를 가진 프로세스를 찾은 후 $t_2$를 $history$에 포함하고 있는 프로세스들이 $t_1$도 가지고 있는지를 확인하면 되며 TLA+ 식으로 나타내면 다음과 같다. $\forall q \in quorum : Len(history[q]) > 1 => \forall i,j \in 1..Len(history[q]) : i > j \Rightarrow \forall q2 \in quorum : (\forall iq2 \in 1..Len(history[q2]) : history[q2][iq2] = history[q][i] => \exists jq2 \in 1..iq2-1 : history[q2][jq2] = history[q][j])$

• • Validity: $quorum$에서 가장 작은 수로 표현되는 프로세스를 $s$라 하면 $s$의 $history$가 언젠가는 유저 요청의 수 만큼 늘어나게 된다는 사실과 이 늘어난 $history$를 $quorum \setminus \{s\}$도 동일하게 가지고 있다는 사실을 TLA+로 표현하면 다음과 같다. $LET\ s = CHOOSE\ x \in quorum : \forall q \in quorum \ \{x\} : x < q IN \langle\rangle(Len(history[s]) = requests \land \forall q \in quorum \ \{s\} : history[q] = history[s])$

• • Integrity: ZAB 프로토콜은 리더 프로세스만 PROPOSE 메시지를 보낼 수 있고 ZAB이 사용하는 채널 모델인 TCP의 integrity속성 때문에 보내진 메시지만 받을 수 있다는 사실로부터 Integrity 속성을 자명하게 도출해낼 수 있기에 따로 표현하지 않았다.

결과 및 평가

완료 작품의 소개

프로토타입 사진 혹은 작동 장면

• TLA+ ToolBox 첫 실행 화면

• ZAB 명세 생성 팝업 창

• ZAB 모델 설정 화면

• ZAB 모델 체킹 결과

완료작품의 평가 및 향후계획

분산 시스템이 따라야 하는 프로토콜은 설계하기 까다롭고 단일 시스템에 비해 버그가 발생할 수 있는 여지가 많다는 것은 잘 알려져있다. 이 논문에서는 산업계에서 널리 사용되고 있는 원자적 브로드캐스트 프로토콜인 ZooKeeper Atomic Broadcast를 TLA+라는 형식 언어를 통해 모델링하고 이 프로토콜이 지켜야 하는 4가지 속성도 마찬가지로 TLA+로 작성하여 기존의 연구에서 이루어졌던 손을 통한 증명을 기계적으로 검증 가능한 형태로 바꾸었다. 프로토콜은 4개의 프로세스, 5개의 프로세스로 구성된 모델에서 성공적으로 속성을 만족했고 이를 통해 프로토콜의 설계에 버그가 없음을 재확인 할 수 있었다. 이 작업을 바탕으로 이 후에는 명세를 발전시켜 fault-model을 만들고 정상적으로 동작하지 않는 프로세스가 존재할 때의 프로토콜이 속성을 지키는지에 대한 확인과 실제 구현에서 사용되고 있는 Fast Leader Election 프로토콜\cite{tap}에 대한 명세를 통해 존재하는 증명과 불일치되는 실제 구현과의 간극을 메우는 일도 생각해 볼 수 있을 것이다.