Spegion: Implicit and Non-Lexical Regions with Sized Allocations
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 \textsc{Spegion}, a language with implicit non-lexical regions, which provides these same memory safety guarantees for programs that go beyond using allocating memory in a stack-like manner in a more concise syntax. We are able to achieve this 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., \textbf{Sp}littable r\textbf{Egion}s, allowing fine grained control over memory allocation. Furthermore, \textsc{Spegion} permits \emph{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 \textsc{Spegion} and prove that it is sound with respect to a small-step operational semantics.
Mon 30 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:15 - 17:39 | Object-Oriented and Dynamic SystemsTechnical Papers at Auditorium M003 Chair(s): Sebastian Erdweg JGU Mainz | ||
16:15 21mTalk | Declarative Dynamic Object Reclassification Technical Papers Riccardo Sieve University of Oslo, Eduard Kamburjan IT University of Copenhagen, Ferruccio Damiani University of Turin, Einar Broch Johnsen University of Oslo | ||
16:36 21mTalk | In-memory Object Graph StoresRemote Technical Papers Aditya Thimmaiah The University of Texas at Austin, Zijian Yi The University of Texas at Austin, Joseph Kenis The University of Texas at Austin, Chris Rossbach University of Texas at Austin; Katana Graph, Milos Gligoric The University of Texas at Austin | ||
16:57 21mTalk | Spegion: Implicit and Non-Lexical Regions with Sized Allocations Technical Papers | ||
17:18 21mTalk | Type-safe and portable support for packed data Technical Papers |