论文部分内容阅读
随着多核时代的到来，共享内存的多线程编程开始普及。多个线程在并发访问共享内存时会存在内存一致性问题。Java语言通过直接在语言层定义内存模型来解决该问题。Java内存模型是保证Java多线程程序安全性和高效性的关键。 迄今为止，Java语言一直沿用5.0版本发布的内存模型。为了同时满足模型的易用性、类型的安全性和编译的高效性三方面的要求，Java内存模型采用了一种非常复杂和晦涩的公理语义。该模型自从发布后，对该模型使用各种形式语义的描述和表示，以及内在缺陷的发现和改进，一直是理论研究的热点问题。对于如何修订Java模型目前尚无定论。另一方面，内存模型相关的并发模块是Java虚拟机实现中最复杂的部分。保证并发模块的实现符合Java内存模型在工业界有着明确的需求。当前对Java内存模型的验证工具都属于静态验证，无法验证虚拟机实现的正确性。因此有必要研究Java内存模型的动态验证方法和工具。 本文从下面两个方面开展了工作: 首先我们通过提取两种最常见编译器优化措施:重排序和指令合并的本质特性，对现有的Java内存模型进行修订，提出了一种新颖的吸收语义模型。我们的定义结合了公理语义和操作语义的优点。其不仅能够支持马里兰大学提供的20个标准测试样例1所展示的全部编译优化，而且能够确保Java内存模型的安全性。据我们所知，在目前所有的替代模型中，只有我们的模型满足Java内存模型的全部要求，并且对现有模型的修改最少。 由于Java内存模型的特殊性，单纯的动态验证方法无法正确验证Java内存模型。我们以动态验证为基础，结合静态分析实现了Java内存模型动态验证工具JMODV2.0。该工具通过wala静态分析工具获取Java多线程程序的控制流图和数据流图。同时，使用JVMTI获取程序对共享变量的读写执行序列。该工具通过确认多线程程序在Java虚拟机的执行结果是否符合Java内存模型的要求，以此验证Java虚拟机的实现是否满足Java内存模型。我们使用JMODV2.0对马里兰大学提供的20个标准测试样例进行了检测，实验结果证明了我们工具的有效性。除了我们的工具之外，目前还未发现其它能正确验证Java内存模型的动态验证工具。