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 be eventually 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 so clear what is the essence of those methods 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: G.Bigliardi and C.Laneve.A type system for JVM threads.In Proc.of 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC2000),2000.
• 3: 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]
• 4: 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]
• 5: 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
• 6: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 7: 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
• 8: 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
• 9: 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]
• 10: 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]
• 11: 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
• 12: 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
• 13: A.Igarashi and N.Kobayashi.Garbage collection based on a linear type system.In Proc.of 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC2000),2000.
• 14: 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]
• 15: Atsushi Igarashi , Naoki Kobayashi, A generic type system for the Pi-calculus, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-141, January 2001, London, United Kingdom
• 16: 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]
• 17: P.C.Kanellakis,H.G.Mairson,and J.C.Mitchell. Uni .cation and ML Type Reconstruction.In J.-L. Lassez and G.D.Plotkin,editors,Computational Logic:Essays in Honor of Alan Robinson, pages 444 -478.The MIT Press,1991.
• 18: 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]
• 19: 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
• 20: 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
• 21: 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
• 22: 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]
• 23: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 24: E.Sumii and N.Kobayashi.A generalized deadlock-free process calculus.In Proc.of Workshop on High-Level Concurrent Language (HLCL '98), ENTCS 16(3),pages 55 -77,1998.
• 25: 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]
• 26: 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]
• 27: P.Wadler.Linear types can change the world. In Programming Concepts and Methods. North Holland, 1990.
• 28: 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]
• 29: D.Walker and K.Watkins.On linear types and regions.In Proc.of ICFP, 2001.
• 30: 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]