07/31, 12:10–12:40 (Asia/Taipei), TR213
言語: English
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.
Our model and reproduction are available online. Also, we've shared one type of errors with the FreeRTOS community. It seems to the community that the error is not a serious problem and our reproduction of the error is unusual. Nevertheless, we still hope to reveal the errors to programmers.
Embedded System Developers/Programmers
Difficulty –中階
youtube_link –
因為 seL4 而對作業系統的驗證感興趣，目前在中研院擔任研究助理