Towards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code
summary
A minimal, purely functional DSL called Barocq compiles via Rocq to readable C by enforcing a strict alias-control discipline so the compiler does zero-cost abstractions at runtime: in-place updates, unboxed layouts, copy propagation and globalization remove needless copies. A static analysis rejects programs whose in-place semantics diverge from copy semantics. The team reimplements the S3K microkernel (~2k lines of Barocq plus some C/assembly) and measures ~3% runtime overhead (≈8% with a temporal fence); artifacts and reproduction data are available.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:31Verifiable system code motivation
- 2:18Barack DSL goals
- 5:12Barack compiler overview
- 7:02Barack buffer example
- 10:17Static analysis for updates
- 12:03Barack to readable C
- 13:28Compilation optimizations
- 14:36S3K kernel overview
- 16:24Barack S3K implementation
- 17:06S3K performance benchmarks
- 18:09Conclusion and future work
- 18:51Q&A
related talks
19mCertified Compilers à la Carte
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
42mSession with the Rocq Development Team
58mFast Cryptographic Code via Partial Evaluation
20mModern DSL compiler architecture in OCaml our experience with Catala
45mLanguage-Oriented Programming with Racket
27mCertified hardware for regexp matching: A rocq library and its workflow
59mCoq to C Translation with Partial Evaluation + Counterexample Generation