CleanQ：一种轻量级、统一的、形式化指定的机器内数据传输接口
摘要：CleanQ：一种高性能的基于描述符的数据传输操作系统接口，具有严格的形式化语义，基于一个简单的、经过形式验证的所有权转移概念，并具有快速的参考实现。CleanQ旨在取代当前在操作系统内核和设备驱动程序中广泛存在的类似但细微不同且规范不明确的基于描述符的接口。CleanQ具有严格的语义，不仅清晰地解释了不同硬件设备和软件用例中接口的实现，还可以像Unix流一样组合模块。我们通过展示基于实现导出的规范不明确会导致生产系统中的安全性和正确性错误，从而激发了CleanQ的动机。我们进一步通过实验证明，对于清晰的设计，几乎没有性能成本：我们展示了操作的几十个周期的开销，并且在Linux上与经过高度调优的Virtio和DPDK实现的端到端性能相当。
作者：Roni Haecki, Lukas Humbel, Reto Achermann, David Cock, Daniel Schwyn, Timothy Roscoe
论文ID：1911.08773
分类：Operating Systems
分类简称：cs.OS
提交时间：2019-11-21