题目：并发程序错误的自动调试技术

随着处理海量数据的计算机集群的普及，基于消息传递的并发程序得到越来越多的应用。随着多核硬件的普及，在互联网、数据库等领域， 为了处理高并发量的访问等，基于共享变量的并发程序也得到了广泛的应用。如何有效的测试、调试这些并发程序中的错误成为一个研究的热点。

在基于消息传递的并发程序方面，现有的调试方法只是简单地收集程序执行信息，然后利用这些信息来辅助定位。 但是这些方法没能提出一个统一的框架来指导调试过程，并进而尝试使调试过程自动化。在基于共享变量的并发程序方面，现有的技术或者不能精确定位到并发错误位置，或者不能给出并发错误的根本原因。 同时这些方法给出的有效信息太少，并不能有效地帮助程序员理解并发错误。

针对这些问题，论文做出了以下贡献：

1. 论文给出了基于同步消息传递的并发程序调试的语义框架。该框架包含一个追踪过程和一个定位过程。追踪过程运行错误测试用例，通过特定的数据结构来收集相关的执行信息。定位过程使用收集到的信息回溯地定位错误的语句，并生成一个表征错误的定位方程，然后通过求解定位方程来尝试修复错误。 根据追踪过程和定位过程的功能，论文分别给出了这两个过程的结构操作语义。

2. 论文提出了通过求解方程组来自动定位并发程序错误区域的方法。该方法包含三步，分别是收集执行信息，生成定位方程组，定位错误区域。论文首先给出了收集执行信息和生成定位方程组过程的操作语义；然后给出了定位错误区域的算法，并且证明了算法可以得到一个跟用户期望违背的程序错误片段；最后给出了一个交互式定位错误
的流程，即通过交互来不断地缩小错误片段。

3. 论文针对基于共享变量的并发错误难于精确定位和难于理解的现状，提出了一个基于边标记通信图的方法来精确定位和帮助理解并发错误。 该方法首先对错误的内存访问对使用统计方法来精确排序；然后对定位出的内存访问对，基于具体的程序执行，寻找并发错误的根本原因，即错误模式； 最后，对给定的错误模式，给出一个执行场景来展示并发错误是如何触发的，从而帮助理解并发错误。基于该方法， 论文实现了原型工具Lucon，实验结果表明Lucon可以精确定位到并发错误的根本原因，同时Lucon的输出信息也的确可以帮助程序员理解错误。