Rights / licenseIn Copyright - Non-Commercial Use Permitted
Object ownership is useful for many applications such as program verification, thread synchronization, and memory management. However, even lightweight ownership type systems impose considerable annotation overhead, which hampers their widespread application. This paper address this issue by presenting a tunable static type inference for Universe types. In contrast to classical type systems, ownership types have no single most general typing. Therefore, our inference is tunable: users can indicate a preference for certain typings by configuring heuristics through weights. A particularly effective way of tuning the static inference is to obtain these weights automatically through runtime ownership inference. We present how the constraints of the Universe type system can be encoded as a boolean satisfiability (SAT) problem, how the runtime ownership inference produces weights from program executions, and how a weightedMax-SAT solver finds a correct Universe typing that optimizes the weights. Our implementation provides the static and runtime inference engines, as well as a visualization tool Show more
Journal / seriesTechnical report / Swiss Federal Institute of Technology Zürich, Department of Computer Science
PublisherETH, Department of Computer Science
SubjectINFERENCE RULES (MATHEMATICAL LOGIC); THEORIE DER PROGRAMMIERUNG; INFERENZREGELN (MATHEMATISCHE LOGIK); THEORY OF PROGRAMMING
Organisational unit02150 - Departement Informatik / Department of Computer Science
NotesTechnical Reports D-INFK.
MoreShow all metadata