엔지니어링 철학: 레슬리 램포트, 코딩 전에 생각하라

핵심 요점

• 코드를 쓰기 전에 생각하고, 그 생각을 적어 두세요. 명세는 건축가의 청사진에 해당하는 소프트웨어 산물입니다. “생각하지 않으면 우리는 반드시” 실수를 하게 됩니다.
• 시간은 전역적이지 않으며, 실재하는 것은 인과성입니다. 신뢰할 수 있는 공유 시계가 없으면, 언제 사건이 일어났는지 묻기를 멈추고 무엇이 무엇을 일으켰는지를 묻게 됩니다.
• 선행 관계와 논리 시계가 인과성을 형식화합니다. 램포트의 부분 순서, 그리고 이를 구현하는 프로세스별 카운터는 벡터 시계와 현대 충돌 해소의 씨앗입니다.
• 정확성을 엄밀하게 정의한 다음, 그것을 증명하세요. 안전성과 활성, 팍소스 합의, 비잔틴 장애 허용, 그리고 TLA+ 명세 언어는 모두 분산 컴퓨팅을 민간 전승이 아니라 수학으로 다룬 데서 나왔습니다.

원칙

“분산 시스템이란, 존재하는지조차 몰랐던 컴퓨터의 고장이 당신 자신의 컴퓨터를 사용할 수 없게 만들 수 있는 시스템이다.” – 레슬리 램포트¹

그는 1987년 자기 연구소의 게시판에 그 문장을 보냈고, 그것은 분산 컴퓨팅에서 가장 많이 인용되는 문장입니다. 직관이 믿기를 거부하는 바로 그것을 짚어 내기 때문이지요.¹ 당신은 자신의 컴퓨터에서 프로그램을 돌리고 있다고 생각합니다. 그렇지 않습니다. 당신은 그것을, 존재를 일일이 헤아려 본 적도 없고 시계가 서로 어긋나며 그중 어느 하나라도 가장 중요한 바로 그 순간에 고장 날 수 있는 기계 무리에 걸쳐 돌리고 있습니다. 당신이 머릿속에 담을 수 있는 시스템과 실제로 돌아가는 시스템은 서로 다른 시스템이며, 그 둘 사이의 간극이 바로 모든 분산 버그가 사는 곳입니다.

램포트의 필생의 작업은 그 간극을 낙관으로 덮어 버리기를 거부하는 일입니다. 그의 신념은 동시성 시스템과 분산 시스템이 직관으로 추론하기에는 너무나 미묘하다는 것이며, 그래서 코드를 한 줄 쓰기 전에 종이 위에서 수학으로 그것들을 추론합니다. “생각한다고 해서 실수를 안 하리라는 보장은 없습니다,” 그는 2013년 와이어드에 말했습니다. “하지만 생각하지 않으면 반드시 실수하게 됩니다.”² 그 생각은 반드시 적어 두어야 합니다. 글쓰기가 곧 엉성한 사고가 드러나는 자리이기 때문입니다. “생각하려면 써야 합니다. 쓰지 않고 생각한다면, 당신은 생각하고 있다고 착각하고 있을 뿐입니다.”³ 건축가는 벽돌 한 장 놓기 전에 청사진을 그립니다. 소프트웨어에서 그에 해당하는 것이 명세이며, 램포트는 우리 시스템이 망가지는 이유가 바로 그 단계를 건너뛰기 때문이라고 자기 경력의 후반부 내내 주장했습니다.⁴

더 깊은 움직임은 시간 그 자체에 관한 것입니다. 물리적 세계에는 여러 기계에 걸쳐 사건의 순서를 매기리라 믿을 수 있는 전역 시계가 없습니다. 그래서 무언가가 언제 일어났는지 묻기를 멈추고 무엇이 무엇을 일으켰는지를 묻기 시작해야 합니다. 분산 계산의 실재하는 구조는 벽시계가 아니라 인과성입니다.⁵ 램포트가 만든 거의 모든 것이 그 한 가지 사실을 진지하게 받아들이는 데서 따라 나오며, 그것은 증거의 관문 밑바닥에 흐르는 것과 같은 신념입니다. 당신이 참이기를 바라는 순서를 그냥 가정할 수는 없습니다. 그 순서를 세워서 확립해야 합니다.

배경

레슬리 램포트는 1941년 2월 7일 뉴욕시에서 태어났습니다.⁶ 1960년 MIT에서 수학 학사를, 그리고 1972년 브랜다이스에서 편미분 방정식의 특이점에 관한 논문으로 수학 박사 학위를 받았습니다.⁶ 그는 컴퓨터 과학자로 훈련받지 않았습니다. 그는 수학자로 훈련받았고, 결코 수학자처럼 행동하기를 멈추지 않았습니다. 그의 경력을 규정짓는 특징은, 대체로 감으로 프로그래밍하던 분야에 수학의 기준—엄밀한 정의, 명시된 가정, 시험이 아닌 증명—을 들여왔다는 점입니다.

그 작업은 네 기관에 걸쳐 이루어졌습니다. 1970년대 매사추세츠 컴퓨터 어소시에이츠에서 그는 사건의 순서 매기기에 관한 토대를 이루는 사고를 했습니다. SRI 인터내셔널(1977–1985)에서는 비잔틴 장군 연구를 내놓았습니다. 디지털 이큅먼트 코퍼레이션의 시스템 연구 센터(1985년부터 컴팩 인수를 거쳐 2001년까지)에서는 팍소스를 썼고 명세 작업을 시작했습니다. 2001년부터 2025년 초 은퇴할 때까지 그는 마이크로소프트 리서치에 있었습니다.⁶ 그 모든 시기에 걸쳐 방법은 한결같았습니다. 모두가 민간 전승처럼 다루던 분산 또는 동시성 컴퓨팅의 문제를 찾아, 정리로 진술할 수 있을 만큼 엄밀하게 정의한 다음, 그 정리를 증명하는 것이었지요.

작업

시간, 시계, 그리고 선행 관계

“분산 시스템에서의 시간, 시계, 그리고 사건의 순서”는 1978년 Communications of the ACM에 실렸으며, 모든 컴퓨터 과학을 통틀어 가장 많이 인용되는 논문 중 하나입니다. 분산 컴퓨팅에서 가장 영향력 있는 작업에 주어지는 데이크스트라상을 2000년에 받았지요.⁵⁶ 그 통찰은 겉보기에는 작습니다. 분산 시스템에는 공유되고 신뢰할 수 있는 시계가 없으므로, 두 사건의 순서를 타임스탬프 비교로 매길 수 없습니다. 당신이 알 수 있는 것은 한 사건이 다른 사건을 일으킬 수 있었는지 여부입니다. 사건 A가 사건 B를 선행한다는 것은, A와 B가 같은 프로세스 위에 있고 A가 먼저인 경우이거나, A가 메시지를 보내는 것이고 B가 그 수신인 경우입니다. 이것들을 사슬처럼 이으면 선행 관계, 곧 형식화된 인과성을 얻습니다.⁵

결정적이면서도 직관에 반하는 귀결은, 선행 관계가 전체 순서가 아니라 부분 순서일 뿐이라는 점입니다. 서로 다른 프로세스 위에 있고 그 사이를 잇는 메시지 사슬이 없는 두 사건은 진정으로 동시적입니다. 어느 쪽이 먼저인지에 관한 사실은 존재하지 않으며, 그렇지 않은 척하는 시스템은 존재하지 않는 순서를 지어내는 셈입니다.⁵ 이어 램포트는 이제 보편적으로 램포트 시계라 불리는 알고리듬을 제시했습니다. 각 프로세스는 카운터를 유지하고, 모든 사건마다 그것을 증가시키며, 나가는 모든 메시지에 그 값을 찍습니다. 수신자는 자기 카운터를, 자기 값과 메시지의 타임스탬프 중 더 큰 값보다 하나 더 큰 값으로 올립니다.⁷ 그 단순한 규칙이 인과성과 일치하는 타임스탬프를 만들어 내며, 그것이 벡터 시계와 버전 벡터, 그리고 현대 분산 데이터베이스의 충돌 해소 기계 전체의 씨앗입니다.

이 논문이 알고리듬을 넘어 중요한 이유는, 그것이 질문을 바꾸어 놓았기 때문입니다. 램포트 이전에는 “이 일이 몇 시에 일어났는가?”가 분산 시스템에서 답할 수 있는 물음으로 여겨졌습니다. 램포트 이후로 정직한 답은 “잘못된 물음입니다—무엇이 그것을 일으켰는지 물으세요”가 되었습니다. 바로 그 재구성이, 그가 분산 컴퓨팅을 기예가 아니라 과학으로 만들었다고 평가받는 까닭입니다.

팍소스, 합의, 그리고 복제 상태 기계

전역 시계가 없고 기계가 고장 난다면, 한 무리의 컴퓨터들이 도대체 어떻게 무언가에—어느 트랜잭션이 커밋되었는지, 누가 잠금을 쥐고 있는지, 로그의 다음 항목이 무엇인지—합의에 이를 수 있을까요? 그 물음이 바로 합의 문제이며, 램포트의 답이 팍소스, 곧 그 이후로 만들어진 거의 모든 장애 허용 시스템의 심장에 있는 알고리듬입니다. 그는 그것을 복제 상태 기계 접근과 짝지었습니다. 모든 복제본이 같은 상태에서 출발해 같은 명령 순서를 같은 차례로 적용하면 그것들은 동일하게 유지됩니다. 그러면 분산 시스템을 일관되게 유지하는 문제 전체가 명령의 순서에 합의하는 문제로 환원되는데, 그것이야말로 팍소스가 제공하는 바입니다.⁶

팍소스가 어떻게 출판되었는가 하는 이야기는 이 분야에서 가장 유명한 경고담입니다. 램포트는 그것을 “시간제 의회”라는 제목으로 써냈는데, 알고리듬을 팍소스라는 가상의 고대 그리스 섬의 입법 절차로 꾸미고, 동료들의 이름을 그리스어 비슷하게 옮긴 이름을 가진 입법자들까지 등장시켰습니다.⁸ 그 농담은 참사였습니다. 심사자들은 그가 진지하지 않다고 여겼고, 논문은 하찮다는 이유로 반려되었으며, 그의 강연에 참석한 사람들은 알고리듬이 아니라 인디아나 존스풍의 설정만 기억했습니다.⁸ 그것은 여러 해 동안 출판되지 못한 채로 있었습니다. Communications of the ACM의 편집자가 결국 1998년 ACM Transactions on Computer Systems에 실었지만, 여전히 그 우화에 싸인 채였습니다.⁸ 분야가 계속 그것을 무시하자, 램포트는 마침내 항복하고 2001년 “쉽게 풀어 쓴 팍소스”를 써서 그리스풍 포장을 벗겨 내고, 그 밑에 정말로 단순한 알고리듬이 있다고 그가 줄곧 주장하던 바를 드러냈습니다.⁸ 그가 끌어낸 교훈은 “사람들이 멍청하다”가 아니었습니다. 옳고 중요한 아이디어조차 그 생각을 가리면 실패한다는 것, 곧 발표는 작업과 별개가 아니라 작업의 일부라는 것이었습니다.

비잔틴 장군 문제

1982년, 로버트 쇼스택, 마셜 피스와 함께 램포트는 “비잔틴 장군 문제”를 발표했고, 이로써 이 분야에 가장 어려운 종류의 장애를 가리키는 언어를 주었습니다.⁶ 고장 난 부품은 비잔틴 부품에 비하면 쉬운 편입니다. 비잔틴 부품이란 멈추는 것이 아니라 거짓말을 하는 부품, 즉 버그든 손상이든 악의든 간에 서로 다른 동료에게 서로 다르고 모순되는 정보를 보내는 부품입니다. 논문의 설정은 이렇습니다. 각각 한 장군이 이끄는 군대의 여러 사단이, 일부 미지의 장군들이 합의를 적극적으로 막으려는 배신자인 상황에서, 전령을 통해 단 하나의 작전—공격이냐 후퇴냐—에 합의해야 합니다. 램포트는 어떤 시스템이 여전히 합의에 이르면서 몇 명의 배신자까지 견딜 수 있는지 그 정확한 한계점을 증명했고, “노드가 거짓말을 하면 어떻게 되는가?”를 막연한 걱정에서 명시된 한계를 지닌 정리로 바꾸어 놓았습니다.

그 정리는, 참여자 중 일부가 적대적인 동안에도 계속 작동해야 하는 모든 시스템의 지적 뿌리이며, 수십 년 뒤 비잔틴이라는 단어가 블록체인 합의의 중심에 자리 잡은 까닭이기도 합니다. 램포트는 암호화폐를 가능하게 하려고 나선 것이 아닙니다. 그는 “장애”가 배신을 포함할 때 장애 허용이 정확히 무엇을 뜻하는지 엄밀하게 정의하려고 나선 것입니다.

TLA+와 명세 (그리고, 그렇습니다, LaTeX)

램포트 경력의 일관된 줄기는 코드를 쓰기 전에 명세해야 한다는 신념이며, TLA+는 그 신념을 도구로 빚어낸 것입니다. 시간 논리 행위(Temporal Logic of Actions)는 시스템이 무엇을 해야 하는지—그 상태들, 그 사이의 단계들, 그리고 시스템이 늘 만족해야 하는 성질(안전성: 나쁜 일은 결코 일어나지 않는다)과 결국 이루어야 하는 성질(활성: 좋은 일은 결국 일어난다)—를 엄밀한 수학적 기술로 적기 위한 언어이며, 이 두 개념은 그가 형식화한 것입니다.⁶ 당신이 명세를 쓰면, 모델 검사기가 상태 공간을 탐색해 당신의 불변식을 깨뜨리는 미묘한 끼어듦의 순서—세 기계가 당신이 상상조차 못 한 차례로 세 가지 일을 할 때만 나타나기에 시험으로는 결코 찾지 못했을 그 버그—를 찾아냅니다. 그의 논증은 건축가의 청사진입니다. 당신은 콘크리트를 붓기 전에 건물을 그리며, 소프트웨어 명세는 바로 그 청사진을, 우리가 가진 가장 엄밀한 언어인 수학으로 적은 것입니다.⁴

그리고 더 조용한 기념비가 하나 있습니다. 1980년대 초, 도널드 커누스의 TeX 위에 쌓아 올려 램포트는 LaTeX를 만들었습니다. 그것은 과학자와 수학자가 문서를 조판하는 기본 방식이 된 매크로 시스템이며, 한 세대의 논문과 학위 논문이 지금과 같은 모습을 띠게 된 이유입니다.⁶ 그것은 전형적인 램포트다운 산물입니다. 그는 자기 작업을 엄밀하게 적어야 했고, 그래서 모두가 그렇게 할 수 있게 해 주는 도구를 만들었습니다. TLA+를 낳은 본능—정밀함을 강제하는 표기법—은 LaTeX를 낳은 본능과 같습니다.

방법

그 방법은 50년 동안 가차 없이 적용된 한 가지 생각입니다. 생각이 곧 작업이며, 그 생각은 코드보다 먼저 적혀야 한다.

시간이 아니라 인과성으로 추론하세요. 신뢰할 수 있는 전역 시계는 없으니, 사건의 순서를 그것이 언제 일어났는가로 매기기를 멈추고 무엇이 무엇을 일으켰는가로 매기세요. 벽시계가 아니라 선행 관계가 실재하는 구조이며, 두 사건이 진정으로 동시적임을 받아들이는 편이 순서를 지어내는 것보다 더 정직합니다.⁵

코드를 쓰기 전에 명세하세요. 정해진 해법이 없는 어떤 일에 대해서든, 멈추어 먼저 생각하세요. 그리고 그 생각은 코딩과 별개입니다. 청사진—곧 명세—을 수학으로 적으세요. 산문이 모호한 자리에서 수학은 단순하고 정밀하기 때문입니다.⁴ “생각하지 않으면 우리는 반드시” 실수하게 됩니다.²

자신이 정말 생각하고 있는지 알아내기 위해 쓰세요. 글쓰기는 어떤 생각이 실재하는지 가늠하는 시험입니다. “쓰지 않고 생각한다면, 당신은 생각하고 있다고 착각하고 있을 뿐입니다.”³ 적어 둘 수 없는 명세는 아직 실제로는 갖지 못한 아이디어입니다.

장애를 엄밀하게 정의하세요. “노드가 거짓말을 하면 어떻게 되는가?”는 그것을 비잔틴 장군으로 진술하고 허용 한계를 증명하기 전까지는 민간 전승입니다. 엄밀한 정의가 걱정을 정리로 바꿉니다.⁶

발표는 정확성의 일부입니다. 팍소스는 여러 해 동안 옳았지만 아무도 그것을 쓸 수 없었습니다. 그리스풍 우화가 아이디어를 파묻었기 때문입니다. 아무도 이해할 수 없는 옳은 결과는 아직 공학으로서 끝맺어지지 않은 것입니다.⁸

영향의 사슬

누가 그를 형성했는가

수학 그 자체. 램포트의 훈련은 컴퓨터 과학이 아니라 수학 박사 과정이었고, 그가 이바지한 바의 전체 모양은 직관으로 프로그래밍해 오던 분야에 수학의 기준—정의, 공리, 증명—을 들여온 일이었습니다.⁶ (형성적 영향)

1970년대 실제 시스템의 장애 허용 문제들. 항공기를 위한 신뢰성 시스템에 관한 SRI의 작업과, 프로토콜 한복판에서 기계가 고장 나는 실제적 공포는, 그가 줄 수 있도록 빚어진 형식적 처리를 요구하는 구체적 문제들—비잔틴 장애, 합의—을 그에게 주었습니다.⁶ (직접적 영향)

에츠허르 데이크스트라. 정확성은 시험이 아니라 증명으로 확립된다는 것, 그리고 동시성 프로그램은 반드시 형식적으로 추론해야 한다는 신념은 램포트의 것이기 이전에 데이크스트라의 것입니다. 램포트가 자기 시계 논문으로 받은 상에는 데이크스트라의 이름이 붙어 있습니다. (직접적 영향)

그가 누구를 형성했는가

모든 분산 데이터베이스, 클라우드 플랫폼, 블록체인. 논리 시계는 분산 저장소의 충돌 해소를 떠받칩니다. 팍소스(그리고 그 후손인 래프트)는 구글의 처비와 스패너, 주키퍼, etcd, 그리고 사실상 모든 클라우드의 조정 계층의 합의 핵심입니다. 비잔틴 장군 결과는 비트코인과 그 이후 모든 장애 허용 합의 프로토콜 밑에 깔린 이론적 바닥입니다.

산업계의 형식적 방법. 아마존 웹 서비스는 S3, DynamoDB를 비롯한 핵심 서비스를 출시하기 전에 명세하고 검사하는 데 TLA+를 쓰는 것으로 유명합니다. 프로덕션이 아니라 설계 단계에서 미묘한 버그를 찾는 것이지요. 램포트의 청사진 논증은 이단에서 관행으로 넘어갔습니다.

이 분야의 어휘. 선행 관계, 안전성과 활성, 복제 상태 기계, 순차 일관성, 비잔틴 장애—이것들은 분산 시스템의 언어에 대한 램포트의 기여가 아니라, 대체로 그 언어 자체입니다.

관통하는 줄기

에츠허르 데이크스트라는 프로그램을 실행하기 전에 옳음을 추론한다고—시험은 버그의 존재를 보일 뿐 그 부재는 결코 보이지 못한다고—주장했고, 램포트는 그 직계 후계자로서, 실행보다 앞선 증명을 순차 프로그램에서 훨씬 더 어려운 동시성의 세계로—시험할 수 없는 버그가 예외가 아니라 통례인 그 세계로—이어 갔습니다. 바버라 리스코프는 데이터 추상화와 치환 가능성으로 프로그램 행위에 관한 형식적 추론을 실용적 원초 개념으로 만들었고, 램포트는 시스템의 시간에 걸친 행위에 관한 형식적 추론을 표준으로 만들어, 한 객체가 무엇을 보장하는지가 아니라 동시성 시스템 전체가 늘 그리고 결국 무엇을 해야 하는지를 명세했습니다. 그리고 도널드 커누스는 알고리듬 분석에 수학적 엄밀함을 들여왔고, 거의 곁가지처럼 그 작업을 엄밀하게 적어 둘 수 있도록 TeX를 만들었습니다. 이는 램포트와 거의 정확히 운을 맞춥니다. 램포트는 같은 이유로 그 위에 LaTeX를 쌓아 올렸고, 명세 자체를 수학적 행위로 만들었지요. “되는 것 같다”를 안다고 치기를 거부한 세 명의 수학자입니다. (시리즈 다리)

이 글에서 내가 얻는 것

내가 간직하는 교훈은, 생각이 곧 작업이며 그 생각은 적어 두기 전까지 실재하지 않는다는 것입니다. 램포트의 청사진 논증이 불편한 이유는 그것이 옳기 때문입니다. 시스템이 프로덕션에서 망가지는 까닭은 코드를 잘못 입력해서인 경우가 거의 없습니다. 동시성과 장애 아래에서 시스템이 실제로 무엇을 해야 하는지 아무도 명세하지 않아서, 코드를 견주어 볼 진술 자체가 없었기 때문입니다. 규율은 구현보다 먼저 명세를, 그 안의 모순이 드러날 만큼 엄밀한 언어로 쓰는 것입니다. 그것은 품질이 유일한 변수라는 것과 같은 기준입니다. 물음은 결코 “이것이 정상 경로를 통과하는가?”가 아니라 “나는 늘 참이어야 하는 바를 정확히 진술했고, 설계가 그것을 지킨다는 것을 증명했는가?”입니다. 내가 코드보다 먼저 PRD를 쓰는 일에 그토록 기대는 까닭이 바로 이것입니다. PRD는 작업복을 입은 램포트의 명세입니다.

지금 내가 만드는 세계—에이전트, 도구 루프, 다중 에이전트 시스템—에서 램포트의 교훈은 거의 모두가 건너뛰고 그 대가를 치르는 교훈입니다. 에이전트 시스템은 곧 분산 시스템입니다. 독립적인 프로세스들, 전역 시계의 부재, 순서가 어긋나거나 아예 도착하지 않는 메시지들, 그리고 조용히 고장 나거나 더 나쁘게는 거짓말을 하는 구성 요소들. 버그는 결코 프롬프트에 있지 않습니다. 버그는 순서에 있습니다. 두 에이전트가 묵은 상태를 두고 행동하거나, 어떤 도구 호출의 결과가 그것을 필요로 했던 결정보다 늦게 도착하거나, 오케스트레이터가 순서를 매긴 척한 “동시적인” 한 쌍의 사건 같은 데 말입니다. 램포트의 규율은 벽시계 직관을 믿기를 멈추고, 인과성과 장애를 명시적으로 추론하며, 무엇이든 엮기 전에 늘 참이어야 하는 바를 적어 두는 것입니다. 짓기 전에 명세한다는 신념, 시스템을 들쑤시는 대신 추론한다는 신념—그것이 1978년의 시계 논문에서 2026년의 에이전트 구동 체계까지 관통하는 줄기이며, 내가 시스템의 성능과 정확성을 나중에 디버깅으로 되찾기를 바라는 것이 아니라 설계 단계에 심어 넣는 속성으로 다루는 까닭입니다.

자주 묻는 질문

레슬리 램포트의 엔지니어링 철학은 무엇인가요?

램포트의 신념은 동시성 시스템과 분산 시스템이 직관으로 추론하기에는 너무 미묘하다는 것이며, 그래서 건축가가 벽돌 한 장 놓기 전에 청사진을 그리듯, 코드를 쓰기 전에 종이 위에서 수학으로 생각해야 한다는 것입니다. 소프트웨어 청사진은 명세이며, 그것을 수학으로 적는 까닭은 수학이 쓸 수 있는 가장 정밀한 언어이기 때문입니다.⁴ 그 밑에는 시간에 대한 입장이 있습니다. 분산 시스템에는 믿을 만한 전역 시계가 없으므로, 계산의 실재하는 구조는 인과성—무엇이 무엇을 일으켰는가—이지 일들이 언제 일어났는가가 아닙니다.⁵ “생각한다고 해서 실수를 안 하리라는 보장은 없습니다,” 그는 말했습니다. “하지만 생각하지 않으면 반드시 실수하게 됩니다.”²

램포트 시계와 선행 관계란 무엇인가요?

선행 관계는 분산 시스템에서 인과성을 램포트가 형식화한 것입니다. 사건 A가 사건 B를 선행한다는 것은, 둘이 같은 프로세스 위에 있고 A가 먼저인 경우이거나, A가 메시지를 보내고 B가 그것을 받는 경우이거나, 그것들을 사슬처럼 이은 경우입니다.⁵ 그것은 부분 순서일 뿐입니다. 서로 다른 프로세스 위에 있고 이어 주는 메시지가 없는 두 사건은 진정으로 동시적이며, 어느 옳은 시스템도 한쪽이 먼저라고 주장할 수 없습니다.⁵ 램포트 시계는 이를 프로세스마다 하나씩의 카운터로 구현합니다. 모든 사건마다 그것을 증가시키고, 나가는 모든 메시지에 그 값을 찍으며, 받을 때는 자기 값과 메시지의 타임스탬프 중 더 큰 값보다 하나 더 큰 값으로 카운터를 올립니다.⁷ 그 결과는 인과성과 일치하는 타임스탬프의 집합이며, 그것이 벡터 시계와 현대 분산 충돌 해소의 토대입니다.

팍소스와 비잔틴 장군 문제란 무엇인가요?

팍소스는 합의—신뢰할 수 없고 고장 날 수도 있는 한 무리의 기계들이 복제 로그의 다음 명령 같은 단일 값에 합의하게 만드는 일—를 위한 램포트의 알고리듬이며, 거의 모든 현대 분산 시스템의 조정 계층을 떠받칩니다. 유명하게도, 그는 그것을 가상의 그리스 의회에 관한 우화(“시간제 의회,” ACM TOCS 1998)로 처음 출판했습니다. 그 농담이 아이디어를 너무 가린 나머지 그는 결국 2001년 “쉽게 풀어 쓴 팍소스”로 다시 썼습니다.⁸ 비잔틴 장군 문제(램포트, 쇼스택, 피스, 1982)는 가장 어려운 장애 양상—그저 고장 나는 것이 아니라 거짓말을 하며 모순된 정보를 보내는 구성 요소—을, 배신자들이 합의를 방해하는 가운데 작전에 합의하려는 장군들로 정의하고, 한 시스템이 몇 명의 배신자까지 견딜 수 있는지 증명합니다.⁶ 그것은 블록체인 합의의 이론적 뿌리입니다.

레슬리 램포트는 왜 튜링상을 받았나요?

ACM은 “인과성과 논리 시계, 안전성과 활성, 복제 상태 기계, 순차 일관성 같은 개념의 발명을 특히 들어, 분산 및 동시성 시스템의 이론과 실제에 이바지한 근본적 공로”를 인정하여 램포트에게 2013년 A.M. 튜링상을 수여했습니다.⁶ 그 표창문은 그의 작업의 폭을 담고 있습니다. 그는 분산 컴퓨팅을 민간 전승에서, 엄밀한 정의와 증명을 갖춘 과학으로 바꾸었고, 이 분야에 그 어휘의 상당 부분을 주었으며, “코드를 쓰기 전에 명세하라”를 실용적 규율로 만들고자 TLA+ 명세 언어를 만들었고, 커누스의 TeX 위에 쌓아 올려 과학과 수학 전반의 표준이 된 조판 시스템 LaTeX를 썼습니다.⁶

출처