In operating system development, concurrency poses significant challenges. It is difficult for humans to manually review concurrent behaviors or to write test cases covering all possible executions, often resulting in critical bugs. Preemption in schedulers serves as a typical example. This paper proposes a development method for concurrent software, such as schedulers. Our method incorporates model checking as an aid for tracing code, simplifying the analysis of concurrent behavior; we refer to this as model checking-assisted code review. While this approach aids in tracing behaviors, the accuracy of the results is limited because of the semantics gap between the modeling language and the programming language. Therefore, we also introduce runtime verification to address this limitation in model checking-assisted code review. We applied our approach to a real-world operating system, Awkernel, as a case study. This new operating system, currently under development for autonomous driving, is designed for preemptive task execution using asynchronous functions in Rust. After implementing our method, we identified several bugs that are difficult to detect through manual reviews or simple tests.

翻译：在操作系统开发中，并发性带来了重大挑战。人类很难手动审查并发行为，也很难编写覆盖所有可能执行路径的测试用例，这常常导致严重错误。调度器中的抢占便是一个典型例子。本文提出了一种针对并发软件（如调度器）的开发方法。我们的方法将模型检测作为辅助代码追踪的工具，以简化对并发行为的分析；我们称之为模型检测辅助代码审查。虽然这种方法有助于追踪行为，但由于建模语言与编程语言之间的语义鸿沟，其结果的准确性受到限制。因此，我们还引入了运行时验证，以弥补模型检测辅助代码审查的这一局限。我们将我们的方法应用于一个真实世界的操作系统 Awkernel 作为案例研究。这个正在为自动驾驶开发的新操作系统，旨在利用 Rust 的异步函数实现抢占式任务执行。在实施我们的方法后，我们发现了多个难以通过人工审查或简单测试检测出的错误。