Computer Science – Programming Languages
Scientific paper
2012-03-16
Computer Science
Programming Languages
Scientific paper
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.
No associations
LandOfFree
Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-352014