CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A verified generational garbage collector for CakeML

Adam Sandberg Eriksson (Institutionen för data- och informationsteknik (Chalmers)) ; Magnus O. Myreen (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)) ; Johannes Åman Pohjala (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers))
Lecture Notes in Computer Science: 8th International Conference on Interactive Theorem Proving, ITP 2017; Brasilia; Brazil; 26 September 2017 through 29 September 2017 (03029743). Vol. 10499 LNCS (2017), p. 444-461.
[Konferensbidrag, refereegranskat]

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.



Denna post skapades 2017-10-02.
CPL Pubid: 252200

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)