Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs
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 thre...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/799/pdf |
| _version_ | 1797268698271055872 |
|---|---|
| author | Antoine Miné |
| author_facet | Antoine Miné |
| author_sort | Antoine Miné |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:37Z |
| format | Article |
| id | doaj.art-6f64b8ea0c8d4860a6100e09fa2d9160 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:37Z |
| publishDate | 2012-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-6f64b8ea0c8d4860a6100e09fa2d91602024-03-08T09:27:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-03-01Volume 8, Issue 110.2168/LMCS-8(1:26)2012799Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C ProgramsAntoine Miné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.https://lmcs.episciences.org/799/pdfcomputer science - programming languagescomputer science - logic in computer scienced.2.4f.3.1f.3.2 |
| spellingShingle | Antoine Miné Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs Logical Methods in Computer Science computer science - programming languages computer science - logic in computer science d.2.4 f.3.1 f.3.2 |
| title | Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs |
| title_full | Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs |
| title_fullStr | Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs |
| title_full_unstemmed | Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs |
| title_short | Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs |
| title_sort | static analysis of run time errors in embedded real time parallel c programs |
| topic | computer science - programming languages computer science - logic in computer science d.2.4 f.3.1 f.3.2 |
| url | https://lmcs.episciences.org/799/pdf |
| work_keys_str_mv | AT antoinemine staticanalysisofruntimeerrorsinembeddedrealtimeparallelcprograms |