Garbage-Collection Safety for Region-Based Type-Polymorphic Programs
Region inference offers a mechanism to reduce (and sometimes entirely remove) the need for reference-tracing garbage collection by inferring where to insert allocation and deallocation instructions in a program at compile time. When the mechanism is combined with techniques for reference-tracing garbage collection, which is helpful in general to support programs with very dynamic memory behaviours, it turns out that region-inference is complementary to adding generations to a reference-tracing collector. However, region-inference and the associated region-representation analyses that make such a memory management strategy perform well in practice are complex, both from a theoretical point-of-view and from an implementation point-of-view.
In this paper, we demonstrate a soundness problem with existing theoretical developments, which have to do with ensuring that, even for higher-order polymorphic programs, no dangling-pointers appear during a reference-tracing collection. This problem has materialised as a practical soundness problem in a real implementation based on region inference. As a solution, we present a modified, yet simple, region type-system that captures garbage-collection effects, even for polymorphic higher-order code, and outline how region inference and region-representation analyses are adapted to the new type system. The new type system allows for associating simpler region type-schemes with functions, compared to original work, makes it possible to combine region-based memory management with partly tag-free reference-tracing (and generational) garbage-collection, and repairs previously derived work that is based on the erroneous published results.
Wed 21 JunDisplayed time zone: Eastern Time (US & Canada) change
13:40 - 15:40 | |||
13:40 20mTalk | Extensible Metatheory Mechanization via Family PolymorphismDistinguished Paper PLDI Research Papers DOI | ||
14:00 20mTalk | Defunctionalization with Dependent Types PLDI Research Papers DOI Pre-print | ||
14:20 20mTalk | Garbage-Collection Safety for Region-Based Type-Polymorphic Programs PLDI Research Papers Martin Elsman University of Copenhagen, Denmark DOI | ||
14:40 20mTalk | Flux: Liquid Types for Rust PLDI Research Papers Nico Lehmann University of California, San Diego, Adam Geller Computer Science, University of British Columbia, Niki Vazou IMDEA Software Institute, Ranjit Jhala University of California at San Diego DOI | ||
15:00 20mTalk | Leveraging Rust Types for Program Synthesis PLDI Research Papers Jonas Fiala ETH Zürich, Shachar Itzhaky Technion, Peter Müller ETH Zurich, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore DOI Pre-print | ||
15:20 20mTalk | Parameterized Algebraic Protocols PLDI Research Papers Andreia Mordido LASIGE, University of Lisbon, Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos LASIGE, University of Lisbon DOI |