Skip to main content
SpringerLink
Log in

Code Generation Using a Formal Model of Reference Counting

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9690))

Included in the following conference series:

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.

This work was supported by NSF Grant CSR-EHCS(CPS)-0834810, NASA Cooperative Agreement NNA10DE73C, and by DARPA under agreement number FA8750-12-C-0284 and FA8750-16-C-0043. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of NSF, NASA, DARPA or the U.S. Government.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Braces are used instead of square brackets to represent holes to avoid confusion with array accesses and updates.

  2. 2.

    All proofs have been omitted due to lack of space.

  3. 3.

    We do not check the count for possible overflow since it would take an extraordinarily long computation to cause a 64-bit counter to overflow [3].

References

  1. Boehm, H.-J., Weiser, M.: Garbage collection in an uncooperative environment. Softw.: Pract. Exp. 18(9), 807–820 (1988)

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  4. George, E.: Collins: a method for overlapping and erasure of lists. Commun. ACM 3(12), 655–657 (1960)

    Article  Google Scholar 

  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. 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. 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 1986

    Google Scholar 

  8. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  9. Harold, J.: McBeth: On the reference counter method. Commun. ACM 6(9), 575 (1963)

    Google Scholar 

  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

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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 1992

    Google Scholar 

Download references

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.

Author information

Authors and Affiliations

  1. École Polytechnique, Palaiseau, France

    Gaspard Férey

  2. Computer Science Laboratory, SRI International, Menlo Park, CA, 94025, USA

    Natarajan Shankar

Authors
  1. Gaspard Férey
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Natarajan Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gaspard Férey .

Editor information

Editors and Affiliations

  1. University of Minnesota, Minneapolis, Minnesota, USA

    Sanjai Rayadurgam

  2. NASA Ames Research Center , Moffett Field, California, USA

    Oksana Tkachuk

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Férey, G., Shankar, N. (2016). Code Generation Using a Formal Model of Reference Counting. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40648-0_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40647-3

  • Online ISBN: 978-3-319-40648-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation