Investigating Analysis Techniques for Concurrent Programs

本文的研究重点是并发软件系统的静态分析。此分析的目的是确定给定的程序或程序规范是否满足某些正确性要求，例如不存在死锁或不存在饥饿。这个研究项目的目标是为并发程序的分析定义新的技术和自动化工具。新技术将旨在扩展和整合现有的分析方法。迄今为止，已经提出了许多分析并发程序的方法。已经实现了一些方法，并在一些著名的并发程序示例上测试了生成的分析工具。然而，目前，对于每种方法可以有效应用于的项目的类型和规模，以及该方法可以有效回答的项目的问题种类，人们知之甚少。一些使用线性代数或基于时间逻辑的技术来执行部分分析的方法特别有前途。将对这些方法进行研究，以确定它们的相对优势和劣势。对现有方法的评价将指导新的分析技术的定义。这方面的初步调查已经确定了扩大和综合现有办法的各种可能性。新的分析技术必须适应自动化分析工具的实现。在评估现有方法和拟议方法的相对优势时，实际实验和绩效结果评价将发挥关键作用。

The focus of this research is the static analysis of concurrent software systems. The purpose of this analysis is to determine whether a given program or program specification satisfies certain correctness requirements, such as freedom of deadlock or absence of starvation. The goal of this research project is to define new techniques and automated tools for the analysis of concurrent programs. The new techniques will be aimed at extending and integrating existing analysis methods. To date a number of approaches to the analysis of concurrent programs have been proposed. Some approaches have been implemented and the resulting analysis tools have been tested on some well-known examples of concurrent programs. At present, however, little is known about the types and sizes of programs to which each approach can be usefully applied, and the kinds of questions about the programs that the approach can effectively answer. Some approaches which use linear algebra or temporal logic based techniques to perform portions of the analysis are especially promising. These approaches will be investigated in an effort to characterize their relative strengths and weaknesses. The evaluation of the existing approaches will guide the definition of new analysis techniques. Preliminary investigations in this area have identified various possibilities for extending and integrating existing approaches. The new analysis techniques must be amenable to the implementation of automated analysis tools. Practical experimentations and the evaluation of performance results will play a crucial role when assessing the relative strengths of existing and proposed approaches.