Sound static deadlock analysis for C/Pthreads (extended version)

Journal article

Abstract:: We present a static deadlock analysis approach 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 precise enough to prove deadlock-freedom for a large number of 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 262 programs from the Debian GNU/Linux distribution with in total 2.6 MLOC in less than 11 hours.

Files:: 1607.06927v1.pdf

(Preview, Author's original, pdf, 443.5KB, Terms of use)

Keywords:: static analysis

abstract interpretation

deadlock detection

lock analysis
Pubs id:: pubs:636595
UUID:: uuid:125d39b2-b45e-432d-9f35-c5cbdaff591c
Local pid:: pubs:636595
Source identifiers:: 636595
Deposit date:: 2016-08-23
ARK identifier:: ark:/29072/ora_125d39b2b45e432d9f35c5cbdaff591c

Copyright holder:: Kroening et al
Notes:: This is an extended version of a conference paper published in ASE 2016: 31st IEEE/ACM International Conference on Automated Software Engineering, available in ORA at https://ora.ox.ac.uk/objects/uuid:c427d70a-ff89-4851-a4ee-48cf6266df4d

Licence:: Terms and Conditions of Use for Oxford University Research Archive

If you are the owner of this record, you can report an update to it here: Report update to this record