Yarrow：调和效应处理程序与基于区域的内存管理
Yarrow: Reconciling Effect Handlers and Region-Based Memory Management
浏览论文内容
中文总结 AI 辅助
研究提出新语言 Yarrow 融合代数效应与基于区域的内存管理，针对二者整合难题提出 Yarrow 逻辑（YL），证明其可靠性，用 YL 证明含代数效应案例研究正确性，避免使用低效堆内存，并用 Iris 分离逻辑框架形式化相关内容。
中文摘要 AI 辅助
我们提出了一种新的类似 ML 的编程语言 Yarrow，它兼具代数效应和基于区域的内存管理。将这些编程语言特性整合到一种语言中具有挑战性：代数效应的非局部控制流打破了基于区域的内存管理所依赖的函数调用和返回的栈规则，多触发效应处理程序打破了区域最多只能退出一次的不变性。我们提出了一种名为 Yarrow 逻辑（YL）的程序逻辑，它支持在存在单触发和多触发效应处理程序的情况下对区域进行安全且模块化的推理。我们证明了该逻辑相对于 Yarrow 的操作语义是可靠的，Yarrow 的操作语义受 OCaml 运行时启发但针对区域进行了优化。我们使用 YL 证明了一些具有代数效应的案例研究的正确性，包括检查点、异步计算和一个后进先出数据结构实现。由于这些案例研究中使用的所有内存位置都在区域中分配，因此避免了使用效率较低的垃圾回收堆内存。我们使用 Rocq 证明器之上的 Iris 分离逻辑框架对 Yarrow 的操作语义、Yarrow 程序逻辑以及所有案例研究进行了形式化。
英文摘要
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.
