Abstract:
Correct design and implementation of concurrent algorithms is a crucial part of modern real-time operating system development. One of the main steps along this way is a verification of such algorithms within the programming language memory model. The article describes an integration of the ThreadSanitizer – broadly used LLVM tool for data race detection – into the RTOS kernel environment and discusses its advantages and disadvantages over other tools for data race detection. Among other things, the semantics of context switches and interrupt management within the happens-before synchronization model is considered. In conclusion the results of a ThreadSanitizer tool integration are provided compared to current approaches of concurrency bugs detection in RTOS kernel.