一句话：提出 Abacus 框架，用精化类型状态建模硬件-软件并发，静态阻止驱动违反设备协议。
硬件既为驱动作者规定了严格的操作规范，又提供了极为宽松的接口，驱动若想遵循设备协议，必须应对由硬件状态动态决定的合法操作集合；而现代硬件还能独立于软件并发地切换状态，进一步加剧了这一困难。本文提出 Abacus 框架，静态地防止驱动违反设备协议。Abacus 对类型状态（type-states）进行精化，以建模硬件-软件并发，并将硬件状态形式化为稳定态与瞬态两类。框架提供领域特定语言，使开发者能以数十行代码编码设备协议不变量，并借助生成的 Abacus 类型状态静态阻止协议缺陷。作者将 Abacus 集成到两个 Rust 操作系统驱动中，发现其在代码大小和运行时性能上几乎不引入开销，能静态检测设备协议违规，并使原本复杂到难以使用的硬件特性变得可用。
Hardware provides driver authors both a strict specification of the operations a driver is allowed to do, and a highly permissive interface full of operations a driver can do. Authoring drivers that adhere to the provided hardware device protocol is challenged by dynamic definitions of what a driver should do based on the hardware's state. This is further complicated by increasingly capable hardware which may transition between states concurrently and independently from the software driver. We present Abacus, a framework that statically prevents drivers from violating device protocols. Abacus refines type-states to model hardware-software concurrency and presents a formalization of hardware states into two families: stable and transient states. The Abacus framework provides a domain specific language for developers to encode device protocol invariants in tens of lines of code, and, using the generated Abacus type-states, statically prevents device protocol bugs. We demonstrate the Abacus framework's practicality by integrating it into drivers in two Rust OSes. We find that Abacus imposes minimal to no overhead in code-size and runtime performance, statically detects device protocol violations, and enables the usage of hardware features that would otherwise be prohibitively complex.
@inproceedings{PotyondyTSMA0P26,
title = {Rage Against the State Machine: Type-Stated Hardware Peripherals for Increased Driver Correctness},
author = {Tyler Potyondy and Anthony Tarbinian and Leon Schuermann and Eric Mugnier and Adin Ackerman and Amit Levy and Pat Pannuto},
booktitle = {ASPLOS},
year = {2026},
doi = {10.1145/3779212.3790207}
}