Safe Transferable Regions
There is an increasing interest in alternative memory management schemes that seek to the combine the convenience of garbage collection and the performance of manual memory management in a single language framework. Unfortunately, ensuring safety in presence of manual memory management remains as great a challenge as ever. In this paper, we present a C#-like object-oriented language called Broom that uses a combination of region type system and lightweight runtime checks to enforce safety in presence of user-managed memory regions called transferable regions. Unsafe transferable regions have been previously used to contain the latency due to unbounded GC pauses. Our approach shows that it is possible to restore safety without compromising on the benefits of transferable regions. We prove the type safety of Broom in a formal framework that includes its C#-inspired features, such as higher-order functions and generics. We complement our type system with a type inference algorithm, which eliminates the need for programmers to write region annotations on types. The inference algorithm has been proven sound and relatively complete. We describe a prototype implementation of the inference algorithm, and our experience of using it to enforce memory safety in dataflow programs.
Thu 19 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:15 | LanguagesECOOP Research Papers at Zurich II Chair(s): Yu David Liu State University of New York, Binghamton | ||
16:00 25mResearch paper | Typed First-Class Traits ECOOP Research Papers DOI | ||
16:25 25mResearch paper | CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs ECOOP Research Papers Stefan Krüger University of Paderborn, Johannes Späth Fraunhofer IEM, Karim Ali University of Alberta, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM, Mira Mezini TU Darmstadt DOI | ||
16:50 25mResearch paper | Safe Transferable Regions ECOOP Research Papers DOI |