Java并发程序的模型提取与模型检测技术研究

摘要

随着多核心处理器系统的发展，分布式并发系统已成为当前主流的软件体系结构。分布式软件的特性导致错误不可重现，使软件排错工作非常困难。Java是在语言级别支持并发的高级语言，其提供的语言特性和大量的类库很好地支持了并发程序的编写。但这些类库都有各自的特点，如果使用不当会造成一些难以发现，却危害严重的问题。同时，Java内存模型JMM（Java Memory Model）允许编译器在优化过程中改变程序的执行顺序，这会让多线程Java程序产生许多意想不到的错误。Java规范中程序的正确性仅仅依赖于程序员编写正确的，不会冲突的代码，很难满足高可靠性软件的要求。 针对上述问题，本文提出了一套对Java多线程并发程序错误进行检测的方法。第一部分工作提出了一种自动化模型检测的技术，并制作了工具JTS（Java To SPIN），实现了对Java并发程序的模型检测与验证。JTS对Java程序进行分析，产生抽象语法树，建立程序的抽象模型。分析中特别针对Java虚拟机的并发机制和类库实现进行了建模，并利用模型检测工具SPIN进行了模型检测。在实验中JTS成功地对多个Java程序进行了模型提取和模型检测，给出了错误路径。JTS建立的模型准确地再现了Java程序的执行过程，发现了其中隐藏的并发程序错误。这种检测方法为发现和修正这类不可重现，难以测试的并发错误提供了一种新的方法和思路，是传统测试方法在并行程序领域的的一种尝试与补充。 第二部分工作提出了另一种新的方法，针对JMM所允许的程序顺序变化，结合程序中的依赖关系、volatile变量和串行化代码等建立模型，进行模型检测。根据这种检测方法，给出了程序的乱序模型和模型检测结果。在模拟执行和检测结果序列中，可以清楚地看到Java多线程并发程序的乱序执行情况。该方法检测现有JMM规范下所有允许的代码顺序变化，可以发现原有技术无法检测的错误，并给出错误路径，推进了高可靠性Java程序的验证工作。

目录

文摘

英文文摘

论文说明：图表目录

声明

第1章绪论

1.1研究背景

1.1.1Java语言

1.1.2模型检测

1.2相关工作介绍

1.3本课题的研究内容

1.4本文组织结构

第2章Java并发程序分析

2.1 Java的并发机制介绍

2.1.1 Java并发程序锁的问题

2.1.2Java并发程序的通信问题

2.1.3Java并发程序的同步问题

2.2 JAVACC简介

2.3 JTB简介

2.3.1产生的文件

2.3.2自动产生的类

2.4小结

第3章模型检测理论及工具

3.1模型检测简介

3.2模型检测工具

3.2.1模型检测工具SPIN

3.2.2SPIN工作原理及相关定义

3.2.3 SPIN的基本结构

3.2.4SPIN搜索算法

3.2.5偏序规约

3.3线性时序逻辑LTL

3.4 Java并发程序模型检测

3.5小结

第4章Java并发程序的模型检测

4.1 Java程序分析

4.2建立promela模型

4.2.1类

4.2.2方法

4.2.3属性

4.2.4方法内部语句

4.3 Java并发程序的特殊控制结构

4.3.1锁模型

4.3.2通信控制模型

4.3.3同步控制模型

4.4检测结果

4.5模拟路径分析

4.6实验

4.7小结

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

5.1模型定义与算法

5.2模型建立与检测

5.2.1简单乱序模型

5.2.2包含Volatile变量的乱序模型

5.2.3包含依赖关系的乱序模型

5.3小结

结 论

参考文献

致 谢

附录