Bringing Effortless Refinement of Data Layouts to Cogent

  • Liam O’ConnorEmail author
  • Zilin Chen
  • Partha Susarla
  • Christine Rizkallah
  • Gerwin Klein
  • Gabriele Keller
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11244)


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.


  1. 1.
    Amani, S., et al.: Cogent: verifying high-assurance file system implementations. In: International Conference on Architectural Support for Programming Languages and Operating Systems, Atlanta, GA, USA, pp. 175–188, April 2016Google Scholar
  2. 2.
    Back, G.: DataScript- a specification and scripting language for binary data. In: Batory, D., Consel, C., Taha, W. (eds.) GPCE 2002. LNCS, vol. 2487, pp. 66–77. Springer, Heidelberg (2002). Scholar
  3. 3.
    Bangert, J., Zeldovich, N.: Nail: a practical tool for parsing and generating data formats. In: Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, pp. 615–628. USENIX Association, Broomfield (2014). presentation/bangert
  4. 4.
    Chen, Z.: Cogent\(^{\Uparrow }\): giving systems engineers a stepping stone (extended abstract). In: The 2017 ACM SIGPLAN Workshop on Type-driven Development (ICFP TyDe 2017) (2017).
  5. 5.
    Cock, D.: Bitfields and tagged unions in C – verification through automatic generation. In: Proceedings of the 5th International Verification Workshop, Sydney, pp. 44–55, August 2008Google Scholar
  6. 6.
    Fisher, K., Gruber, R.: PADS: a domain-specific language for processing ad hoc data. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 295–304. ACM, New York (2005). Scholar
  7. 7.
    Fisher, K., Mandelbaum, Y., Walker, D.: The next 700 data description languages. J. ACM 57(2), 10:1–10:51. Scholar
  8. 8.
    Fisher, K., Walker, D.: The PADS project: an overview. In: Proceedings of the 14th International Conference on Database Theory, pp. 11–17. ACM, New York (2011).
  9. 9.
    Keller, G., et al.: File systems deserve verification too! In: Workshop on Programming Languages and Operating Systems (PLOS), Farmington, Pennsylvania, USA, pp. 1–7, November 2013Google Scholar
  10. 10.
    Klein, G., et al.: seL4: formal verification of an OS kernel. In: ACM Symposium on Operating Systems Principles, pp. 207–220. ACM, Big Sky, October 2009Google Scholar
  11. 11.
    Klein, G., Sewell, T., Winwood, S.: Refinement in the formal verification of the seL4 microkernel. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323–339. Springer, Boston (2010). Scholar
  12. 12.
    McCann, P.J., Chandra, S.: PacketTypes: abstract specification of network protocol messages. In: Proceedings of the ACM Conference on Communications, pp. 321–333. ACM, New York (2000).
  13. 13.
    O’Connor, L., et al.: Refinement through restraint: bringing down the cost of verification. In: International Conference on Functional Programming, Nara, Japan, September 2016Google Scholar
  14. 14.
    Rizkallah, C., et al.: A framework for the automatic formal verification of refinement from Cogent to C. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 323–340. Springer, Cham (2016). Scholar
  15. 15.
    de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. No. 47 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1998)Google Scholar
  16. 16.
    Schirmer, N.: Verification of sequential imperative programs in Isabelle/HOL. Ph.D. thesis, Technische Universität München (2006)Google Scholar
  17. 17.
    Tuch, H.: Formal memory models for verifying C systems code. Ph.D. thesis, UNSW, Sydney, Australia, August 2008Google Scholar
  18. 18.
    Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, pp. 97–108. ACM, January 2007Google Scholar
  19. 19.
    Wang, Y., Gaspes, V.: An embedded language for programming protocol stacks in embedded systems. In: Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 63–72. ACM, New York (2011).

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Liam O’Connor
    • 1
    Email author
  • Zilin Chen
    • 1
    • 2
  • Partha Susarla
    • 2
  • Christine Rizkallah
    • 1
  • Gerwin Klein
    • 1
    • 2
  • Gabriele Keller
    • 1
  1. 1.UNSW AustraliaSydneyAustralia
  2. 2.Data61, CSIRO (Formerly NICTA)SydneyAustralia

Personalised recommendations