Trustworthy Systems

Bringing effortless refinement of data layouts to Cogent

Authors

Liam O'Connor, Zilin Chen, Partha Susarla Ajay, Christine Rizkallah, Gerwin Klein and Gabriele Keller

DATA61

UNSW Sydney

Abstract

The language Cogent allows low-level operating system components to be modelled as pure mathematical functions operating on algebraic data types, which makes it highly suitable for verification in an interactive theorem prover. Furthermore, the Cogent compiler translates these models into imperative C programs, and provides a proof that this compilation is a refinement of the functional model. There remains a gap, however, between the C data structures used in the operating system, and the algebraic data types used by Cogent . This forces the programmer to write a large amount of boilerplate marshalling code to connect the two, which can lead to a significant runtime performance overhead due to excessive copying. In this paper, we outline our design for a data description language and data refinement framework, called Dargent, which provides the programmer with a means to specify how Cogent represents its algebraic data types. From this specification, the compiler can then generate the C code which manipulates the C data structures directly. Once fully realised, this extension will enable more code to be automatically verified by Cogent, smoother interoperability with C, and substantially improved performance of the generated code.

BibTeX Entry

  @inproceedings{OConnorDavis_CSRKK_18,
    address          = {Limassol, Cyprus},
    author           = {O'Connor, Liam and Chen, Zilin and Susarla Ajay, Partha and Rizkallah, Christine and Klein, Gerwin
                        and Keller, Gabriele},
    booktitle        = {International Symposium on Leveraging Applications of Formal Methods, Verification and Validation},
    date             = {2018-11-5},
    doi              = {https://doi.org/10.1007/978-3-030-03418-4\_9},
    month            = nov,
    pages            = {134-149},
    paperurl         = {https://trustworthy.systems/publications/full_text/OConnorDavis_CSRKK_18.pdf},
    publisher        = {Springer},
    title            = {Bringing Effortless Refinement of Data Layouts to {Cogent}},
    year             = {2018}
  }

Download