Compiling an Haskell EDSL to C: A new C back-end for the Copilot runtime verification framework

Abstract

Electronics and computers are all around us, ranging from cellphones to aircraft avionics. Some systems, including aircraft and nuclear powerplants, are considered safety-critical: failure can lead to the injury or death of humans. These ultra-critical systems require a very small probability of failure (<10^-9), and are strictly certified by regulatory bodies.

Static software verification can aid in improving the safety of these systems, but only scales for a limited number of properties. Functional verification often requires the use of interactive theorem provers and are not practical for industrial scale systems. There is also a push to apply highly nondeterministic techniques such as machine learning in safety-critical systems, which cannot be verified using traditional proof techniques. Runtime verification, where specifications are checked during execution can allow us to verify software systems that cannot be verified by other means. The Haskell based Copilot runtime verification framework has been developed as part of a NASA project applying runtime verification to real-time embedded C programs. A lack of first class support for arrays and structs limited Copilot's practical usability. By replacing the current Atom and SBV-based code generation back-ends by a new, custom designed one, we are able to implement both arrays and structs as first class members of our specification. Both C structs and arrays are not straightforward to represent in Haskell, and require special attention. In particular type literals have been used to implement a safer array than Haskell normally allows.

Having native support for structs and arrays simplifies monitor specifications, and makes writing them easier and quicker. In addition, a tailored code generator also allows us to improve on the readability of the generated output code, making debugging and tracing easier, which in the end aids in making systems safer.