
Open access
Date
2009Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
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
Permanent link
https://doi.org/10.3929/ethz-a-006843105Publication status
publishedJournal / series
Technical Report / ETH Zurich, Department of Computer ScienceVolume
Publisher
ETH, Department of Computer ScienceSubject
INFERENCE RULES (MATHEMATICAL LOGIC); THEORIE DER PROGRAMMIERUNG; INFERENZREGELN (MATHEMATISCHE LOGIK); THEORY OF PROGRAMMINGOrganisational unit
02150 - Dep. Informatik / Dep. of Computer Science
Notes
Technical Reports D-INFK.More
Show all metadata
ETH Bibliography
yes
Altmetrics