---

Download: PDF.

“Tunable Universe Type Inference” by W. Dietl, M. D. Ernst, and P. Müller, Department of Computer Science. ETH Zurich technical report 659, Dec. 2009. Updated March 2010.

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 weighted Max-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.

Keywords: Universe types, ownership inference, tunable static and runtime approach

Download: PDF.

BibTeX entry:

@techreport{DietlErnstMueller09,
   author = {W. Dietl and M. D. Ernst and P. M{"u}ller},
   title = {{Tunable Universe Type Inference}},
   institution = {Department of Computer Science, ETH Zurich},
   month = dec,
   note = {Updated March 2010}
}

---

---