Sound static deadlock analysis for C/Pthreads

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

[img] 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
Q Science > QA Mathematics > QA0076 Computer software
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