FreeRTOS is a popular real-time kernel. It supports multiple microarchitectures, including ARM and RISC-V. Also, it provides synchronous primitives and three scheduling policies for performing real-time tasks. In this talk, we aim to reason the FreeRTOS’ scheduling behaviors with the Spin model checker. The Spin model checker can exhaustively check an abstract model of a multithreading program against given properties. Especially, it interleaves the behaviors of every single threaded model and tries to report an counterexample which violating the given properties on the model. We manually build an abstract model of the FreeRTOS’ scheduling behaviors at the C code level and leverage assertions in FreeRTOS’ demonstrations as properties.
Although we aren’t the first to model FreeRTOS, we do have interesting results. The model checker reports two types of errors under different scheduling policies. In order to show they are not spurious, we successfully reproduce those types of errors on a STM32F429 board. We find similar results on a SiFive-HiFive-Rev-B board.
About Kai
因為 seL4 而對作業系統的驗證感興趣，目前在中研院擔任研究助理