Yarrow: Reconciling Effects Handlers and Region-Based Memory Management
Programming Languages
Summary
The authors introduce Yarrow, a new programming language that combines algebraic effects with region-based memory management, which is tricky because these features can conflict. To handle this, they created Yarrow Logic (YL), a system that helps programmers reason safely about memory regions even when effects cause complex control flow. They proved YL is sound and demonstrated its use with examples like checkpointing and asynchronous tasks, showing efficient memory use without relying on garbage collection. Their work is formally verified using a proof framework called Iris within the Rocq Prover.
Authors
Anders Alnor Mathiasen, Amin Timany, Lars Birkedal
Abstract
We present a new ML-like programming language Yarrow with algebraic effects and region-based memory management. Reconciling these programming language features into one language is challenging: the non-local control flow of algebraic effects break the stack discipline of function calls and returns that region-based memory management relies on, and multi-shot effect handlers break the invariant that regions can be exited at most once. We present a program logic, called Yarrow Logic (YL), that supports safe and modular reasoning about regions in the presence of one-shot and multi-shot effect handlers. We prove the logic sound w.r.t. the operational semantics of Yarrow which is inspired by the runtime of OCaml but refined for regions. We use YL to prove correctness of a number of case studies with algebraic effects, including checkpointing, asynchronous computation and a LIFO data structure implementation. Since all memory locations used in these case studies are allocated in regions, these case studies avoid using the less efficient garbage collected heap memory. We have formalized Yarrow's operational semantics, the Yarrow program logic, and all our case studies using the Iris separation logic framework on top of the Rocq Prover.