Abstract
Region-based memory management is an alternative to standard tracing garbage collection that makes operation such as memory deallocation explicit but verifiably safe. In this article, we present a new compiler intermediate language, called the Capability Language (CL), that supports region-based memory management and enjoys a provably safe type systems. Unlike previous region-based type system, region lifetimes need not be lexically scoped, and yet the language may be checked for safety without complex analyses. Therefore, our type system may be deployed in settings such as extensible operating systems where both the performance and safety of untrusted code is important. The central novelty of the language is the use of static capabilities to specify the permissibility of various operations, such as memory access and deallocation. In order to ensure capabilities are relinquished properly, the type system tracks aliasing information using a form of bounded quantification. Moreover, unlike previous work on region-based type systems, the proof of soundness of our type system is relatively simple, employing only standard syntactic techniques. In order to show how our language may be used in practice, we show how to translate a variant of Tofte and Talpin's high-level type-and-effects system for region-based memory management into our language. When combined with known region inference algorithms, this translation provides a way to compile source-level languages to CL.
- Abramsky, S. 1993. Computational interpretations of linear logic. Theoretical Computer Science 111, 3-57.]] Google ScholarDigital Library
- Aiken, A., F~hndrich, M., and Levien, R. 1995. Better static memory management: Improving region-based analysis of higher-order languages. In ACM Conference on Programming Language Design and Implementation. ACM Press, La Jolla, California, 174-185.]] Google ScholarDigital Library
- Alpern, B. and Schneider, F. 1987. Recognizing safety and liveness. Distributed Computing 2, 117-126.]]Google ScholarDigital Library
- Baker, H. G. 1978. List processing in real-time on a serial computer. Communications of the ACM 21, 4, 280-294.]] Google ScholarDigital Library
- Bershad, B., Savage, S. , Pardyak, P. , Sirer, E., Fiuczynski, M., Becker, D., Chambers, C., and Eggers, S. 1995. Extensibility, safety and performance in the SPIN operating system. In Fifteenth ACM Symposium on Operating Systems Principles. ACM Press, Copper Mountain, 267-284.]] Google ScholarDigital Library
- Birkedal, L., Rothwell, N., Tofte, M., and Turner, D. N. 1993. The ML Kit (version 1). Tech. Rep. 93/14, Department of Computer Science, University of Copenhagen.]]Google Scholar
- Birkedal, L., Tofte, M., and Vejlstrup, M. 1996. From region inference to von Neumann machines via region representation inference. In Twenty-Third ACM Symposium on Principles of Programming Languages. ACM Press, St. Petersburg, 171-183.]] Google ScholarDigital Library
- Blelloch, G. and Greiner, J. 1996. A provably time and space efficient implementation of NESL. In ACM International Conference on Functional Programming. ACM Press, Philadelphia, 213- 225.]] Google ScholarDigital Library
- Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculus of capabilities. In Twenty-Sixth ACM Symposium on Principles of Programming Languages. ACM Press, San Antonio, 262-275.]] Google ScholarDigital Library
- Crary, K., Weirich, S., and Morrisett, G. 1998. Intensional polymorphism in type-erasure semantics. In ACM International Conference on Functional Programming. ACM Press, Baltimore, 301-312.]] Google ScholarDigital Library
- Danvy, O. and Filinski, A. 1992. Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science 2, 4 (Dec.), 361-391.]]Google ScholarCross Ref
- Danvy, O., Dzafic, B., and Pfenning, F. 1999. On proving syntactic properties of CPS programs. In Third International Workshop on Higher-Order Operational Techniques in Semantics, A. Gordon and A. Pitts, Eds. Electronic Notes in Computer Science, vol. 26. Elsevier, Paris, 19-31.]]Google Scholar
- Filinski, A. 1996. Controlling effects. Ph.D. thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania.]]Google Scholar
- Fischer, M. J. 1972. Lambda calculus schemata. In Proceedings of the ACM Conference on Proving Assertions about Programs. 104-109.]] Google ScholarDigital Library
- Flanagan, C. and Abadi, M. 1999. Types for safe locking. In Lecture Notes in Computer Science, S. Swierstra, Ed. Vol. 1576. Springer-Verlag, Amsterdam, 91-108. Appeared in the Eighth European Symposium on Programming.]] Google ScholarDigital Library
- Gay, D. and Aiken, A. 1998. Memory management with explicit regions. In ACM Conference on Programming Language Design and Implementation. ACM Press, Montreal, 313 - 323.]] Google ScholarDigital Library
- Gifford, D. K. and Lucassen, J. M. 1986. Integrating functional and imperative programming. In ACM Conference on Lisp and Functional Programming. ACM Press, Cambridge, Massachusetts, 28-38.]] Google ScholarDigital Library
- Girard, J.-Y. 1987. Linear logic. Theoretical Computer Science 50, 1-102.]] Google ScholarDigital Library
- Harper, R. and Lillibridge, M. 1993. Explicit polymorphism and CPS conversion. In Twentieth ACM Symposium on Principles of Programming Languages. ACM Press, Charleston, 206-219.]] Google ScholarDigital Library
- Harper, R. and Morrisett, G. 1995. Compiling polymorphism using intensional type analysis. In Twenty-Second ACM Symposium on Principles of Programming Languages. ACM Press, San Francisco, 130-141.]] Google ScholarDigital Library
- Hawblitzel, C., Chang, C.-C., Czajkowski, G., Hu, D., and von Eicken, T. 1998. Implementing multiple protection domains in Java. In 1998 USENIX Annual Technical Conference. USENIX, New Orleans.]] Google ScholarDigital Library
- Hawblitzel, C. and von Eicken, T. 1999. Type system support for dynamic revocation. In ACM SIGPLAN workshop on Compiler Support for System Software. ACM Press, Atlanta.]]Google Scholar
- Jouvelot, P. and Gifford, D. K. 1991. Algebraic reconstruction of types and effects. In Eighteenth ACM Symposium on Principles of Programming Languages. ACM Press, Orlando, 303-310.]] Google ScholarDigital Library
- Kozen, D. 1998. Efficient code certification. Tech. Rep. TR98-1661, Cornell University. Jan.]] Google ScholarDigital Library
- Lafont, Y. 1988. The linear abstract machine. Theoretical Computer Science 59, 157-180.]] Google ScholarDigital Library
- Launchbury, J. and Peyton Jones, S. L. 1995. State in Haskell. LISP and Symbolic Computation 8, 4 (Dec.), 293-341.]] Google ScholarDigital Library
- Lindholm, T. and Yellin, F. 1996. The Java Virtual Machine Specification. Addison-Wesley, Menlo Park, California.]] Google ScholarDigital Library
- Lucassen, J. M. 1987. Types and effects-towards the integration of functional and imperative programming. Ph.D. thesis, MIT Laboratory for Computer Science.]]Google Scholar
- Milner, R., Tofte, M., Harper, R., and MacQueen, D. 1997. The Definition of Standard ML (Revised). MIT Press, Boston.]] Google ScholarDigital Library
- Minamide, Y. 1999. Space-profiling semantics of the call-by-value lambda calculus and the CPS transformation. In Third International Workshop on Higher-Order Operational Techniques in Semantics, A. D. Gordon and A. Pitts, Eds. Electronic Notes in Computer Science, vol. 26. Elsevier, Paris, 103-118.]]Google ScholarCross Ref
- Moggi, E. 1991. Notions of computation and monads. Information and Computation 93, 55-92.]] Google ScholarDigital Library
- Morrisett, G. and Harper, R. 1997. Semantics of memory management for polymorphic languages. In Higher-Order Operational Techniques in Semantics, A. Gordon and A. Pitts, Eds. Publications of the Newton Institute. Cambridge University Press, Cambridge, UK.]] Google ScholarDigital Library
- Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., and Zdancewic, S. 2000. Typed Assembly Language for the Intel IA32 architecture. See http://www.cs.cornell.edu/talc for the latest implementation.]]Google Scholar
- Morrisett, G., Felleisen, M., and Harper, R. 1995. Abstract models of memory management. In ACM Conference on Functional Programming and Computer Architecture. ACM Press, La Jolla, 66-77.]] Google ScholarDigital Library
- Morrisett, G., Walker, D., Crary, K., and Glew, N. 1998. From System F to Typed Assembly Language. In Twenty-Fifth ACM Symposium on Principles of Programming Languages. ACM Press, San Diego, 85-97.]] Google ScholarDigital Library
- Morrisett, G., Walker, D., Crary, K., and Glew, N. 1999. From System F to Typed Assembly Language. ACM Transactions on Progamming Languages and Systems 21, 3 (May), 528-569.]] Google ScholarDigital Library
- Necula, G. 1997. Proof-carrying code. In Twenty-Fourth ACM Symposium on Principles of Programming Languages. ACM Press, Paris, 106-119.]] Google ScholarDigital Library
- Necula, G. and Lee, P. 1996. Safe kernel extensions without run-time checking. In Proceedings of Operating System Design and Implementation. USENIX assoc., Seattle, 229-243.]] Google ScholarDigital Library
- Necula, G. and Lee, P. 1998. The design and implementation of a certifying compiler. In ACM Conference on Programming Language Design and Implementation. ACM Press, Montreal, 333 - 344.]] Google ScholarDigital Library
- Peyton Jones, S. L. and Wadler, P. 1993. Imperative functional programming. In Twentieth ACM Symposium on Principles of Programming Languages. ACM Press, Charleston, South Carolina.]] Google ScholarDigital Library
- Plotkin, G. D. 1975. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science 1, 125-159.]]Google ScholarCross Ref
- Reynolds, J. C. 1972. Definitional interpreters for higher-order programming languages. In Conference Record of the 25th National ACM Conference. Boston, 717-740.]] Google ScholarDigital Library
- Reynolds, J. C. 1978. Syntactic control of interference. In Fifth ACM Symposium on Principles of Programming Languages. ACM Press, Tucson, Arizona, 39-46.]] Google ScholarDigital Library
- Reynolds, J. C. 1989. Syntactic control of interference, part 2. In Automata, Languages and Programming: 16th International Colloquium. Lecture Notes in Computer Science, vol. 372. Springer-Verlag, Stresa, Italy, 704-722.]] Google ScholarDigital Library
- Sabry, A. and Felleisen, M. 1993. Reasoning about programs in continuation-passing style. LISP and Symbolic Computation 6, 3/4, 289-360.]] Google ScholarDigital Library
- Schneider, F. 2000. Enforceable security policies. ACM Transactions on Information and System Security 3, 1 (Feb.).]] Google ScholarDigital Library
- Smith, F., Walker, D., and Morrisett, G. 2000. Alias types. In Lecture Notes in Computer Science, G. Smolka, Ed. Vol. 1782. Springer-Verlag, Berlin, 366-381. Appeared in the Ninth European Symposium on Programming.]] Google ScholarDigital Library
- Tofte, M. and Birkedal, L. 1998. A region inference algorithm. Transactions on Programming Languages and Systems 20, 4 (Nov.), 734-767.]] Google ScholarDigital Library
- Tofte, M. and Talpin, J.-P. 1994. Implementation of the typed call-by-value calculus using a stack of regions. In Twenty-First ACM Symposium on Principles of Programming Languages. ACM Press, Portland, Oregon, 188-201.]] Google ScholarDigital Library
- Tofte, M. and Talpin, J.-P. 1997. Region-based memory management. Information and Computation 132, 2, 109-176.]] Google ScholarDigital Library
- Wadler, P. 1990. Linear types can change the world! In Programming Concepts and Methods, M. Broy and C. Jones, Eds. North Holland, Sea of Galilee, Israel. IFIP TC 2 Working Conference.]]Google Scholar
- Wadler, P. 1993. A taste of linear logic. In Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 711. Springer-Verlag, Gdansk, Poland.]] Google ScholarDigital Library
- Wahbe, R., Lucco, S., Anderson, T., and Graham, S. 1993. Efficient software-based fault isolation. In Fourteenth ACM Symposium on Operating Systems Principles. ACM Press, Asheville, 203-216.]] Google ScholarDigital Library
- Walker, D. 2000. A type system for expressive security policies. In Twenty-Seventh ACM Symposium on Principles of Programming Languages. ACM Press, Boston, 254-267.]] Google ScholarDigital Library
- Walker, D. and Morrisett, G. 2000. Alias types for recursive data structures. In Workshop on Types in Compilation. Montreal.]] Google ScholarDigital Library
- Wilson, P. R. 1992. Uniprocessor garbage collection techniques. In International Workshop on Memory Management, Y. Bekkers and J. Cohen, Eds. Number 637 in Lecture Notes in Computer Science. Springer-Verlag, St. Malo, 1-42.]] Google ScholarDigital Library
- Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Information and Computation 115, 1, 38-94.]] Google ScholarDigital Library
- Wulf, W. A., Levin, R., and Harbison, S. P. 1981. Hydra/C.mmp: An Experimental Computer System. McGraw-Hill, New York, NY.]]Google Scholar
Index Terms
- Typed memory management via static capabilities
Recommendations
Typed memory management in a calculus of capabilities
POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesAn increasing number of systems rely on programming language technology to ensure safety and security of low-level code. Unfortunately, these systems typically rely on a complex, trusted garbage collector. Region-based type systems provide an ...
From system F to typed assembly language
We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides ...
Intensional analysis of quantified types
Compilers for polymorphic languages can use run-time type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data structures. Intensional type analysis is a type-theoretic ...
Comments