More Web Proxy on the site http://driver.im/

Article

A type system for reachability and acyclicity

Authors:

John PotterAuthors Info & Claims

ECOOP'05: Proceedings of the 19th European conference on Object-Oriented Programming

Pages 479 - 503

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

Published: 25 July 2005 Publication History

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.

References

[1]

J. Aldrich and C. Chambers. Ownership domains: Separating aliasing policy from mechanism. In European Conference for Object-Oriented Programming (ECOOP), July 2004.

[2]

P. S. Almeida. Balloon types: Controlling sharing of state in data types. Lecture Notes in Computer Science, 1241:32-59, 1997.

[3]

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

[4]

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

Digital Library

[5]

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

Digital Library

[6]

D. G. Clarke, J. Noble, and J. M. Potter. Simple ownership types for object containment. In European Conference for Object-Oriented Programming (ECOOP), 2001.

Digital Library

[7]

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

Digital Library

[8]

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

Digital Library

[9]

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

Digital Library

[10]

R. Ghiya and L. J. Hendren. 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, pages 1-15. ACM Press, 1996.

Digital Library

[11]

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

Digital Library

[12]

B. Hackett and R. Rugina. Region-based shape analysis with tracked locations. In POPL, pages 310-323, 2005.

Digital Library

[13]

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

Digital Library

[14]

L. J. Hendren, J. Hummel, and A. Nicolau. 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), volume 27, pages 249-260, New York, NY, 1992. ACM Press.

Digital Library

[15]

M. Hind. 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, pages 54-61. ACM Press, 2001.

Digital Library

[16]

J. Hogg. Islands: aliasing protection in object-oriented languages. In Conference proceedings on Object-oriented programming systems, languages, and applications, pages 271-285. ACM Press, 1991.

Digital Library

[17]

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

Digital Library

[18]

A. Igarashi and M. Viroli. On variance-based subtyping for parametric types. In Proceedings of the 16th European Conference on Object-Oriented Programming, pages 441-469. Springer-Verlag, 2002.

Digital Library

[19]

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

[20]

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

Digital Library

[21]

K. Rustan, M. Leino, and P. Müller. Object invariants in dynamic contexts. In European Conference for Object-Oriented Programming (ECOOP), 2004.

[22]

M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value lambda-calculus using a stack of regions. In Symposium on Principles of Programming Languages, pages 188-201, 1994.

Digital Library

[23]

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

Digital Library

[24]

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

Digital Library

[25]

D. M. Volpano and G. Smith. A type-based approach to program security. In TAPSOFT, pages 607-621, 1997.

Digital Library

[26]

R. Wilhelm, S. Sagiv, and T. W. Reps. Shape analysis. In Computational Complexity, pages 1-17, 2000.

Digital Library

Cited By

Bao YWei GBračevac OJiang YHe QRompf T(2021)Reachability types: tracking aliasing and separation in higher-order functional programsProceedings of the ACM on Programming Languages10.1145/34855165:OOPSLA(1-32)Online publication date: 20-Oct-2021
https://dl.acm.org/doi/10.1145/3485516
Clarke DÖstlund JSergey IWrigstad T(2013)Ownership typesAliasing in Object-Oriented Programming10.5555/2554511.2554516(15-58)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554516
Dietl WDrossopoulou SMüller P(2012)Separating ownership topology and encapsulation with generic universe typesACM Transactions on Programming Languages and Systems10.1145/2049706.204970933:6(1-62)Online publication date: 3-Jan-2012
https://dl.acm.org/doi/10.1145/2049706.2049709
Show More Cited By

A type system for reachability and acyclicity
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
2. Theory of computation
  1. Semantics and reasoning

Recommendations

Reachability-based acyclicity analysis by Abstract Interpretation

In programming languages with dynamic use of memory, such as Java, knowing that a reference variable x points to an acyclic data structure is valuable for the analysis of termination and resource usage (e.g., execution time or memory consumption). For ...
FlowCFL: generalized type-based reachability analysis: graph reduction and equivalence of CFL-based and type-based reachability

Reachability analysis is a fundamental program analysis with a wide variety of applications. We present FlowCFL, a type-based reachability analysis that accounts for mutable heap data. The underlying semantics of FlowCFL is Context-Free-Language (CFL)-...
Context-sensitive data-dependence analysis via linear conjunctive language reachability
POPL '17

Many program analysis problems can be formulated as graph reachability problems. In the literature, context-free language (CFL) reachability has been the most popular formulation and can be computed in subcubic time. The context-sensitive data-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ECOOP'05: Proceedings of the 19th European conference on Object-Oriented Programming

July 2005

630 pages

ISBN:354027992X

Editor:
Andrew P. Black
Department of Computer Science, Portland State University

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 25 July 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bao YWei GBračevac OJiang YHe QRompf T(2021)Reachability types: tracking aliasing and separation in higher-order functional programsProceedings of the ACM on Programming Languages10.1145/34855165:OOPSLA(1-32)Online publication date: 20-Oct-2021
https://dl.acm.org/doi/10.1145/3485516
Clarke DÖstlund JSergey IWrigstad T(2013)Ownership typesAliasing in Object-Oriented Programming10.5555/2554511.2554516(15-58)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554516
Dietl WDrossopoulou SMüller P(2012)Separating ownership topology and encapsulation with generic universe typesACM Transactions on Programming Languages and Systems10.1145/2049706.204970933:6(1-62)Online publication date: 3-Jan-2012
https://dl.acm.org/doi/10.1145/2049706.2049709
Garbervetsky DGorín DNeisen A(2011)Enforcing structural invariants using dynamic framesProceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software10.5555/1987389.1987399(65-80)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987389.1987399
Potanin ANoble JClarke DBiddle R(2006)Generic ownership for generic JavaACM SIGPLAN Notices10.1145/1167515.116750041:10(311-324)Online publication date: 16-Oct-2006
https://dl.acm.org/doi/10.1145/1167515.1167500
Potanin ANoble JClarke DBiddle RTarr PCook WBiddle RGabriel R(2006)Generic ownership for generic JavaProceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications10.1145/1167473.1167500(311-324)Online publication date: 23-Oct-2006
https://dl.acm.org/doi/10.1145/1167473.1167500
Lu YPotter J(2006)Protecting representation with effect encapsulationACM SIGPLAN Notices10.1145/1111320.111106941:1(359-371)Online publication date: 11-Jan-2006
https://dl.acm.org/doi/10.1145/1111320.1111069
Lu YPotter JMorrisett GJones S(2006)Protecting representation with effect encapsulationConference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1111037.1111069(359-371)Online publication date: 11-Jan-2006
https://dl.acm.org/doi/10.1145/1111037.1111069
Lu YPotter J(2006)On ownership and accessibilityProceedings of the 20th European conference on Object-Oriented Programming10.1007/11785477_6(99-123)Online publication date: 3-Jul-2006
https://dl.acm.org/doi/10.1007/11785477_6

View Options

View options

Media

Figures

Other

Tables

View Table of Contents