关键词: Java内存模型, 模型检测, Java并发程序, 多线程, 软件测试

Abstract: 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.

Key words: Java memory model；model checking；concurrent Java program；multithreaded；software testing