Detecting Fair Non-termination in Multithreaded Programs

Abstract. We develop compositional analysis algorithms for detecting nontermination in multithreaded programs. Our analysis explores fair and ultimatelyperiodic 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 e...

• Type: Journal
• Year: 2012
• Where: CAV
• Authors: Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal
• Keywords: Analysis Algorithms, CAV 2012, Exclusion Protocols, Hardware, Prototype Tool