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.
Description
Detecting Fair Non-termination in Multithreaded Programs | SpringerLink
%0 Conference Paper
%1 Atig:2012:DFNT
%A Atig, Mohamed Faouzi
%A Bouajjani, Ahmed
%A Emmi, Michael
%A Lal, Akash
%B Computer Aided Verification
%C Berlin, Heidelberg
%D 2012
%E Madhusudan, P.
%E Seshia, Sanjit A.
%I Springer
%K Concurrency Detection Multithreading SharedMemory Termination
%P 210--226
%T Detecting Fair Non-termination in Multithreaded Programs
%X 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.
%@ 978-3-642-31424-7
@inproceedings{Atig:2012:DFNT,
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.},
added-at = {2019-08-06T15:26:45.000+0200},
address = {Berlin, Heidelberg},
author = {Atig, Mohamed Faouzi and Bouajjani, Ahmed and Emmi, Michael and Lal, Akash},
biburl = {https://www.bibsonomy.org/bibtex/2f9dd09a5947edc5a79c9cd1ec3376032/gron},
booktitle = {Computer Aided Verification},
description = {Detecting Fair Non-termination in Multithreaded Programs | SpringerLink},
editor = {Madhusudan, P. and Seshia, Sanjit A.},
interhash = {ce4f506ca69da609ce853a7ef7fac230},
intrahash = {f9dd09a5947edc5a79c9cd1ec3376032},
isbn = {978-3-642-31424-7},
keywords = {Concurrency Detection Multithreading SharedMemory Termination},
pages = {210--226},
publisher = {Springer},
timestamp = {2019-08-06T15:26:45.000+0200},
title = {Detecting Fair Non-termination in Multithreaded Programs},
year = 2012
}