Part of the book series:Lecture Notes in Computer Science ((LNPSE,volume 9690))
Included in the following conference series:
1609Accesses
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 likeC.
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
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 7435
- Price includes VAT (Japan)
- Softcover Book
- JPY 9294
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Braces are used instead of square brackets to represent holes to avoid confusion with array accesses and updates.
- 2.
All proofs have been omitted due to lack of space.
- 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
Boehm, H.-J., Weiser, M.: Garbage collection in an uncooperative environment. Softw.: Pract. Exp.18(9), 807–820 (1988)
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)
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
George, E.: Collins: a method for overlapping and erasure of lists. Commun. ACM3(12), 655–657 (1960)
Felleisen, N.: On the expressive power of programming languages. In: Jones, N. (ed.) ESOP 1990. LNCS, vol. 432, pp. 35–75. Springer, Heidelberg (1990)
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)
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
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM52(7), 107–115 (2009)
Harold, J.: McBeth: On the reference counter method. Commun. ACM6(9), 575 (1963)
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
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)
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
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
École Polytechnique, Palaiseau, France
Gaspard Férey
Computer Science Laboratory, SRI International, Menlo Park, CA, 94025, USA
Natarajan Shankar
- Gaspard Férey
You can also search for this author inPubMed Google Scholar
- Natarajan Shankar
You can also search for this author inPubMed Google Scholar
Corresponding author
Correspondence toGaspard Férey.
Editor information
Editors and Affiliations
University of Minnesota, Minneapolis, Minnesota, USA
Sanjai Rayadurgam
NASA Ames Research Center , Moffett Field, California, USA
Oksana Tkachuk
Rights 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
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)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative