基于Java内存模型的并发程序模型检测

Model Checking the Concurrent Programs Based on the Java Memory Model

为了提高性能,Java内存模型允许编译器在优化过程中改变代码的执行顺序,同时该技术也会造成共享数据的更新顺序与本来的执行顺序不同。在多线程Java并发程序中,这些代码乱序执行会引起很多难以发现的错误。现有的Java程序模型检测技术并没有考虑这些顺序改变的问题。因此,本文提出了一种建立包含多线程交互及线程内代码乱序执行的完整模型,并利用模型检测工具进行穷举检测的算法。该算法可以发现原有技术无法发现的新问题,更好地检测高可靠性要求的Java并发程序。

In order to improve the performance, the Java Memory Model allows the compiler to change the execution order. A variety of caches will change the modification order of the shared data too. In multithreaded concurrent Java programs, this ＂out of order＂ will cause lots of problems which are hard to detect. The existing Java model checking techniques do not consider these order changes. Therefore, this paper proposes an approach which builds a complete model including thread interactions and ＂out of order＂ execution in a single thread. This algorithm can find problems which are omitted by the existing method, as well as check and verify the programs which require high reliability better.