Compiling an Haskell EDSL to C: A new C back-end for the Copilot runtime verification framework
Summary
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.