Amazon Web Services의 시스템 정확성 실천 사례

 (cacm.acm.org)
2P by GN⁺ | ★ favorite | 댓글 1개
  • AWS는 보안·내구성·무결성·가용성을 지키기 위해 시스템 정확성을 핵심 기반으로 삼고, TLA+에서 시작해 모델 검사·퍼징·속성 기반 테스트·런타임 검증·형식 증명까지 적용 범위를 넓혀왔음
  • TLA+는 전통적 테스트로 잡기 어려운 버그를 초기에 제거하고 성능 최적화에 대한 확신을 줬지만, 개발자 접근성을 높이기 위해 P 프로그래밍 언어와 PObserve 같은 도구가 함께 도입됨
  • S3 ShardStore의 속성 기반 테스트, 결정적 시뮬레이션, Aurora Limitless Database의 SQL 퍼징은 형식 기법을 일상적인 개발·통합 테스트에 더 가깝게 끌어온 사례임
  • Fault Injection Service는 API 오류, I/O 일시 중지, 인스턴스 실패 같은 장애를 주입해 복원력 메커니즘을 검증하며, Amazon.com은 Prime Day 2024 준비 과정에서 FIS 기반 실험 733건을 실행함
  • Cedar, Firecracker, Graviton 2 RSA 최적화처럼 보안 경계와 성능 최적화가 중요한 영역에서는 형식 증명이 쓰이고, 높은 학습 곡선과 도구 접근성은 여전히 채택의 제약으로 남아 있음

AWS가 시스템 정확성을 다루는 방식

  • AWS는 고객이 신뢰할 수 있는 서비스를 제공하려면 보안, 내구성, 무결성, 가용성의 높은 기준을 유지해야 하며, 시스템 정확성이 이를 뒷받침함
  • 2015년 CACM의 “How Amazon Web Services Uses Formal Methods”는 AWS 핵심 서비스의 정확성을 보장하기 위한 접근을 소개했고, 이후 이 서비스들은 AWS 고객에게 널리 쓰이게 됨
  • 초기 중심 도구는 Leslie Lamport가 개발한 형식 명세 언어 TLA+ 였음
    • 전통적인 테스트로 놓칠 수 있는 미묘한 버그를 개발 초기에 발견하고 제거하는 데 도움을 줌
    • 시스템 정확성을 유지하면서 공격적인 성능 최적화를 구현할 수 있다는 확신을 제공함
  • 15년 전 AWS의 테스트 관행은 주로 빌드 시점 단위 테스트와 제한적인 배포 시점 통합 테스트에 의존했음
  • 이후 AWS는 형식 기법과 준형식 기법을 개발 과정에 통합함
    • 정리 증명, 연역 검증, 모델 검사
    • 속성 기반 테스트, 퍼징, 런타임 모니터링

P 프로그래밍 언어와 PObserve

  • AWS는 2010년대 초 형식 기법을 초기 팀 밖으로 확장하면서 많은 엔지니어가 TLA+ 학습과 생산성 확보에 어려움을 겪는다는 점을 확인함
  • TLA+는 수학에 가까운 고수준 추상 언어라는 점이 강점이지만, 명령형 언어에 익숙한 개발자에게는 접근 장벽이 됨
  • 분산 시스템 모델링과 분석을 위한 상태 머신 기반 언어 P가 이 간극을 줄이는 역할을 맡음
    • 개발자는 시스템 설계를 통신하는 상태 머신으로 모델링함
    • 이 정신 모델은 마이크로서비스와 서비스 지향 아키텍처(SOA)를 많이 다루는 Amazon 개발자에게 익숙함
    • P는 2019년부터 AWS에서 개발됐고 전략적 오픈소스 프로젝트로 유지됨
  • 여러 AWS 대표 제품 팀이 P를 시스템 설계 정확성 검토에 사용함
    • 스토리지: Amazon S3, EBS
    • 데이터베이스: Amazon DynamoDB, MemoryDB, Aurora
    • 컴퓨트: EC2, IoT
  • S3는 eventual consistency에서 strong read-after-write consistency로 이전하는 과정에서 P를 사용함
    • S3 인덱스 서브시스템은 빠른 데이터 조회를 가능하게 하는 객체 메타데이터 저장소임
    • 강한 일관성을 달성하려면 S3 인덱스 프로토콜 스택에 여러 비자명한 변경이 필요했음
    • P는 프로토콜 설계를 형식 모델링·검증해 설계 수준 버그를 초기에 제거하고, 위험한 최적화를 모델 검사로 확인할 수 있게 함
  • 2023년 AWS P 팀은 PObserve를 구축함
    • 분산 시스템 실행에서 나온 구조화 로그를 사용함
    • 로그가 시스템의 형식 P 명세가 허용하는 동작과 일치하는지 사후 검증함
    • Rust나 Java 같은 언어로 작성된 프로덕션 구현과 설계 시점 P 명세 사이의 간극을 줄임
    • 설계 시점 검증과 구현의 런타임 모니터링을 연결해 형식 명세 투자의 가치를 높임

경량 형식 기법을 개발 흐름에 붙이는 방식

  • AWS는 경량 형식 기법을 도입해 형식 기법을 엔지니어링 팀의 개발·테스트 흐름에 더 가깝게 가져감

  • 속성 기반 테스트

    • Amazon S3의 ShardStore는 개발 주기 전반에서 정확성 테스트와 개발 속도 향상을 위해 속성 기반 테스트를 사용함
    • 여러 기법을 함께 써서 사람이 기대 동작을 명세하고, 자동화된 테스트가 더 많은 입력과 실패 조건을 탐색하게 함
      • 개발자가 제공한 정확성 명세
      • 코드 커버리지 지표로 입력 분포를 안내하는 커버리지 가이드 퍼징
      • 하드웨어 및 기타 시스템 실패를 테스트 중 시뮬레이션하는 장애 주입
      • 반례를 자동으로 축소해 사람이 디버깅하기 쉽게 하는 최소화

  • 결정적 시뮬레이션

    • 결정적 시뮬레이션 테스트는 분산 시스템을 단일 스레드 시뮬레이터에서 실행하고 모든 무작위성의 출처를 제어함
      • 스레드 스케줄링
      • 타이밍
      • 메시지 전달 순서
    • 개발자는 분산 프로토콜의 특정 단계에서 참여자가 실패하는 상황처럼 특정 실패·성공 시나리오를 작성할 수 있음
    • 테스트 프레임워크가 비결정성을 제어하므로, 과거 버그를 유발한 순서 같은 흥미로운 실행 순서를 지정할 수 있음
    • 스케줄러는 순서 퍼징이나 가능한 모든 순서 탐색으로 확장될 수 있음
    • 지연과 실패 상황의 시스템 속성 테스트를 통합 테스트보다 빌드 시점에 가깝게 이동시켜 개발을 가속하고 동작 커버리지를 넓힘
    • AWS의 스레드 순서와 시스템 실패 빌드 시점 테스트 작업 일부는 shuttle과 turmoil 프로젝트로 오픈소스화됨

  • 지속적 퍼징과 무작위 테스트 입력 생성

    • 지속적 퍼징, 특히 커버리지 가이드 기반의 확장 가능한 테스트 입력 생성은 통합 시점의 시스템 정확성 테스트에 효과적임
    • Amazon Aurora의 데이터 샤딩 기능인 Aurora Limitless Database 개발에서는 두 가지 핵심 속성 검증에 퍼징을 광범위하게 사용함
    • SQL 쿼리와 전체 트랜잭션을 퍼징해 샤드에 걸친 SQL 실행 논리 분할이 올바른지 검증함
    • 대량의 무작위 SQL 스키마, 데이터셋, 쿼리를 합성해 테스트 대상 엔진에서 실행하고, 샤딩되지 않은 엔진 기반 오라클과 결과를 비교함
    • SQLancer가 개척한 접근 같은 다른 검증 방식도 함께 사용함
    • 퍼징과 장애 주입 테스트의 결합은 데이터베이스의 원자성, 일관성, 격리성 같은 정확성 측면에도 유용함
      • 트랜잭션을 자동 생성함
      • 형식적으로 명세된 정확성 오라클로 올바른 동작을 정의함
      • 트랜잭션과 트랜잭션 내부 문장의 가능한 인터리빙을 테스트 대상 시스템에 실행함
      • Elle 같은 접근을 따라 격리성 같은 속성을 사후 검증함

Fault Injection Service와 장애 상황 검증

  • AWS는 2021년 초 Fault Injection Service(FIS) 를 출시해 장애 주입 기반 테스트를 다양한 AWS 고객이 사용할 수 있게 함
  • FIS는 AWS 인프라의 테스트 또는 프로덕션 배포에 시뮬레이션 장애를 주입할 수 있음
    • API 오류
    • I/O 일시 중지
    • 실패한 인스턴스
  • 장애 주입은 아키텍처에 구축된 복원력 메커니즘이 실제로 가용성을 개선하고, 새로운 정확성 문제를 만들지 않는지 확인하게 해줌
    • 장애 조치
    • 헬스 체크
  • FIS 기반 장애 주입 테스트는 AWS 고객과 Amazon 내부에서 널리 사용됨
  • Amazon.com은 Prime Day 2024 준비 과정에서 FIS 기반 장애 주입 실험 733건을 실행함
  • 2014년 Yuan 등은 테스트한 분산 시스템의 치명적 장애 92%가 비치명적 오류의 잘못된 처리에서 촉발됐다고 분석함
  • 정상 경로의 치명적 장애가 드문 이유는 정상 경로가 자주 실행되고, 더 잘 테스트되며, 오류 경로보다 훨씬 단순하기 때문임
  • 장애 주입 테스트와 FIS는 장애와 실패 상황에서 시스템 동작을 더 쉽게 테스트하게 해 정상 경로와 오류 경로의 버그 밀도 격차를 줄임
  • 장애 주입 자체는 형식 기법으로 간주되지 않지만 형식 명세와 결합될 수 있음
    • 기대 동작을 형식 명세로 정의함
    • 장애 주입 중과 이후 결과를 명세된 동작과 비교함
    • 지표와 로그 오류만 확인하거나 사람이 육안으로 판단하는 방식보다 더 많은 버그를 잡을 수 있음

준안정성과 창발적 시스템 동작

  • 최근 10년 동안 특정 부류의 시스템 실패인 준안정 실패(metastable failures) 에 대한 관심이 커짐
  • 준안정 실패는 과부하나 캐시 비움 같은 트리거가 분산 시스템을 개입 없이는 회복하지 못하는 상태로 밀어 넣는 실패임
    • 개입 예시는 부하를 정상보다 낮게 줄이는 것임
  • 이 실패 부류는 클라우드 시스템의 비가용성에 중요한 기여 요인 중 하나임
  • 일반적인 준안정 동작에서는 부하 증가에 따라 처음에는 goodput이 증가하다가 포화되고, 혼잡을 거쳐 goodput이 0 또는 0에 가까워짐
  • 이후 시스템은 부하를 조금 줄이는 것만으로 건강한 상태로 돌아가지 못하며, 부하를 크게 줄여야 회복될 수 있음
  • 이 동작은 단순한 시스템에서도 나타날 수 있고, 대부분의 시스템에서 타임아웃 후 재시도 클라이언트 로직으로도 촉발될 수 있음
  • 전통적인 분산 시스템 형식 모델링은 보통 안전성(safety)과 활성성(liveness)에 초점을 맞추지만, 준안정 실패는 이 분류에 깔끔하게 들어가지 않는 동작이 있음을 보여줌
  • AWS는 창발적 시스템 동작을 이해하기 위해 이산 사건 시뮬레이션을 더 많이 활용함
    • 맞춤형 시스템 시뮬레이션에 투자함
    • TLA+와 P 같은 언어로 만든 기존 시스템 모델을 시뮬레이션에 사용할 수 있는 도구에 투자함
  • TLA+의 TLC 같은 완전 탐색 모델 검사기를 확률적 시뮬레이션으로 확장하면 사후 지연 분포 같은 통계 결과를 생성할 수 있음
  • 이런 확장은 지연 시간 SLA 달성 가능성 이해 같은 작업에 모델 검사를 활용하게 함

형식 증명이 필요한 보안 경계

  • 권한 부여와 가상화 같은 중요한 보안 경계에서는 앞서의 형식 기법만으로 충분하지 않을 수 있으며, 정확성 증명이 큰 투자 가치가 있음

  • Cedar 권한 정책 언어

    • AWS는 2023년 세밀한 권한을 지정하는 정책 작성을 위한 Cedar 권한 정책 언어를 도입함
    • Cedar는 자동 추론과 형식 증명을 고려해 설계됨
    • 구현은 검증 친화적 프로그래밍 언어 Dafny로 구축됨
    • Dafny를 통해 구현이 여러 보안 속성을 만족한다는 점을 증명함
    • 이 증명은 테스트를 넘어서는 수학적 의미의 증명임
    • 팀은 Dafny 코드를 정확성 오라클로 사용하는 차등 테스트도 적용해 프로덕션 준비가 된 Rust 구현의 정확성을 검증함
    • Cedar 구현과 함께 Dafny 코드와 테스트 절차를 오픈소스로 공개해 사용자가 정확성 작업을 확인할 수 있게 함

  • Firecracker VMM

    • Firecracker 가상 머신 모니터는 virtio라는 저수준 프로토콜을 사용해 네트워크 카드나 SSD 같은 에뮬레이션된 하드웨어 장치를 VM 내부 게스트 커널에 노출함
    • 이 에뮬레이션 장치는 신뢰할 수 없는 게스트와 신뢰된 호스트 사이의 가장 복잡한 상호작용이므로 중요한 보안 경계임
    • Firecracker 팀은 Rust 코드를 형식적으로 추론할 수 있는 Kani를 사용해 이 보안 경계의 핵심 속성을 증명함
    • 이 증명은 게스트가 무엇을 시도하더라도 경계의 중요한 속성이 유지됨을 보장함
    • AWS는 Kani, Dafny, Lean과 이를 구동하는 SMT solver 같은 기반 도구 개발을 지원함
    • 형식 모델과 명세는 여러 방식으로 재사용됨
      • 설계 시점 모델 검사
      • 런타임 모니터링에서 정확성 오라클 역할
      • 창발적 시스템 동작 시뮬레이션
      • 핵심 속성의 증명 구축

정확성을 넘어선 성능과 비용 효과

  • 형식 기법은 클라우드 시스템 성능을 안전하게 개선하는 데도 중요함
  • Aurora 관계형 데이터베이스 엔진의 핵심 커밋 프로토콜을 P와 TLA+ 로 모델링한 결과, 안전성 속성을 희생하지 않고 분산 커밋 비용을 2 네트워크 왕복에서 1.5 네트워크 왕복으로 줄일 기회를 찾음
  • 이런 성과는 형식 기법을 도입한 팀에서 흔함
    • 분산 프로토콜을 깊게 생각하고 형식적으로 작성하는 과정이 구조화된 사고를 강제함
    • 프로토콜 구조와 풀어야 할 문제에 대한 더 깊은 통찰을 줌
    • 제안된 설계 최적화가 올바른지 형식적으로 확인하거나 증명할 수 있으면 분산 시스템 엔지니어가 위험을 늘리지 않고 더 과감한 설계를 선택할 수 있음
  • 생산성과 비용 효과는 고수준 설계 최적화에만 국한되지 않음
  • AWS 팀은 ARM 기반 Graviton 2 프로세서에서 RSA 공개키 암호화 구현 최적화를 찾아 처리량을 최대 94% 개선할 수 있었음
  • HOL Light 대화형 정리 증명기를 사용해 이 최적화의 정확성을 증명함
  • 클라우드 CPU 사이클의 높은 비율이 암호화에 쓰이므로 이런 최적화는 인프라 비용 절감, 지속가능성 지원, 고객이 체감하는 성능 개선에 기여할 수 있음

남은 과제와 향후 기회

  • AWS는 지난 15년 동안 형식·준형식 테스트 방법을 확장하는 데 성공했지만, 산업적 채택에는 여전히 과제가 남아 있음
  • 형식 기법 도구의 주요 장벽은 가파른 학습 곡선과 전문 도메인 지식 요구임
  • 많은 도구가 여전히 학술적 성격을 갖고 있으며 사용자 친화적 인터페이스가 부족함
  • 잘 정착된 준형식 접근도 채택 장벽이 남아 있음
    • 결정적 시뮬레이션은 AWS와 FoundationDB 같은 프로젝트에서 성공적으로 쓰인 핵심 분산 시스템 테스트 기법이지만, AWS에 합류하는 숙련된 분산 시스템 개발자에게도 낯선 경우가 있음
    • 장애 주입 테스트, 속성 기반 테스트, 퍼징 같은 검증된 방법론에서도 비슷한 격차가 존재함
  • 분산 시스템 개발자에게 이런 테스트 방법과 도구를 교육하고, 엄밀한 사고 방식을 가르치는 일이 필요함
  • 교육 격차는 학계 수준에서 시작됨
    • 기본적인 형식 추론 접근도 드물게 가르쳐짐
    • 상위 기관 졸업생도 이런 도구를 채택하기 어려움
    • 형식 기법과 자동 추론은 산업 적용에 중요하지만 여전히 틈새 분야로 여겨짐
  • 준안정성과 대규모 시스템의 다른 창발적 속성도 비슷한 인식 과제를 가진 중요한 연구 영역임
    • “타임아웃 시 N번 재시도”처럼 준안정 시스템 동작을 유발할 수 있는 관행이 알려진 문제에도 계속 널리 권장됨
    • 창발적 시스템 동작 이해를 위한 현재 도구와 기법은 초기 단계임
    • 시스템 안정성 모델링은 비용이 많이 들고 복잡함
  • AWS는 대형 언어 모델과 AI 어시스턴트가 형식 기법의 실무 채택 문제를 완화하는 데 크게 도움이 될 것으로 봄
    • AI 보조 단위 테스트가 인기를 얻은 것처럼, 개발자가 형식 모델과 명세를 만드는 데 도움을 줄 수 있음
    • 고급 기법이 더 넓은 개발자 커뮤니티에 접근 가능해질 수 있음

AWS가 계속 투자하는 정확성 체계

  • 신뢰할 수 있고 안전한 소프트웨어를 만들려면 시스템 정확성을 추론하는 다양한 접근이 필요함
  • AWS는 단위 테스트와 통합 테스트 같은 업계 표준 테스트와 함께 여러 기법을 채택함
    • 모델 검사
    • 퍼징
    • 속성 기반 테스트
    • 장애 주입 테스트
    • 결정적 시뮬레이션
    • 이벤트 기반 시뮬레이션
    • 실행 추적의 런타임 검증
  • 형식 명세는 AWS의 여러 테스트 관행에서 올바른 답을 제공하는 테스트 오라클로 중요한 역할을 함
  • 정확성 테스트와 형식 기법은 이미 얻은 투자 수익을 바탕으로 AWS의 핵심 투자 영역으로 남아 있음

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • 결정적 시뮬레이션 테스트를 언어에 독립적으로 해주는 좋은 오픈소스 라이브러리가 있는지 궁금함
    컨테이너 안에 도구를 띄우고, 테스트 실행 시점에 네트워킹·스토리지 등을 테스트 맥락에서 결정적으로 만들 수 있을 것 같음
    Antithesis가 대략 이런 일을 하지만, 아직 오픈소스는 못 봤고, 애플리케이션보다 한 단계 아래 계층에서 결정성이 제공되면 더 좋겠음
    AI에 크게 낙관적이진 않지만, 테스트는 실제 애플리케이션 요구사항을 피드백 루프로 삼을 수 있어서 빛을 발할 수 있는 영역 같고, 궁극적으로 형식 검증을 더 실용적으로 만들어 소프트웨어를 더 엄밀한 분야로 만들 수 있길 바람

    • 역사적으로 결정적 시뮬레이션 테스트(DST) 도입에는 큰 장벽이 두 가지 있었음
      첫째, 예전에는 전체 시스템을 특정 시뮬레이션 프레임워크 중심으로 만들어야 했고 의존성도 거의 못 가져갔음
      둘째, 약한 탐색이나 입력 생성으로 스스로를 속이기 너무 쉬워서, 실제로는 사소하지 않은 것을 테스트하지 않는데도 모든 테스트가 초록색으로 보이기 쉬움
      Antithesis는 이 둘을 해결하려 하지만 매우 어렵고, 임의의 소프트웨어에 신뢰성 있게 결정성을 덧씌우는 방법은 잘 모름
      Facebook의 Hermit 프로젝트가 결정적 Linux 사용자 공간으로 이를 시도했지만 중단됐고, 우리도 하이퍼바이저를 만들기 전에 비슷하게 해봤지만 잘 작동하지 않았음
      결정적 컴퓨터는 테스트를 넘어 범용적으로 유용한 기술 원시 요소라서 언젠가 누군가 만들거나, 우리가 오픈소스로 공개할 수도 있음
    • https://apple.github.io/foundationdb/testing.html
      https://www.youtube.com/watch?v=4fFDFbi3toc
    • QEMU를 한 스레드에서 100% 에뮬레이션 모드로 돌리면 완전히 결정적인 머신은 비교적 쉽게 얻을 수 있을 것 같음
      하지만 원하는 것은 제어 가능한 결정적 실행이고, 그건 훨씬 어려움
      여러 프로세스가 흥미로운 조건을 유발하는 특정 순서로 움직이게 하려면 CPU와 운영체제 스케줄러 수준에서 보면 매우 복잡해지고, 언어 독립적인 구성을 만들기도, 원하는 대로 조종하기도 어렵고, 관련 없는 세부사항에 파묻힐 수 있음
      예전에 여러 JVM 스레드를 특정한 락스텝 방식으로 실행하게 하는 훨씬 단순한 것을 만든 적이 있는데, 입출력 작업과 시스템 시간 진행을 스텁 처리하고 제어했음
      이걸로 비동기적으로 연결된 여러 컴포넌트를 특정 상호작용 패턴으로 실행할 수 있었고, 스레드 활성화 순서뿐 아니라 입출력 실패와 재시도까지 다룰 수 있었으며, 운영 전에 골치 아픈 버그 몇 개를 찾아냈음
      다만 전체 시스템이 아니라 특정 동기화 지점만 제어하는 과감한 단순화 덕분에 가능했고, 명시적 동기화를 잊어 생기는 일반적인 데이터 경쟁은 잡지 못함
    • gdb로 디버깅 가능한 언어라면 https://rr-project.org/가 있음
    • Joe Armstrong이 속성 기반 테스트로 Dropbox를 테스트하는 내용의 발표를 한 적이 있음

  • S3는 지금까지 본 소프트웨어 중에서도 가장 놀라운 축에 듦
    몇 년 전 전체 시스템에 강한 읽기-쓰기 후 일관성을 그냥 추가한 일은 정말 대단한 소프트웨어 엔지니어링이었음
    https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-rea...

    • 읽기-쓰기 후 일관성을 가능하게 한 재설계를 인덱스 팀이 하던 시기에 S3 Lifecycle에서 일할 수 있어 정말 즐거웠음
      S3는 밖에서 보이는 만큼 인상적이고, 내부 구현과 조직 구조까지 포함하면 적어도 그만큼 더 인상적이라고 자신 있게 말할 수 있음
    • Google Cloud Storage는 S3보다 훨씬 오래전부터 그 기능을 갖고 있었고, GCS가 훨씬 더 잘 생각하고 만든 제품처럼 보임
    • S3는 엄밀히 말해 소프트웨어 조각이라기보다 서비스임
      그리고 S3가 GCS나 Azure Blob보다 낫다고 보기도 어려움

  • 예전에 Leslie Lamport와 Buridan's Principle 논문 등에 관해 이메일을 주고받은 적이 있는데, 오늘 그의 웹사이트에 가보니 TLA+ 와 PlusCal에 관한 내용이 많았고 아직도 유지하고 있었음
    https://lamport.azurewebsites.net/tla/peterson.html?back-lin...
    수학을 프로그래밍에 가져오고 동시성 시스템의 원조격인 사람이, AWS 같은 산업 현장에서 쓰는 시스템 설계 언어를 만든 건 너무 자연스럽게 느껴짐
    분산 시스템을 만드는 더 많은 사람이 그가 만든 것을 쓰면 좋겠고, 큰 시스템에서는 정확성 증명이 중요함

    • 관심 있는 사람을 위한 팁으로, Claude Opus with Extended Thinking은 기존 코드를 TLA+ 명세로 바꾸는 데 꽤 뛰어난 것 같음
      개인 Rust 프로젝트에서 여러 버그를 찾았고, 예를 들어 Snake 게임에서 뱀이 180도 회전할 수 있는 버그를 잡았음
      직장에서도 락과 활성성 관련 속성을 가진 큐 같은 작은 핵심 C++ 컴포넌트를 검증해봤음
      다른 모델도 시도했지만 Opus 외에는 구문이나 명세 논리에서 계속 문제가 생겼음
    • 작은 규모라도 중요하고 널리 쓰이는 유틸리티, 예를 들면 SSH나 터미널 같은 곳에도 정확성 증명은 좋을 수 있음
    • 그건 할 수 없음
      모델 검사기는 작성한 속성을 탐색한 유한 상태 공간 안에서 명세가 만족한다는 것만 말해줌

  • 훌륭한 글이고, 인프라 제어 평면을 만든다면 상태 기계는 필수라고 봄
    다만 P가 반드시 필요했는지는 확신이 없음
    우리는 13년 넘게 인프라 제어 평면을 만들고 있고, 모든 반복을 Ruby로 구축했는데 매우 잘 맞았음
    https://www.ubicloud.com/blog/building-infrastructure-contro...

  • 92% 통계가 정말 흥미로움
    클러스터를 무너뜨리는 건 보통 화려한 장애가 아니라, 해롭지 않아 보이는 재시도가 상태를 조금씩 새게 만들다가 어느 금요일 새벽 2시에 모든 것이 깨지는 경우임
    명백한 대재난보다 평범하고 조용한 실패에 더 많은 엔지니어링 시간을 배정해야 할 것 같고, 진짜 시체는 거기에 묻혀 있음

    • 생존자 편향일 수도 있음
      이미 해결된 큰 이슈들은 해결됐기 때문에 문제를 일으키지 않고, 해결되지 않은 작은 이슈들 일부가 무작위로 큰 장애를 일으키는 것일 수 있음

  • P 언어에 대해 궁금했던 점이 있음
    초기에는 Microsoft에서 Windows USB 스택 런타임에 실제로 쓰이는 C 코드를 생성하는 데 사용된 것 같은데, 지금은 더 이상 프로덕션 코드를 생성하는 데 쓰지 않는 듯함
    같은 질문을 여기서 했고, 어떤 발표에서도 비슷한 질문이었던 것 같음
    https://news.ycombinator.com/item?id=34284557
    생성된 코드가 커널에서 쓰일 수 있다면, 자원 제약이 더 적은 클라우드에서도 쓸 수 있을 것 같음

  • 흥미롭게 들리지만 AWS에서 일해본 적도 없고 TLA+ 나 P에 이미 익숙하지도 않아서, 둘 중 하나라도 hello world 예제가 있었으면 좋았겠음
    그런 예시가 없으니 좋은 설계와 테스트 과정으로도 잡아야 할 것들에 불필요한 고통을 더하는 것처럼 들림
    글 안에 기본 예제가 있었다면 이것들이 실제로 무엇을 하는지 더 잘 이해할 수 있었을 것임

    • 좋아하는 TLA+ 빠른 데모는 이것임: https://gist.github.com/hwayne/39782de71f14dc9addb75f3bec515...
      N개의 스레드가 공유 카운터를 원자적이지 않게 증가시키는 모델이고, 속성은 “카운터가 결국 모델의 스레드 수와 같아진다”임
      TLA+로 검사하면 한 스레드가 다른 값을 덮어쓰는 경쟁 조건을 찾아냄
      이 버그 있는 설계의 구현을 직접 작성해봤는데, 내 컴퓨터에서는 실행의 0.1% 미만에서만 경쟁이 발생해서 직접 테스트로 잡기는 매우 어려움
      대부분의 TLA+ 명세는 이보다 훨씬 복잡한 시스템용이지만, 오류가 비교적 단순해서 좋은 데모임
    • TLA Plus 예제 저장소가 아주 좋음: https://github.com/tlaplus/Examples
      DieHard 문제처럼 단순한 것부터 시작하는 것을 추천함
    • 형식 기법을 쓰는 핵심 이유는 테스트가 절대로 모든 것을 잡을 수 없기 때문임
    • 테스트는 어떤 문제 부류의 특정 인스턴스에 대해 구현이 맞다는 것을 보일 뿐이고, 형식 검증은 그 부류 전체를 증명함
      애너그램을 반환하는 함수가 있다면 테스트는 몇몇 단어 쌍에 대해 맞다는 것을 보일 수 있음
      하지만 모든 단어에 대해 증명하려면 형식 검증이 필요하고, 그 과정에서 정의되지 않은 동작이나 라이브러리 버그 때문에 생기는 까다로운 오류를 잡게 됨
    • “좋은 설계”에서 좋은이라는 말이 너무 많은 것을 떠안고 있음
      TLA+/PlusCal의 목적은 설계의 건전성에 대한 증명을 갖는 것임

  • 업계가 TDD 같은 것에 도달했다는 게 흥미로움
    숫자 두 개를 더하는 함수처럼 단순한 것에도 제대로 작동하지 않는데 말임
    일부 극단적 경우에 완전히 쓸모없는 것은 아니지만, 형식적 기반이 전혀 없다는 점에서 이미 단서가 있었어야 함
    Uncle Bob 시대에는 검토되지 않은 나쁜 아이디어가 너무 많았고, 프로세스 “의식”까지 갖춘 종교에 훨씬 가까웠음

  • 속성 기반 테스트와 퍼징이 형식 기법과 관련 있다는 건 이해됨
    검사 대상이 형식 명세의 일부처럼 보이고, 어떤 의미에서는 모델 검사가 확인하는 검사의 부분집합이기 때문임
    하지만 런타임 모니터링을 “준형식 접근”이라고 부르는 건 상당히 억지처럼 보임

    • PObserve 같은 것을 이용한 런타임 모니터링이라면 준형식 접근이 맞음
      일반적인 알람이나 지표 수집을 말하는 게 아님

  • Promela와 SPIN은 글에서 설명하는 것보다 더 높은 수준이라고 보면 맞을지 궁금함

    • 저자 중 한 명인데, 약 10년 전에 Promela로 분산 시스템 작업을 해봤지만 그 영역에 딱 맞는다는 느낌은 들지 않았음
      멋진 아이디어가 있긴 하고, 언젠가 다시 살펴볼 가치는 있을 수 있음
답변달기