Functional programming languages support non-destructive updates via structural sharing, creating a fundamental tradeoff in memory representation: pointer-based heaps preserve sharing but degrade layout locality, while serialized heaps prioritize locality at the cost of duplication. Gibbon addresses this tradeoff by using adaptive serialization: as the program updates its heap, the memory manager improves locality through serialization, falling back to indirection where sharing is unavoidable.

In this work, we formalize key parts of Gibbon’s memory model, including the statics and dynamics of adaptive serialization. We then present a unified, type-directed memory model with two realizations: location-addressable memory (LAM) for local execution and content-addressable memory (CAM) for persistence and distributed deduplication. The key abstraction in both models is a notion of explicit boundary datatypes mediating between sharing and serialization. In LAM, boundaries facilitate adaptive serialization and enable our soundness proofs. In CAM, the same boundaries enable an efficient chunking policy, whereby candidate chunk points are selected via rolling-hash cuts. We establish efficiency via a static bound on the number of tokens between consecutive boundaries, bounding reserialization costs.

We work in the purely functional setting, where structural sharing is observationally transparent and content-addressed identity is well defined. We formalize both models with operational semantics and prove soundness with respect to ordinary functional values. For CAM, we prove a locality theorem: the work required for an update scales with the depth of the modified path rather than the size of the value. Consequently, large persistent values can be updated incrementally, with unchanged substructures shared automatically across versions and across machines. Together, these results show that a single boundary discipline can unify local structural sharing and distributed deduplication within one type-theoretic foundation.

Tue 25 Aug

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 15:00
Memory Models, Garbage Collection, and ConcurrencyICFP Papers at IP126 Auditorium
Chair(s): Mae Milano Princeton University
13:30
18m
Talk
Tail Modulo Async-AwaitRemote
ICFP Papers
Emma Nardino École Normale Supérieure de Lyon / LIP, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Gabriel Radanne Inria, Yannick Zakowski Inria
DOI Pre-print File Attached
13:48
18m
Talk
Set-Theoretic Types for Erlang in PracticeRemote
ICFP Papers
Albert Schimpf University of Kaiserslautern-Landau, Annette Bieniusa RPTU Kaiserslautern-Landau
DOI
14:06
18m
Talk
Mode Crossing
ICFP Papers
Benjamin Peters MPI-SWS, Jules Jacobs Jane Street, Diana Kalinichenko Jane Street, Liam Stevenson Jane Street, Aspen Smith Jane Street, Derek Dreyer MPI-SWS, Richard A. Eisenberg Jane Street
DOI
14:24
18m
Talk
A Separation Logic for Parallel Time Complexity with Work and Span Credits
ICFP Papers
Alexandre Moine New York University, Sam Westrick New York University, Joseph Tassarotti New York University
DOI Pre-print
14:42
18m
Talk
LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
ICFP Papers
Michael Rainey Carnegie Mellon University, Michael Borkowski Purdue University, Michael Vollmer University of Kent, Chaitanya S. Koparkar Indiana University, Mikah Kainen Purdue University, Vidush Singhal Purdue University
DOI Pre-print