Static analysis of run-time errors in embedded critical parallel C programs
From MaRDI portal
Publication:3000591
DOI10.1007/978-3-642-19718-5_21zbMATH Open1239.68021arXiv1203.3724OpenAlexW1531955077MaRDI QIDQ3000591FDOQ3000591
Publication date: 19 May 2011
Published in: Programming Languages and Systems (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1203.3724
Cites Work
- Title not available (Why is that?)
- The octagon abstract domain
- Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
- Title not available (Why is that?)
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Concurrency verification. Introduction to compositional and noncompositional methods
- Time, clocks, and the ordering of events in a distributed system
- An axiomatic proof technique for parallel programs
- Tools and Algorithms for the Construction and Analysis of Systems
- Proving the Correctness of Multiprocess Programs
- On the verification problem for weak memory models
- The Java memory model
- Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model
Cited In (7)
- Model Checking Concurrent Programs
- Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
- Static analysis of embedded real-time concurrent software with dynamic priorities
- Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
- Verification of concurrent programs using Petri net unfoldings
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- Title not available (Why is that?)
Uses Software
Recommendations
This page was built for publication: Static analysis of run-time errors in embedded critical parallel C programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000591)
