아직 구축되지 않은 시스템에서 복원력 결함을 어떻게 발견할 수 있을까?

설계 자체를 분석 가능한 시스템으로 다룬다면 코드를 작성하기 전에 가장 위험한 시스템 결함 중 일부를 발견할 수 있다. 이것이 Hillel Wayne의 발표가 다루는 핵심이다. 그는 형식 기법의 원리가 미래의 시스템을 검사하고 복원력, 동시성, 장애 문제를 운영 오류로 발전하기 전에 발견하는 데 어떻게 도움을 주는지 설명한다.

Wayne은 먼저 그가 «작업 실행기»라고 부르는 것을 단순화한 예로 든다. 시스템이 작업이 완료되었는지 확인한 다음 완료 표시를 하고, 그 후 작업을 실행하는 방식이다. 이 순서는 논리적으로 보이지만 실행 중 장애가 발생하면 무너진다. 작업이 완료된 것으로 기록된 뒤 재시도될 수 있으므로 작업이 실제로 실행되지 않을 수 있다. 완료 기록을 실행 이후로 옮기면 또 다른 문제가 나타난다. 두 개의 동시 실행기가 어느 쪽도 완료를 기록하기 전에 같은 작업을 두 번 실행할 수 있기 때문이다.

이는 단순히 이론적인 문제가 아니다. 발표는 이를 택배 발송 시스템에서 주문이 두 번 발송될 수 있는 사례, 스케줄링 시스템에서 같은 시간대가 두 사람에게 예약될 수 있는 사례, 요청이 반복될 때 애플리케이션 설치 메커니즘이 파괴적인 동작에 빠질 수 있는 사례와 연결한다.

무엇이 «올바른지» 정의하는 것부터 시작하라

Wayne은 시스템 요구 사항을 참 또는 거짓 중 하나인 이진 속성의 형태로 작성하자고 제안한다. 예를 들어 작업이 두 번 이상 실행되지 않아야 한다는 것은 나쁜 일이 발생하는 것을 막는 안전 속성이고, 작업이 적어도 한 번 실행되어야 한다는 것은 원하는 일이 발생하도록 보장하는 생존성 속성이다.

발표는 속성들이 모두 같은 강도를 갖는 것은 아니라고 강조한다. 초당 10,000개의 질의를 처리할 수 있는 시스템은 초당 2개의 질의를 처리한다는 속성을 자동으로 만족하지만, 그 반대는 성립하지 않는다. 따라서 강한 속성을 통과하면 더 약한 속성들의 집합이 올바르다는 증거가 될 수 있는 반면, 더 약한 속성의 실패는 결함 원인의 범위를 좁히는 데 도움이 된다. Wayne은 이 생각을 테스트 피라미드와 연결한다. 많은 단위 테스트가 제한된 수의 엔드투엔드 테스트보다 오류를 진단하는 데 더 유용할 수 있다는 것이다.

단순화된 모델이 핵심 문제를 드러낸다

Wayne은 시스템을 모든 세부 사항으로 표현하는 대신 필요한 최소한의 상태를 포함하는 추상 모델을 구축하라고 권한다. 여기에는 알고리즘의 현재 단계, 작업이 완료된 것으로 표시되었는지 여부, 작업이 실행된 횟수가 포함된다. 이를 통해 장애와 재시도 상황을 비롯해 가능한 상태와 시스템이 거칠 수 있는 경로를 탐색할 수 있다.

형식 기법에서는 이 모델과 속성을 논리식으로 인코딩한 다음 모델 검사기와 SMT 솔버 같은 도구로 검사할 수 있다. 그러나 발표의 실용적인 핵심은 이러한 도구를 직접 사용할 것을 요구하지 않는다. 엔지니어는 상태와 가능한 전이를 추적함으로써 같은 사고방식을 채택할 수 있다.

동시성과 장애에서의 «적대자» 요소

Wayne은 사용자 입력, 동시성, 무작위성, 타임아웃, 서버 중단과 같은 모든 비결정성의 원천을 항상 최악의 결과를 선택하는 «적대자»로 상상하자고 제안한다. 시스템이 끝없이 재시도할 수 있다면 이 적대자는 매번 장애를 선택할 것이며, 이로써 이론적으로 성공이 가능하더라도 생존성 속성이 보장되지 않는다는 점이 드러난다.

또한 두 개의 동시 실행기가 존재하면 일부 변수를 각 프로세스에 고유한 지역 변수로, 다른 변수는 시스템과 외부 세계가 공유하는 변수로 표현해야 한다고 설명한다. 서로 다른 실행 순서를 탐색하면 각 실행기는 개별적으로는 정상으로 보이더라도 작업이 두 번 실행되는 상태에 도달할 수 있다.

가정은 설계의 일부다

시스템의 올바름은 시스템의 속성뿐 아니라 시스템이 작동하는 환경에 대한 가정에도 의존한다. 어떤 설계는 프로세스가 전혀 실패하지 않는다는 강한 가정을 요구할 수 있지만, 다른 설계는 장애가 제한된 횟수만 발생한다면 작동할 수 있다. Wayne은 단계의 순서를 바꾸면 생존성에 대한 가정을 완화할 수 있지만, 동시에 한 번에 하나의 실행기만 존재하도록 보장해야 하는 것처럼 안전성 요구 사항이 늘어날 수 있다고 지적한다.

운영 환경이 바뀌면 상황도 달라진다. 강한 일관성을 갖는 데이터베이스에 의존하다가 최종 일관성으로 전환하면 시스템 코드가 바뀌지 않더라도 이전에 참이었던 속성이 더 이상 보장되지 않을 수 있다. 따라서 서비스 제공업체나 데이터베이스에 대한 가정을 외부적인 세부 사항으로 간주해서는 안 된다. 이는 설계의 올바름을 위한 직접적인 조건이다.

실제로 무엇이 달라지는가?

이 방법의 실질적인 가치는 테스트를 대체하거나 모든 프로젝트에서 형식 도구를 사용하자고 주장하는 데 있지 않다. 그보다는 설계 질문을 더 엄밀하게 만드는 데 있다. 가능한 상태는 무엇인가? 사건의 최악의 순서는 무엇인가? 우리가 실제로 통제하는 것은 무엇인가? 팀이 보장할 수 없는 가정은 무엇인가? 요구되는 속성이 강할수록, 또는 환경의 예측 가능성이 낮을수록 시스템은 더 복잡한 설계를 필요로 하거나 요구되는 속성을 완화해야 한다. 예를 들어 «모든 메시지를 처리한다»는 조건을 «메시지를 처리하거나 배달 못한 메시지 목록으로 보낸다»로 바꾸는 방식이다.

Wayne은 이러한 아이디어를 형식 기법에서 파생된 사고 도구로 제시하며, 공학적 판단을 바로 대체하는 방법으로 제시하지는 않는다. 모든 시스템에서 여전히 열려 있는 질문은 사용된 모델과 가정이 얼마나 정확한가이다. 어떤 상태가 누락되거나 팀이 환경이 보장하지 않는 동작을 가정한다면, 분석은 실제 시스템과 닮지 않은 모델이 올바르다는 사실만 입증할 수 있다.