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