Sciweavers

ESOP
2011
Springer

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

13 years 2 months ago
Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs
We present a static analysis by Abstract Interpretation to check for run-time errors in parallel 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. Our method iterates a slightly modified non-parallel analysis over each thread in turn, until thread interferences stabilize. We prove the soundness of the method with respect to a sequential consistent semantics and a reasonable weakly consistent memory semantics. We then show how to take into account mutual exclusion and thread priorities through partitioning over the scheduler state. We present preliminary experimental results analyzing a real program with our prototype, Th´es´ee, and demonstrate the scalability of our approach.
Antoine Miné
Added 27 Aug 2011
Updated 27 Aug 2011
Type Journal
Year 2011
Where ESOP
Authors Antoine Miné
Comments (0)