Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Software-defined radio (SDR) promises to bring the flexibility and rapid iterative workflow of software to radio protocol design. Many factors make achieving this promise challenging, not least of which are the high data rates and timing requirements of real-world radio protocols. The Ziria language and accompanying compiler demonstrated that a high-level language can compete in this demanding space, but extracting reusable lessons from this success is difficult due to Ziria's lack of a formal semantics. Our first contribution is a core language, operational semantics, and type system for Ziria.
The insight we gained through developing this operational semantics led to our second contribution, consisting of two program transformations. The first is fusion, which can eliminate intermediate queues in Ziria programs. Fusion subsumes many one-off optimizations performed by the original Ziria compiler. The second transformation is pipeline coalescing, which reduces execution overhead by batching IO. Pipeline coalescing relies critically on fusion and provides a much simpler story for the original Ziria compiler's "vectorization" transformation. These developments serve as the basis of our third contribution, a new compiler for Ziria that produces significantly faster code than the original compiler. The new compiler leverages our intermediate language to help eliminate unnecessary memory traffic.
As well as providing a firm foundation for the Ziria language, our work on an operational semantics resulted in very real software engineering benefits. These benefits need not be limited to SDR—the core language and accompanying transformations we present are applicable to other domains that require processing streaming data at high speed.
Tue 5 SepDisplayed time zone: Belfast change
10:30 - 12:00
|Persistence for the Masses: RRB-Vectors in a Systems Language
Juan Pedro Bolívar Puente Independent Consultant, Sinusoidal EngineeringDOI Pre-print
|Verified Low-Level Programming Embedded in F*
Jonathan Protzenko Microsoft Research, n.n., Jean-Karim Zinzindohoué Inria, France, Aseem Rastogi Microsoft Research, Tahina Ramananandro Microsoft Research, n.n., Peng Wang Massachusetts Institute of Technology, USA, Santiago Zanella-Béguelin Microsoft Research, n.n., Antoine Delignat-Lavaud Microsoft Research, n.n., Cătălin Hriţcu Inria Paris, Karthikeyan Bhargavan Inria, France, Cédric Fournet Microsoft Research, n.n., Nikhil Swamy Microsoft Research, n.n.DOI
|Verifying Efficient Function Calls in CakeML
Scott Owens University of Kent, UK, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan Carnegie Mellon University, USADOI
|Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Geoffrey Mainland Drexel University, USADOI