动态并发分析：多线程与过程调用的可达性研究

本文主要探讨了多线程程序的分析与验证，特别是在处理动态线程创建和递归过程调用时的复杂性。作者艾哈迈德·布阿贾尼、哈维尔·埃斯帕萨和泰西尔·图伊利针对这类并发程序提出了一个通用的方法，他们的研究焦点在于如何在理论上和实践上克服不可判定的可达性问题。 首先，他们构建了一个理论模型，这个模型以控制配置的术语重写规则为基础，用来描述这类程序的行为。由于该模型的可达性问题被认为是不可判定的，即无法通过常规手段确定所有可能的计算路径，他们转而寻求一种策略来计算抽象的计算路径集。这种方法的核心是通过计算路径语言的约束系统的最小解，从而得到程序行为的近似表示。 他们提出的具体成果包括：(1) 一种系统结构，它能够从一个过程项（例如，程序的一部分）T中学习并选择合适的组合策略，应用到另一个过程项T上；(2) 一个基于抽象解释的通用框架，这个框架提供了灵活的方式来处理不同抽象领域中的分析，允许精确度和效率之间的权衡。 文章强调，多线程程序与过程调用的分析与验证是当前计算机科学中一个关键的挑战，尤其是在处理动态并发性和递归特性时，因为这可能导致不可预测的行为。他们之前的工作（参考[5]）已经展示了如何通过实例化这种通用框架，实现对这类程序的分析，尽管存在不确定性，但依然能够找到有用的上近似分析结果。 关键词包括：多线程程序与过程调用、进程代数、程序分析、验证。论文发表于《理论计算机科学电子笔记》第138期，2005年，受到Elsevier的CCBY-NC-ND许可，可公开访问。整个研究旨在推动多线程程序分析技术的发展，以便为实际的程序设计和验证提供更加有效的方法。