Pierre-Evariste Dagand, Andrew Baumann, and Timothy Roscoe
We address a persistent problem with using domain-specific languages to write operating systems: the effort of implementing, checking, and debugging the DSL usually outweighs any of its benefits. Because these DSLs generate C by templated string concatenation, they are tedious to write, fragile, and incompatible with automated verification tools.
We present Filet-o-Fish (FoF), a semantic language to ease DSL construction. Building a DSL using FoF consists of safely composing semantically-rich building blocks. This has several advantages: input files for the DSL are formal specifications of the system’s functionality, automated testing of the DSL is possible via existing tools, and we can prove that the C code generated by a given DSL respects the semantics expected by the developer.
Early experience has been good: FoF is in daily use as part of the tool chain of the Barrelfish multicore OS, which makes extensive use of domain-specific languages to generate low-level OS code. We have found that the ability to rapidly generate DSLs we can
rely on has changed how we have designed the OS.
In Proceedings of the 5th Workshop on Programming Languages and Operating Systems
|Address||Big Sky, MT, USA|