Paper Info
Title
Detecting fair non-termination in multithreaded programs
Abstract
We develop compositional analysis algorithms for detecting non-termination in multithreaded programs. Our analysis explores fair and ultimately-periodic executions--i.e., those in which the infinitely-often enabled threads repeatedly execute the same sequences of actions over and over. By limiting the number of context-switches each thread is allowed along any repeating action sequence, our algorithm quickly discovers practically-arising non-terminating executions. Limiting the number of context-switches in each period leads to a compositional analysis in which we consider each thread separately, in isolation, and reduces the search for fair ultimately-periodic executions in multithreaded programs to state-reachability in sequential programs. We implement our analysis by a systematic code-to-code translation from multithreaded programs to sequential programs. By leveraging standard sequential analysis tools, our prototype tool Mutant is able to discover fair non-terminating executions in typical mutual exclusion protocols and concurrent data-structure algorithms.
Year
DOI
Venue
2012
10.1007/978-3-642-31424-7_19
CAV
Keywords
Field
DocType
concurrent data-structure algorithm,ultimately-periodic execution,non-terminating execution,multithreaded program,fair non-terminating execution,compositional analysis,standard sequential analysis tool,fair ultimately-periodic execution,sequential program,compositional analysis algorithm,fair non-termination,sequential analysis,computer science
Analysis tools,Programming language,Computer science,Theoretical computer science,Thread (computing),Linear temporal logic,Mutual exclusion,Limiting,Context switch
Conference
Citations 
PageRank 
References 
16
0.60
19
Authors
4
Name
Order
Citations
PageRank
Mohamed Faouzi Atig150540.94
Ahmed Bouajjani22663184.84
Michael Emmi336521.76
Akash Lal453732.12