Aliasing is crucial for supporting useful implementation patterns, but it makes reasoning about programs difficult. To deal with this problem, numerous type-based aliasing control mechanisms have been proposed, expressing properties such as uniqueness. Uniqueness, however, is black-and-white: either a reference is unique or it can be arbitrarily aliased; and global: excluding aliases throughout the entire system, making code brittle to changing requirements. Disjointness domains, a new approach to alias control, address this problem by enabling more graduations between uniqueness and arbitrary reference sharing. They allow expressing aliasing constraints local to a certain set of variables (either stack variables or fields) for instance that no aliasing occurs between variables within some set of variables but between such sets or the opposite, that aliasing occurs within that set but not between different sets. A hierarchy of disjointness domains controls the flow of references through a program, helping the programmer reason about disjointness and enforce local alias invariants. The resulting system supports fine-grained control of aliasing between both variables and objects, making aliasing explicit to programmers, compilers, and tooling. This paper presents a formal account of disjointness domains along with examples. Disjointness domains provide novel means of expressing may-alias kinds of constraints, which may prove useful in compiler optimisation and verification.
Slides (pdf) (disjointness_domains.pdf) | 4.19MiB |
Slides (keynote) (disjointness_domains.key) | 3.43MiB |
Fri 30 OctDisplayed time zone: Eastern Time (US & Canada) change
15:30 - 17:00 | |||
15:30 22mTalk | A Co-Contextual Formulation of Type Rules and its Application to Incremental Type Checking OOPSLA Sebastian Erdweg TU Darmstadt, Germany, Oliver Bračevac TU Darmstadt, Edlira Kuci TU Darmstadt, Germany, Matthias Krebs TU Darmstadt, Germany, Mira Mezini TU Darmstadt Link to publication Pre-print | ||
15:52 22mTalk | Disjointness Domains for Fine-Grained Aliasing OOPSLA Stephan Brandauer Uppsala University, Dave Clarke Uppsala University, Sweden and KU Leuven, Belgium, Tobias Wrigstad Uppsala University Link to publication File Attached | ||
16:15 22mTalk | The Chemical Approach to Typestate-Oriented Programming OOPSLA DOI | ||
16:37 22mTalk | Customizable Gradual Polymorphic Effects for Scala OOPSLA DOI |