Skip to main content
SpringerLink
Log in

Tunable Static Inference for Generic Universe Types

  • Conference paper
ECOOP 2011 – Object-Oriented Programming (ECOOP 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6813))

Included in the following conference series:

Abstract

Object ownership is useful for many applications, including program verification, thread synchronization, and memory management. However, the annotation overhead of ownership type systems hampers their widespread application. This paper addresses this issue by presenting a tunable static type inference for Generic Universe Types. In contrast to classical type systems, ownership types have no single most general typing. Our inference chooses among the legal typings via heuristics. Our inference is tunable: users can indicate a preference for certain typings by adjusting the heuristics or by supplying partial annotations for the program. We present how the constraints of Generic Universe Types can be encoded as a boolean satisfiability (SAT) problem and how a weighted Max-SAT solver finds a correct Universe typing that optimizes the weights. We implemented the static inference tool, applied our inference tool to four real-world applications, and inferred interesting ownership structures.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Agarwal, R., Stoller, S.D.: Type Inference for Parameterized Race-Free Java. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 149–160. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Vetta, A. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 1–25. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Aldrich, J., Kostadinov, V., Chambers, C.: Alias annotations for program understanding. In: OOPSLA, pp. 311–330 (2002)

    Google Scholar 

  4. Baker, H.G.: Unify and conquer (garbage, updating, aliasing) in functional languages. In: LISP and functional programming (LFP), pp. 218–226 (1990)

    Google Scholar 

  5. Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7, 59–64 (2010), http://www.sat4j.org/

    Google Scholar 

  6. Boyapati, C.: SafeJava: A Unified Type System for Safe Programming. PhD thesis, MIT (2004)

    Google Scholar 

  7. Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA, pp. 211–230 (2002)

    Google Scholar 

  8. Cameron, N., Drossopoulou, S., Noble, J., Smith, M.: Multiple ownership. In: OOPSLA, pp. 441–460 (2007)

    Google Scholar 

  9. Chin, B., Markstrum, S., Millstein, T., Palsberg, J.: Inference of user-defined type qualifiers and qualifier rules. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 264–278. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Clarke, D., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA (1998)

    Google Scholar 

  11. Clarke, D., Wrigstad, T.: External uniqueness is unique enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, Springer, Heidelberg (2003)

    Google Scholar 

  12. Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL, pp. 207–212 (1982)

    Google Scholar 

  13. Dietl, W.: Universe Types: Topology, Encapsulation, Genericity, and Tools. PhD thesis, Department of Computer Science, ETH Zurich (2009)

    Google Scholar 

  14. Dietl, W., Drossopoulou, S., Müller, P.: Generic Universe Types. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 28–53. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT) 4(8), 5–32 (2005)

    Article  Google Scholar 

  16. Ernst, M.-D.: Type annotations specification (JSR 308) (September 12, 2008), http://types.cs.washington.edu/jsr308/

  17. Ernst, M.D., Millstein, T.D., Weld, D.S.: Automatic SAT-compilation of planning problems. In: IJCAI, pp. 1169–1176 (1997)

    Google Scholar 

  18. Flanagan, C., Freund, S.N.: Type inference against races. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 116–132. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Greenfieldboyce, D., Foster, J.S.: Type qualifier inference for Java. In: OOPSLA, pp. 321–336 (2007)

    Google Scholar 

  20. Grothoff, C., Palsberg, J., Vitek, J.: Encapsulating objects with confined types. In: OOPSLA, pp. 241–253 (2001)

    Google Scholar 

  21. Guo, P.J., Perkins, J.H., McCamant, S., Ernst, M.D.: Dynamic inference of abstract types. In: ISSTA, pp. 255–265 (2006)

    Google Scholar 

  22. Kieżun, A., Ernst, M.D., Tip, F., Fuhrer, R.M.: Refactoring for parameterizing Java classes. In: ICSE, pp. 437–446 (2007)

    Google Scholar 

  23. Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML reference manual (2008), http://www.jmlspecs.org/

  24. Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Vetta, A. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  25. Liu, Y.D., Smith, S.: Pedigree types. In: IWACO (2008)

    Google Scholar 

  26. Ma, K., Foster, J.S.: Inferring aliasing and encapsulation properties for Java. In: OOPSLA, pp. 423–440 (2007)

    Google Scholar 

  27. Max-SAT evaluation input and output format (February 2010), http://www.maxsat.udl.cat/10/requirements/

  28. Milanova, A.: Static inference of Universe types. In: IWACO (2008)

    Google Scholar 

  29. Milanova, A., Liu, Y.: Practical static ownership inference. Technical Report RPI/DCS-09-04, Rensselaer Polytechnic Institute (March 2010)

    Google Scholar 

  30. Milanova, A., Vitek, J.: Static dominance inference. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 211–227. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  31. Moelius, S.E., Souter, A.L.: An object ownership inference algorithm and its application. In: Mid-Atlantic Student Workshop on Programming Languages and Systems (2004)

    Google Scholar 

  32. Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  33. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming 62, 253–286 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  34. Müller, P., Rudich, A.: Ownership transfer in Universe Types. In: OOPSLA, pp. 461–478 (2007)

    Google Scholar 

  35. O’Callahan, R., Jackson, D.: Lackwit: A program understanding tool based on type inference. In: ICSE, pp. 338–348 (1997)

    Google Scholar 

  36. Palsberg, J.: Type-based analysis and applications. In: PASTE, pp. 20–27 (2001)

    Google Scholar 

  37. Papi, M.M., Ali, M., Correa Jr., T.L., Perkins, J.H., Ernst, M.D.: Practical pluggable types for Java. In: ISSTA, pp. 201–212 (2008)

    Google Scholar 

  38. Poetzsch-Heffter, A., Geilmann, K., Schäfer, J.: Infering ownership types for encapsulated object-oriented program components. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. LNCS, vol. 4444, pp. 120–144. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  39. Potanin, A., Noble, J., Clarke, D., Biddle, R.: Generic ownership for generic Java. In: OOPSLA, pp. 311–324 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Washington, USA

    Werner Dietl & Michael D. Ernst

  2. ETH Zurich, Switzerland

    Peter Müller

Authors
  1. Werner Dietl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael D. Ernst
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Software Technology group, Technische Universität, Darmstadt, Germany

    Mira Mezini

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dietl, W., Ernst, M.D., Müller, P. (2011). Tunable Static Inference for Generic Universe Types. In: Mezini, M. (eds) ECOOP 2011 – Object-Oriented Programming. ECOOP 2011. Lecture Notes in Computer Science, vol 6813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22655-7_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22655-7_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22654-0

  • Online ISBN: 978-3-642-22655-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation