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.
CITATION STYLE
Mukherjee, S., Kumar, A., & D’Souza, D. (2017). Detecting all high-level dataraces in an RTOS kernel. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10145 LNCS, pp. 405–423). Springer Verlag. https://doi.org/10.1007/978-3-319-52234-0_22
Mendeley helps you to discover research relevant for your work.