Detecting All High-Level Dataraces in an RTOS Kernel
Authors: Suvam Mukherjee, Arun Kumar and Deepak D'Souza
A high-level race occurs when an execution interleaves instructions
corresponding to user-annotated critical
accesses to shared memory structures.
Such races are good indicators of atomicity violations.
We propose a technique for detecting all high-level
dataraces in a system library like the kernel
API of a real-time operating system (RTOS) that relies on flag-based
scheduling and synchronization.
Our methodology is based on
model-checking, but relies on a meta-argument to bound the number of
task processes needed to orchestrate a race.
We describe our approach
in the context of FreeRTOS, a popular RTOS in the embedded domain.