Towards Model Checking Linux Interrupts Behavior for SMP Systems
Sergey Mikhailovich Staroletov · 2023
The interrupt handling subsystem is an essential component of modern operating systems, playing a critical role in the functioning of desktop, cyber-physical, and server systems. It is responsible for managing and processing asynchronous events that occur during system operation, such as hardware interrupts generated by input/output devices or software interrupts triggered by system calls. In Linux, the interrupt subsystem is highly configurable, with various options available for interrupt generators, their handlers, controllers, and types of interrupts. However, interrupts processing can become particularly complex in systems with multiple logical processors or SMP systems. In such environments, asynchronous messages are prevalent, making them susceptible to subtle failures that can be challenging to detect and diagnose. To ensure the correctness of message processing algorithms in such systems, it is proposed to use formal verification techniques. More precisely, model checking is a method of formal verification that involves systematically exploring all possible system states to check whether a given property holds under all conditions. To this end, this article discusses a plan for Linux code-inspired interrupt simulation strategies to check the correctness of their processing. By simulating interrupt handling code in a controlled environment, it is possible to identify and eliminate potential sources of errors and ensure that the system operates correctly under all conditions. This approach takes a step toward improving the robustness of interrupt handling in operating systems using simulation and verification the behavior in the model checker environment without actual code running.