一句话：提出 SL♢，用空间信用与 pointed-by 断言在含分配、GC 与并发的语言中控制堆空间消耗并证明其可靠性。
本文关注在存在动态内存分配和垃圾回收时，如何对程序的堆空间消耗进行推理与控制。作者提出分离逻辑 SL♢，其核心机制是空间信用：对象分配时消耗信用，仅当用户能证明一组对象已不可达、因而可被回收时，逻辑释放才产生信用。为证明不可达性，用户维护 pointed-by 断言，记录每个对象的直接前驱。验证语言 SpaceLang 具有可变状态、共享内存并发和代码指针。论文证明了 SL♢ 的可靠性，并给出若干简单示例说明其用法。
We present SL♢, a Separation Logic that allows controlling the heap space consumption of a program in the presence of dynamic memory allocation and garbage collection. A user of the logic works with space credits, a resource that is consumed when an object is allocated and produced when a group of objects is logically deallocated, that is, when the user is able to prove that it has become unreachable and therefore can be collected. To prove such a fact, the user maintains pointed-by assertions that record the immediate predecessors of every object. Our calculus, SpaceLang, has mutable state, shared-memory concurrency, and code pointers. We prove that SL♢ is sound and present several simple examples of its use.
@article{paperbot1576,
title = {A separation logic for heap space under garbage collection},
author = {Jean-Marie Madiot and François Pottier},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498672}
}