SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Sat 18 Oct 2025 15:00 - 15:15 at Orchid Small - Proofs Chair(s): Peter Thiemann

Although existing garbage collectors (GCs) perform extremely well on typical programs, there still exist pathological programs for which modern GCs significantly degrade performance. This observation begs the question: might there exist a ‘holy grail’ GC algorithm, as yet undiscovered, guaranteeing both constant-length pause times and that memory is collected promptly upon becoming unreachable? For decades, researchers have understood that such a GC is not always possible, i.e., some pathological behavior is unavoidable when the program can make heap cycles and operates near the memory limit, regardless of the GC algorithm used. However, this understanding has until now been only informal, lacking a rigorous formal proof.

This paper complements that informal understanding with a rigorous proof, showing with mathematical certainty that every GC algorithm that can implement a realistic mutator-observer interface has some patholog- ical program that forces it to either introduce a long GC pause into program execution or reject an allocation even though there is available space. Hence, language designers must either accept these pathological scenarios and design heuristic approaches that minimize their impact (e.g., generational collection), or restrict programs and environments to a strict subset of the behaviors allowed by our mutator-observer–style interface (e.g., by enforcing a type system that disallows cycles or overprovisioning memory).

We do not expect this paper to have any effect on garbage collection practice. Instead, it provides the first mathematically rigorous answers to these interesting questions about the limits of garbage collection. We do so via rigorous reductions between GC and the dynamic graph connectivity problem in complexity theory, so future algorithms and lower bounds from either community transfer to the other via our reductions.

We end by describing how to adapt techniques from the graph data structures community to build a garbage collector making worst-case guarantees that improve performance on our motivating, pathologically memory-constrained scenarios, but in practice find too much overhead to recommend for typical use.

Sat 18 Oct

Displayed time zone: Perth change

13:45 - 15:30
ProofsOOPSLA at Orchid Small
Chair(s): Peter Thiemann University of Freiburg
13:45
15m
Talk
Adaptive Shielding via Parametric Safety Proofs
OOPSLA
Yao Feng Tsinghua University, Jun Zhu Nankai University, André Platzer Karlsruhe Institute of Technology (KIT), Jonathan Laurent Carnegie Mellon University / Karlsruhe Institute of Technology
14:00
15m
Talk
Certified Decision Procedures for Width-Independent Bitvector Predicates
OOPSLA
Siddharth Bhat University of Cambridge, Leo Stefanesco University of Cambridge, Chris Hughes Independent Researcher, Tobias Grosser University of Cambridge
14:15
15m
Talk
Checking $\delta$-Satisfiability of Reals with Integrals
OOPSLA
Cody Rivera University of Illinois, Urbana-Champaign, Bishnu Bhusal University of Missouri, Rohit Chadha University of Missouri, A. Prasad Sistla University of Illinois at Chicago, Mahesh Viswanathan University of Illinois at Urbana-Champaign
14:30
15m
Talk
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
OOPSLA
John C. Kolesar Yale University, Shan Ali Yale University, Timos Antonopoulos Yale University, Ruzica Piskac Yale University
14:45
15m
Talk
Incremental Certified Programming
OOPSLA
Tomás Diaz University of Chile, Kenji Maillard Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile
15:00
15m
Talk
Pathological Cases for a Class of Reachability-Based Garbage Collectors
OOPSLA
Matthew Sotoudeh Stanford University
Link to publication
15:15
15m
Talk
SafeTree: Expressive Tree Policies for Microservices
OOPSLA
Karuna Grewal Cornell University, Brighten Godfrey UIUC and Broadcom, Justin Hsu Cornell University