TL;DR

  • 명세와 코드의 동기화는 추상화 수준을 낮춰야 해 비용이 크므로, 대부분의 기업에는 명세만으로 코드를 생성하거나 구현과 명세를 증명으로 맞추는 방식이 경제적이지 않음.
  • 명세는 설계와 환경을 함께 표현하고 코드보다 높은 추상화 수준에서 간결하게 작성할 수 있음.
  • 코드와 동기화되지 않더라도 명세는 설계 결함과 구현 오류를 구분하게 해 시스템 구축과 버그 수정 속도를 높이는 순이익을 제공함.
  • 명세의 특정 부분에서 코드를 생성하는 연구가 진행 중이며, 명세에서 테스트를 생성하는 방식은 코드 생성보다 실현 가능성이 높음.
  • MongoDB는 TLA+ 모델의 상태 그래프를 약 5,000개 테스트로 변환했지만, 맞춤 코드가 필요하고 대상이 저수준 결정적 프로그램이라는 한계가 있음.

동기화 비용은 너무 큼

  • 명세와 코드를 맞추는 방법은 명세에서 복잡한 프로그램을 생성하는 프로그램 추출(program extraction)과, 독립적으로 작성한 코드가 명세와 일치함을 증명하는 세련(refinement) 두 가지임. Coq와 Agda 같은 정리 증명기(theorem prover)는 프로그램 추출 기능을 제공하며, seL4 팀은 C 코드에 세련 방식을 적용함.
  • 추출하거나 세련할 수 있는 명세는 동기화되지 않은 명세보다 작성하기 훨씬 어려움. 명세는 프로그램보다 높은 추상화 수준에서 작성할 수 있어 더 간결하고 핵심에 집중할 수 있지만, 동기화를 위해서는 코드 수준에 가까워져야 하므로 추상화의 이점을 잃음.
  • 예를 들어 PlusCal에서는 독자가 큐에서 값을 꺼내 자신의 합계에 더하는 동작을 몇 줄로 표현할 수 있음. 실제 프로그램에는 독자 설정, 큐 읽기, 합계 저장 코드가 필요하며, 저장소가 Postgres나 redis 같은 별도 시스템이면 클라이언트 라이브러리도 필요함. 여기에 로깅, 하트비트, 이벤트 훅 등 여러 부수적 관심사도 더해짐.
  • 명세 전체를 구현할 수 없는 경우도 있음. 기계와 세계의 구분에 따라 명세는 설계 중인 시스템뿐 아니라 시스템 주변 환경도 표현할 수 있음.
  • AWS SQS를 큐로 사용하는 경우 연결에 실패하거나 메시지가 중복될 가능성이 있음. 시스템이 구현하는 것은 이런 상황 자체가 아니라 이를 감지하고 대응하는 코드임.
  • 명세에는 연결 불가 시 오류 상태를 설정하고, 중복 메시지 시 합계만 갱신하며, 정상 경로에서는 합계를 갱신한 뒤 큐의 첫 항목을 제거하는 동작을 함께 표현할 수 있음.
  • 명세와 코드를 동기화하려면 명세를 코드 수준에 더 가깝게 만들어야 하며, 이는 상당한 비용을 수반함. 대부분의 기업에는 감당하기 어려운 비용임.

그래도 명세는 가치가 있음

  • 운영 환경에서 버그가 발생했을 때 명세가 있으면 설계를 잘못 구현했거나 설계의 가정, 예를 들어 큐가 완전히 신뢰할 수 있다는 가정이 틀렸을 가능성으로 원인을 좁힐 수 있음.
  • 명세가 없으면 여기에 설계 자체의 결함 가능성까지 더해짐. 설계 결함은 가장 위험하고 수정 비용도 큼. 한 발표에서는 설계 결함 하나로 팀이 1년간 재작업했다고 추산함.
  • 명세 없이 설계 결함을 정확히 진단하기도 어려움. 설계 버그를 구현 버그로 오인해 고치면 잠시 문제가 사라졌다가 모두가 잊을 즈음 다시 나타나는 경우가 있음. 새 설계에 버그가 없는지도 다시 확인해야 함.
  • 따라서 코드와 동기화하지 않더라도 형식 기법(formal methods)은 순이익임. 검증된 설계를 바탕으로 시스템을 더 빠르게 구축하고 버그를 더 빠르게 수정할 수 있으며, 발견된 버그가 적어도 구현 오류라는 확신을 얻을 수 있음.
  • 설계 가정이 잘못된 경우는 약점으로 남지만, 일반적으로 작동하는 설계에서 하나의 가정이 깨진 상황에 대응하는 편이 애초에 제대로 작동했는지 알 수 없는 임시방편 설계를 고치는 것보다 쉬움.

진행 중인 연구

  • 앞서 동기화가 불가능하다고 설명한 부분은 흥미로운 연구를 충분히 다루지 못한 설명임.
  • 명세에서 코드를 저렴하게 생성하는 방식은 일반적으로 실현 가능하지 않을 수 있지만, 특정 명세 하위 집합에서는 가능함. 연구 프로젝트 PGo는 PlusCal 변형을 Go 코드로 변환함. 예제가 공개돼 있지만, 가까운 시일 안에 프로덕션 준비가 끝날 것으로 보이지는 않음.
  • 명세에서 테스트를 생성하는 접근은 더 유망함. 여러 기업이 이를 수행했으며, 공개 사례 중 가장 잘 알려진 곳은 MongoDB임.

이 목적을 위해 새 TLA+ 명세를 작성하고 TLC 모델 검사기가 탐색한 상태 공간을 이용해 운영 변환(OT) 알고리즘의 일부를 검증하는 C++ 및 Golang 테스트 사례를 생성함. 모델을 변경할 때마다 테스트 사례를 자동 생성해 실행할 수 있으며, 두 구현이 동등성을 유지하는 데 필요한 변경을 수행하는지 확인함.

  • MongoDB는 TLA+ 명세의 상태 그래프를 내보낸 뒤 선형 동작 집합으로 분해하고, 이를 약 5,000개 테스트로 변환함. 테스트를 통과하는 구현은 여러 개일 수 있으므로, 테스트는 코드보다 추상적이라고 볼 수 있어 코드 생성보다 격차가 작음.
  • TLA+ 모델 검사기에는 테스트 생성에 유용한 기능이 있음.
  • 시뮬레이션 모드로 무작위 추적을 가져올 수 있음.
  • ALIAS로 추적 출력 내용을 세밀하게 조정할 수 있음.
  • 모델 검사 중 하위 프로세스를 호출하는 입출력 확장 기능(IO extension)을 테스트 하네스 구동에 활용할 수 있음.
  • 중요한 제한 사항은 두 가지임.
  • MongoDB 팀은 이 방식을 구현하기 위해 맞춤 코드를 다수 작성했으며, 명세를 테스트로 변환하는 기성 솔루션은 없음.
  • 대상이 저수준 결정적 프로그램이어서 TLA+를 코드에 비교적 가깝게 유지할 수 있었음. 분산 시스템의 테스트 하네스를 작성하는 일은 훨씬 어려움.
  • 이런 한계에도 명세 기반 테스트 생성은 유망한 방향임.

댓글 모음

  • 그래프 유형에 관한 글에 대한 여러 반응 중 흥미로운 내용을 모아 댓글 모음으로 정리함. datalog과 루빅스 큐브에 관한 내용이 포함됨.

각주

  • PlusCal은 순수 TLA+로 컴파일되는 도메인 특화 언어(DSL)임. 여기서는 이에 대응하는 TLA+ 구문이 외부 독자에게 다소 읽기 어렵다는 이유로 PlusCal을 사용함.