Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
复制标题
DOI：
10.29007/c7v2
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
M. Kuntz;S. Leue;Christoph Scheben
中科院分区：
文献类型：
--
作者：
M. Kuntz;S. Leue;Christoph Scheben
目前，还没有已知的方法可以实现并发程序的非终止证明，这些并发程序通过 FIFO 消息队列进行异步通信。这些程序可以用 Java 或 Promela 等高级语言编写。我们提出第一种方法来证明此类程序的不终止性。除了整数之外，我们考虑的程序还可能包含队列作为数据结构。我们在整数域中提出队列及其操作的表示，并生成不变量，帮助我们使用定理证明方法证明所选控制流循环的非终止。我们通过将原型工具实现应用于许多案例研究来说明这种方法。
Currently, no approaches are known that allow for non-termination proofs of concurrent programs which account for asynchronous communication via FIFO message queues. Those programs may be written in high-level languages such as Java or Promela. We present a first approach to prove nontermination for such programs. In addition to integers, the programs that we consider may contain queues as data structures. We present a representation of queues and the operations on them in the domain of integers, and generate invariants that help us prove non-termination of selected control flow loops using a theorem proving approach. We illustrate this approach by applying a prototype tool implementation to a number of case studies.