A Verified Generational Garbage Collector for CakeML

被引:0
|
作者
Adam Sandberg Ericsson
Magnus O. Myreen
Johannes Åman Pohjola
机构
[1] Chalmers University of Technology,
[2] Data61/CSIRO,undefined
来源
Journal of Automated Reasoning | 2019年 / 63卷
关键词
Interactive theorem proving; Formal methods; Garbage collection; Compiler verification;
D O I
暂无
中图分类号
学科分类号
摘要
This paper presents the verification of a generational copying garbage collector for the CakeML runtime system. The proof is split into an algorithm proof and an implementation proof. The algorithm proof follows the structure of the informal intuition for the generational collector’s correctness, namely, a partial collection cycle in a generational collector is the same as running a full collection on part of the heap, if one views pointers to old data as non-pointers. We present a pragmatic way of dealing with ML-style mutable state, such as references and arrays, in the proofs. The development has been fully integrated into the in-logic bootstrapped CakeML compiler, which now includes command-line arguments that allow configuration of the generational collector. All proofs were carried out in the HOL4 theorem prover.
引用
收藏
页码:463 / 488
页数:25
相关论文
共 50 条
  • [21] Performance Comparative Analysis on Garbage First Garbage Collector and Z Garbage Collector
    Zhang, Jiayi
    2021 IEEE 3rd International Conference on Frontiers Technology of Information and Computer, ICFTIC 2021, 2021, : 733 - 740
  • [22] Optimal tenuring collection times for a generational garbage collector based on continuous damage model
    Nakagawa, T. (toshi-nakagawa@aitech.ac.jp), 1600, RAMS Consultants (09):
  • [23] Verified Compilation of CakeML to Multiple Machine-Code Targets
    Fox, Anthony
    Myreen, Magnus O.
    Tan, Yong Kiam
    Kumar, Ramana
    PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17, 2017, : 125 - 137
  • [24] The CakeML Compiler Explorer Tracking Intermediate Representations in a Verified Compiler
    Hjort, Rikard
    Holmgren, Jakob
    Persson, Christian
    TRENDS IN FUNCTIONAL PROGRAMMING (TFP 2017), 2018, 10788 : 135 - 148
  • [25] PARALLEL GENERATIONAL GARBAGE COLLECTION
    SHARMA, R
    SOFFA, ML
    SIGPLAN NOTICES, 1991, 26 (11): : 16 - 32
  • [26] Garbage collector in Paris
    Le Lay, Stephane
    TRAVAIL GENRE ET SOCIETES, 2015, (33): : 105 - +
  • [27] Complementary garbage collector
    Matsui, S
    Tanaka, Y
    Maeda, A
    Nakanishi, M
    MEMORY MANAGEMENT, 1995, 986 : 163 - 177
  • [28] CALCULATING A GARBAGE COLLECTOR
    BERGER, U
    MEIXNER, W
    MOLLER, B
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 544 : 137 - 192
  • [29] Hot-swapping between a Mark&Sweep and a Mark&Compact garbage collector in a generational environment
    Printezis, T
    USENIX ASSOCIATION PROCEEDINGS JAVA(TM) VIRTUAL MACHINE RESEARCH AND TECHNOLOGY SYMPOSIUM, 2001, : 171 - 184
  • [30] A generational parallel garbage collection for CMP
    Yang, Bin
    ICIC Express Letters, 2011, 5 (11): : 4203 - 4208