Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs

TL;DR

This paper introduces a static analysis method based on Abstract Interpretation for detecting run-time errors in embedded real-time parallel C programs, focusing on thread interactions, mutual exclusion, and scheduling.

Contribution

It extends existing static analysis techniques to handle multi-threaded embedded C programs with real-time scheduling and mutual exclusion, ensuring soundness under various memory models.

Findings

Proven soundness with respect to sequential and weak memory models.

Applied to industrial code with scalable results.

Implemented in the Thésée prototype tool.

Abstract

We present a static analysis by Abstract Interpretation to check for run-time errors in parallel and multi-threaded C programs. Following our work on Astr\'ee, we focus on embedded critical programs without recursion nor dynamic memory allocation, but extend the analysis to a static set of threads communicating implicitly through a shared memory and explicitly using a finite set of mutual exclusion locks, and scheduled according to a real-time scheduling policy and fixed priorities. Our method is thread-modular. It is based on a slightly modified non-parallel analysis that, when analyzing a thread, applies and enriches an abstract set of thread interferences. An iterator then re-analyzes each thread in turn until interferences stabilize. We prove the soundness of our method with respect to the sequential consistency semantics, but also with respect to a reasonable weakly consistent memory semantics. We also show how to take into account mutual exclusion and thread priorities through a partitioning over an abstraction of the scheduler state. We present preliminary experimental results analyzing an industrial program with our prototype, Th\'es\'ee, and demonstrate the scalability of our approach.