Kroening, Daniel, Poetzl, Daniel, Schrammel, Peter and Wachter, Björn (2016) Sound static deadlock analysis for C/Pthreads. In: 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016). ACM, New York, USA, pp. 379-390. ISBN 978145033845
![]() |
PDF
- Accepted Version
Restricted to SRO admin only Download (531kB) |
Abstract
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 context- and 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.
Item Type: | Book Section |
---|---|
Additional Information: | 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016), September 3-7, 2016, Singapore. |
Keywords: | Deadlock analysis, Static analysis, Abstract interpretation |
Schools and Departments: | School of Engineering and Informatics > Informatics |
Subjects: | Q Science > QA Mathematics > QA0075 Electronic computers. Computer science |
Depositing User: | Peter Schrammel |
Date Deposited: | 04 Aug 2016 10:58 |
Last Modified: | 23 Nov 2016 15:24 |
URI: | http://sro.sussex.ac.uk/id/eprint/62219 |
View download statistics for this item
📧 Request an update