Trustworthy Systems

Connecting choreography languages with verified stacks

Authors

Alejandro Gomez-Londono and Johannes Åman Pohjola

DATA61

Chalmers University of Technology

UNSW Sydney

Abstract

With ever increasing availability of verified stacks capable of guaranteeing end-to-end correctness on applications—like compilers (CakeML, CompCert) or even critical software systems (seL4)—one can now realistically write a program, along with a proof describing any desirable property, and have it compiled into a correct executable implementation of the original program. However, most of these approaches can only really deal with sequential programs and provide no support for reasoning about the correctness of multiple (con-current) programs. To address these shortcomings, we propose a choreographic language where the behavior of a system consisting of several endpoints, is described on a global level, that can be subsequently projected and compiled into its individual components. We are developing an end-to-end proof of correctness that ensures i) the deadlock-freedom of the generated set of endpoints and ii) the preservation of all behavior of the system down to the binary level. Our implementation uses the verified CakeML compiler as a backend and takes advantages of its verified stack.

BibTeX Entry

  @misc{GomezLondono_AAmanPohjola_18,
    address          = {Oslo, Norway},
    author           = {Gomez-Londono, Alejandro and {\AA}man Pohjola, Johannes},
    booktitle        = {Nordic Workshop on Programming Theory},
    date             = {2018-10-24},
    isbn             = {9788273684509},
    month            = oct,
    note             = { at Nordic Workshop on Programming Theory},
    paperurl         = {https://trustworthy.systems/publications/full_text/GomezLondono_AAmanPohjola_18.pdf},
    publisher        = {N/A},
    title            = {Connecting Choreography Languages With Verified Stacks},
    year             = {2018}
  }

Download