Pattern-Based Verification for Multithreaded Programs
Pattern-Based Verification for Multithreaded Programs
复制标题
多线程程序基于模式的验证
DOI：
10.1145/2629644
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Tomás Poch
中科院分区：
文献类型：
--
作者：
Javier Esparza;Pierre Ganty;Tomás Poch
基于模式的验证检查遵循给定模式的程序执行的正确性，该模式是基于形式为w1*…wn*的程序转换字母表的正则表达式。对于多线程程序，模式的字母表由对共享存储的读和写给出。我们研究了具有共享计数器和有限变量的多线程程序的基于模式验证的复杂性。虽然无限制验证对于具有递归过程的抽象多线程程序是不可判定的，而对于抽象多线程While程序（即使没有计数器）是PSPACE-complete的，但我们表明，基于模式的验证对于这两个类都是NP-complete的，即使在存在计数器的情况下也是如此。然后，我们进行了多参数分析，以研究问题的三个自然参数（线程数+计数器+变量，线程的最大大小，模式的大小）和与线程结构相关的两个参数（每个线程的最大过程数和过程调用的最长简单路径）的复杂性。我们提出了一种算法，对于固定数量的线程、计数器、变量和模式大小，该算法解决了在（lsp+≥log （pr+1）²）时间内的验证问题，其中线程的最大大小为每个线程的最大过程数，过程调用的最长简单路径为每个线程的最大过程数。
Pattern-based verification checks the correctness of program executions that follow a givenpattern, a regular expression over the alphabet of program transitions of the formw1*…wn*. For multithreaded programs, the alphabet of the pattern is given by the reads and writes to the shared storage. We study the complexity of pattern-based verification for multithreaded programs with shared counters and finite variables. While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs (even without counters), we show that pattern-based verification is NP-complete for both classes, even in the presence of counters. We then conduct a multiparameter analysis to study the complexity of the problem on its three natural parameters (number of threads+counters+variables, maximal size of a thread, size of the pattern) and on two parameters related to thread structure (maximal number of procedures per thread and longest simple path of procedure calls). We present an algorithm that for a fixed number of threads, counters, variables, and pattern size solves the verification problem instO(lsp+ ⌈ log (pr+1) ⌉)time, wherestis the maximal size of a thread,pris the maximal number of procedures per thread, andlspis the longest simple path of procedure calls.
登录
查看更多内容
影响因子：
0.8
作者：
J. Gathen;M. Sieveking
通讯作者：
M. Sieveking
DOI：
10.1007/978-3-642-28872-2_25
发表时间：
2012
期刊：
ArXiv
影响因子：
--
作者：
Zhenyue Long;Georgel Calin;R. Majumdar;R. Meyer
通讯作者：
R. Meyer
形成方法 Syst Des DOI 10.1007/s10703-011-0136-y 有界欠近似
DOI：
--
发表时间：
--
期刊：
影响因子：
--
作者：
M. Krishnaveni
通讯作者：
M. Krishnaveni
Zing：并发软件的模型检查器
DOI：
--
发表时间：
2004
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Tony Andrews;S. Qadeer;S. Rajamani;J. Rehof;Yichen Xie
通讯作者：
Yichen Xie
锁链的有界性与无界性：表征成对 CFL 的可判定性 - 通过锁进行通信的线程的可达性
DOI：
10.1109/lics.2009.45
发表时间：
2009
期刊：
2009 24th Annual IEEE Symposium on Logic In Computer Science
影响因子：
--
作者：
Vineet Kahlon
通讯作者：
Vineet Kahlon