University of Sussex
Browse

File(s) under permanent embargo

Sound static deadlock analysis for C/Pthreads

chapter
posted on 2023-06-09, 02:23 authored by Daniel Kroening, Daniel Poetzl, Peter Schrammel, Björn Wachter
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.

History

Publication status

  • Published

File Version

  • Accepted version

Publisher

ACM

Page range

379-390

Book title

31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016)

Place of publication

New York, USA

ISBN

978145033845

Department affiliated with

  • Informatics Publications

Notes

31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016), September 3-7, 2016, Singapore.

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2016-08-04

First Compliant Deposit (FCD) Date

2016-08-04

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC