Contractions Are Abstractions - Towards Effective Memory Management in ReML
summary
Work in progress extends ReML and the MLKit region/effect inference backend to let programmers write abstract region annotations that map to many concrete regions via contraction-based collapsing, so a single virtual region R can represent ~8–20 inferred regions in realistic data types. The system adds disjointness effect constraints to guarantee absence of allocation races, supports lead‑floating of intermediate compiler passes to free memory early, and targets a proof that dropping contractions and using the inferred regions still preserves memory safety and near‑optimal allocation.
AI-written summary · about
chapters (9)
- 0:00Effective memory management
- 2:11Region-based memory management
- 7:55Region inference and type systems
- 13:44Explicit region annotations
- 17:02Programming large systems
- 20:56Contractions for region unification
- 25:11Virtual regions and efficiency
- 28:05Ongoing work and future
- 31:53Q&A
related talks
34mModular Storage Mode Analysis
30mCompositional Deep Argument Flattening
18mParallelism in a Region Inference Context
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
27mRegions as Continuation Marks
11mEnabling Composition of Kernels and Compilers
51mRibbit with Memory Morphisms