Detecting Fair Non-termination in Multithreaded Programs
Detecting Fair Non-termination in Multithreaded Programs
复制标题
检测多线程程序中的公平非终止
DOI：
10.1007/978-3-642-31424-7_19
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
A. Lal
中科院分区：
文献类型：
--
作者：
M. Atig;A. Bouajjani;M. Emmi;A. Lal
我们开发的成分分析算法检测非终止多线程程序。我们的分析探讨了公平和最终定期执行死刑的问题，即，其中无限频繁启用的线程反复执行相同的动作序列。通过限制上下文切换的数量，每个线程被允许沿着任何重复的动作序列，我们的算法快速发现实际产生的非终止执行。限制在每个时期的上下文切换的数量导致一个组成分析，我们认为每个线程单独的，孤立的，并减少了搜索公平的最终定期执行多线程程序中的顺序程序的状态可达性。我们实现了我们的分析，从多线程程序到顺序程序的系统代码到代码的翻译。通过利用标准的顺序分析工具，我们的原型工具突变是能够发现公平的非终止执行典型的互斥协议和并发数据结构算法。
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.