skip to main content
research-article
Open Access

Local reasoning about a copying garbage collector

Published:01 August 2008Publication History
Skip Abstract Section

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.

References

  1. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  2. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  3. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  4. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  5. Appel, A. W. and Gonçalves, M. J. R. 1993. Hash-consing garbage collection. Tech. rep. CS-TR-412-93, Princeton University.]]Google ScholarGoogle Scholar
  6. Ben-Ari, M. 1984. Algorithms for on-the-fly garbage collection. ACM Trans. Program. Lang. Syst. 6, 3, 333--344.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  8. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  9. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  10. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  11. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  12. Bornat, R. 2003. Correctness of copydag via local reasoning. Private Communication.]]Google ScholarGoogle Scholar
  13. 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 ScholarGoogle Scholar
  14. 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 ScholarGoogle Scholar
  15. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  16. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  17. Cheney, C. J. 1970. A nonrecursive list compacting algorithm. Comm. ACM 13, 11, 677--678.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. Coupet-Grimal, S. 2003. C. nouvet. J. Logic Comput. 13, 6, 815--833.]]Google ScholarGoogle ScholarCross RefCross Ref
  19. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  20. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  21. 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 ScholarGoogle Scholar
  22. Goto, E. 1974. Monocopy and associative algorithms in extended lisp. Tech. rep. TR 74-03, University of Tokyo.]]Google ScholarGoogle Scholar
  23. Gries, D. and Levin, G. 1980. Assignment and procedure call proof rules. ACM Trans. Program. Lang. Syst. 2, 4, 564--579.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Guttmann, J., Ramsdell, J., and Wand, M. 1994. VLISP: A verified implementation of scheme. Lisp Symb. Comput. 8, 1--2, 5--32.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. 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 ScholarGoogle Scholar
  26. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  27. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  28. 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 ScholarGoogle Scholar
  29. Hoare, C. A. R. 1969. An axiomatic approach to computer programming. Comm. ACM 12, 583, 576--580.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  31. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  32. Mehta, F. and Nipkow, T. 2003. Proving pointer programs in higher-order logic. In Proceedings of the Conference on Automated Deduction (CADE-19).]]Google ScholarGoogle Scholar
  33. Monnier, S. and Shao, Z. 2002. Typed regions. Tech. rep. YALEU/DCS/TR-1242, Department of Computer Science, Yale University, New Haven, CT.]]Google ScholarGoogle Scholar
  34. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  35. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  36. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  37. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  38. 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 ScholarGoogle Scholar
  39. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  40. Owicki, S. and Gries, D. 1976. An axiomatic proof technique for parallel programs. Acta Informatica 6, 4, 319--340.]]Google ScholarGoogle ScholarDigital LibraryDigital Library
  41. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  42. Pixley, C. 1988. An incremental garbage collection algorithm for multimutator systems. Distrib. Comput. 3, 1, 41--50.]]Google ScholarGoogle ScholarDigital LibraryDigital Library
  43. Pym, D. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logics Series. vol. 26, Kluwer.]]Google ScholarGoogle Scholar
  44. Reynolds, J. C. 1981. The Craft of Programming. Prentice-Hall International Series in Computer Science. Prentice-Hall.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  45. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  46. Russinoff, D. M. 1994. A mechanically verified incremental garbage collector. Formal Aspects Comput. 6, 359--390.]]Google ScholarGoogle ScholarDigital LibraryDigital Library
  47. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  48. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  49. 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 ScholarGoogle Scholar
  50. Tofte, M. and Birkedal, L. 1998. A region inference algorithm. ACM Trans. Program. Lang. Syst. 20, 4, 734--767.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  51. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  52. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  53. Wadler, P. L. 1976. Analysis of an algorithm for real time garbage collection. Comm. ACM 19, 9, 491--500.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  54. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  55. 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 ScholarGoogle ScholarCross RefCross Ref
  56. Yang, H. 2001. Local reasoning for stateful programs. Ph. D. thesis, University of Illinois, Urbana-Champaign.]] Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Local reasoning about a copying garbage collector

          Recommendations

          Comments

          Login options

          Check if you have access through your login credentials or your institution to get full access on this article.

          Sign in

          Full Access

          • Published in

            cover image ACM Transactions on Programming Languages and Systems
            ACM Transactions on Programming Languages and Systems  Volume 30, Issue 4
            July 2008
            358 pages
            ISSN:0164-0925
            EISSN:1558-4593
            DOI:10.1145/1377492
            Issue’s Table of Contents

            Copyright © 2008 ACM

            Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

            Publisher

            Association for Computing Machinery

            New York, NY, United States

            Publication History

            • Published: 1 August 2008
            • Accepted: 1 August 2006
            • Revised: 1 November 2005
            • Received: 1 July 2004
            Published in toplas Volume 30, Issue 4

            Permissions

            Request permissions about this article.

            Request Permissions

            Check for updates

            Qualifiers

            • research-article
            • Research
            • Refereed

          PDF Format

          View or Download as a PDF file.

          PDF

          eReader

          View online with eReader.

          eReader