Light
code header

Floorplan: Spatial Layout in Memory Management Systems

Samuel Z. Guyer and Karl Cronburg — GPCE 2019, co-located with SPLASH, Athens, Greece.

Memory managers — garbage collectors in particular — need precise control over how objects are laid out in memory. Generational collectors divide the heap into regions; compacting collectors move objects; region-based allocators carve up contiguous address ranges. All of this layout logic is currently embedded implicitly in the allocator code, invisible to static analysis and difficult to reason about.

Floorplan is a domain-specific language for making that layout explicit. A Floorplan specification describes a memory manager's spatial structure using a small set of layout operators — contiguous regions, disjoint regions, partitioned spaces — that compose into a full description of the heap's organization. The goal is to make the spatial assumptions underlying a memory manager's correctness conditions checkable at the language level rather than discovered through runtime failures.

The presentation covers Floorplan's layout operators, the motivating cases from real garbage collectors, and the path from specification to verified implementation.

Materials