Ada/SPARK on Genode

The Genode OS Framework is written in C++, but has support (to one degree or another) for writing components in several other languages. Perhaps foremost of these is Ada/SPARK, thanks in part to active development/support by Componolit, which maintains the Ada/SPARK toolset for Genode (SPARK is a subset of Ada, designed to be verifiable).

On Genodians.org, there have been three recent articles exploring the use of Ada/SPARK on Genode, each approaching the subject from a different angle.

First, in “C++ and SPARK as a Continuum“, Genode co-founder Norman Feske shows how to create hybrid C++/SPARK components. There are a few restrictions, but the results fit well with the Genode component philosophy.

By regarding C++ and SPARK as a continuum rather than an black-and-white decision, we can use SPARK at places where we regard formal verification as most valuable while not restricting Genode components to be entirely static. It gives us Genode developers the chance to slowly embrace the application of formal methods and recognize their benefit in practice.

Second, Martin Stein takes the first steps toward converting (a fork of) the in-house “base-hw” kernel to Ada in “Spunky: A Kernel Using Ada – Part 1: RPC“. This is just the beginning of this project, so stay tuned.

What should I say? Thanks to the almost pedantic need for correctness of the Ada compiler and the sheer endless chain of complains it kept throwing at me, the final image worked out of the box and put a big smile on my face.

Third, Johannes Kliemann of Componolit dives into the deep end of the pool in “SPARK as an Extremum: Components in Pure SPARK“, which describes the arduous journey that led them to create an API for creating components completely in SPARK.

With the realization that generated bindings are not feasible and both binding and API need to be created by hand, previous API limitations such as functions that are not allowed in SPARK could be removed. This API should not resemble any characteristics of any language or platform that implements it. The goal was to create a pure SPARK API for asynchronous verified components. The result is the Componolit Ada Interface, an interface collection that provides component startup, shutdown and platform interaction.

As you can see, even though the Genode core has become pretty mature, there is still much interesting research and experimentation being done on the eternal quest for more trustworthy computing.