Article

Formal semantics of weak references

Authors:

Kevin Donnelly,

Assaf KfouryAuthors Info & Claims

ISMM '06: Proceedings of the 5th international symposium on Memory management

Pages 126 - 137

https://doi.org/10.1145/1133956.1133974

Published: 10 June 2006 Publication History

Abstract

Weak references are references that do not prevent the object they point to from being garbage collected. Many realistic languages, including Java, SML/NJ, and Haskell to name a few, support weak references. However, there is no generally accepted formal semantics for weak references. Without such a formal semantics it becomes impossible to formally prove properties of such a language and the programs written in it.We give a formal semantics for a calculus called λ_weak that includes weak references and is derived from Morrisett, Felleisen, and Harper's λgc. The semantics is used to examine several issues involving weak references. We use the framework to formalize the semantics for the key/value weak references found in Haskell. Furthermore, we consider a type system for the language and show how to extend the earlier result that type inference can be used to collect reachable garbage. In addition we show how to allow collection of weakly referenced garbage without incurring the computational overhead often associated with collecting a weak reference which may be later used. Lastly, we address the non-determinism of the semantics by providing both an effectively decidable syntactic restriction and a more general semantic criterion, which guarantee a unique result of evaluation.

References

[1]

APPEL, A. W. Runtime tags aren't necessary. Lisp and Symbolic Computation 2, 2 (1989), 153--162.

[2]

BAKER, H. G. Unify and conquer. In LFP '90: Proceedings of the 1990 ACM conference on LISP and functional programming (New York, NY, USA, 1990), ACM Press, pp. 218--226.

Digital Library

[3]

CHAILLOUX, E., MANOURY, P., AND PAGANO, B. Developing Applications with Objective Caml. O'Reilly, France, 2000.

[4]

DONNELLY, K., AND KFOURY, A. J. Some considerations on formalsemantics for weak references. Technical Report Don+Kfo:BUCS-TR-2005-X, Department of Computer Science, Boston University,July 2005. http://types.bu.edu/reports/Don+Kfo:BUCS-TR-2005-X.html.

[5]

HALLETT, J. J., AND KFOURY, A. J. A formal semantics for weak references. Technical Report Hal+Kfo:BUCS-TR-2005-X, Department of Computer Science, Boston University, May 2005. http://types.bu.edu/reports/Hal+Kfo:BUCS-TR-2005-X.html.

[6]

HAYES, B. Ephemerons: a new finalization mechanism. In OOPSLA'97: Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (New York, NY, USA, 1997), ACM Press, pp. 176--183.

Digital Library

[7]

THE HUGS/GHC TEAM. Hugs/GHC Extension Libraries: Weak. http://www.dcs.gla.ac.uk/fp/software/ghc/lib/hg-libs-15.html.

[8]

PEYTON JONES, S. L., MARLOW, S., AND ELLIOTT, C. Stretching the storage manager: Weak pointers and stable names in haskell. In IFL '99: Selected Papers from the 11th International Workshop on Implementation of Functional Languages (London, UK, 2000), Springer-Verlag, pp. 37--58.

Digital Library

[9]

MERIZEN, F., ZENDRA, O., AND COLNET, D. Designing efficient and safe non-strong references in eiffel with parametric types. Research Report A04-R-149, INRIA Lorraine / LORIA UMR 7503, Sep 2004.

[10]

MORRISETT, G., FELLEISEN, M., AND HARPER, R. Abstract models of memory management. In FPCA '95: Proceedings of the seventh international conference on Functional programming languages and computer architecture (New York, NY, USA, 1995), ACM Press, pp. 66--77.

Digital Library

[11]

MORRISETT, G., AND HARPER, R. Semantics of memory management for polymorphic languages. In Higer Order Operational Techniques in Semantics, A. Gordon and A. Pitts, Eds. Newton Institute, Cambridge University Press, 1997.

Digital Library

[12]

THE SMLOFNJ TEAM. SML of NJ Structure Documentation: The WEAK signature. http://www.smlnj.org/doc/SMLofNJ/pages/weak.html.

[13]

SUN MICROSYSTEMS. Java 2 Platform SE v1.3.1: package java.lang.ref. http://java.sun.com/j2se/1.3/docs/api/java/lang/ref/packagesummary.html.

[14]

TOLMACH, A. P. Tag-free garbage collection using explicit type parameters. In LISP and Functional Programming (1994), pp. 1--11.

Digital Library

[15]

WRIGHT, A. K., AND FELLEISEN, M. A syntactic approach to type soundness. Information and Computation 115, 1 (1994), 38--94.

Digital Library

Cited By

Yamazaki TNakamaru TShioya RUgawa TChiba S(2023)Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake?Proceedings of the ACM on Programming Languages10.1145/35912447:PLDI(591-614)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591244
Soldevila MZiliani BSilvestre B(2022)From Specification to Testing: Semantics Engineering for Lua 5.2Journal of Automated Reasoning10.1007/s10817-022-09638-y66:4(905-952)Online publication date: 11-Aug-2022
https://doi.org/10.1007/s10817-022-09638-y
Prabhu PBeard SApostolakis SZaks AAugust DEvripidou SStenström PO'Boyle M(2018)MemoDynProceedings of the 27th International Conference on Parallel Architectures and Compilation Techniques10.1145/3243176.3243193(1-12)Online publication date: 1-Nov-2018
https://dl.acm.org/doi/10.1145/3243176.3243193
Show More Cited By

Index Terms

Formal semantics of weak references
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

A calculus for java's reference objects

Java's Reference objects provide the programmer with limited control over the process of memory management. Although reference objects are often helpful, they introduce nondeterminism into program evaluation and lead to ambiguous program outcome. In ...
The formal semantics of SDL-2000: status and perspectives
ITU-T system design languages (SDL)

In November 1999, the current version of specification and description language (SDL), commonly referred to as SDL-2000, passed through ITU-T. In November 2000, the formal semantics of SDL- 2000 was officially approved to become part of the SDL language ...
A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification
FormaliSE '24: Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)

ACSL is a behavioral interface specification language for C. It is used by Frama-C, a framework including several formal methods-based techniques for verifying C code with respect to ACSL annotations. Currently, there is no formal definition of the ACSL ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISMM '06: Proceedings of the 5th international symposium on Memory management

June 2006

202 pages

ISBN:1595932216

DOI:10.1145/1133956

General Chair:
Erez Petrank
Technion - Israel Institute of Technology
,
Program Chair:
Eliot Moss
University of Massachusetts, Amherst

Copyright © 2006 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 June 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ISMM06

Sponsor:

ISMM06: The 2006 International Symposium on Memory Management

June 10 - 11, 2006

Ontario, Ottawa, Canada

Acceptance Rates

Overall Acceptance Rate 72 of 156 submissions, 46%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
270
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)3

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yamazaki TNakamaru TShioya RUgawa TChiba S(2023)Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake?Proceedings of the ACM on Programming Languages10.1145/35912447:PLDI(591-614)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591244
Soldevila MZiliani BSilvestre B(2022)From Specification to Testing: Semantics Engineering for Lua 5.2Journal of Automated Reasoning10.1007/s10817-022-09638-y66:4(905-952)Online publication date: 11-Aug-2022
https://doi.org/10.1007/s10817-022-09638-y
Prabhu PBeard SApostolakis SZaks AAugust DEvripidou SStenström PO'Boyle M(2018)MemoDynProceedings of the 27th International Conference on Parallel Architectures and Compilation Techniques10.1145/3243176.3243193(1-12)Online publication date: 1-Nov-2018
https://dl.acm.org/doi/10.1145/3243176.3243193
Kaylor JLaufer KThiruvathukal G(2012)Simplifying domain modeling and memory management in user-mode filesystems with the NOFS framework2012 IEEE International Conference on Electro/Information Technology10.1109/EIT.2012.6220733(1-6)Online publication date: May-2012
https://doi.org/10.1109/EIT.2012.6220733
Gabay YKfoury A(2007)A calculus for java's reference objectsACM SIGPLAN Notices10.1145/1294297.129429942:8(9-17)Online publication date: 1-Aug-2007
https://dl.acm.org/doi/10.1145/1294297.1294299

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents