Sound static deadlock analysis for C/Pthreads
We present a static deadlock analysis for C/Pthreads. The design of our method has been guided by the requirement to analyse real-world code. Our approach is sound (i.e., misses no deadlocks) for programs that have defined behaviour according to the C standard and the Pthreads specification, and is...
| Hlavní autoři: | , , , |
|---|---|
| Médium: | Conference item |
| Vydáno: |
Association for Computing Machinery
2016
|
| _version_ | 1826295359696011264 |
|---|---|
| author | Kroening, D Poetzl, D Schrammel, P Wachter, B |
| author_facet | Kroening, D Poetzl, D Schrammel, P Wachter, B |
| author_sort | Kroening, D |
| collection | OXFORD |
| description | We present a static deadlock analysis for C/Pthreads. The design of our method has been guided by the requirement to analyse real-world code. Our approach is sound (i.e., misses no deadlocks) for programs that have defined behaviour according to the C standard and the Pthreads specification, and is precise enough to prove deadlock-freedom for a large number of such programs. The method consists of a pipeline of several analyses that build on a new contextand thread-sensitive abstract interpretation framework. We further present a lightweight dependency analysis to identify statements relevant to deadlock analysis and thus speed up the overall analysis. In our experimental evaluation, we succeeded to prove deadlock-freedom for 292 programs from the Debian GNU/Linux distribution with in total 2.3 MLOC in 4 hours. |
| first_indexed | 2024-03-07T03:59:49Z |
| format | Conference item |
| id | oxford-uuid:c427d70a-ff89-4851-a4ee-48cf6266df4d |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:59:49Z |
| publishDate | 2016 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:c427d70a-ff89-4851-a4ee-48cf6266df4d2022-03-27T06:21:32ZSound static deadlock analysis for C/PthreadsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:c427d70a-ff89-4851-a4ee-48cf6266df4dSymplectic Elements at OxfordAssociation for Computing Machinery2016Kroening, DPoetzl, DSchrammel, PWachter, BWe present a static deadlock analysis for C/Pthreads. The design of our method has been guided by the requirement to analyse real-world code. Our approach is sound (i.e., misses no deadlocks) for programs that have defined behaviour according to the C standard and the Pthreads specification, and is precise enough to prove deadlock-freedom for a large number of such programs. The method consists of a pipeline of several analyses that build on a new contextand thread-sensitive abstract interpretation framework. We further present a lightweight dependency analysis to identify statements relevant to deadlock analysis and thus speed up the overall analysis. In our experimental evaluation, we succeeded to prove deadlock-freedom for 292 programs from the Debian GNU/Linux distribution with in total 2.3 MLOC in 4 hours. |
| spellingShingle | Kroening, D Poetzl, D Schrammel, P Wachter, B Sound static deadlock analysis for C/Pthreads |
| title | Sound static deadlock analysis for C/Pthreads |
| title_full | Sound static deadlock analysis for C/Pthreads |
| title_fullStr | Sound static deadlock analysis for C/Pthreads |
| title_full_unstemmed | Sound static deadlock analysis for C/Pthreads |
| title_short | Sound static deadlock analysis for C/Pthreads |
| title_sort | sound static deadlock analysis for c pthreads |
| work_keys_str_mv | AT kroeningd soundstaticdeadlockanalysisforcpthreads AT poetzld soundstaticdeadlockanalysisforcpthreads AT schrammelp soundstaticdeadlockanalysisforcpthreads AT wachterb soundstaticdeadlockanalysisforcpthreads |