A Verified Generational Garbage Collector for CakeML

被引:8
作者
Ericsson, Adam Sandberg [1 ]
Myreen, Magnus O. [1 ]
Pohjola, Johannes Aman [2 ]
机构
[1] Chalmers Univ Technol, Gothenburg, Sweden
[2] Data61 CSIRO, Sydney, NSW, Australia
基金
瑞典研究理事会;
关键词
Interactive theorem proving; Formal methods; Garbage collection; Compiler verification;
D O I
10.1007/s10817-018-9487-z
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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
页数:26
相关论文
共 20 条
[1]  
Anand A, 2017, COQ PROGRAMMING LANG
[2]   The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it) [J].
Davis, Jared ;
Myreen, Magnus O. .
JOURNAL OF AUTOMATED REASONING, 2015, 55 (02) :117-183
[3]   ON-FLY GARBAGE COLLECTION - EXERCISE IN COOPERATION [J].
DIJKSTRA, EW ;
LAMPORT, L ;
MARTIN, AJ ;
SCHOLTEN, CS ;
STEFFENS, EFM .
COMMUNICATIONS OF THE ACM, 1978, 21 (11) :966-975
[4]   A Verified Generational Garbage Collector for CakeML [J].
Ericsson, Adam Sandberg ;
Myreen, Magnus O. ;
Pohjola, Johannes Aman .
INTERACTIVE THEOREM PROVING (ITP 2017), 2017, 10499 :444-461
[5]  
Gammie P, 2015, ACM SIGPLAN NOTICES, V50, P99, DOI [10.1145/2813885.2738006, 10.1145/2737924.2738006]
[6]  
Gonthier G., 1996, LECT NOTES COMPUTER, V1102
[7]  
Harrison J, 2005, LECT NOTES COMPUT SC, V3603, P114
[8]  
Hawblitzel C., 2014, S OP SYST DES IMPL, P165
[9]  
Hawblitzel C, 2010, LOG METH COMPUT SCI, V6
[10]  
McCreight A., 2008, THESIS