Effect Types and Region-Based Memory Management
Fritz Henglein, Henning Makholm, Henning Niss · The MIT Press eBooks · 2004
Type-based program analysis is program analysis based on the concepts, theories and technologies developed for type systems and employed in the definition of programming languages. It is a vast field of research with numerous applications and considerable practical impact. Applications include strictness analysis, data representation analysis, binding-time analysis, soft typing (also called dynamic typing inference), boxing analysis, pointer aliasing, value flow analysis (and all its applications), region-based memory management, communication topology analysis, Year 2000 type analysis, cryptographic protocol verification, locking, race detection, and others; see Palsberg (2001) for an overview of additional applications. This chapter presents type-based program analysis based on type and effect systems (or effect type systems) and illustrates their application in region-based memory management, which is the chapter’s ultimate focus. Classical type systems express properties of values, not the computations leading to those values. Effect types describe all important effects of computation, not just their results. Region-based memory management refers to programming where heap data is allocated in individually managed regions that are explicitly allocated and deallocated. As we shall see, state-of-the-art region-based memory management employs effect type systems to ensure region safety, which guarantees that no accesses to unallocated or deallocated regions occur at run time.