Refinement Proofs in Rust Using Ghost Locks

당신이 거대하고 고속으로 작동하는 디지털 도시를 건설하고 있다고 상상해 보십시오. 당신에게는 교통 신호등, 우편 배달원, 전력망이 이론적으로 어떻게 작동해야 하는지를 보여주는 아름답고 완벽한 설계도(추상 모델)가 냅킨 위에 그려져 있습니다. 그리고 당신에게는 실제 노동자들, 녹슨 파이프, 교통 체증이 존재하는 실제의 무질서한 건설 현장(구체적 구현)이 있습니다.

컴퓨터 과학의 큰 문제는 다음과 같습니다: 건설 속도를 늦추거나 노동자들이 끝없는 서류 작업을 하느라 일을 멈추게 하지 않으면서도, 어떻게 하면 실제의 무질서한 건설 현장이 완벽한 냅킨 설계도를 실제로 따르고 있다는 것을 증명할 수 있는가 하는 점입니다.

오랫동안 이를 위한 도구들은 두 가지 극단적인 선택지였습니다. 옵션 A는 설계도를 바탕으로 당신을 대신해 도시를 건설하는 로봇이었습니다. 그것은 완벽했지만, 건물들은 투박하고 느리며 잘못된 재료를 사용했습니다. 옵션 B는 실제 도시의 벽돌 하나하나를 검사하는 검사팀이었습니다. 그들은 철저했지만, 도시가 매우 구체적이고 경직된 방식으로 지어질 것을 요구했으며, 오직 그들이 사용하는 특정하고 오래된 도구를 사용할 때만 작동했습니다.

주요 발견: "고스트 락(Ghost Lock)" 기법
이 논문의 저자들은 Rust 프로그래밍 언어를 사용하여 이 간극을 메울 새로운 방법을 발명했습니다. 그들은 이를 **"고스트 락을 이용한 Rust에서의 정제 증명(Refinement Proofs in Rust Using Ghost Locks)"**이라고 부릅니다.

고스트 락을 마법 같고 투명한 열쇠라고 생각해 보십시오.

• 설계도 (모델): 팀은 코드 내부에 도시의 규칙을 담은 "고스트" 버전의 규칙을 만듭선합니다. 이 고스트 도시는 (우편함에 편지가 몇 통 있는지와 같은) 완벽한 상태를 추적합니다.
• 실제 도시 (코드): 실제 프로그램은 빠르고 효율적으로 실행되며 현대적인 기술들을 사용합니다.
• 열쇠: 작업자(컴퓨터 스레드)가 실재하는 도시의 무언가를 변경해야 할 때, 그들은 먼저 고스트 락을 집어 들어야 합니다.
  • 락을 잡고 있는 동안, 그들은 고스트 도시를 들여다보며 현재 상태를 확인할 수 있습니다.
  • 그들은 자신의 일을 수행합니다.
  • 일을 마친 후, 그들은 락을 다시 내려놓습니다. 하지만 여기서 마법이 일어납니다. 그들은 락에게 자신이 방금 무엇을 했는지(예: "편지를 보냈다" 또는 "편지를 쓰레기통에 버렸다") 정확히 속삭여야 합니다.
  • 락은 체크합니다: "방금 네가 한 일이 고스트 도시의 규칙과 일치하는가?" 만약 그렇다면 아주 잘된 일입니다! 만약 아니라면, 증명은 실패합니다.

이 락은 "고스트"이기 때문에 프로그램이 실제로 실행될 때는 사라집니다. 이는 성능을 저하시키지 않습니다. 마치 당신이 건물을 떠나는 순간 사라지는, 당신의 상상 속에만 존재하는 보안 요원이 당신이 규칙을 잘 따랐는지 확인하는 것과 같습니다.

그들이 "아니오"라고 말하는 것들
저자들은 자신들의 방법이 무엇이 아닌지를 명확히 밝히고 있습니다.

• 로봇 건설자 없음: 그들은 설계도로부터 코드를 자동으로 생성하는 아이디어를 명시적으로 거부합니다. 그들은 느린 자동 생성 코드로 대체하는 것이 아니라, 기존의 빠르고 인간이 작성한 코드가 올바르다는 것을 증명하기를 원합니다.
• 경직된 구조 없음: 그들은 수학을 더 쉽게 만들기 위해 프로그래머가 코드를 특정하고 경직된 형태로 작성하도록 강요하는 방식에 반대합니다. 그들의 방법은 여러 작업이 동시에 발생하는 멀티스레드 프로그램을 포함하여, 무질서하고 복잡한 실제 세계의 코드 구조에서도 작동합니다.
• "아마도" 식의 안전성 없음: 그들은 자신들의 방법이 작동한다고 단순히 제안하는 데 그치지 않고, 증명했습니다. 단순히 시뮬레이션을 실행한 것이 아니라, 논리를 단계별로 체크하는 형식 검증기(매우 똑똑한 수학 로봇)를 사용하여 실제 코드가 반드시 설계도를 따라야 함을 확인했습니다.

"라이브니스(Liveness)" 퍼즐
안전성(Safety)은 쉽습니다: "기차가 충돌했는가?" (아니라면? 좋습니다.)
하지만 **라이브니스(Liveness)**는 어떨까요? 이것은 "기차가 언젠가 도착할 것인가?"라는 질문입니다.
저자들은 이 문제 또한 해결했습니다. 그들은 특수한 논리(LTL이라 불리는)를 사용하여 시스템이 단순히 충돌을 피하는 것뿐만 아니라, 실제로 계속 앞으로 나아가고 있음을 증명했습니다. 그들은 "진전(progress)"을 하나의 부채처럼 취급했습니다. 만약 노드(작업자)가 메시지를 보내겠다고 약속하면, 그들은 결국 그 약속을 "갚아야" 합니다. 만약 그들이 갚지 않고 계속 미룬다면, 증명 시스템이 그들을 잡아냅니다.

증명: 실제 세계 테스트
이것이 단순한 이론이 아님을 보여주기 위해, 그들은 세 가지 실제적인 것들을 구축하고 검증했습니다.

1. Memcached: 유명한 인터넷 캐싱 시스템의 단순화된 버전입니다. 그들은 네트워크 오류나 메시지 유실이 발생하더라도 시스템이 일관성을 유지함을 증명했습니다. 그들은 세 가지 버전으로 구축했습니다: 처음에는 단순한 버전, 그다음은 많은 스레드가 있는 버전, 마지막으로 매우 세밀한 잠금(예: 도서관의 모든 선반마다 별도의 잠금을 두는 것)이 적용된 버전입니다. 모델은 동일하게 유지되었지만 코드는 더 복잡해졌으며, 증명은 여전히 유효했습니다.
2. 생산자/소비자 큐 (Producer/Consumer Queue): 한 사람이 줄에 아이템을 넣고 다른 사람이 그것을 꺼내는 시스템입니다. 그들은 보통 충돌을 일으키는 위험한 저수준 메모리 기술(unsafe code)을 사용하더라도, 고스트 락이 체크하는 "검증된 셀(Verified Cell)"로 감싸면 이 시스템이 정상 작동함을 증명했습니다.
3. Paxos와 Hash Set: 그들은 복잡한 합의 알고리즘(Paxos)과 락 프리(lock-free) 해시 셋을 검증하여, 이 방법이 다양한 분산 시스템에서 작동함을 보여주었습니다.

수치 데이터
그들은 Intel Core i9-10885H 2.40GHz CPU와 16 GiB RAM을 갖춘 컴퓨터에서 테스트를 수행했습니다.

• Memcached 시스템의 경우, 검증에는 (첫 번째 버전의 경우) 약 334.7초에서 (가장 복잡한 버전의 경우) 최대 379.7초가 걸렸습니다.
• 모델 정의와 증명을 위해 작성한 코드는, 까다로운 "라이브니스(진전)" 증명을 포함하더라도 전체 시간과 주석 작업에 약 10% 정도를 추가했습니다.
• Memcached 모델 정의를 위한 총 코드 라인 수는 약 225줄이었고, 명세(specification)/고스트 코드는 약 286줄이었습니다.

결론
이 논문은 높은 수준의 추상적인 계획으로부터 복잡하고 효율적인 실제 Rust 프로그램이 그 계획을 완벽하게 따른다는 것을 증명할 수 있음을 보여줍니다. 그들은 코드를 느리거나 경직되게 만들지 않고도 이 일을 해냈습니다. 그들은 고스트 락을 사용하여 프로그램이 규칙을 엿보고, 자신의 일을 수행하며, 규칙을 따랐음을 증명하면서도, 최종 제품에서는 고스트 가드가 사라지게 했습니다. 이는 당신의 케이크를 (빠르고 유연한 코드로) 먹으면서도, 동시에 (수학적으로 증명된 안전성과 진전을) 가질 수 있는 방법입니다.