Validating direct memory access interfaces with conformance checking
Validating direct memory access interfaces with conformance checking
复制标题
通过一致性检查验证直接内存访问接口
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Fei Xie
中科院分区：
文献类型：
--
作者：
Li Lei;Kai Cong;Zhenkun Yang;Fei Xie
直接存储器访问（DMA）接口是外围设备及其设备驱动程序之间的硬件/软件（HW/SW）接口的常见且重要的组成部分。我们提出了一个硬件/软件协同验证框架来验证设备及其驱动程序的DMA接口实现。该框架采用设备的虚拟原型作为参考模型，并分两个阶段执行协同验证：（1）一致性检查，检查设备与其虚拟原型之间的DMA接口一致性;（2）属性检查，检查设备/驱动程序跨DMA接口的交互。在一致性检查中，虚拟原型通过将相同的驱动程序请求序列带到设备来推断设备状态转换。属性检查验证通过虚拟原型公开的设备状态转换上的系统属性。该框架通过检测设备和驱动程序中的DMA接口错误来辅助硬件/软件集成验证。此外，我们已经开发了三个关键技术：捕获写策略，部分捕获和环境输入预测，以解决两个主要的挑战，在扩展框架：DMA捕获开销和不精确的环境输入模拟。我们已经将这种方法应用于四个以太网适配器，发现12个严重的DMA接口错误的设备，他们的虚拟原型和驱动程序。结果表明，我们的方法有很大的潜力，在促进硬件/软件协同验证。
Direct Memory Access (DMA) interfaces are a common and important component of Hardware/Software (HW/SW) interfaces between peripheral devices and their device drivers. We present a HW/SW co-validation framework to validate DMA interface implementations of a device and its driver. This framework employs a virtual prototype of the device as a reference model and performs co-validation in two stages: (1) conformance checking which checks the DMA interface conformance between the device and its virtual prototype; (2) property checking which checks device/driver interactions across the DMA interface. In conformance checking, the virtual prototype infers the device state transitions by taking the same driver request sequence to the device. Property checking verifies system properties over the device state transitions exposed through the virtual prototype. This framework assists HW/SW integration validation by detecting DMA interface bugs in both devices and drivers. Furthermore, we have developed three key techniques: capture-on-write policy, partial capture, and environmental input prediction, to address two major challenges in scaling the framework: DMA capture overhead and imprecise environmental input simulation. We have applied this approach to four Ethernet adapters, discovering 12 serious DMA interface bugs from the devices, their virtual prototypes and their drivers. The results demonstrate that our approach has major potential in facilitating HW/SW co-validation.