A Case Study on Model Checking and Runtime Verification for Awkernel

TL;DR

The paper addresses the challenge of verifying concurrent operating-system components for autonomous driving by proposing a development method that combines model checking-assisted code review with runtime verification. It applies this approach to Awkernel, a Rust-based OS, by translating code line-by-line into Promela for Spin-driven model checking and embedding a DFA-based monitor for runtime verification. The authors identify two concurrency bugs—one related to preemption timing and another to task transitions—and demonstrate how the hybrid approach helps uncover issues that are hard to detect through manual review alone. While effective in practice, the approach contends with semantic gaps between Rust and Promela and substantial computational resource requirements, highlighting both its utility and its limitations for real-world OS development.

Abstract

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.

Figures (9)

• Figure 1: Overview of task scheduling and interrupt handling. The primary core does not execute tasks but handles interrupts. When an interrupt occurs, the primary core sends an inter-processor interrupt to the non-primary cores. The non-primary cores then fetch tasks from the scheduling queue and execute them.
• Figure 2: Code snippet of procedure that runs on non-primary cores in Awkernel.
• Figure 3: Code snippet of the Promela description that corresponds to the procedure running on non-primary cores in Awkernel.
• Figure 4: Overview of code review model design that is used in the model checking.
• Figure 5: First diagram about task transitions in Awkernel; the diagram was created as the first model representing our understanding of the task transition. It was used as the base of the monitor while conducting runtime verification.