USENIX OSDI 2025

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를 개발하였다.

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으로 전달되어 오버헤드를 최소화 하였다.

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을 제시하였다.

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를 줄였다.

Scheduling and Resource Management

Söze: One Network Telemetry Is All You Need for Per-flow Weighted Bandwidth Allocation at Scale

Weighted bandwidth allocation은 데이터 센터에서 많이 사용되지만, 정확하게 측정하는 것은 매우 도전적인 과제이다. Soze는 lightwedight한 weighted bandwidth를 보다 정확하게 추적할 수 있는 기법을 개발하였다.

Decouple and Decompose: Scaling Resource Allocation with DeDe

효율적인 Resource allocation은 여러개의 VM들이 효율적으로 자원을 공유하기 위해서 필수적이다. 하지만 점점 Scale이 커져가면서, 기존의 Optimization방식들을 특정 Application에 맞추어 최적화 시키거나, 아니면 특정 워크로드에 대한 가정을 전제로만 작동하였다. DeDe는 이러한 Resource allocation문제가 본질적으로 분리 가능하다고 주장한다. 즉, 각각 Tenant들의 독립적인 제약하에서, 전체 시스템의 효율성을 최적화 하여야 한다고 주장한다. DeDe는 Decouple-and-decompose방식을 도입하여서, 병렬적으로 전체 최적화 문제를 각 자원 및 각 수요 단위의 하위 문제로 분해하는 방식을 개발하였다.

Scalio: Scaling up DPU-based JBOF Key-value Store with NVMe-oF Target Offload

DPU 기반 Just a Bunch of Flash (JBOF) 솔루션은 에너지 효율적이고 비용 효과적인 아키텍처이지만, 확장성에 한계가 있다. 이는 대부분의 SSD I/O 처리를 DPU 내부의 CPU에 의존하기 때문이다. Scalio는 이러한 한계를 해결하기 위해 SSD I/O 연산을 최대한 DPU의 네트워크 I/O 기능과 NVMe over Fabrics Target Offload를 활용하여, CPU가 아닌 경로로 오프로딩하였다. 또한 Scalio는 bursty write와 hot read 트래픽을 효율적으로 처리하기 위해 2계층 메모리 설계(two-layer memory design)를 도입하였다. CPU의 캐시와 달리 DPU와 SSD 간의 DRAM 상태는 하드웨어 캐시 일관성(coherence)이 자동으로 보장되지 않기 때문에, Scalio는 RDMA 기반의 캐시 일관성 프로토콜을 설계하여 시스템 전반에서 데이터 일관성을 유지한다.