Resource usage analysis

ABSTRACT

It is an important criterion of program correctness that a program accesses resources in a valid manner. For example, a memory region that has been allocated should eventually be deallocated, and after the deallocation, the region should no longer be accessed. A file that has been opened should be eventually closed. So far, most of the methods to analyze this kind of property have been proposed in rather specific contexts (like studies of memory management and verification of usage of lock primitives), and it was not clear what the essence of those methods was or how methods proposed for individual problems are related. To remedy this situation, we formalize a general problem of analyzing resource usage as a resource usage analysis problem, and propose a type-based method as a solution to the problem.

REFERENCES

• 1: Alexander Aiken , Manuel Fähndrich , Raph Levien, Better static memory management: improving region-based analysis of higher-order languages, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.174-185, June 18-21, 1995, La Jolla, California, United States
• 2: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 3: Bigliardi, G. and Laneve, C. 2000. A type system for JVM threads. In Proceedings of 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC2000) (Montreal, Que., Canada). ACM, New York.
• 4: Lars Birkedal , Mads Tofte , Magnus Vejlstrup, From region inference to von Neumann machines via region representation inference, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237771]
• 5: Bruno Blanchet, Escape analysis: correctness proof, implementation and experimental results, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.25-37, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268949]
• 6: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 7: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 8: Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 9: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 10: Cormac Flanagan , Martín Abadi, Object Types against Races, Proceedings of the 10th International Conference on Concurrency Theory, p.288-303, August 24-27, 1999
• 11: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 12: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 13: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 14: Stephen N. Freund , John C. Mitchell, The type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.6, p.1196-1250, Nov. 1999 [doi>10.1145/330643.330646]
• 15: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 16: Jay Gischer, Shuffle languages, Petri nets, and context-sensitive grammars, Communications of the ACM, v.24 n.9, p.597-605, Sept. 1981 [doi>10.1145/358746.358767]
• 17: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 18: Jörgen Gustavsson , Josef Svenningsson, A Usage Analysis with Bounded Usage Polymorphism and Subtyping, Selected Papers from the 12th International Workshop on Implementation of Functional Languages, p.140-157, September 04-07, 2000
• 19: John Hannan, A Type-based Analysis for Stack Allocation in Functional Languages, Proceedings of the Second International Symposium on Static Analysis, p.172-188, September 25-27, 1995
• 20: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 21: Igarashi, A. and Kobayashi, N. 2000a. Garbage collection based on a linear type system. In Proceedings of 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC2000) (Montreal, Que., Canada) ACM, New York. (Published as Technical Report CMU-CS-00-161, Carnegie Mellon University, Pittsburgh, PA.)
• 22: Atsushi Igarashi , Naoki Kobayashi, Type reconstruction for linear &pgr;-calculus with I/O subtyping, Information and Computation, v.161 n.1, p.1-44, Aug. 25, 2000 [doi>10.1006/inco.2000.2872 ]
• 23: Atsushi Igarashi , Naoki Kobayashi, A generic type system for the Pi-calculus, Theoretical Computer Science, v.311 n.1-3, p.121-163, 23 January 2004 [doi>10.1016/S0304-3975(03)00325-6]
• 24: Futoshi Iwama , Naoki Kobayashi, A new type system for JVM lock primitives, Proceedings of the ASIAN symposium on Partial evaluation and semantics-based program manipulation, p.71-82, September 12-14, 2002, Aizu, Japan [doi>10.1145/568173.568182]
• 25: Joanna Jędrzejowicz , Andrzej Szepietowski, Shuffle languages are in P, Theoretical Computer Science, v.250 n.1-2, p.31-53, Jan 6, 2001 [doi>10.1016/S0304-3975(99)00109-7 ]
• 26: Kanellakis, P. C., Mairson, H. G., and Mitchell, J. C. 1991. Unification and ML type reconstruction. In Computational Logic: Essays in Honor of Alan Robinson, J.-L. Lassez and G. D. Plotkin, Eds. The MIT Press, Cambridge, Mass., 444--478.
• 27: Naoki Kobayashi, Quasi-linear types, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.29-42, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292546]
• 28: Naoki Kobayashi, Type-based useless variable elimination, Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.84-93, January 22-23, 2000, Boston, Massachusetts, United States
• 29: Naoki Kobayashi, Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness, Proceedings of the International Conference IFIP on Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, p.365-389, August 17-19, 2000
• 30: Naoki Kobayashi, Time regions and effects for resource usage analysis, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 31: Naoki Kobayashi , Shin Saito , Eijiro Sumii, An Implicitly-Typed Deadlock-Free Process Calculus, Proceedings of the 11th International Conference on Concurrency Theory, p.489-503, August 22-25, 2000
• 32: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 33: Greg Morrisett , Matthias Felleisen , Robert Harper, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.66-77, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224182]
• 34: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 35: Jakob Rehof , Torben Ægidius Mogensen, Tractable constraints in finite semilattices, Science of Computer Programming, v.35 n.2-3, p.191-221, Nov.1.1999 [doi>10.1016/S0167-6423(99)00011-8 ]
• 36: Davide Sangiorgi , David Walker, PI-Calculus: A Theory of Mobile Processes, Cambridge University Press, New York, NY, 2001
• 37: Sumii, E. and Kobayashi, N. 1998. A generalized deadlock-free process calculus. In Proc. of Workshop on High-Level Concurrent Language (HLCL'98). ENTCS, vol. 16(3). 55--77.
• 38: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• 39: David N. Turner , Philip Wadler , Christian Mossin, Once upon a type, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.1-11, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224168]
• 40: Wadler, P. 1990. Linear types can change the world! In Programming Concepts and Methods. North Holland, Amsterdam, The Netherland.
• 41: David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]
• 42: David Walker , Kevin Watkins, On regions and linear types (extended abstract), Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 43: Keith Wansbrough , Simon Peyton Jones, Once upon a polymorphic type, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-28, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292545]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics; Program analysis
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Keywords:
Resource usage, type inference