24 lines
32 KiB
HTML
24 lines
32 KiB
HTML
<!doctype html><html lang=en dir=auto data-theme=auto><head><meta charset=utf-8><meta http-equiv=X-UA-Compatible content="IE=edge"><meta name=viewport content="width=device-width,initial-scale=1,shrink-to-fit=no"><meta name=robots content="index, follow"><title>SOSP 2024 Digest | Publish Assistant</title><meta name=keywords content="operating-systems,distributed-systems,storage,cloud,formal-verification,ml-systems,security,serverless"><meta name=description content="13 papers selected.
|
||
|
||
Verus: A Practical Foundation for Systems Verification
|
||
Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 et al.
|
||
TL;DR — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency.
|
||
Why notable — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date."><meta name=author content="Publish Assistant"><link rel=canonical href=https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/digests/sosp-2024/><link crossorigin=anonymous href=/vincent/publish-assistant/assets/css/stylesheet.d72f07832e13c592b3edba91680bfe70f01daac396179bcace0ac36e8e0494c6.css integrity="sha256-1y8Hgy4TxZKz7bqRaAv+cPAdqsOWF5vKzgrDbo4ElMY=" rel="preload stylesheet" as=style><link rel=icon href=https://pub.sqrt.fr/vincent/publish-assistant/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://pub.sqrt.fr/vincent/publish-assistant/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://pub.sqrt.fr/vincent/publish-assistant/favicon-32x32.png><link rel=apple-touch-icon href=https://pub.sqrt.fr/vincent/publish-assistant/apple-touch-icon.png><link rel=mask-icon href=https://pub.sqrt.fr/vincent/publish-assistant/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><link rel=alternate hreflang=en href=https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/digests/sosp-2024/><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--code-block-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51);color-scheme:dark}.list{background:var(--theme)}.toc{background:var(--entry)}}</style></noscript><script>localStorage.getItem("pref-theme")==="dark"?document.querySelector("html").dataset.theme="dark":localStorage.getItem("pref-theme")==="light"?document.querySelector("html").dataset.theme="light":window.matchMedia("(prefers-color-scheme: dark)").matches?document.querySelector("html").dataset.theme="dark":document.querySelector("html").dataset.theme="light"</script><meta property="og:url" content="https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/digests/sosp-2024/"><meta property="og:site_name" content="Publish Assistant"><meta property="og:title" content="SOSP 2024 Digest"><meta property="og:description" content="13 papers selected.
|
||
Verus: A Practical Foundation for Systems Verification Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 et al.
|
||
TL;DR — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency.
|
||
Why notable — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date."><meta property="og:locale" content="en_us"><meta property="og:type" content="article"><meta property="article:section" content="cloud-edge"><meta property="article:published_time" content="2024-11-05T00:00:00+00:00"><meta property="article:modified_time" content="2024-11-05T00:00:00+00:00"><meta property="article:tag" content="Operating-Systems"><meta property="article:tag" content="Distributed-Systems"><meta property="article:tag" content="Storage"><meta property="article:tag" content="Cloud"><meta property="article:tag" content="Formal-Verification"><meta property="article:tag" content="Ml-Systems"><meta name=twitter:card content="summary"><meta name=twitter:title content="SOSP 2024 Digest"><meta name=twitter:description content="13 papers selected.
|
||
Verus: A Practical Foundation for Systems Verification Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 et al.
|
||
TL;DR — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency.
|
||
Why notable — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date."><script type=application/ld+json>{"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Edge and Cloud Systems","item":"https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/"},{"@type":"ListItem","position":2,"name":"Digests","item":"https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/digests/"},{"@type":"ListItem","position":3,"name":"SOSP 2024 Digest","item":"https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/digests/sosp-2024/"}]}</script><script type=application/ld+json>{"@context":"https://schema.org","@type":"BlogPosting","headline":"SOSP 2024 Digest","name":"SOSP 2024 Digest","description":"13 papers selected.\nVerus: A Practical Foundation for Systems Verification Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 et al.\nTL;DR — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency.\nWhy notable — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date.\n","keywords":["operating-systems","distributed-systems","storage","cloud","formal-verification","ml-systems","security","serverless"],"articleBody":"13 papers selected.\nVerus: A Practical Foundation for Systems Verification Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 et al.\nTL;DR — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency.\nWhy notable — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date.\n→ Read paper Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation Anish Athalye, Henry Corrigan-Gibbs, M. Frans Kaashoek, Joseph Tassarotti et al.\nTL;DR — A modular verification methodology lets developers prove end-to-end that a system leaks no sensitive information, bridging the gap from high-level spec all the way to circuit-level hardware behavior.\nWhy notable — Side-channel leakage across abstraction layers is notoriously hard to reason about; this work provides a principled, mechanized framework to do so, setting a new bar for hardware-software co-verification of secure systems.\n→ Read paper Autobahn: Seamless high speed BFT Neil Giridharan, Florian Suri-Payer, Ittai Abraham, Lorenzo Alvisi et al.\nTL;DR — Autobahn is a BFT consensus protocol that achieves high throughput under normal operation while seamlessly falling back to a slow path during faults, eliminating the throughput cliff common in prior BFT designs.\nWhy notable — Byzantine fault-tolerant systems have historically traded peak performance for safety margins; Autobahn’s seamless transition between fast and slow paths closes that gap and is likely to influence the next generation of production BFT deployments.\n→ Read paper Fast, Flexible, and Practical Kernel Extensions Kumar Kartikeya Dwivedi, Rishabh R. Iyer, Sanidhya Kashyap\nTL;DR — A new kernel extension framework surpasses eBPF’s safety and flexibility constraints by using a combination of ahead-of-time compilation and a lean verification layer, enabling complex kernel extensions with near-native performance.\nWhy notable — eBPF has become ubiquitous for in-kernel programmability, but its verifier fundamentally limits expressiveness; this work re-examines those trade-offs and offers a path toward richer, safer kernel extensions with broad applicability to networking, tracing, and storage.\n→ Read paper Tiered Memory Management: Access Latency is the Key! Midhul Vuppalapati, Rachit Agarwal 0001\nTL;DR — A principled tiered-memory manager that tracks per-page access latency rather than access frequency achieves substantially better performance for modern workloads on heterogeneous DRAM/CXL/NVM memory hierarchies.\nWhy notable — As CXL-attached memory becomes mainstream, frequency-based page migration policies inherited from NUMA systems are increasingly inadequate; this paper reframes the problem around latency and provides a practical, deployable design.\n→ Read paper Fast \u0026 Safe IO Memory Protection Benny Rubin, Saksham Agarwal, Qizhe Cai, Rachit Agarwal 0001\nTL;DR — A hardware-software co-design eliminates the performance overhead of IOMMU-based DMA isolation by allowing safe, fine-grained IO memory protection without full page-table walks on the critical path.\nWhy notable — DMA attacks remain a real threat yet IOMMU protection is widely disabled in production because of latency costs; this work makes protection affordable and is directly relevant to cloud, NIC, and storage subsystem designers.\n→ Read paper SWARM: Replicating Shared Disaggregated-Memory Data in No Time Antoine Murat, Clément Burgelin, Athanasios Xygkis, Igor Zablotchi et al.\nTL;DR — SWARM replicates data in disaggregated-memory clusters with near-zero latency overhead by exploiting one-sided RDMA operations and a carefully designed protocol that avoids coordination on the read path.\nWhy notable — Disaggregated memory is an emerging data-center architecture; providing fault tolerance without sacrificing its key latency advantage is an open problem, and SWARM’s approach is both novel and practically relevant.\n→ Read paper Morph: Efficient File-Lifetime Redundancy Management for Cluster File Systems Timothy Kim, Sanjith Athlur, Saurabh Kadekodi, Francisco Maturana et al.\nTL;DR — Morph dynamically transitions files through redundancy schemes (replication → erasure coding) based on observed file age and access patterns, substantially reducing storage overhead in large-scale cluster file systems.\nWhy notable — Static redundancy policies waste significant capacity in practice; Morph’s lifecycle-aware approach is validated at Google scale and provides a compelling template for storage systems serving diverse workloads.\n→ Read paper PowerInfer: Fast Large Language Model Serving with a Consumer-grade GPU Yixin Song, Zeyu Mi, Haotong Xie, Haibo Chen 0001\nTL;DR — PowerInfer exploits the activation sparsity of LLMs to partition computation between a consumer GPU and CPU, achieving high inference throughput without data-center hardware.\nWhy notable — Democratizing LLM inference beyond cloud hardware is a pressing systems challenge; PowerInfer’s sparsity-aware approach delivers surprising performance on commodity hardware and has already influenced a wave of follow-on work.\n→ Read paper LoongServe: Efficiently Serving Long-Context Large Language Models with Elastic Sequence Parallelism Bingyang Wu, Shengyu Liu, Yinmin Zhong, Peng Sun 0006 et al.\nTL;DR — LoongServe introduces elastic sequence parallelism that dynamically adjusts the number of workers handling each long-context request to minimize GPU idle time and satisfy latency SLOs.\nWhy notable — Long-context inference strains fixed parallelism strategies, creating severe resource fragmentation; LoongServe’s elasticity primitive addresses this gap and is directly applicable to production LLM serving infrastructure.\n→ Read paper Unifying serverless and microservice workloads with SigmaOS Ariel Szekely, Adam Belay, Robert Morris 0005, M. Frans Kaashoek\nTL;DR — SigmaOS is an OS-level abstraction that treats serverless functions and microservices as first-class, interchangeable computational units, simplifying resource management and improving utilization for mixed workloads.\nWhy notable — The artificial split between serverless and microservice programming models imposes significant operational complexity; SigmaOS’s unified abstraction from the MIT systems group offers a clean architectural answer with demonstrated performance gains.\n→ Read paper Cookie Monster: Efficient On-Device Budgeting for Differentially-Private Ad-Measurement Systems Pierre Tholoniat, Kelly Kostopoulou, Peter McNeely, Prabhpreet Singh Sodhi et al.\nTL;DR — Cookie Monster implements practical on-device differential-privacy budget management for ad attribution, showing that strong privacy guarantees can be enforced locally without destroying ad-measurement utility.\nWhy notable — Browser vendors are actively replacing third-party cookies with privacy-preserving attribution APIs; this paper provides rigorous analysis of the privacy-utility trade-off and offers deployable techniques relevant to both industry standards and future OS-level privacy primitives.\n→ Read paper Efficient Reproduction of Fault-Induced Failures in Distributed Systems with Feedback-Driven Fault Injection Jia Pan, Haoze Wu, Tanakorn Leesatapornwongsa, Suman Nath et al.\nTL;DR — A feedback-guided fault injection framework automatically reproduces complex distributed-system failures triggered by rare fault combinations, dramatically reducing the manual effort needed to diagnose and fix them.\nWhy notable — Fault-induced failures in distributed systems are notoriously hard to reproduce; the paper’s closed-loop search strategy is a methodological advance for reliability testing and is likely to influence both academic research and industrial chaos-engineering tools.\n→ Read paper ","wordCount":"1097","inLanguage":"en","datePublished":"2024-11-05T00:00:00Z","dateModified":"2024-11-05T00:00:00Z","author":{"@type":"Person","name":"Publish Assistant"},"mainEntityOfPage":{"@type":"WebPage","@id":"https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/digests/sosp-2024/"},"publisher":{"@type":"Organization","name":"Publish Assistant","logo":{"@type":"ImageObject","url":"https://pub.sqrt.fr/vincent/publish-assistant/favicon.ico"}}}</script></head><body id=top><header class=header><nav class=header-nav><div class=logo><a href=https://pub.sqrt.fr/vincent/publish-assistant/ accesskey=h title="Publish Assistant (Alt + H)">Publish Assistant</a>
|
||
<span class=logo-sep>/</span>
|
||
<a class=logo-topic href=/vincent/publish-assistant/cloud-edge/ title="Edge and Cloud Systems">Edge and Cloud Systems</a><div class=logo-switches><button id=theme-toggle class=theme-toggle accesskey=t title="(Alt + T)" aria-label="Toggle theme">
|
||
<svg class="moon" width="18" height="18" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg>
|
||
<svg class="sun" width="18" height="18" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu class=menu><li><a href=/vincent/publish-assistant/cloud-edge/venues/ title=Venues><span>Venues</span></a></li><li><a href=/vincent/publish-assistant/cloud-edge/calendar/ title=Calendar><span>Calendar</span></a></li><li><a href=/vincent/publish-assistant/cloud-edge/digests/ title=Digests><span class=active>Digests</span></a></li></ul></nav></header><main class=main><article class=post-single><header class=post-header><nav class=breadcrumbs role=navigation aria-label=Breadcrumb><a href=/vincent/publish-assistant/cloud-edge/digests/>Digests</a>
|
||
<svg viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="feather feather-chevron-right"><polyline points="9 18 15 12 9 6"/></svg></nav><h1 class="post-title entry-hint-parent">SOSP 2024 Digest</h1><div class=post-meta><span title='2024-11-05 00:00:00 +0000 UTC'>November 5, 2024</span> · <span>Publish Assistant</span></div></header><div class="post-content md-content"><p>13 papers selected.</p><hr><h3 id=verus-a-practical-foundation-for-systems-verification>Verus: A Practical Foundation for Systems Verification<a hidden class=anchor aria-hidden=true href=#verus-a-practical-foundation-for-systems-verification>#</a></h3><p><em>Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 <em>et al.</em></em></p><p><strong>TL;DR</strong> — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency.</p><p><strong>Why notable</strong> — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date.</p><p><a href=https://doi.org/10.1145/3694715.3695952>→ Read paper</a></p><hr><h3 id=modular-verification-of-secure-and-leakage-free-systems-from-application-specification-to-circuit-level-implementation>Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation<a hidden class=anchor aria-hidden=true href=#modular-verification-of-secure-and-leakage-free-systems-from-application-specification-to-circuit-level-implementation>#</a></h3><p><em>Anish Athalye, Henry Corrigan-Gibbs, M. Frans Kaashoek, Joseph Tassarotti <em>et al.</em></em></p><p><strong>TL;DR</strong> — A modular verification methodology lets developers prove end-to-end that a system leaks no sensitive information, bridging the gap from high-level spec all the way to circuit-level hardware behavior.</p><p><strong>Why notable</strong> — Side-channel leakage across abstraction layers is notoriously hard to reason about; this work provides a principled, mechanized framework to do so, setting a new bar for hardware-software co-verification of secure systems.</p><p><a href=https://doi.org/10.1145/3694715.3695956>→ Read paper</a></p><hr><h3 id=autobahn-seamless-high-speed-bft>Autobahn: Seamless high speed BFT<a hidden class=anchor aria-hidden=true href=#autobahn-seamless-high-speed-bft>#</a></h3><p><em>Neil Giridharan, Florian Suri-Payer, Ittai Abraham, Lorenzo Alvisi <em>et al.</em></em></p><p><strong>TL;DR</strong> — Autobahn is a BFT consensus protocol that achieves high throughput under normal operation while seamlessly falling back to a slow path during faults, eliminating the throughput cliff common in prior BFT designs.</p><p><strong>Why notable</strong> — Byzantine fault-tolerant systems have historically traded peak performance for safety margins; Autobahn’s seamless transition between fast and slow paths closes that gap and is likely to influence the next generation of production BFT deployments.</p><p><a href=https://doi.org/10.1145/3694715.3695942>→ Read paper</a></p><hr><h3 id=fast-flexible-and-practical-kernel-extensions>Fast, Flexible, and Practical Kernel Extensions<a hidden class=anchor aria-hidden=true href=#fast-flexible-and-practical-kernel-extensions>#</a></h3><p><em>Kumar Kartikeya Dwivedi, Rishabh R. Iyer, Sanidhya Kashyap</em></p><p><strong>TL;DR</strong> — A new kernel extension framework surpasses eBPF’s safety and flexibility constraints by using a combination of ahead-of-time compilation and a lean verification layer, enabling complex kernel extensions with near-native performance.</p><p><strong>Why notable</strong> — eBPF has become ubiquitous for in-kernel programmability, but its verifier fundamentally limits expressiveness; this work re-examines those trade-offs and offers a path toward richer, safer kernel extensions with broad applicability to networking, tracing, and storage.</p><p><a href=https://doi.org/10.1145/3694715.3695950>→ Read paper</a></p><hr><h3 id=tiered-memory-management-access-latency-is-the-key>Tiered Memory Management: Access Latency is the Key!<a hidden class=anchor aria-hidden=true href=#tiered-memory-management-access-latency-is-the-key>#</a></h3><p><em>Midhul Vuppalapati, Rachit Agarwal 0001</em></p><p><strong>TL;DR</strong> — A principled tiered-memory manager that tracks per-page access latency rather than access frequency achieves substantially better performance for modern workloads on heterogeneous DRAM/CXL/NVM memory hierarchies.</p><p><strong>Why notable</strong> — As CXL-attached memory becomes mainstream, frequency-based page migration policies inherited from NUMA systems are increasingly inadequate; this paper reframes the problem around latency and provides a practical, deployable design.</p><p><a href=https://doi.org/10.1145/3694715.3695968>→ Read paper</a></p><hr><h3 id=fast--safe-io-memory-protection>Fast & Safe IO Memory Protection<a hidden class=anchor aria-hidden=true href=#fast--safe-io-memory-protection>#</a></h3><p><em>Benny Rubin, Saksham Agarwal, Qizhe Cai, Rachit Agarwal 0001</em></p><p><strong>TL;DR</strong> — A hardware-software co-design eliminates the performance overhead of IOMMU-based DMA isolation by allowing safe, fine-grained IO memory protection without full page-table walks on the critical path.</p><p><strong>Why notable</strong> — DMA attacks remain a real threat yet IOMMU protection is widely disabled in production because of latency costs; this work makes protection affordable and is directly relevant to cloud, NIC, and storage subsystem designers.</p><p><a href=https://doi.org/10.1145/3694715.3695943>→ Read paper</a></p><hr><h3 id=swarm-replicating-shared-disaggregated-memory-data-in-no-time>SWARM: Replicating Shared Disaggregated-Memory Data in No Time<a hidden class=anchor aria-hidden=true href=#swarm-replicating-shared-disaggregated-memory-data-in-no-time>#</a></h3><p><em>Antoine Murat, Clément Burgelin, Athanasios Xygkis, Igor Zablotchi <em>et al.</em></em></p><p><strong>TL;DR</strong> — SWARM replicates data in disaggregated-memory clusters with near-zero latency overhead by exploiting one-sided RDMA operations and a carefully designed protocol that avoids coordination on the read path.</p><p><strong>Why notable</strong> — Disaggregated memory is an emerging data-center architecture; providing fault tolerance without sacrificing its key latency advantage is an open problem, and SWARM’s approach is both novel and practically relevant.</p><p><a href=https://doi.org/10.1145/3694715.3695945>→ Read paper</a></p><hr><h3 id=morph-efficient-file-lifetime-redundancy-management-for-cluster-file-systems>Morph: Efficient File-Lifetime Redundancy Management for Cluster File Systems<a hidden class=anchor aria-hidden=true href=#morph-efficient-file-lifetime-redundancy-management-for-cluster-file-systems>#</a></h3><p><em>Timothy Kim, Sanjith Athlur, Saurabh Kadekodi, Francisco Maturana <em>et al.</em></em></p><p><strong>TL;DR</strong> — Morph dynamically transitions files through redundancy schemes (replication → erasure coding) based on observed file age and access patterns, substantially reducing storage overhead in large-scale cluster file systems.</p><p><strong>Why notable</strong> — Static redundancy policies waste significant capacity in practice; Morph’s lifecycle-aware approach is validated at Google scale and provides a compelling template for storage systems serving diverse workloads.</p><p><a href=https://doi.org/10.1145/3694715.3695981>→ Read paper</a></p><hr><h3 id=powerinfer-fast-large-language-model-serving-with-a-consumer-grade-gpu>PowerInfer: Fast Large Language Model Serving with a Consumer-grade GPU<a hidden class=anchor aria-hidden=true href=#powerinfer-fast-large-language-model-serving-with-a-consumer-grade-gpu>#</a></h3><p><em>Yixin Song, Zeyu Mi, Haotong Xie, Haibo Chen 0001</em></p><p><strong>TL;DR</strong> — PowerInfer exploits the activation sparsity of LLMs to partition computation between a consumer GPU and CPU, achieving high inference throughput without data-center hardware.</p><p><strong>Why notable</strong> — Democratizing LLM inference beyond cloud hardware is a pressing systems challenge; PowerInfer’s sparsity-aware approach delivers surprising performance on commodity hardware and has already influenced a wave of follow-on work.</p><p><a href=https://doi.org/10.1145/3694715.3695964>→ Read paper</a></p><hr><h3 id=loongserve-efficiently-serving-long-context-large-language-models-with-elastic-sequence-parallelism>LoongServe: Efficiently Serving Long-Context Large Language Models with Elastic Sequence Parallelism<a hidden class=anchor aria-hidden=true href=#loongserve-efficiently-serving-long-context-large-language-models-with-elastic-sequence-parallelism>#</a></h3><p><em>Bingyang Wu, Shengyu Liu, Yinmin Zhong, Peng Sun 0006 <em>et al.</em></em></p><p><strong>TL;DR</strong> — LoongServe introduces elastic sequence parallelism that dynamically adjusts the number of workers handling each long-context request to minimize GPU idle time and satisfy latency SLOs.</p><p><strong>Why notable</strong> — Long-context inference strains fixed parallelism strategies, creating severe resource fragmentation; LoongServe’s elasticity primitive addresses this gap and is directly applicable to production LLM serving infrastructure.</p><p><a href=https://doi.org/10.1145/3694715.3695948>→ Read paper</a></p><hr><h3 id=unifying-serverless-and-microservice-workloads-with-sigmaos>Unifying serverless and microservice workloads with SigmaOS<a hidden class=anchor aria-hidden=true href=#unifying-serverless-and-microservice-workloads-with-sigmaos>#</a></h3><p><em>Ariel Szekely, Adam Belay, Robert Morris 0005, M. Frans Kaashoek</em></p><p><strong>TL;DR</strong> — SigmaOS is an OS-level abstraction that treats serverless functions and microservices as first-class, interchangeable computational units, simplifying resource management and improving utilization for mixed workloads.</p><p><strong>Why notable</strong> — The artificial split between serverless and microservice programming models imposes significant operational complexity; SigmaOS’s unified abstraction from the MIT systems group offers a clean architectural answer with demonstrated performance gains.</p><p><a href=https://doi.org/10.1145/3694715.3695947>→ Read paper</a></p><hr><h3 id=cookie-monster-efficient-on-device-budgeting-for-differentially-private-ad-measurement-systems>Cookie Monster: Efficient On-Device Budgeting for Differentially-Private Ad-Measurement Systems<a hidden class=anchor aria-hidden=true href=#cookie-monster-efficient-on-device-budgeting-for-differentially-private-ad-measurement-systems>#</a></h3><p><em>Pierre Tholoniat, Kelly Kostopoulou, Peter McNeely, Prabhpreet Singh Sodhi <em>et al.</em></em></p><p><strong>TL;DR</strong> — Cookie Monster implements practical on-device differential-privacy budget management for ad attribution, showing that strong privacy guarantees can be enforced locally without destroying ad-measurement utility.</p><p><strong>Why notable</strong> — Browser vendors are actively replacing third-party cookies with privacy-preserving attribution APIs; this paper provides rigorous analysis of the privacy-utility trade-off and offers deployable techniques relevant to both industry standards and future OS-level privacy primitives.</p><p><a href=https://doi.org/10.1145/3694715.3695965>→ Read paper</a></p><hr><h3 id=efficient-reproduction-of-fault-induced-failures-in-distributed-systems-with-feedback-driven-fault-injection>Efficient Reproduction of Fault-Induced Failures in Distributed Systems with Feedback-Driven Fault Injection<a hidden class=anchor aria-hidden=true href=#efficient-reproduction-of-fault-induced-failures-in-distributed-systems-with-feedback-driven-fault-injection>#</a></h3><p><em>Jia Pan, Haoze Wu, Tanakorn Leesatapornwongsa, Suman Nath <em>et al.</em></em></p><p><strong>TL;DR</strong> — A feedback-guided fault injection framework automatically reproduces complex distributed-system failures triggered by rare fault combinations, dramatically reducing the manual effort needed to diagnose and fix them.</p><p><strong>Why notable</strong> — Fault-induced failures in distributed systems are notoriously hard to reproduce; the paper’s closed-loop search strategy is a methodological advance for reliability testing and is likely to influence both academic research and industrial chaos-engineering tools.</p><p><a href=https://doi.org/10.1145/3694715.3695979>→ Read paper</a></p></div><footer class=post-footer><ul class=post-tags><li><a href=https://pub.sqrt.fr/vincent/publish-assistant/tags/operating-systems/>Operating-Systems</a></li><li><a href=https://pub.sqrt.fr/vincent/publish-assistant/tags/distributed-systems/>Distributed-Systems</a></li><li><a href=https://pub.sqrt.fr/vincent/publish-assistant/tags/storage/>Storage</a></li><li><a href=https://pub.sqrt.fr/vincent/publish-assistant/tags/cloud/>Cloud</a></li><li><a href=https://pub.sqrt.fr/vincent/publish-assistant/tags/formal-verification/>Formal-Verification</a></li><li><a href=https://pub.sqrt.fr/vincent/publish-assistant/tags/ml-systems/>Ml-Systems</a></li><li><a href=https://pub.sqrt.fr/vincent/publish-assistant/tags/security/>Security</a></li><li><a href=https://pub.sqrt.fr/vincent/publish-assistant/tags/serverless/>Serverless</a></li></ul><nav class=paginav><a class=prev href=https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/digests/middleware-2024/><span class=title>« Prev</span>
|
||
<span>Middleware 2024 Digest</span>
|
||
</a><a class=next href=https://pub.sqrt.fr/vincent/publish-assistant/cloud-edge/digests/socc-2024/><span class=title>Next »</span>
|
||
<span>SoCC 2024 Digest</span></a></nav></footer></article></main><footer class=footer><span>© 2026 <a href=https://pub.sqrt.fr/vincent/publish-assistant/>Publish Assistant</a></span> ·
|
||
<span>Powered by
|
||
<a href="https://gohugo.io/?utm_source=papermod" rel=noopener target=_blank>Hugo</a> &
|
||
<a href=https://github.com/adityatelange/hugo-PaperMod/ rel=noopener target=_blank>PaperMod</a></span></footer><a href=#top id=top-link class="top-link hidden" aria-label="go to top" title="Go to Top (Alt + G)" accesskey=g><svg viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="feather feather-chevrons-up"><polyline points="17 11 12 6 7 11"/><polyline points="17 18 12 13 7 18"/></svg>
|
||
</a><script>let menu=document.getElementById("menu");if(menu){const e=localStorage.getItem("menu-scroll-position");e&&(menu.scrollLeft=parseInt(e,10)),menu.onscroll=function(){localStorage.setItem("menu-scroll-position",menu.scrollLeft)}}document.querySelectorAll('a[href^="#"]').forEach(e=>{e.addEventListener("click",function(e){e.preventDefault();var t=this.getAttribute("href").substr(1);window.matchMedia("(prefers-reduced-motion: reduce)").matches?document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView():document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView({behavior:"smooth"}),t==="top"?history.replaceState(null,null," "):history.pushState(null,null,`#${t}`)})})</script><script>var toplink=document.getElementById("top-link");window.onscroll=function(){const e=window.innerHeight;document.body.scrollTop>e||document.documentElement.scrollTop>e?toplink.classList.remove("hidden"):toplink.classList.add("hidden")}</script><script>document.getElementById("theme-toggle").addEventListener("click",()=>{const e=document.querySelector("html");e.dataset.theme==="dark"?(e.dataset.theme="light",localStorage.setItem("pref-theme","light")):(e.dataset.theme="dark",localStorage.setItem("pref-theme","dark"))})</script></body></html> |