一句话：为 Ziria 无线协议语言建立核心语言、操作语义与类型系统，并据此提出融合与流水线合并变换，实现更快的编译器。
软件定义无线电希望将软件的灵活迭代带入无线协议设计，但高数据率与时序要求使高层语言难以胜任；原 Ziria 编译器虽证明可行，却缺少形式语义，成功经验难以复用。本文首先为 Ziria 给出核心语言、操作语义与类型系统，并由此设计两种程序变换：融合可消除 Ziria 程序中的中间队列，流水线合并通过批处理 IO 降低执行开销，且后者依赖融合并简化了原编译器的“向量化”。基于这些变换，作者实现新的 Ziria 编译器，利用中间语言减少不必要的内存流量，生成代码显著快于原编译器。该工作既为 Ziria 奠定形式基础，也表明操作语义能带来实际软件工程收益，其核心语言与变换可用于其他高速流数据处理领域。
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.
@article{Mainland17,
title = {Better living through operational semantics: an optimizing compiler for radio protocols},
author = {Geoffrey Mainland},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110263}
}