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 기반의 캐시 일관성 프로토콜을 설계하여 시스템 전반에서 데이터 일관성을 유지한다.

Distributed Systems and Data Centers 2

Fork in the Road: Reflections and Optimizations for Cold Start Latency in Production Serverless Systems

Severless system의 cold start문제를 해결하는 논문이다. 발견된 문제는 1. serverless framework자체의 오버헤드를 무시한점 2. end-to-end가 아닌 특정 파트만을 optimization한점이다. 이를 해결하기 위해서 1. control path를 최적화 하고 2. resource contention latency를 줄이며 3. user code initilization latency를 줄일 수 있는 기법들을 적용하여서 AFaas라는 framework를 개발하였다.

Kamino: Efficient VM Allocation at Scale with Latency-Driven Cache-Aware Scheduling

VM Allocation는 caching을 사용해서 VM Allocation latency를 줄인다. 그러나 기존의 Load-balancing기반의 Scheudler는 Caching에 의한 효과를 반영하지 않기 때문sub-optimal하다. 이 논문은 VM Allocation Caching State를 반영하는 최적의 Scheduler를 디자인하였다.

Kernel and Operating Systems

Extending Applications Safely and Efficiently

논문은 EIM과 bpftime이라는 모델을 개발하였다. 본 논문은 사용자 공간 애플리케이션(userspace application)을 보다 쉽고 효율적으로 확장하기 위한 모델을 제안한다. EIM은 확장(extension)이 수행할 수 있는 동작을 리소스(resource)로 간주하며, 이를 통해 확장 가능한 기능들을 체계적으로 정의하고 관리할 수 있도록 하였다. 이러한 EIM 모델을 기반으로, 논문은 bpftime이라는 프레임워크를 설계하였다. Bpftime은 eBPF를 활용하여 EIM 모델을 효과적으로 반영할 수 있도록 구현되었다. 또한 Bpftime은 eBPF, Intel MPK와 같은 다양한 격리 모델(Isolation models), 그리고 동적 바이너리 리라이팅(Dynamic Binary Rewriting) 등의 기법들을 활용하여 효율적이고 안전한 확장 시스템을 구축하였다.

Tintin: A Unified Hardware Performance Profiling Infrastructure to Uncover and Manage Uncertainty

Hardware performance counter는 정확도와 어디서 이벤트가 발생하였는지를 정밀하게 탐색하는 것이 중요하나, 기존의 시스템은 부족한 부분이 있었다. Tintin은 modular three-componenet디자인을 통해서 이러한 도전과제를 해결하였다. Tintin은 불확실함을 runtime에서 파악하여, 최소화 하기 위한 방향으로 scheduling하고, application에 어느정도의 불확실함이 있는지 리포트하는 시스템을 제시하였다. 또한 Event Profiling Context라는 새로운 OS primitive을 제시하여 다양한 profiling 요구사항을 통합시켰다.

Building Bridges: Safe Interactions with Foreign Languages through Omniglot

Memory 그리고 Type-safe한 언어는 모든 시스템의 버그를 해결하낟고 주장한다. 그러나 실제로는, unsafe한 파트가 항상 존재하기 때문에 불가능하다. Omniglot은 Rust의 safety와 soundness에 대한 면밀한 분석을 통해서 Unsafe한 파트(즉 unsafe library)와 아닌 Safe라이브러리의 분리를 통해서 안전한 시스템을 달성하고자 하였다. Omniglot은 kernel와 POSIX Compatible user-level library두 모델로 포팅되었으며, 두 경우 모두 성능과 안정성 모두 State-of-the-art의 경향을 보였다.

KRR: Efficient and Scalable Kernel Record Replay

Kernel의 버그를 찾기 위해서 Record하고 Replay하는 기법은 Scalabe하지 않다. KRR은 커널의 Record-Replay해야 하는 범위를 줄여서, Scalable한 시스템을 구축하는 것을 목표로 하였다. 기존의 모든 Stack을 Record하는 접근방식과는 다르게, KRR은 split-recoder디자인을 적용해서 guest와 host가 서로 협력하며 kernel execution을 record하도록 하였다.

Deterministic Client: Enforcing Determinism on Untrusted Machine Code

DeCl은 x86-64 및 Arm64 기반의 untrusted machine code를 결정론적으로 실행하기 위한 software-based sandboxing 시스템이다. 이 시스템은 Software Fault Isolation(SFI) 기법을 응용하여 단순한 메모리 격리를 넘어 결정론적 동작(determinism)을 강제하는 데 활용하였다. DeCl은 간결하고 효율적인 machine code verifier를 통해, trusted compiler나 interpreter 없이도 프로그램의 결정론적 실행을 보장하였다. 또한, DeCl은 deterministic preemption을 보장하는 두 가지 metering 기법을 도입하고, sandboxed 코드를 position-oblivious하게 처리함으로써 기존의 소프트웨어 격리와도 결합 가능하도록 설계하였다. DeCl은 interpreter와 JIT compiler의 장점을 동시에 제공하면서도, 낮은 CPU 오버헤드, 빠른 초기화 시간, 작은 신뢰 기반(trusted code base)을 보였다.

Disentangling the Dual Role of NIC Receive Rings

기존 네트워크 시스템은 각 CPU 코어마다 Rx 링을 두어 패킷을 수신하지만, 이로 인해 전체 I/O working set이 커지고 LLC를 초과해 메모리 대역폭 병목이 발생한다. 이를 해결하기 위한 기존 방식(shRing)은 Rx 링을 공유하지만, 부하 불균형 상황에서 병목이 생긴다. 논문에서는 이러한 병목이 두 개의 독립적인 producer-consumer 구조가 불필요하게 얽혀 있기 때문이라고 주장한다. 구체적으로는 다음 두 가지가 구분되지 않아 문제가 발생한다고 본다: (1) 메모리 할당(memory allocation): CPU가 빈 버퍼를 생성하고 NIC가 이를 소비하여 패킷을 저장 (1) 패킷 전달(packet delivery): NIC가 패킷을 생성하고 CPU가 이를 소비하여 처리. 이러한 구조적 문제를 해결하기 위해, 저자들은 rxBisect라는 새로운 CPU-NIC 인터페이스를 제안한다. rxBisect는 기존 Rx 링 하나를 두 개의 독립적인 링(메모리 할당용 링과 패킷 전달용 링)으로 분리함으로써, 메모리 할당과 패킷 수신을 독립적으로 수행할 수 있도록 한다. 이로 인해 코어 간 빈 버퍼를 효율적으로 전달할 수 있으며, 부하 불균형 상황에서도 병목 없이 동작할 수 있다.

XSched: Preemptive Scheduling for Diverse XPUs

다양한 XPU들을 효율적으로 사용하기 위해서 preeemptive scheduling이 가능한 flexible scheduler를 디자인 하였다. 하나의 통합된 preemptible command queue abstraction을 제공하며, 이러한 Abstraction을 제공하기 위해서, multi-level hardware model을 제시하였다.

EMT: An OS Framework for New Memory Translation Architectures

EMT(Extensible Memory Translation)는 리눅스 기반의 메모리 변환(memory translation) 프레임워크로, Radix tree나 Hash table 등 다양한 구조를 사용하는 최신 하드웨어 메모리 변환 방식을 유연하게 지원하도록 설계되었다. 기존 리눅스 메모리 관리 시스템은 새로운 하드웨어 구조를 적용하기 어렵다는 한계가 있었고, EMT는 이러한 확장성 부족 문제를 해결한다. EMT는 아키텍처에 독립적인 인터페이스를 제공하며, 다음과 같은 핵심 기능을 지원한다: (1) 다양한 메모리 변환 아키텍처(radix tree, hash table 등)에 대한 범용적 대응 (2) 하드웨어 특화 최적화(Hardware-specific optimization)의 지원 (3) 최신 하드웨어 및 OS의 구조적 복잡성에 대한 유연한 수용 (4) 기존 고정형 구현에 비해 성능 손실이 거의 없는 수준의 오버헤드. EMT위에 리눅스 메모리 관리 기능을 포팅한 결과, 확장성을 제공하면서도 성능 저하 없이 기존 시스템과 유사한 효율을 유지할 수 있었다. 또한 EMT는 실험적 메모리 변환 구조인 ECPT와 FPT를 OS에 구현하고 최적화할 수 있는 기반을 제공하였다.

Tiered Memory Management Beyond Hotness

메모리 시스템은 hotness에 기반해서 데이터를 어떤 memory node에 놓을지 결정하지만, hotness로 판단하는 것이 항상 optimial한 것은 아니다. 따라서 Amortized offcore latency (AOL)라는 metric을 도입하여서 더욱 효율적인 data placement가 가능하도록 하였다. AOL을 바탕으로 SOAR과 ALTO라는 새로운 data placement policy또한 제시하였다.

Privacy and Security

MettEagle: Costs and Benefits of Implementing Containers on Microkernels

Container기반 시스템은 Seccomp와 같은 시스템을 사용해서 Isolation을 보장하지만, 복잡한 커널 구조로 인해서 TCB가 크다는 단점이 있다. Microkernel기반의 시스템에서는 통합적인 Authority라는 것이 없기에 Container같은 시스템을 만들기 힘들다. 이 논문은 Microkernel기반의 OS에서 가볍고 더 안전한 container infrastructure을 개발하는 것을 목적으로 한다. Microkernel에서 커널을 만들경우 TCB가 줄어드는 등의 장점이 있다는 것을 제시하였다.