Skip to main content
SpringerLink
Log in

A Type System for Reachability and Acyclicity

  • Conference paper
ECOOP 2005 - Object-Oriented Programming (ECOOP 2005)

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

Included in the following conference series:

Abstract

The desire for compile-time knowledge about the structure of heap contexts is currently increasing in many areas. However, approaches using whole program analysis are too weak in terms of both efficiency and accuracy. This paper presents a novel type system that enforces programmer-defined constraints on reachability via references or pointers, and restricts reference cycles to be within definable parts of the heap. Such constraints can be useful for program understanding and reasoning about effects and invariants, for information flow security, and for run-time optimizations and memory management.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 1–25. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Almeida, P.S.: Balloon types: Controlling sharing of state in data types. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 32–59. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  3. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. In: Eisenbach, S., Leavens, G.T., Müller, P., Poetzsch-Heffter, A., Poll, E. (eds.) Formal Techniques for Java-like Programs (FTfJP) (July 2003) Published as Technical Report 408 from ETH Zurich

    Google Scholar 

  4. Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (November 2002)

    Google Scholar 

  5. Clarke, D.: Object Ownership and Containment. PhD thesis, School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia (2001)

    Google Scholar 

  6. Clarke, D.G., Noble, J., Potter, J.M.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, p. 53. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pp. 48–64. ACM Press, New York (1998)

    Chapter  Google Scholar 

  8. Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  9. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)

    Article  MATH  Google Scholar 

  10. Ghiya, R., Hendren, L.J.: Is it a tree, a dag, or a cyclic graph? a shape analysis for heap-directed pointers in c. In: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 1–15. ACM Press, New York (1996)

    Chapter  Google Scholar 

  11. Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Region-based memory management in cyclone. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 282–293. ACM Press, New York (2002)

    Chapter  Google Scholar 

  12. Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL, pp. 310–323 (2005)

    Google Scholar 

  13. Heintze, N., Riecke, J.G.: The SLam calculus: programming with secrecy and integrity. In: Conference record of POPL ’98: the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, January 19–21, pp. 365–377. ACM Press, New York (1998)

    Chapter  Google Scholar 

  14. Hendren, L.J., Hummel, J., Nicolau, A.: Abstractions for recursive pointer data structures: Improving the analysis and transformation of imperative programs. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI), vol. 27, pp. 249–260. ACM Press, New York (1992)

    Google Scholar 

  15. Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp. 54–61. ACM Press, New York (2001)

    Chapter  Google Scholar 

  16. Hogg, J.: Islands: aliasing protection in object-oriented languages. In: Conference proceedings on Object-oriented programming systems, languages, and applications, pp. 271–285. ACM Press, New York (1991)

    Chapter  Google Scholar 

  17. Hummel, J., Hendren, L.J., Nicolau, A.: A language for conveying the aliasing properties of dynamic, pointer-based data structures. In: 8th International Parallel Processing Symposium, Cancun, Mexico, pp. 208–216 (1994)

    Google Scholar 

  18. Igarashi, A., Viroli, M.: On variance-based subtyping for parametric types. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 441–469. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Müller, P., Poetzsch-Heffter, A.: Universes: A type system for controlling representation exposure. Programming Languages and Fundamentals of Programming (1999)

    Google Scholar 

  20. Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Symposium on Principles of Programming Languages, pp. 228–241 (1999)

    Google Scholar 

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

    Chapter  Google Scholar 

  22. Tofte, M., Talpin, J.-P.: Implementation of the typed call-by-value lambda-calculus using a stack of regions. In: Symposium on Principles of Programming Languages, pp. 188–201 (1994)

    Google Scholar 

  23. Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation (1997)

    Google Scholar 

  24. Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(3), 167–187 (1996)

    Google Scholar 

  25. Volpano, D.M., Smith, G.: A type-based approach to program security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 607–621. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  26. Wilhelm, R., Sagiv, S., Reps, T.W.: Shape analysis. In: Computational Complexity, pp. 1–17 (2000)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Languages and Compilers Group, School of Computer Science and Engineering, The University of New South Wales, Sydney, 2052, Australia

    Yi Lu & John Potter

Authors
  1. Yi Lu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Potter
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Portland State University,  

    Andrew P. Black

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lu, Y., Potter, J. (2005). A Type System for Reachability and Acyclicity. In: Black, A.P. (eds) ECOOP 2005 - Object-Oriented Programming. ECOOP 2005. Lecture Notes in Computer Science, vol 3586. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11531142_21

Download citation

  • DOI: https://doi.org/10.1007/11531142_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-27992-1

  • Online ISBN: 978-3-540-31725-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation