Distributed Systems and Data Centers I
Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols
Distributed protocols들은 올바르게 설계하기 어렵다. 이를 위해서 Formal verification을 이용해서 Protocol이 Safety property를 만족하는지를 Verification하는 과정이 필요하다. Formal verification을 위해서 Inductive invariant들을 분석해야 하지만, 올바른 Inductive invariant를 찾는 것은 매우 어려운 작업이여서, 기존의 방식들은 수작업 혹은 제한된 논리(Fragment of logic)에서만 작동하였다. 이 논문은 자동으로 이러한 Inductive invariant들을 찾아가는 두개의 key insight를 제시하였다. Provenance Invariants라는 개념을 도입하여서 호스트 내의 변수와 그 값을 만들게 된 원인을 자동으로 찾아 내었고, Atomic Sharding이라는 알고리즘을 통해서 각 프로토콜 단계를 정적 분석하였다. 최종적으로 Basilisk라는 도구를 구현하여서, 기존보다 훨씬 일반적인 논리를 다루지만 자동화된 분산 프로토콜용 정적 분석기를 개발하였다.
Deriving Semantic Checkers from Tests to Detect Silent Failures in Production Distributed Systems
Distributed system에서 Semantic적으로는 버그이지만, 명시적인 에러를 가져오지는 않는 미묘한 버그들을 잡기 위해서 System test code로부터 Semantic checker를 유도할 수 있는 시스템을 개발하였다. 이를 통해서 T2C라는 시스템을 설계하여, 기존 시스템 대비 더 일반적이고 큰 분산 어플리케이션에도 안정적으로 동작하는 Semantic checker를 개발하였다.
Picsou: Enabling Replicated State Machines to Communicate Efficiently
FineMem: Breaking the Allocation Overhead vs. Memory Waste Dilemma in Fine-Grained Disaggregated Memory Management
RDMA기반의 Memory disaggregation 시스템은 효율적인 작동을 위해서 메모리를 몇 GB로 할당하고 해제하기 때문에 불필요한 메모리 오버헤드가 발생한다. FineMem은 High-performance, Fine-grained RDMA memory allocation을 목적으로 개발되었다. RDMA메로리를 등록(Registration)하는 비용을 줄이기 위해서 Per-compute node MR pre-registration기법을 고안하였으며, Memory isolation을 위해서 RDMA memory windows와 Trusted allocation service를 각각의 컴퓨팅 노드위에서 동작하도록 구현하였다. 또한 메모리 노드의 CPU와 Matadata의 Consistency를 효율적으로 관리하기 위한 Lock free one-sided RDMA protocol를 Logging을 통해서 동작하도록 하였다. 결과적으로 FineMem은 Remote memory allocation latency를 최대 95%까지 줄이는데 성공하였다.
To PRI or Not To PRI, That's the question
SR-IOV나 I/O Device passthrough와 같은 방식은 Page fault를 지원하지 않기 때문에 Memory Pinning을 강제하기하여 메모리 Utilization에 부정적인 영향을 끼친다. 논문은 IOMMU, OS, Devices와 같은 시스템들이 Device-side I/O Page fault(IOPA)를 지원하기 위해서 어떻게 디자인되어야 하는지를 연구하였다. 최종적으로 VIO라는 IOPA를 효과적으로 사용하는 Dynamic I/O Device passthrough시스템을 제시하였다. 핵심 아이디어는 Shadow available queue를 활용하여, 실시간 IOPS 압력에 따라 디바이스를 VIO 모드와 패스스루 모드 간에 동적으로 전환하는 것이다. 이를 통해 성능과 자원 활용도를 동시 달성한다. 또한, IOPA-snooping을 통해 각 DMA 요청을 확인하여 IOPF(페이지 폴트)를 제거하고, 인터럽트는 직접 VM으로 전달되어 오버헤드를 최소화 하였다.
Enabling Efficient GPU Communication over Multiple NICs with FuseLink
Database Systems
Tigon: A Distributed Database for a CXL Pod
Distributed system에서 Transactional을 효율적으로 구현하기 위해서 Tigon은 CXL메모리의 Atomic operation을 활용하면서도, CXL memory의 High latency와 Lower bandwidth문제, 그리고 Cross-host cache coherence에 대한 하드웨어적인 Limitation을 극복할 수 있는 Design을 제시하였다.
Mako: Speculative Distributed Transactions with Geo-Replication
Quake: Adaptive Indexing for Vector Search
Approximate nearest neighbor(ANN)를 찾기 위한 Vector search는 워크로드가 Dynamic하거나 Skewed하면 성능이 느려진다. Quake는 워크로드의 패턴에 따라서 변화하는 cost model를 이용한 Multi-level partitioning와 새로운 recall estimation model을 이용하여 쿼리 수행 파라미터를 동적으로 새 설정하는 방식을 제시하여, Vector search 알고리즘의 효율성을 높였다.
Achieving Low-Latency Graph-Based Vector Search via Aligning Best-First Search Algorithm with SSD
PipeANN이라는 On-disk 기반 그래프 기반 Nearest neighbor search알고리즘을 제안하였다. PipeANN은 SSD 특성에 최적화된 best-first search 알고리즘을 적용하여, 검색 단계 간 strict한 연산-I/O 순서를 피함으로써 기존 시스템 대비 Latency를 줄였다.