Loading [MathJax]/jax/output/SVG/jax.js
We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 22 Issue 3
May  2007
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Chun-Xiao Lin, Yi-Yun Chen, Long Li, Bei Hua. Garbage Collector Verification for Proof-Carrying Code[J]. Journal of Computer Science and Technology, 2007, 22(3): 426-437.
Citation: Chun-Xiao Lin, Yi-Yun Chen, Long Li, Bei Hua. Garbage Collector Verification for Proof-Carrying Code[J]. Journal of Computer Science and Technology, 2007, 22(3): 426-437.
shu

Garbage Collector Verification for Proof-Carrying Code

  • Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China

More Information
  • Received Date: September 18, 2006
  • Revised Date: March 19, 2007
  • Published Date: May 14, 2007
    Abstract
  • We present the verification of themachine-level implementation of a conservative variant of the standardmark-sweep garbage collector in a Hoare-style program logic. Thespecification of the collector is given on a machine-level memory modelusing separation logic, and is strong enough to preserve the safetyproperty of any common mutator program. Our verification is fullyimplemented in the Coq proof assistant and can be packed immediately asfoundational proof-carrying code package. Our work makes importantattempt toward building fully certified production-quality garbagecollectors.
    • FullText(HTML)
    • References (25)
  • [1]
    Necula G. Proof-carrying code. In -\it Proc. 24th ACM Symp. Principles of Prog. Lang}., New York, ACM Press, January 1997, pp.106∼119.
    [2]
    Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. -\it ACM Trans. Prog. Lang. and Sys.}, 1999, 21(3): 527∼568.
    [3]
    Jones R E. Garbage Collection: Algorithms for Automatic Dynamic Memory Management. Chichester: Wiley, July 1996, With a chapter on Distributed Garbage Collection by R. Lins.
    [4]
    Boehm H, Weiser M. Garbage collection in an uncooperative environment. -\it Software Practice and Exp.}, 1988, 18(9): 807∼820.
    [5]
    Feng X Y, Shao Z, Vaynberg A -\it et al}. Modular verification of assembly code with stack-based control abstractions. In -\it Proc. 2006 ACM Conf. Prog. Lang. Design and Impl.}, Ottawa, Canada, June 2006, ACM Press, pp.401∼414.
    [6]
    Reynolds J C. Separation logic: A logic for shared mutable data structures. In -\it Proc. 17th IEEE Symp. Logic in Comp. Sci}., Washington DC, USA, IEEE Comp. Soc., 2002, pp.55∼74.
    [7]
    Coq Development Team. The Coq proof assistant reference manual. Coq release v8.0, October 2005.
    [8]
    Appel A W. Foundational proof-carrying code. In -\it Proc. 16th IEEE Symp. Logic in Comp. Sci.}, IEEE Comp. Soc., Boston, USA, June 2001, pp.247∼258.
    [9]
    Feng X, Ni Z, Shao Z, Guo Y. An open framework for foundational proof-carrying code. In -\it Proc. 3rd ACM SIGPLAN Workshop on Types in Lang. Design and Impl.}, Nice, France, ACM Press, January 2007, pp.67∼78.
    [10]
    McCreight A, Shao Z, Lin C, Li L. A General Framework for Certifying Garbage Collectors and Their Mutators. In -\it Proc. 2007 ACM SIGPLAN Conf. Prog. Lang. Design and Impl.}, San Diego, CA, USA, June 2007, ACM Press. (Paper to appear)
    [11]
    Lin C, McCreight A, Shao Z, Chen Y, Guo Y. Foundational typed assembly language with certified garbage collection. In -\it Proc. 1st IEEE & IFIP International Symp. Theoretical Aspects of Soft. Eng.}, Shanghai, China, June 2007, IEEE Comp. Soc. (Paper to appear)
    [12]
    Lin C, Chen Y, Li L, Hua B. Garbage collector verification for proof-carrying code (documents and Coq implementation). 2006, http://ssg.ustcsz.edu.cn/∼cxlin/gcpaper/.
    [13]
    C Paulin-Mohring. Inductive definitions in the system Coq---Rules and properties. In -\it Proc. 1st Int. Conf. Typed Lambda Calculi and Applications}, Utrecht, The Netherlands, -\it LNCS}, Vol.664, Springer-Verlag, 1993, pp.328∼345.
    [14]
    MIPS Technologies, Inc. MIPS32--\rm TM}} Architecture for Programmers Volume II: The MIPS32--\rm TM}} Instruction Set. v2.50.
    [15]
    Birkedal L, Torp-Smith N, Reynolds J C. Local reasoning about a copying garbage collector. In -\it Proc. 31st ACM Symp. Principles of Prog. Lang.}, New York, USA, ACM Press, 2004, pp.220∼231.
    [16]
    Howard W A. The formulas-as-types notion of construction. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, 1980, pp.479∼490.
    [17]
    Marti N, Affeldt R, Yonezawa A. Formal verification of the heap manager of an operating system using separation logic. In -\it Proc. ICFEM2006, Lecture Notes in Computer Science}, Volume 4260, Canberra, September 1998, Springer-Verlag, pp.225∼244.
    [18]
    Dijkstra E W, Lamport L, Martin A J -\it et al}. On-the-fly garbage collection: An exercise in cooperation. -\it Commun. ACM}, 1978, 21(11): 966∼975.
    [19]
    Ben-Ari M. Algorithms for on-the-fly garbage collection. -\it ACM Trans. Prog. Lang. and Sys.}, 1984, 6(3): 333∼344.
    [20]
    Russinoff D M. A mechanically verified incremental garbage collector. -\it Formal Aspects of Computing}, 1994, 6: 359∼390.
    [21]
    Jackson P. Verifying a garbage collection algorithm. In -\it Proc. 11th Int. Conf. Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science}, Canberra, Australia, Volume 1479, Springer-Verlag, 2006, pp.225∼244.
    [22]
    L. Burdy. B vs. Coq to prove a garbage collector. In -\it Proc. 14th Int. Conf. Theorem Proving in Higher Order Logics}, Edinburgh, UK, Boulton R J, Jackson P B (eds.), September 2001, pp.85∼97.
    [23]
    Wang D C, Appel A W. Type-preserving garbage collectors. In -\it Proc. 28th ACM Symp. Principles of Prog. Lang.}, New York, USA, ACM Press, 2001, pp.166∼178.
    [24]
    Monnier S, Saha B, Shao Z. Principled scavenging. In -\it Proc. 2001 ACM Conf. Prog. Lang. Design and Impl.}, New York, ACM Press, 2001, pp.81∼91.
    [25]
    Hawblitzel C, Huang H, Wittie L, Chen J. A garbage-collecting typed assembly language. In -\it Proc. The Third ACM SIGPLAN Workshop on Types in Language Design and Implementation}, Nice, France, ACM Press, January 2007, pp.41∼52.
    • Relative Articles

  • Related Articles

    [1]Yu Guo, Xin-Yu Jiang, Yi-Yun Chen. Certification of Thread Context Switching[J]. Journal of Computer Science and Technology, 2010, 25(4): 827-840. DOI: 10.1007/s11390-010-1064-9
    [2]Long Li, Yu Zhang, Yi-Yun Chen, Yong Li. Certifying Concurrent Programs Using Transactional Memory[J]. Journal of Computer Science and Technology, 2009, 24(1): 110-121.
    [3]Lin Hong, Chen Guoliang. Program Constructionby Verifying Specification[J]. Journal of Computer Science and Technology, 1998, 13(6): 597-607.
    [4]Zhou Qihai. An Improved Graphic Representation for Structured Program Design[J]. Journal of Computer Science and Technology, 1991, 6(2): 205-208.
    [5]Zhu Hong. Program Transformation by Solving Equations[J]. Journal of Computer Science and Technology, 1991, 6(2): 167-177.
    [6]Zhu Hong, Jin Lingzi. A Knowledge-Based Approach to Program Synthesis from Examples[J]. Journal of Computer Science and Technology, 1991, 6(1): 47-58.
    [7]Li Wei. A Type-Theoretic Approach to Program Development[J]. Journal of Computer Science and Technology, 1990, 5(3): 209-224.
    [8]Lu Qi, Zhang Fubo, Qian Jiahua. Program Slicing:Its Improved Algorithm and Application in Verification[J]. Journal of Computer Science and Technology, 1988, 3(1): 29-39.
    [9]Hou Luoming. A General and Formal Method for the Program Static Analysis[J]. Journal of Computer Science and Technology, 1987, 2(2): 115-123.
    [10]Tang Tonggao, Zhao Zhaokeng. Stack Method in Program Semantics[J]. Journal of Computer Science and Technology, 1987, 2(1): 51-63.
    • Supplements (0)

Catalog

    Get Citation
    XML
    Article views (27) PDF downloads (4517) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return