We are convinced that formally specified Domain-Specific Languages (DSLs) can foster a new way of designing reliable operating systems. Traditionally, safety is enforced in a top-down manner: the system is implemented in a high-level language and proved correct in this formalism. Then, a sequence of proofs shows that this correctness is preserved along the way to machine code.
However, this approach is not practical for commodity operating systems. Therefore, we advocate a bottom-up approach: while developing the operating system, we are to face repeating patterns that would deserve to be abstracted away and formalized. Driver interactions or communication interfaces are two such examples.
By defining a DSL per problem, we are able to address these two issues at the same time: first, we abstract the low-level details behind semantically-rich DSL constructs and, second, we formalize the problems thanks to a mechanized semantics. Unlike the top-down approach that aims at solving all problems at once, we propose a philosophy of small-steps, in which abstractions are iteratively built and stacked up.
This lead us to design Filet-o-Fish (FoF), as a language to specify the semantics of DSLs. As a side-effect of its extreme precision, FoF can also be compiled to C. Therefore, DSL compilers can entirely rely on FoF to implement the back-end, which transforms a processed input into C. Not only does FoF provide a formal ground to DSLs but it also considerably eases their development.
To support our claims, we have developed two DSLs, Fugu and Hamlet. Fugu is a self-contained proof-of-concept that conveys the essence of FoF design philosophy. Beyond the pedagogical interest, it also alleviates the difficult problem of error management in an operating system. Hamlet, on the other hand, is a full-featured DSL: it aims at automatically generating the resource accounting infrastructure from a set of declarative rules. Because resource management is safety-critical, Hamlet also demonstrates how FoF can be leveraged to reason at a higher-level thanks to its mechanized semantics. A correctness proof of the FoF-to-C compiler backs our position: we do not have to reason about C code anymore and we can conveniently reason about FoF code only, being ensured that the generated C code respects the FoF semantic.