Spegion: Implicit and Non-Lexical Regions with Sized Allocations

TL;DR

Spegion introduces an implicit, effect-based region management system with sized allocations, enabling safe, fine-grained memory control without explicit annotations or substructural types.

Contribution

It presents Spegion, a novel language that achieves safe, non-lexical region management with a concise syntax and effect system, avoiding complex type systems.

Findings

Type safety is proven for Spegion's system.

Supports fine-grained, sized region allocations.

Enables implicit, non-lexical memory management.

Abstract

Region based memory management is a powerful tool designed with the goal of ensuring memory safety statically. The region calculus of Tofte and Talpin is a well known example of a region based system, which uses regions to manage memory in a stack-like fashion. However, the region calculus is lexically scoped and requires explicit annotation of memory regions, which can be cumbersome for the programmer. Other systems have addressed non-lexical regions, but these approaches typically require the use of a substructural type system to track the lifetimes of regions. We present Spegion, a language with implicit non-lexical regions, which provides these same memory safety guarantees for programs that go beyond using memory allocation in a stack-like manner. We are able to achieve this with a concise syntax, and without the use of substructural types, relying instead on an effect system to enforce constraints on region allocation and deallocation. These regions may be divided into sub-regions, i.e., Splittable rEgions, allowing fine grained control over memory allocation. Furthermore, Spegion permits sized allocations, where each value has an associated size which is used to ensure that regions are not over-allocated into. We present a type system for Spegion and prove it is type safe with respect to a small-step operational semantics.