
doi: 10.1145/3498672
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.
Separation logic, Program verification, CCS Concepts: • Theory of computation → Separation logic, Tracing garbage collection, Live data, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Separation logic, Program verification, CCS Concepts: • Theory of computation → Separation logic, Tracing garbage collection, Live data, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 8 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
