Trustworthy Systems

Do you have space for dessert? A verified space cost semantics for CakeML programs

Authors

Alejandro Gomez-Londono, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus Myreen and Yong Kiam Tan

DATA61

Carnegie Mellon University

Chalmers University of Technology

UNSW Sydney

Abstract

Garbage collectors relieve the programmer from manual memory management, but lead to compiler-generated machine code that can behave differently (e.g. out-of-memory errors) from the source code. To ensure that the generated code behaves exactly like the source code, programmers need a way to answer questions of the form: what is a sufficient amount of memory for my program to never reach an out-of-memory error? This paper develops a cost semantics that can answer such questions for CakeML programs. The work described in this paper is the first to be able to answer such questions with proofs in the context of a language that depends on garbage collection. We demonstrate that positive answers can be used to transfer liveness results proved for the source code to liveness guarantees about the generated machine code. Without guarantees about space usage, only safety results can be transferred from source to machine code. Our cost semantics is phrased in terms of an abstract intermediate language of the CakeML compiler, but results proved at that level map directly to the space cost of the compiler-generated machine code. All of the work described in this paper has been developed in the HOL4 theorem prover.

BibTeX Entry

  @inproceedings{GomezLondono_ASMT_20,
    address          = {Chicago, IL},
    author           = {Gomez-Londono, Alejandro and {\AA}man Pohjola, Johannes and Syeda, Hira Taqdees and Myreen, Magnus
                        and Tan, Yong Kiam},
    booktitle        = {OOPSLA},
    doi              = {https://doi.org/10.1145/3428272},
    month            = nov,
    pages            = {204:1-29},
    paperurl         = {https://trustworthy.systems/publications/full_text/GomezLondono_ASMT_20.pdf},
    publisher        = {ACM},
    title            = {Do You Have Space for Dessert? {A} Verified Space Cost Semantics for {CakeML} Programs},
    video            = {https://youtu.be/zDA7RrG3G04},
    volume           = {4},
    year             = {2020}
  }

Download