Abstract
We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We state semantically what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation logics to formally specify partial correctness of Cheney's copying garbage collector in our program logic. Finally, we prove that our implementation of Cheney's algorithm meets its specification using the logic we have given and auxiliary variables.
- Aditya, S. and Caro, A. 1993. Compiler-directed type reconstruction for polymorphic languages. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA'93). Copenhagen, Denmark. ACM Press, 74--82.]] Google ScholarDigital Library
- Aditya, S., Flood, C. H., and Hicks, J. E. 1994. Garbage collection for strongly-typed languages using run-time type reconstruction. In Proceedings of the ACM Conference on LISP and Functional Programming (LFP'94). Orlando, FL, ACM Press, 12--23.]] Google ScholarDigital Library
- Ahmed, A., Jia, L., and Walker, D. 2003. Reasoning about hierarchical storage. In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03). Ottawa, Canada. IEEE Press.]] Google ScholarDigital Library
- Appel, A. W. 2001. Foundational proof carrying code. In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS'01). Boston, MA. IEEE Press.]] Google ScholarDigital Library
- Appel, A. W. and Gonçalves, M. J. R. 1993. Hash-consing garbage collection. Tech. rep. CS-TR-412-93, Princeton University.]]Google Scholar
- Ben-Ari, M. 1984. Algorithms for on-the-fly garbage collection. ACM Trans. Program. Lang. Syst. 6, 3, 333--344.]] Google ScholarDigital Library
- Berdine, J., Calcagno, C., and O'Hearn, P. W. 2005. Symbolic execution with separation logic. In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS'05), Tsukuba, Japan. Springer Verlag, 52--68.]] Google ScholarDigital Library
- Biering, B., Birkedal, L., and Torp-Smith, N. 2005. BI-hyperdoctrines and higher order separation logic. In Proceedings of the European Symposium on Programming (ESoP'05). Edinburgh, Scotland, 233--247.]] Google ScholarDigital Library
- Birkedal, L., Torp-Smith, N., and Reynolds, J. 2004. Local reasoning about a copying garbage collector. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'04). Venice, Italy, 220--231.]] Google ScholarDigital Library
- Birkedal, L., Torp-Smith, N., and Yang, H. 2005. Semantics of separation-logic typing and higher-order frame rules. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS'05), Chicago, IL. IEEE Press, 260--269.]] Google ScholarDigital Library
- Bornat, R. 2000. Proving pointer programs in Hoare logic. In Proceedings of the 5th International Conference on Mathematics of Program Construction. Vol. 1837. Lecture Notes In Computer Science, Springer Verlag, 102--126.]] Google ScholarDigital Library
- Bornat, R. 2003. Correctness of copydag via local reasoning. Private Communication.]]Google Scholar
- Bornat, R., Calcagno, C., and O'Hearn, P. 2004. Local reasoning, separation and aliasing. In Proceedings of the Conference on Semantics, Program Analysis, and Computing Environments (SPACE'04). Venice, Italy.]]Google Scholar
- Burdy, L. 2001. B vs Coq to prove a garbage collector. In Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01). Lecture Notes in Computer Science, Vol. 2152. Springer Verlag.]]Google Scholar
- Calcagno, C., Ishtiaq, S., and O'Hearn, P. W. 2000. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. In Proceedings of the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP'00). Montreal, Canada.]] Google ScholarDigital Library
- Calcagno, C., O'Hearn, P. W., and Bornat, R. 2003. Program logic and equivalence in the presence of garbage collection. Theor. Comput. Sci. 298, 3, 557--587.]] Google ScholarDigital Library
- Cheney, C. J. 1970. A nonrecursive list compacting algorithm. Comm. ACM 13, 11, 677--678.]] Google ScholarDigital Library
- Coupet-Grimal, S. 2003. C. nouvet. J. Logic Comput. 13, 6, 815--833.]]Google ScholarCross Ref
- Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of Programming Languages (POPL'99). San Antonio, TX. 262--275.]] Google ScholarDigital Library
- Dijkstra, E. W., Lamport, L., Martin, A. J., Scholten, G. S., and Steffens, E. M. F. 1978. On-the-fly garbage collection: an exercise in cooperation. Comm. ACM 21, 11, 965--975.]] Google ScholarDigital Library
- Fluet, M. and Wang, D. 2004. Implementation and performance evaluation of a safe runtime system in Cyclone. In Informal Proceedings of the 2nd Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE'04). Venice, Italy. ACM/SIGPLAN.]]Google Scholar
- Goto, E. 1974. Monocopy and associative algorithms in extended lisp. Tech. rep. TR 74-03, University of Tokyo.]]Google Scholar
- Gries, D. and Levin, G. 1980. Assignment and procedure call proof rules. ACM Trans. Program. Lang. Syst. 2, 4, 564--579.]] Google ScholarDigital Library
- Guttmann, J., Ramsdell, J., and Wand, M. 1994. VLISP: A verified implementation of scheme. Lisp Symb. Comput. 8, 1--2, 5--32.]] Google ScholarDigital Library
- Guttmann, J. D., Monk, L. G., Ramsdell, J. D., Farmer, W. M., and Swarup, V. 1992. A guide to VLISP, a verified programming language implementation. Tech. rep. M92B091, The MITRE Corporation.]]Google Scholar
- Hallenberg, N., Elsman, M., and Tofte, M. 2002. Combining region inference and garbage collection. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02). Berlin, Germany. ACM Press.]] Google ScholarDigital Library
- Havelund, K. 1999. Mechanical verification of a garbage collector. In Proceedings of the 4th International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA'99). San Juan, Puerto Rico.]] Google ScholarDigital Library
- Hawblitzel, C., Wei, E., Huang, H., Krupski, E., and Wittie, L. 2004. Low-level linear memory management. In Proceedings of the Conference on Semantics, Program Analysis, and Computing Environments (SPACE'04). Venice, Italy.]]Google Scholar
- Hoare, C. A. R. 1969. An axiomatic approach to computer programming. Comm. ACM 12, 583, 576--580.]] Google ScholarDigital Library
- Jackson, P. B. 1998. Verifying a garbage collection algorithm. In Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98), Lecture Notes in Computer Science, vol. 1479, Springer Verlag, 225--244.]] Google ScholarDigital Library
- Jim, T., Morrisett, G., Grossman, D., Hicks, M., Cheney, J., and Wang, Y. 2002. Cyclone: A safe dialect of C. In Proceedings of the USENIX Annual Technical Conference. Monterey, CA. 275--288.]] Google ScholarDigital Library
- Mehta, F. and Nipkow, T. 2003. Proving pointer programs in higher-order logic. In Proceedings of the Conference on Automated Deduction (CADE-19).]]Google Scholar
- Monnier, S. and Shao, Z. 2002. Typed regions. Tech. rep. YALEU/DCS/TR-1242, Department of Computer Science, Yale University, New Haven, CT.]]Google Scholar
- Morrisett, G., Felleisen, M., and Harper, R. 1995. Abstract models of memory management. In Proceedings of the 7th International Conference on Functional Programming Languages and Computer Architecture (FPCA'95), La Jolla, CA. ACM Press, 66--77.]] Google ScholarDigital Library
- Morrisett, G., Walker, D., Crary, K., and Glew, N. 1999. From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21, 3, 527--568.]] Google ScholarDigital Library
- Necula, G. C. 1997. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'97). Paris, France, 106--119.]] Google ScholarDigital Library
- Necula, G. C. and Lee, P. 1996. Safe kernel extensions without run-time checking. In Proceedings of the 2nd USENIX Symposium on Operating Systems Design and Implementation (OSDI'96). Berkeley, CA. 229--243.]] Google ScholarDigital Library
- O'Hearn, P. W. 2004. Resources, concurrency and local reasoning. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), Lecture Notes in Computer Science, vol. 3170, 49--67.]]Google Scholar
- O'Hearn, P. W., Reynolds, J. C., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'01). Berlin, Germany.]] Google ScholarDigital Library
- Owicki, S. and Gries, D. 1976. An axiomatic proof technique for parallel programs. Acta Informatica 6, 4, 319--340.]]Google ScholarDigital Library
- Petersen, L., Harper, R., Crary, K., and Pfenning, F. 2003. A type theory for memory allocation and data layout. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03). New Orleans, LA. 172--184.]] Google ScholarDigital Library
- Pixley, C. 1988. An incremental garbage collection algorithm for multimutator systems. Distrib. Comput. 3, 1, 41--50.]]Google ScholarDigital Library
- Pym, D. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logics Series. vol. 26, Kluwer.]]Google Scholar
- Reynolds, J. C. 1981. The Craft of Programming. Prentice-Hall International Series in Computer Science. Prentice-Hall.]] Google ScholarDigital Library
- Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02). Copenhagen, Denmark. IEEE Press, 55--74.]] Google ScholarDigital Library
- Russinoff, D. M. 1994. A mechanically verified incremental garbage collector. Formal Aspects Comput. 6, 359--390.]]Google ScholarDigital Library
- Smith, F., Walker, D., and Morrisett, G. 2000. Alias types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP'00). Berlin, Germany. 366--381.]] Google ScholarDigital Library
- Stoyle, G., Hicks, M., Bierman, G., Sewell, P., and Neamtiu, I. 2005. Mutatis mutandis: Safe and predictable dynamic software updating. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05). Long Beach, CA. ACM Press, 183--194.]] Google ScholarDigital Library
- Swarup, V., Farmer, W. M., Guttmann, J. D., Monk, L. G., and Ramsdell, J. D. 1992. The VLISP byte-code interpreter. Tech. rep. M 92B096, The MITRE Corporation.]]Google Scholar
- Tofte, M. and Birkedal, L. 1998. A region inference algorithm. ACM Trans. Program. Lang. Syst. 20, 4, 734--767.]] Google ScholarDigital Library
- Tofte, M., Birkedal, L., Elsman, M., and Hallenberg, N. 2004. A retrospective on region-based memory management. Higher-Order Symb. Comput. 17, 3, 245--265.]] Google ScholarDigital Library
- Tofte, M. and Talpin, J.-P. 1994. Implementation of the call-by-value lambda-calculus using a stack of regions. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'94), Portland, OR. 188--201.]] Google ScholarDigital Library
- Wadler, P. L. 1976. Analysis of an algorithm for real time garbage collection. Comm. ACM 19, 9, 491--500.]] Google ScholarDigital Library
- Wang, D. and Appel, A. W. 2001. Type preserving garbage collectors. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01). London, UK. 166--178.]] Google ScholarDigital Library
- Weber, T. 2004. Towards mechanized program verification with separation logic. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'04). Karpacz, Poland.]]Google ScholarCross Ref
- Yang, H. 2001. Local reasoning for stateful programs. Ph. D. thesis, University of Illinois, Urbana-Champaign.]] Google ScholarDigital Library
Index Terms
Local reasoning about a copying garbage collector
Recommendations
Local reasoning about a copying garbage collector
POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then state what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation ...
Local reasoning about a copying garbage collector
POPL '04We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then state what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation ...
A generational on-the-fly garbage collector for Java
PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementationAn on-the-fly garbage collector does not stop the program threads to perform the collection. Instead, the collector executes in a separate thread (or process) in parallel to the program. On-the-fly collectors are useful for multi-threaded applications ...
Comments