Advertisement

Code Generation Using a Formal Model of Reference Counting

  • Gaspard FéreyEmail author
  • Natarajan Shankar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9690)

Abstract

Reference counting is a popular technique for memory management. It tracks the number of active references to a data object during the execution of a program. Reference counting allows the memory used by a data object to be freed when there are no active references to it. We develop the metatheory of reference counting by presenting an abstract model for a functional language with arrays. The model is captured by an intermediate language and its operational semantics, defined both with and without reference counting. These two semantics are shown to correspond by means of a bisimulation. The reference counting implementation allows singly referenced data objects to be updated in place, i.e., without copying. The main motivation for our model of reference counting is in soundly translating programs from a high-level functional language, in our case, an executable fragment of the PVS specification language, to efficient code with a compact footprint in a small subset of a low-level imperative language like C.

Notes

Acknowledgments

An earlier version of the intermediate language used here was developed by the second author in collaboration with Basile Clement (École Normal Supérieure, Paris) and Simon Halfon (École Normal Supérieure, Cachan). We thank them for many illuminating conversations on topics related to this paper. We thank Greg Morrisett (Cornell University), Sam Owre (SRI), Bruno Dutertre (SRI), Andrew Tolmach (Portland State University), Jean-Christophe Filliâtre (LRI Université Paris-Sud), John Launchbury (DARPA I20), Robin Larrieu (École Polytechnique), and the anonymous referees for their helpful suggestions and useful feedback.

References

  1. 1.
    Boehm, H.-J., Weiser, M.: Garbage collection in an uncooperative environment. Softw.: Pract. Exp. 18(9), 807–820 (1988)Google Scholar
  2. 2.
    Chirimar, J., Gunter, C.A., Riecke, J.G.: Reference counting as a computational interpretation of linear logic. J. Funct. Program. 6(2), 195–244 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Clochard, M., Filliâtre, J.-C., Paskevich, A.: How to avoid proving the absence of integer overflows. In: Gurfinkel, A., et al. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 94–109. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-29613-5_6 CrossRefGoogle Scholar
  4. 4.
    George, E.: Collins: a method for overlapping and erasure of lists. Commun. ACM 3(12), 655–657 (1960)CrossRefGoogle Scholar
  5. 5.
    Felleisen, N.: On the expressive power of programming languages. In: Jones, N. (ed.) ESOP 1990. LNCS, vol. 432, pp. 35–75. Springer, Heidelberg (1990)Google Scholar
  6. 6.
    Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations (with retrospective). In: McKinley, K.S. (ed.) Best of PLDI, pp. 502–514. ACM (1993)Google Scholar
  7. 7.
    Hudak, P.: A semantic model of reference counting and its abstraction (detailed summary). In: Proceedings of 1986 ACM Conference on LISP and Functional Programming, pp. 351–363. ACM, August 1986Google Scholar
  8. 8.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  9. 9.
    Harold, J.: McBeth: On the reference counter method. Commun. ACM 6(9), 575 (1963)Google Scholar
  10. 10.
    Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: prolegomena to the design of PVS. IEEE Trans. Softw. Eng. 21(2), 107–125 (1995). PVS home page: http://pvs.csl.sri.com CrossRefGoogle Scholar
  11. 11.
    Shankar, N.: Static analysis for safe destructive updates in a functional language. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol. 2372, pp. 1–24. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Wilson, P.R.: Uniprocessor garbage collection techniques. In: Proceedings of International Workshop on Memory Management, IWMM 1992, St. Malo, France, pp. 1–42, 17–19 September 1992Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.École PolytechniquePalaiseauFrance
  2. 2.Computer Science Laboratory, SRI InternationalMenlo ParkUSA

Personalised recommendations